let M, N be Subset of V; :: thesis: M + N = N + M
for x being object st x in M + N holds
x in N + M
proof
let x be object ; :: 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 ;
for x being object st x in N + M holds
x in M + N
proof
let x be object ; :: 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 ;
hence M + N = N + M by A1; :: thesis: verum