let x, y be R_eal; :: thesis: ( x in REAL & y in REAL implies x + y in REAL )
assume ( x in REAL & y in REAL ) ; :: thesis: x + y in REAL
then consider a, b being Real such that
A1: ( x = a & y = b & x + y = a + b ) by SUPINF_2:def 2;
thus x + y in REAL by A1; :: thesis: verum