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