theorem :: ABSVALUE:7

for x being Real holds |.(1 / x).| = 1 / |.x.| by COMPLEX1:80;