let r, r1 be Real; :: thesis: [r1,(r1 + r)] in addRel (REAL,r)
( r1 in REAL & r1 + r in REAL ) by XREAL_0:def 1;
hence [r1,(r1 + r)] in addRel (REAL,r) by Th11; :: thesis: verum