∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] [inst_3 : LinearOrder B] [OrderTopology B] (e e' : Trivialization F proj),
  ∀ a ∈ e.baseSet,
    a ∈ e'.baseSet →
      (∀ (p : Z), proj p = a → ↑e p = ↑e' p) → e.baseSet ∩ frontier (Set.Iic a) = e'.baseSet ∩ frontier (Set.Iic a)