theorem Th21: :: ABSVALUE:22

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