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:83, SQUARE_1:95, XREAL_1:65;
hence abs x < 1 by COMPLEX1:158; :: thesis: verum