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 & A is closed )
let A be Subset of X; :: thesis: ( A is condensed & Cl (Int A) c= Int (Cl A) implies ( A is open & A is closed ) )
assume ( A is condensed & Cl (Int A) c= Int (Cl A) ) ; :: thesis: ( A is open & A is closed )
then ( A is open_condensed & A is closed_condensed ) by Th9;
hence ( A is open & A is closed ) by TOPS_1:106, TOPS_1:107; :: thesis: verum