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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A ^^ B) \ (A ^^ C) or x in A ^^ (B \ C) )
assume x in (A ^^ B) \ (A ^^ C) ; :: thesis: x in A ^^ (B \ C)
then A1: ( x in A ^^ B & not x in A ^^ C ) by XBOOLE_0:def 5;
then consider a, b being Element of E ^omega such that
A2: ( a in A & b in B & x = a ^ b ) by Def1;

now

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

end;

hence x in A ^^ (B \ C) by A1, A2, Def1; :: thesis: verum

end;

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

proof

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

now

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

end;

hence x in (B \ C) ^^ A by A3, A4, Def1; :: thesis: verum

end;