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:32
.= (Cl ((K ` ) \/ ((L ` ) ` ))) ` by XBOOLE_1:54
.= ((Cl (K ` )) \/ (Cl L)) ` by PRE_TOPC:50
.= ((Cl L) ` ) /\ (Int K) by XBOOLE_1:53 ;
L c= Cl L by PRE_TOPC:48;
then A2: (Cl L) ` c= L ` by SUBSET_1:31;
Int L c= L by Th44;
then L ` c= (Int L) ` by SUBSET_1:31;
then (Cl L) ` c= (Int L) ` by A2, XBOOLE_1:1;
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:32; :: thesis: verum