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 A' = A as Subset of X ;
assume A /\ (Int (Cl A)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: Int (Cl A) = {}
then A' misses Int (Cl A') by XBOOLE_0:def 7;
then Cl A misses Int (Cl A) by TSEP_1:40;
then ( (Cl A) /\ (Int (Cl A)) = {} & Int (Cl A) c= Cl A ) by TOPS_1:44, XBOOLE_0:def 7;
hence Int (Cl A) = {} by XBOOLE_1:28; :: thesis: verum