let T be TopSpace; :: thesis: for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds

A is 1st_class

let A be Subset of T; :: thesis: ( ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) implies A is 1st_class )

assume A1: ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) ; :: thesis: A is 1st_class

A is 1st_class

let A be Subset of T; :: thesis: ( ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) implies A is 1st_class )

assume A1: ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) ; :: thesis: A is 1st_class