theorem :: ABSVALUE:26

for r being Real holds 0 <= r + |.r.|