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

for x being object st x in N + M holds

x in M + N

hence M + N = N + M by A1; :: thesis: verum

for x being object st x in M + N holds

x in N + M

proof

then A1:
M + N c= N + M
;
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;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

for x being object st x in N + M holds

x in M + N

proof

then
N + M c= M + N
;
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;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

hence M + N = N + M by A1; :: thesis: verum