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 ) )
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 A1: A is supercondensed ; :: thesis: ( Int A is regular_open & Border A is empty )
then Int (Cl A) = Int A by Def1;
then Int (Cl A) c= Cl (Int A) by PRE_TOPC:48;
then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37;
hence ( Int A is regular_open & Border A is empty ) by A1, Def1, Th24; :: thesis: verum

end;

assume A2: ( Int A is regular_open & Border A is empty ) ; :: thesis: A is supercondensed
then A3: Int A = Int (Cl (Int A)) by TOPS_1:def 8;
(Int (Cl A)) \ (Cl (Int A)) is empty by A2, Th24;
then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;
then A4: Int (Int (Cl A)) c= Int (Cl (Int A)) by TOPS_1:48;
Int A c= Int (Cl A) by PRE_TOPC:48, TOPS_1:48;
then Int (Cl A) = Int A by A3, A4, XBOOLE_0:def 10;
hence A is supercondensed by Def1; :: thesis: verum