let X be TopSpace; :: thesis: for A being Subset of X st A is condensed holds
( Int (Cl A) = Int A & Cl A = Cl (Int A) )
let A be Subset of X; :: thesis: ( A is condensed implies ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) )
assume A is condensed ; :: thesis: ( Int (Cl A) = Int A & Cl A = Cl (Int A) )
then ( Int (Cl A) c= A & A c= Cl (Int A) ) by TOPS_1:def 6;
then A1: ( Int (Int (Cl A)) c= Int A & Cl A c= Cl (Cl (Int A)) ) by PRE_TOPC:49, TOPS_1:48;
( A c= Cl A & Int A c= A ) by PRE_TOPC:48, TOPS_1:44;
then ( Int A c= Int (Cl A) & Cl (Int A) c= Cl A ) by PRE_TOPC:49, TOPS_1:48;
hence ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) by A1, XBOOLE_0:def 10; :: thesis: verum