theorem :: JORDAN2B:22

for r1, r2 being Real holds |[(r1 + r2)]| = |[r1]| + |[r2]| by RVSUM_1:13;