theorem Th16: :: ABSVALUE:16

for x being Real st sgn x = 0 holds
x = 0