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