∀ {α : Type u_4} {Has : Set α → Prop} {has_empty : Has ∅} {has_compl : ∀ {a : Set α}, Has a → Has aᶜ}
  {has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)}
  {Has_1 : Set α → Prop} {has_empty_1 : Has_1 ∅} {has_compl_1 : ∀ {a : Set α}, Has_1 a → Has_1 aᶜ}
  {has_iUnion_nat_1 :
    ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has_1 (f i)) → Has_1 (⋃ i, f i)},
  { Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat } =
      { Has := Has_1, has_empty := has_empty_1, has_compl := has_compl_1, has_iUnion_nat := has_iUnion_nat_1 } →
    Has = Has_1