theorem :: ABSVALUE:28

for r, s being Real holds
( not |.r.| = |.s.| or r = s or r = - s )