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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) (Y + p) or x in (X (+) Y) + p )
assume x in X (+) (Y + p) ; :: thesis: x in (X (+) Y) + p
then consider x2, y2 being Point of T such that
A1: ( x = x2 + y2 & x2 in X ) and
A2: y2 in Y + p ;
consider y3 being Point of T such that
A3: ( y2 = y3 + p & y3 in Y ) by A2;
( x = (x2 + y3) + p & x2 + y3 in X (+) Y ) by A1, A3, RLVECT_1:def 3;
hence x in (X (+) Y) + p ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (+) Y) + p or x in X (+) (Y + p) )
assume x in (X (+) Y) + p ; :: thesis: x in X (+) (Y + p)
then consider x2 being Point of T such that
A4: x = x2 + p and
A5: x2 in X (+) Y ;
consider x3, y3 being Point of T such that
A6: x2 = x3 + y3 and
A7: x3 in X and
A8: y3 in Y by A5;
A9: y3 + p in Y + p by A8;
x = x3 + (y3 + p) by A4, A6, RLVECT_1:def 3;
hence x in X (+) (Y + p) by A7, A9; :: thesis: verum