let T be TopSpace; :: thesis: for A being Subset of T holds

( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )

let A be Subset of T; :: thesis: ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )

A1: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;

thus ( A is subcondensed implies ( Cl A is regular_closed & Border A is empty ) ) :: thesis: ( Cl A is regular_closed & Border A is empty implies A is subcondensed )

A3: Cl A is regular_closed and

A4: Border A is empty ; :: thesis: A is subcondensed

(Int (Cl A)) \ (Cl (Int A)) is empty by A4, Th21;

then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;

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

Cl A = Cl (Int (Cl A)) by A3, TOPS_1:def 7;

then Cl (Int A) = Cl A by A5, A1, XBOOLE_0:def 10;

hence A is subcondensed ; :: thesis: verum

( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )

let A be Subset of T; :: thesis: ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )

A1: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;

thus ( A is subcondensed implies ( Cl A is regular_closed & Border A is empty ) ) :: thesis: ( Cl A is regular_closed & Border A is empty implies A is subcondensed )

proof

assume that
assume A2:
A is subcondensed
; :: thesis: ( Cl A is regular_closed & Border A is empty )

then Cl (Int A) = Cl A ;

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

then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37;

hence ( Cl A is regular_closed & Border A is empty ) by A2, Th21; :: thesis: verum

end;then Cl (Int A) = Cl A ;

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

then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37;

hence ( Cl A is regular_closed & Border A is empty ) by A2, Th21; :: thesis: verum

A3: Cl A is regular_closed and

A4: Border A is empty ; :: thesis: A is subcondensed

(Int (Cl A)) \ (Cl (Int A)) is empty by A4, Th21;

then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;

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

Cl A = Cl (Int (Cl A)) by A3, TOPS_1:def 7;

then Cl (Int A) = Cl A by A5, A1, XBOOLE_0:def 10;

hence A is subcondensed ; :: thesis: verum