theorem :: ABSVALUE:1

for x being Real holds
( |.x.| = x or |.x.| = - x ) by Def1;