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_open & B c= A & A c= Cl B ) )

let A be Subset of T; :: thesis: ( A is condensed iff ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) )

thus ( A is condensed implies ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) ) :: thesis: ( ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) implies A is condensed )

A4: B c= A and

A5: A c= Cl B ; :: thesis: A is condensed

A6: Int (Cl B) = B by A3, TOPS_1:def 8;

Int B c= Int A by A4, TOPS_1:19;

then A7: Cl (Int B) c= Cl (Int A) by PRE_TOPC:19;

A8: Cl (Int B) = Cl B by A3, Def2;

Int A c= Int (Cl B) by A5, TOPS_1:19;

then Cl (Int A) c= Cl B by A6, PRE_TOPC:19;

then A9: Cl B = Cl (Int A) by A7, A8, XBOOLE_0:def 10;

Cl B c= Cl A by A4, PRE_TOPC:19;

then A10: Int (Cl B) c= Int (Cl A) by TOPS_1:19;

Cl A c= Cl (Cl B) by A5, PRE_TOPC:19;

then Int (Cl A) c= Int (Cl (Cl B)) by TOPS_1:19;

then B = Int (Cl A) by A6, A10, XBOOLE_0:def 10;

hence A is condensed by A4, A5, A9, Th10; :: thesis: verum

( A is condensed iff ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) )

let A be Subset of T; :: thesis: ( A is condensed iff ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) )

thus ( A is condensed implies ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) ) :: thesis: ( ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B ) implies A is condensed )

proof

given B being Subset of T such that A3:
B is regular_open
and
assume A1:
A is condensed
; :: thesis: ex B being Subset of T st

( B is regular_open & B c= A & A c= Cl B )

then A2: Cl (Int A) = Cl A ;

take Int (Cl A) ; :: thesis: ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) )

Int (Cl A) = Int A by A1;

hence ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) ) by A2, PRE_TOPC:18, TOPS_1:16; :: thesis: verum

end;( B is regular_open & B c= A & A c= Cl B )

then A2: Cl (Int A) = Cl A ;

take Int (Cl A) ; :: thesis: ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) )

Int (Cl A) = Int A by A1;

hence ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) ) by A2, PRE_TOPC:18, TOPS_1:16; :: thesis: verum

A4: B c= A and

A5: A c= Cl B ; :: thesis: A is condensed

A6: Int (Cl B) = B by A3, TOPS_1:def 8;

Int B c= Int A by A4, TOPS_1:19;

then A7: Cl (Int B) c= Cl (Int A) by PRE_TOPC:19;

A8: Cl (Int B) = Cl B by A3, Def2;

Int A c= Int (Cl B) by A5, TOPS_1:19;

then Cl (Int A) c= Cl B by A6, PRE_TOPC:19;

then A9: Cl B = Cl (Int A) by A7, A8, XBOOLE_0:def 10;

Cl B c= Cl A by A4, PRE_TOPC:19;

then A10: Int (Cl B) c= Int (Cl A) by TOPS_1:19;

Cl A c= Cl (Cl B) by A5, PRE_TOPC:19;

then Int (Cl A) c= Int (Cl (Cl B)) by TOPS_1:19;

then B = Int (Cl A) by A6, A10, XBOOLE_0:def 10;

hence A is condensed by A4, A5, A9, Th10; :: thesis: verum