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 that
A1: A is condensed and
A2: Cl (Int A) c= Int (Cl A) ; :: thesis: ( A is open & A is closed )
A3: A is closed_condensed by A1, A2, Th7;
A is open_condensed by A1, A2, Th7;
hence ( A is open & A is closed ) by A3, TOPS_1:66, TOPS_1:67; :: thesis: verum