theorem Th20: :: ABSVALUE:21

for x being Real st x <> 0 holds
(sgn x) * (sgn (1 / x)) = 1