let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z
let X, Y, Z be Subset of T; :: thesis: X (+) (Y (+) Z) = (X (+) Y) (+) Z
thus X (+) (Y (+) Z) c= (X (+) Y) (+) Z :: according to XBOOLE_0:def 10 :: thesis: (X (+) Y) (+) Z c= X (+) (Y (+) Z)

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X (+) (Y (+) Z) or p in (X (+) Y) (+) Z )
assume p in X (+) (Y (+) Z) ; :: thesis: p in (X (+) Y) (+) Z
then consider x1, p2 being Point of T such that
A1: ( p = x1 + p2 & x1 in X ) and
A2: p2 in Y (+) Z ;
consider y, z being Point of T such that
A3: ( p2 = y + z & y in Y ) and
A4: z in Z by A2;
set p3 = x1 + y;
( p = (x1 + y) + z & x1 + y in X (+) Y ) by A1, A3, RLVECT_1:def 3;
hence p in (X (+) Y) (+) Z by A4; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in (X (+) Y) (+) Z or p in X (+) (Y (+) Z) )
assume p in (X (+) Y) (+) Z ; :: thesis: p in X (+) (Y (+) Z)
then consider x1, p2 being Point of T such that
A5: p = x1 + p2 and
A6: x1 in X (+) Y and
A7: p2 in Z ;
consider y, z being Point of T such that
A8: x1 = y + z and
A9: y in X and
A10: z in Y by A6;
set p3 = z + p2;
( p = y + (z + p2) & z + p2 in Y (+) Z ) by A5, A7, A8, A10, RLVECT_1:def 3;
hence p in X (+) (Y (+) Z) by A9; :: thesis: verum