∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B) (a : F), { proj := b, snd := a } ∈ (Z.localTrivAt b).source