∀ {X : Type u} (IsOpen IsOpen_1 : Set X → Prop) (e_IsOpen : IsOpen = IsOpen_1) (isOpen_univ : IsOpen Set.univ)
  (isOpen_inter : ∀ (s t : Set X), IsOpen s → IsOpen t → IsOpen (s ∩ t))
  (isOpen_sUnion : ∀ (s : Set (Set X)), (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)),
  { IsOpen := IsOpen, isOpen_univ := isOpen_univ, isOpen_inter := isOpen_inter, isOpen_sUnion := isOpen_sUnion } =
    { IsOpen := IsOpen_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }