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
per cases ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) by A1;
suppose A2: Int (Cl A) = Int (Cl (Int A)) ; :: thesis: A is 1st_class
Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16;
hence A is 1st_class by A2; :: thesis: verum
end;
suppose A3: Cl (Int A) = Cl (Int (Cl A)) ; :: thesis: A is 1st_class
Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18;
hence A is 1st_class by A3; :: thesis: verum
end;
end;