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

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