let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X being Subset of T
for x, y being Point of T holds (X + x) + y = X + (x + y)
let X be Subset of T; :: thesis: for x, y being Point of T holds (X + x) + y = X + (x + y)
let x, y be Point of T; :: thesis: (X + x) + y = X + (x + y)
thus (X + x) + y c= X + (x + y) :: according to XBOOLE_0:def 10 :: thesis: X + (x + y) c= (X + x) + y
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in (X + x) + y or p in X + (x + y) )
assume p in (X + x) + y ; :: thesis: p in X + (x + y)
then consider x2 being Point of T such that
A1: p = x2 + y and
A2: x2 in X + x ;
consider x3 being Point of T such that
A3: x2 = x3 + x and
A4: x3 in X by A2;
p = x3 + (x + y) by A1, A3, RLVECT_1:def 3;
hence p in X + (x + y) by A4; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X + (x + y) or p in (X + x) + y )
assume p in X + (x + y) ; :: thesis: p in (X + x) + y
then consider x2 being Point of T such that
A5: ( p = x2 + (x + y) & x2 in X ) ;
( p = (x2 + x) + y & x2 + x in X + x ) by A5, RLVECT_1:def 3;
hence p in (X + x) + y ; :: thesis: verum