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 A is condensed ; :: thesis: ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B )
then A1: ( Int (Cl A) = Int A & Cl (Int A) = Cl A ) by Def3;
take U = Cl (Int A); :: thesis: ( U is regular_closed & Int U c= A & A c= U )
thus ( U is regular_closed & Int U c= A & A c= U ) by A1, PRE_TOPC:48, TOPS_1:44; :: thesis: verum

end;

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