let x be Real; :: thesis: ( x ^2 < 1 implies |.x.| < 1 )
assume x ^2 < 1 ; :: thesis: |.x.| < 1
then sqrt (x ^2) < 1 by SQUARE_1:18, SQUARE_1:27, XREAL_1:63;
hence |.x.| < 1 by COMPLEX1:72; :: thesis: verum