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:78;
hence x ^2 < 1 by COMPLEX1:161; :: thesis: verum