theorem :: REALALG2:79

for R being preordered domRing
for P being Preordering of R
for a, b being b₂ -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))