theorem :: ABSVALUE:2

for x being Real holds
( x = 0 iff |.x.| = 0 ) by COMPLEX1:47;