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 = { (u + v) where u, v is Point of X : ( u in x + M & v in N ) } by RUSUB_4:def 10;
A2: x + (M + N) = { (x + u) where u is Point of X : u in M + N } by RUSUB_4:def 9;
A3: x + M = { (x + u) where u is Point of X : u in M } by RUSUB_4:def 9;
A4: M + N = { (u + v) where u, v is Point of X : ( u in M & v in N ) } by RUSUB_4:def 10;
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 set ; :: 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 A1;
consider u' being Point of X such that
A8: x + u' = u and
A9: u' in M by A3, A6;
A10: x + (u' + v) = z by A5, A8, RLVECT_1:def 6;
u' + v in M + N by A4, A7, A9;
hence z in x + (M + N) by A2, A10; :: thesis: verum

end;

let z be set ; :: 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
A11: x + u = z and
A12: u in M + N by A2;
consider w, v being Point of X such that
A13: w + v = u and
A14: w in M and
A15: v in N by A4, A12;
A16: (x + w) + v = z by A11, A13, RLVECT_1:def 6;
x + w in x + M by A3, A14;
hence z in (x + M) + N by A1, A15, A16; :: thesis: verum