let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for x, y being Point of T holds {x} + y = {y} + x
let x, y be Point of T; :: thesis: {x} + y = {y} + x
thus {x} + y c= {y} + x :: according to XBOOLE_0:def 10 :: thesis: {y} + x c= {x} + y

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {x} + y or x1 in {y} + x )
assume x1 in {x} + y ; :: thesis: x1 in {y} + x
then consider p1 being Point of T such that
A1: x1 = p1 + y and
A2: p1 in {x} ;
{p1} c= {x} by A2, ZFMISC_1:31;
then A3: x1 = x + y by A1, ZFMISC_1:18;
y in {y} by TARSKI:def 1;
hence x1 in {y} + x by A3; :: thesis: verum

end;

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {y} + x or x1 in {x} + y )
assume x1 in {y} + x ; :: thesis: x1 in {x} + y
then consider p1 being Point of T such that
A4: x1 = p1 + x and
A5: p1 in {y} ;
{p1} c= {y} by A5, ZFMISC_1:31;
then A6: x1 = x + y by A4, ZFMISC_1:18;
x in {x} by TARSKI:def 1;
hence x1 in {x} + y by A6; :: thesis: verum