let T be TopSpace; :: thesis: for A being Subset of T holds
( A is supercondensed iff Int (Cl A) c= A )
let A be Subset of T; :: thesis: ( A is supercondensed iff Int (Cl A) c= A )
thus ( A is supercondensed implies Int (Cl A) c= A ) by TOPS_1:16; :: thesis: ( Int (Cl A) c= A implies A is supercondensed )
assume Int (Cl A) c= A ; :: thesis: A is supercondensed
then A1: Int (Int (Cl A)) c= Int A by TOPS_1:19;
Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
then Int A = Int (Cl A) by A1, XBOOLE_0:def 10;
hence A is supercondensed ; :: thesis: verum