let TS be TopSpace; :: thesis: for K, L being Subset of TS holds Int (K \ L) c= (Int K) \ (Int L)
let K, L be Subset of TS; :: thesis: Int (K \ L) c= (Int K) \ (Int L)
A1: Int (K \ L) = (Cl ((K /\ (L `)) `)) ` by SUBSET_1:13
.= (Cl ((K `) \/ ((L `) `))) ` by XBOOLE_1:54
.= ((Cl (K `)) \/ (Cl L)) ` by PRE_TOPC:20
.= ((Cl L) `) /\ (Int K) by XBOOLE_1:53 ;
L c= Cl L by PRE_TOPC:18;
then A2: (Cl L) ` c= L ` by SUBSET_1:12;
Int L c= L by Th16;
then L ` c= (Int L) ` by SUBSET_1:12;
then (Cl L) ` c= (Int L) ` by A2;
then Int (K \ L) c= (Int K) /\ ((Int L) `) by A1, XBOOLE_1:26;
hence Int (K \ L) c= (Int K) \ (Int L) by SUBSET_1:13; :: thesis: verum