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