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 ;
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 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 ; :: thesis: verum
end;
assume that
A3: Int A is regular_open and
A4: Border A is empty ; :: thesis:
(Int (Cl A)) \ (Cl (Int A)) is empty by ;
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 ;
then Int (Cl A) = Int A by ;
hence A is supercondensed ; :: thesis: verum