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

proof

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

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in {(0. T)} + x )
assume a in {x} ; :: thesis: a in {(0. T)} + x
then {a} c= {x} by ZFMISC_1:31;
then a = x by ZFMISC_1:18;
then A3: a = (0. T) + x ;
0. T in {(0. T)} by ZFMISC_1:31;
hence a in {(0. T)} + x by A3; :: thesis: verum