let GX be TopStruct ; :: thesis: for T being Subset of GX holds Int T misses Fr T
let T be Subset of GX; :: thesis: Int T misses Fr T
Fr T = (Cl T) /\ (((Cl (T `)) `) `)
.= (Cl T) \ ((Cl (T `)) `) by SUBSET_1:13 ;
hence Int T misses Fr T by XBOOLE_1:79; :: thesis: verum