let T be TopSpace; :: thesis: for F, G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl (F \ G)
let F, G be Subset-Family of T; :: thesis: (Cl F) \ (Cl G) c= Cl (F \ G)
for X being set st X in (Cl F) \ (Cl G) holds
X in Cl (F \ G)

proof

let X be set ; :: thesis: ( X in (Cl F) \ (Cl G) implies X in Cl (F \ G) )
assume A1: X in (Cl F) \ (Cl G) ; :: thesis: X in Cl (F \ G)
then A2: ( X in Cl F & not X in Cl G ) by XBOOLE_0:def 5;
reconsider X0 = X as Subset of T by A1;
consider W being Subset of T such that
A3: X0 = Cl W and
A4: W in F by A2, PCOMPS_1:def 3;
not W in G by A2, A3, PCOMPS_1:def 3;
then W in F \ G by A4, XBOOLE_0:def 5;
hence X in Cl (F \ G) by A3, PCOMPS_1:def 3; :: thesis: verum

end;

hence (Cl F) \ (Cl G) c= Cl (F \ G) by TARSKI:def 3; :: thesis: verum