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

proof

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

end;

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