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

proof

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

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x + (M + N) or z in (x + M) + N )
assume z in x + (M + N) ; :: thesis: z in (x + M) + N
then consider u being Point of X such that
A9: x + u = z and
A10: u in M + N by A1;
consider w, v being Point of X such that
A11: w + v = u and
A12: w in M and
A13: v in N by A3, A10;
A14: x + w in x + M by A2, A12;
(x + w) + v = z by A9, A11, RLVECT_1:def 3;
hence z in (x + M) + N by A4, A13, A14; :: thesis: verum