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 + p) (+) Y = (X (+) Y) + p
let X, Y be Subset of T; :: thesis: for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p
let p be Point of T; :: thesis: (X + p) (+) Y = (X (+) Y) + p
thus (X + p) (+) Y c= (X (+) Y) + p :: according to XBOOLE_0:def 10 :: thesis: (X (+) Y) + p c= (X + p) (+) Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X + p) (+) Y or x in (X (+) Y) + p )
assume x in (X + p) (+) Y ; :: thesis: x in (X (+) Y) + p
then consider x2, y2 being Point of T such that
A1: x = x2 + y2 and
A2: x2 in X + p and
A3: y2 in Y ;
consider x3 being Point of T such that
A4: ( x2 = x3 + p & x3 in X ) by A2;
( x = (x3 + y2) + p & x3 + y2 in X (+) Y ) by A1, A3, A4, 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 + p) (+) Y )
assume x in (X (+) Y) + p ; :: thesis: x in (X + p) (+) Y
then consider x2 being Point of T such that
A5: x = x2 + p and
A6: x2 in X (+) Y ;
consider x3, y3 being Point of T such that
A7: x2 = x3 + y3 and
A8: x3 in X and
A9: y3 in Y by A6;
A10: x3 + p in X + p by A8;
x = (x3 + p) + y3 by A5, A7, RLVECT_1:def 3;
hence x in (X + p) (+) Y by A9, A10; :: thesis: verum