let X be non empty add-associative addLoopStr ; :: thesis: for x, y being Point of X
for M being Subset of X holds (x + y) + M = x + (y + M)
let x, y be Point of X; :: thesis: for M being Subset of X holds (x + y) + M = x + (y + M)
let M be Subset of X; :: thesis: (x + y) + M = x + (y + M)
A1: x + (y + M) = { (x + u) where u is Point of X : u in y + M } by RUSUB_4:def 8;
A2: y + M = { (y + u) where u is Point of X : u in M } by RUSUB_4:def 8;
A3: (x + y) + M = { ((x + y) + u) where u is Point of X : u in M } by RUSUB_4:def 8;
thus (x + y) + M c= x + (y + M) :: according to XBOOLE_0:def 10 :: thesis: x + (y + M) c= (x + y) + M

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (x + y) + M or z in x + (y + M) )
assume z in (x + y) + M ; :: thesis: z in x + (y + M)
then consider u being Point of X such that
A4: ( (x + y) + u = z & u in M ) by A3;
( x + (y + u) = z & y + u in y + M ) by A2, A4, RLVECT_1:def 3;
hence z in x + (y + M) by A1; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x + (y + M) or z in (x + y) + M )
assume z in x + (y + M) ; :: thesis: z in (x + y) + M
then consider u being Point of X such that
A5: x + u = z and
A6: u in y + M by A1;
consider v being Point of X such that
A7: y + v = u and
A8: v in M by A2, A6;
(x + y) + v = z by A5, A7, RLVECT_1:def 3;
hence z in (x + y) + M by A3, A8; :: thesis: verum