let X be TopSpace; :: thesis: for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds
( A is open_condensed & A is closed_condensed )
let A be Subset of X; :: thesis: ( A is condensed & Cl (Int A) c= Int (Cl A) implies ( A is open_condensed & A is closed_condensed ) )
assume A1: A is condensed ; :: thesis: ( not Cl (Int A) c= Int (Cl A) or ( A is open_condensed & A is closed_condensed ) )
then A2: Int (Cl A) c= A by TOPS_1:def 6;
A3: A c= Cl (Int A) by A1, TOPS_1:def 6;
assume A4: Cl (Int A) c= Int (Cl A) ; :: thesis: ( A is open_condensed & A is closed_condensed )
then Cl (Int A) c= A by A2;
then A5: A = Cl (Int A) by A3;
A c= Int (Cl A) by A3, A4;
then A = Int (Cl A) by A2;
hence ( A is open_condensed & A is closed_condensed ) by A5, TOPS_1:def 7, TOPS_1:def 8; :: thesis: verum