let X be TopSpace; :: thesis: for A being Subset of X st A misses Int (Cl A) holds
Int (Cl A) = {}
let A be Subset of X; :: thesis: ( A misses Int (Cl A) implies Int (Cl A) = {} )
reconsider A9 = A as Subset of X ;
assume A /\ (Int (Cl A)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: Int (Cl A) = {}
then A9 misses Int (Cl A9) ;
then Cl A misses Int (Cl A) by TSEP_1:36;
then (Cl A) /\ (Int (Cl A)) = {} ;
hence Int (Cl A) = {} by TOPS_1:16, XBOOLE_1:28; :: thesis: verum