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:17
.= Int ((Int A) /\ ((Int A) `)) by TOPS_1:17
.= Int ({} T) by A1
.= {} T ; :: thesis: verum