theorem :: RELSET_3:21

for r being Real
for X being real-membered set holds addRel (X,r) = ((curry addreal) . r) |_2 X