let T be TopStruct ; :: thesis: for A being Subset of T holds
( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
let A be Subset of T; :: thesis: ( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
([#] T) \ (([#] T) \ A) = A by Th3;
then A1: ( A is open iff ([#] T) \ A is closed ) ;
hence ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) by Th22; :: thesis: ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open )
assume ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A ) ; :: thesis: A is open
hence A is open by A1, Th22; :: thesis: verum