let r1, r2 be real number ; :: thesis: |[(r1 + r2)]| = |[r1]| + |[r2]|
reconsider r1 = r1, r2 = r2 as Real by XREAL_0:def 1;
reconsider rr1 = |[r1]|, rr2 = |[r2]| as Element of REAL 1 by EUCLID:22;
|[(r1 + r2)]| = rr1 + rr2 by RVSUM_1:13;
hence |[(r1 + r2)]| = |[r1]| + |[r2]| by EUCLID:64; :: thesis: verum