now :: thesis: for I, J being Subset of R holds I + J = J + I

let I, J be Subset of R; :: thesis: I + J = J + I

A1: now :: thesis: for u being object st u in J + I holds
u in I + J

let u be object ; :: thesis: ( u in J + I implies u in I + J )
assume u in J + I ; :: thesis: u in I + J
then ex a, b being Element of R st
( u = a + b & a in J & b in I ) ;
hence u in I + J ; :: thesis: verum

end;

now :: thesis: for u being object st u in I + J holds
u in J + I

let u be object ; :: thesis: ( u in I + J implies u in J + I )
assume u in I + J ; :: thesis: u in J + I
then ex a, b being Element of R st
( u = a + b & a in I & b in J ) ;
hence u in J + I ; :: thesis: verum

end;

hence I + J = J + I by A1, TARSKI:2; :: thesis: verum

end;

hence for I, J being Subset of R holds I + J = J + I ; :: thesis: verum