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 )

A1: now

A2: A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) by Th20;
A3: (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) c= A ^^ ((B \/ C) \ (B /\ C)) by Th22;
(A ^^ B) \+\ (A ^^ C) = ((A ^^ B) \/ (A ^^ C)) \ ((A ^^ B) /\ (A ^^ C)) by XBOOLE_1:101
.= (A ^^ (B \/ C)) \ ((A ^^ B) /\ (A ^^ C)) by Th21 ;
then (A ^^ B) \+\ (A ^^ C) c= (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) by A2, XBOOLE_1:34;
then (A ^^ B) \+\ (A ^^ C) c= A ^^ ((B \/ C) \ (B /\ C)) by A3, XBOOLE_1:1;
hence (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) by XBOOLE_1:101; :: thesis: verum

end;

now

A4: (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) by Th20;
A5: ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by Th22;
(B ^^ A) \+\ (C ^^ A) = ((B ^^ A) \/ (C ^^ A)) \ ((B ^^ A) /\ (C ^^ A)) by XBOOLE_1:101
.= ((B \/ C) ^^ A) \ ((B ^^ A) /\ (C ^^ A)) by Th21 ;
then (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) by A4, XBOOLE_1:34;
then (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by A5, XBOOLE_1:1;
hence (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A by XBOOLE_1:101; :: thesis: verum

end;

hence ( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A ) by A1; :: thesis: verum