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

proof

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

end;

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