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

( 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