theorem :: ABSVALUE:27

for r being Real holds 0 <= (- r) + |.r.|