∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (toFun : ι → Set X) (carrier : Set ι) (isOpen : ∀ (i : ι), IsOpen (toFun i)) (subset_iUnion : s ⊆ ⋃ i, toFun i)
  (closure_subset : ∀ {i : ι}, i ∈ carrier → closure (toFun i) ⊆ u i)
  (pred_of_mem : ∀ {i : ι}, i ∈ carrier → p (toFun i)) (apply_eq : ∀ {i : ι}, i ∉ carrier → toFun i = u i)
  (toFun_1 : ι → Set X) (carrier_1 : Set ι) (isOpen_1 : ∀ (i : ι), IsOpen (toFun_1 i))
  (subset_iUnion_1 : s ⊆ ⋃ i, toFun_1 i) (closure_subset_1 : ∀ {i : ι}, i ∈ carrier_1 → closure (toFun_1 i) ⊆ u i)
  (pred_of_mem_1 : ∀ {i : ι}, i ∈ carrier_1 → p (toFun_1 i)) (apply_eq_1 : ∀ {i : ι}, i ∉ carrier_1 → toFun_1 i = u i),
  ({ toFun := toFun, carrier := carrier, isOpen := isOpen, subset_iUnion := subset_iUnion,
        closure_subset := closure_subset, pred_of_mem := pred_of_mem, apply_eq := apply_eq } =
      { toFun := toFun_1, carrier := carrier_1, isOpen := isOpen_1, subset_iUnion := subset_iUnion_1,
        closure_subset := closure_subset_1, pred_of_mem := pred_of_mem_1, apply_eq := apply_eq_1 }) =
    (toFun = toFun_1 ∧ carrier = carrier_1)