let P, G, C be set ; :: thesis: ( C c= G implies P \ C = (P \ G) \/ (P /\ (G \ C)) )
assume A1: C c= G ; :: thesis: P \ C = (P \ G) \/ (P /\ (G \ C))
thus P \ C c= (P \ G) \/ (P /\ (G \ C)) :: according to XBOOLE_0:def 10 :: thesis: (P \ G) \/ (P /\ (G \ C)) c= P \ C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P \ C or x in (P \ G) \/ (P /\ (G \ C)) )
assume x in P \ C ; :: thesis: x in (P \ G) \/ (P /\ (G \ C))
then ( ( x in P & not x in G ) or ( x in P & x in G & not x in C ) ) by XBOOLE_0:def 5;
then ( x in P \ G or ( x in P & x in G \ C ) ) by XBOOLE_0:def 5;
then ( x in P \ G or x in P /\ (G \ C) ) by XBOOLE_0:def 4;
hence x in (P \ G) \/ (P /\ (G \ C)) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (P \ G) \/ (P /\ (G \ C)) or x in P \ C )
assume x in (P \ G) \/ (P /\ (G \ C)) ; :: thesis: x in P \ C
then ( x in P \ G or x in P /\ (G \ C) ) by XBOOLE_0:def 3;
then ( x in P \ G or ( x in P & x in G \ C ) ) by XBOOLE_0:def 4;
then ( x in P & not x in C ) by A1, XBOOLE_0:def 5;
hence x in P \ C by XBOOLE_0:def 5; :: thesis: verum