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