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

( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )

let A be Subset of T; :: thesis: ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )

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

thus ( A is supercondensed implies ( Int A is regular_open & Border A is empty ) ) :: thesis: ( Int A is regular_open & Border A is empty implies A is supercondensed )

A3: Int A is regular_open and

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

(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: Int (Int (Cl A)) c= Int (Cl (Int A)) by TOPS_1:19;

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

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

hence A is supercondensed ; :: thesis: verum

( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )

let A be Subset of T; :: thesis: ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )

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

thus ( A is supercondensed implies ( Int A is regular_open & Border A is empty ) ) :: thesis: ( Int A is regular_open & Border A is empty implies A is supercondensed )

proof

assume that
assume A2:
A is supercondensed
; :: thesis: ( Int A is regular_open & Border A is empty )

then Int (Cl A) = Int A ;

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

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

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

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

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

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

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

A3: Int A is regular_open and

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

(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: Int (Int (Cl A)) c= Int (Cl (Int A)) by TOPS_1:19;

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

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

hence A is supercondensed ; :: thesis: verum