∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace F]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : TopologicalSpace B] [inst_4 : FiberBundle F E] (x : Bundle.TotalSpace F E),
  (trivializationAt F E x.proj).toOpenPartialHomeomorph ∈
    (fun e => e.toOpenPartialHomeomorph) '' trivializationAtlas F E