let x be R_eal; :: thesis: |.|.x.|.| = |.x.|
0 <= |.x.| by Th51;
hence |.|.x.|.| = |.x.| by EXTREAL1:def 3; :: thesis: verum