consider y being Element of Y;
consider x being Element of X;
reconsider x = x, y = y as R_eal ;
x + y = x + y ;
hence not X + Y is empty by Def5; :: thesis: verum