let TS be TopSpace; :: thesis: for K, L being Subset of TS holds (Cl K) \ (Cl L) c= Cl (K \ L)
let K, L be Subset of TS; :: thesis: (Cl K) \ (Cl L) c= Cl (K \ L)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Cl K) \ (Cl L) or x in Cl (K \ L) )
(Cl K) \/ (Cl L) = Cl (K \/ L) by PRE_TOPC:20
.= Cl ((K \ L) \/ L) by XBOOLE_1:39
.= (Cl (K \ L)) \/ (Cl L) by PRE_TOPC:20 ;
then A1: ( x in (Cl K) \/ (Cl L) iff ( x in Cl (K \ L) or x in Cl L ) ) by XBOOLE_0:def 3;
assume A2: x in (Cl K) \ (Cl L) ; :: thesis: x in Cl (K \ L)
then x in Cl K by XBOOLE_0:def 5;
hence x in Cl (K \ L) by A2, A1, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis: verum