theorem :: RELSET_3:25

for r being Real holds addRel (REAL,r) = { [r1,(r1 + r)] where r1 is Real : verum }