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 A is condensed ; :: thesis: ( not Cl (Int A) c= Int (Cl A) or ( A is open_condensed & A is closed_condensed ) )
then A1: ( Int (Cl A) c= A & A c= Cl (Int A) ) by TOPS_1:def 6;
assume Cl (Int A) c= Int (Cl A) ; :: thesis: ( A is open_condensed & A is closed_condensed )
then ( A c= Int (Cl A) & Cl (Int A) c= A ) by A1, XBOOLE_1:1;
then ( A = Int (Cl A) & A = Cl (Int A) ) by A1, XBOOLE_0:def 10;
hence ( A is open_condensed & A is closed_condensed ) by TOPS_1:def 7, TOPS_1:def 8; :: thesis: verum