theorem :: RELSET_3:24

for r, r1 being Real holds [r1,(r1 + r)] in addRel (REAL,r)