begin
Lm1:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x, y being Point of T holds {x} + y = {y} + x
Lm2:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for p, x being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
Lm3:
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (-) B) (+) B c= X
begin
begin
begin
begin
:: Translation of X according to p