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

( 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