let T be TopSpace; :: thesis: for A being Subset of T holds Int (A /\ (Cl (A ` ))) = {} T
let A be Subset of T; :: thesis: Int (A /\ (Cl (A ` ))) = {} T
A1: Int A misses (Int A) ` by XBOOLE_1:79;
thus Int (A /\ (Cl (A ` ))) = Int (A /\ (((Cl (A ` )) ` ) ` ))
.= Int (A /\ ((Int A) ` )) by TOPS_1:def 1
.= (Int (Int A)) /\ (Int ((Int A) ` )) by TOPS_1:46
.= Int ((Int A) /\ ((Int A) ` )) by TOPS_1:46
.= Int ({} T) by A1, XBOOLE_0:def 7
.= {} T ; :: thesis: verum