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

proof

consider y being Element of J;
consider x being Element of I;
x + y 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