let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)
let X, B, C be Subset of T; :: thesis: X (+) (B \/ C) = (X (+) B) \/ (X (+) C)
thus X (+) (B \/ C) c= (X (+) B) \/ (X (+) C) :: according to XBOOLE_0:def 10 :: thesis: (X (+) B) \/ (X (+) C) c= X (+) (B \/ C)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) (B \/ C) or x in (X (+) B) \/ (X (+) C) )
assume x in X (+) (B \/ C) ; :: thesis: x in (X (+) B) \/ (X (+) C)
then consider y3, y4 being Point of T such that
A1: ( x = y3 + y4 & y3 in X ) and
A2: y4 in B \/ C ;
( y4 in B or y4 in C ) by A2, XBOOLE_0:def 3;
then ( x in { (y1 + y2) where y1, y2 is Point of T : ( y1 in X & y2 in B ) } or x in { (y1 + y2) where y1, y2 is Point of T : ( y1 in X & y2 in C ) } ) by A1;
hence x in (X (+) B) \/ (X (+) C) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (+) B) \/ (X (+) C) or x in X (+) (B \/ C) )
assume x in (X (+) B) \/ (X (+) C) ; :: thesis: x in X (+) (B \/ C)
then ( x in X (+) B or x in X (+) C ) by XBOOLE_0:def 3;
then consider y3, y4 being Point of T such that
A3: ( ( x = y3 + y4 & y3 in X & y4 in B ) or ( x = y3 + y4 & y3 in X & y4 in C ) ) ;
y4 in B \/ C by A3, XBOOLE_0:def 3;
hence x in X (+) (B \/ C) by A3; :: thesis: verum