let P, G, C be set ; :: thesis: ( C c= G implies P \ C = (P \ G) \/ (P /\ (G \ C)) )
assume C c= G ; :: thesis: P \ C = (P \ G) \/ (P /\ (G \ C))
then A1: P \ G c= P \ C by Th34;
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 object ; :: 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;

( P /\ (G \ C) = (P /\ G) \ C & (P /\ G) \ C c= P \ C ) by Th17, Th33, Th49;
hence (P \ G) \/ (P /\ (G \ C)) c= P \ C by A1, Th8; :: thesis: verum