not { (x + y) where x, y is Element of R : ( x in I & y in J ) } is empty

proof

set y = the Element of J;
set x = the Element of I;
the Element of I + the Element of J in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
hence not { (x + y) where x, y is Element of R : ( x in I & y in J ) } is empty ; :: thesis: verum

end;

hence not I + J is empty ; :: thesis: verum