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 object st X in (Cl F) \ (Cl G) holds
X in Cl (F \ G)

proof

let X be object ; :: 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 reconsider X0 = X as Subset of T ;
X in Cl F by A1, XBOOLE_0:def 5;
then consider W being Subset of T such that
A2: X0 = Cl W and
A3: W in F by PCOMPS_1:def 2;
not X in Cl G by A1, XBOOLE_0:def 5;
then not W in G by A2, PCOMPS_1:def 2;
then W in F \ G by A3, XBOOLE_0:def 5;
hence X in Cl (F \ G) by A2, PCOMPS_1:def 2; :: thesis: verum

end;

hence (Cl F) \ (Cl G) c= Cl (F \ G) ; :: thesis: verum