theorem :: ABSVALUE:30

for r being Real st r <= 0 holds
|.r.| = - r