now

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

A1: now

let u be set ; :: thesis: ( u in I + J implies u in J + I )
assume u in I + J ; :: thesis: u in J + I
then consider a, b being Element of R such that
A2: ( u = a + b & a in I & b in J ) ;
thus u in J + I by A2; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in J + I implies u in I + J )
assume u in J + I ; :: thesis: u in I + J
then consider a, b being Element of R such that
A3: ( u = a + b & a in J & b in I ) ;
thus u in I + J by A3; :: 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