theorem :: RELSET_3:22

for r, r1, r2 being Real
for X being real-membered set holds
( [r1,r2] in addRel (X,r) iff ( r1 in X & r2 in X & r2 = r + r1 ) ) by Th11;