theorem :: ABSVALUE:29

for m being Nat holds m = |.m.| ;