let V be non empty Abelian addLoopStr ; :: thesis: for M, N being Subset of V holds N + M = M + N
let M, N be Subset of V; :: thesis: N + M = M + N
for x being set st x in M + N holds
x in N + M

proof

let x be set ; :: thesis: ( x in M + N implies x in N + M )
assume x in M + N ; :: thesis: x in N + M
then ex u1, v1 being Element of V st
( x = u1 + v1 & u1 in M & v1 in N ) ;
hence x in N + M ; :: thesis: verum

end;

then A1: M + N c= N + M by TARSKI:def 3;
for x being set st x in N + M holds
x in M + N

proof

let x be set ; :: thesis: ( x in N + M implies x in M + N )
assume x in N + M ; :: thesis: x in M + N
then ex u1, v1 being Element of V st
( x = u1 + v1 & u1 in N & v1 in M ) ;
hence x in M + N ; :: thesis: verum

end;

then N + M c= M + N by TARSKI:def 3;
hence N + M = M + N by A1, XBOOLE_0:def 10; :: thesis: verum