theorem :: ABSVALUE:24

for x being Real holds sgn x = sgn (1 / x)