∀ {α : Type u_6} (sets : Set (Set α)) (nonempty : sets.Nonempty)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (sets_1 : Set (Set α))
  (nonempty_1 : sets_1.Nonempty) (inter_sets_1 : ∀ {x y : Set α}, x ∈ sets_1 → y ∈ sets_1 → ∃ z ∈ sets_1, z ⊆ x ∩ y),
  ({ sets := sets, nonempty := nonempty, inter_sets := inter_sets } =
      { sets := sets_1, nonempty := nonempty_1, inter_sets := inter_sets_1 }) =
    (sets = sets_1)