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) ) )
A1: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
assume A2: A is condensed ; :: thesis: ( Int (Cl A) = Int A & Cl A = Cl (Int A) )
then Int (Cl A) c= A by TOPS_1:def 6;
then A3: Int (Int (Cl A)) c= Int A by TOPS_1:19;
A c= Cl (Int A) by A2, TOPS_1:def 6;
then A4: Cl A c= Cl (Cl (Int A)) by PRE_TOPC:19;
Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
hence ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) by A3, A4, A1; :: thesis: verum