let T be TopSpace; 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; ( 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 ) )
( ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) implies A is condensed )
given B being Subset of T such that A3:
B is regular_closed
and
A4:
Int B c= A
and
A5:
A c= B
; 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; verum