let x be real number ; :: thesis: ( abs x < 1 implies x ^2 < 1 )
assume abs x < 1 ; :: thesis: x ^2 < 1
then (abs x) ^2 < 1 ^2 by SQUARE_1:16;
hence x ^2 < 1 by COMPLEX1:75; :: thesis: verum