∀ {B : Type u_1} {F : Type u_3} {E : B → Type u_2} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {e : Pretrivialization F Bundle.TotalSpace.proj},
  e ∈ a.pretrivializationAtlas → ContinuousOn (↑e.toPartialEquiv) e.source