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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^^ (B /\ C) or x in (A ^^ B) /\ (A ^^ C) )
assume x in A ^^ (B /\ C) ; :: thesis: x in (A ^^ B) /\ (A ^^ C)
then consider a, bc being Element of E ^omega such that
A1: ( a in A & bc in B /\ C & x = a ^ bc ) by Def1;
( bc in B & bc in C ) by A1, XBOOLE_0:def 4;
then ( x in A ^^ B & x in A ^^ C ) by A1, Def1;
hence x in (A ^^ B) /\ (A ^^ C) by XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (B /\ C) ^^ A or x in (B ^^ A) /\ (C ^^ A) )
assume x in (B /\ C) ^^ A ; :: thesis: x in (B ^^ A) /\ (C ^^ A)
then consider bc, a being Element of E ^omega such that
A2: ( bc in B /\ C & a in A & x = bc ^ a ) by Def1;
( bc in B & bc in C ) by A2, XBOOLE_0:def 4;
then ( x in B ^^ A & x in C ^^ A ) by A2, Def1;
hence x in (B ^^ A) /\ (C ^^ A) by XBOOLE_0:def 4; :: thesis: verum

end;