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

proof

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

end;

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