let T be TopSpace; :: thesis: for A being Subset of T holds
( A is subcondensed iff A c= Cl (Int A) )
let A be Subset of T; :: thesis: ( A is subcondensed iff A c= Cl (Int A) )
thus ( A is subcondensed implies A c= Cl (Int A) ) :: thesis: ( A c= Cl (Int A) implies A is subcondensed )

proof

assume A is subcondensed ; :: thesis: A c= Cl (Int A)
then Cl (Int A) = Cl A by Def2;
hence A c= Cl (Int A) by PRE_TOPC:48; :: thesis: verum

end;

assume A c= Cl (Int A) ; :: thesis: A is subcondensed
then A1: 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 A1, XBOOLE_0:def 10;
hence A is subcondensed by Def2; :: thesis: verum