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

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

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

( P /\ (G \ C) = (P /\ G) \ C & (P /\ G) \ C c= P \ C )
by Th17, Th33, Th49;
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;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

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