let E be set ; :: thesis: for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )
let A, B, C be Subset of (E ^omega); :: thesis: ( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )
thus (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) :: thesis: (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ^^ B) \ (A ^^ C) or x in A ^^ (B \ C) )
assume A1: x in (A ^^ B) \ (A ^^ C) ; :: thesis: x in A ^^ (B \ C)
then x in A ^^ B by XBOOLE_0:def 5;
then consider a, b being Element of E ^omega such that
A2: a in A and
A3: b in B and
A4: x = a ^ b by Def1;

A5: now :: thesis: ( not b in C implies x in A ^^ (B \ C) )

assume not b in C ; :: thesis: x in A ^^ (B \ C)
then b in B \ C by A3, XBOOLE_0:def 5;
hence x in A ^^ (B \ C) by A2, A4, Def1; :: thesis: verum

end;

not x in A ^^ C by A1, XBOOLE_0:def 5;
hence x in A ^^ (B \ C) by A2, A4, A5, Def1; :: thesis: verum

end;

thus (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B ^^ A) \ (C ^^ A) or x in (B \ C) ^^ A )
assume A6: x in (B ^^ A) \ (C ^^ A) ; :: thesis: x in (B \ C) ^^ A
then x in B ^^ A by XBOOLE_0:def 5;
then consider b, a being Element of E ^omega such that
A7: b in B and
A8: ( a in A & x = b ^ a ) by Def1;

A9: now :: thesis: ( not b in C implies x in (B \ C) ^^ A )

assume not b in C ; :: thesis: x in (B \ C) ^^ A
then b in B \ C by A7, XBOOLE_0:def 5;
hence x in (B \ C) ^^ A by A8, Def1; :: thesis: verum

end;

not x in C ^^ A by A6, XBOOLE_0:def 5;
hence x in (B \ C) ^^ A by A8, A9, Def1; :: thesis: verum

end;