let T be TopSpace; :: thesis: for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) )
let A be Subset of T; :: thesis: ( A is condensed iff ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) )
thus ( A is condensed implies ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) ) :: thesis: ( ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) implies A is condensed )

proof

assume A1: A is condensed ; :: thesis: ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B )
then A2: Cl (Int A) = Cl A ;
take Cl (Int A) ; :: thesis: ( Cl (Int A) is regular_closed & Int (Cl (Int A)) c= A & A c= Cl (Int A) )
Int (Cl A) = Int A by A1;
hence ( Cl (Int A) is regular_closed & Int (Cl (Int A)) c= A & A c= Cl (Int A) ) by A2, PRE_TOPC:18, TOPS_1:16; :: thesis: verum

end;

given B being Subset of T such that A3: B is regular_closed and
A4: Int B c= A and
A5: A c= B ; :: thesis: A is condensed
A6: Cl (Int B) = B by A3, TOPS_1:def 7;
Cl A c= Cl B by A5, PRE_TOPC:19;
then Int (Cl A) c= Int (Cl B) by TOPS_1:19;
then A7: Int (Cl A) c= Int B by A3, Def1;
Cl (Int B) c= Cl A by A4, PRE_TOPC:19;
then Int B c= Int (Cl A) by A6, TOPS_1:19;
then A8: Int B = Int (Cl A) by A7, XBOOLE_0:def 10;
Int A c= Int B by A5, TOPS_1:19;
then A9: Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
Int (Int B) c= Int A by A4, TOPS_1:19;
then Cl (Int (Int B)) c= Cl (Int A) by PRE_TOPC:19;
then Cl (Int A) = B by A6, A9, XBOOLE_0:def 10;
hence A is condensed by A4, A5, A8, Th10; :: thesis: verum