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 ) )
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 A1: A is subcondensed ; :: thesis: ( Cl A is regular_closed & Border A is empty )
then Cl (Int A) = Cl A by Def2;
then Int (Cl A) c= Cl (Int A) by TOPS_1:44;
then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37;
hence ( Cl A is regular_closed & Border A is empty ) by A1, Def2, Th24; :: thesis: verum

end;

assume A2: ( Cl A is regular_closed & Border A is empty ) ; :: thesis: A is subcondensed
then A3: Cl A = Cl (Int (Cl A)) by TOPS_1:def 7;
(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: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:49;
Cl (Int A) c= Cl A by PRE_TOPC:49, TOPS_1:44;
then Cl (Int A) = Cl A by A3, A4, XBOOLE_0:def 10;
hence A is subcondensed by Def2; :: thesis: verum