let x be Real; :: thesis: ( |.x.| < 1 implies x ^2 < 1 )
assume |.x.| < 1 ; :: thesis: x ^2 < 1
then |.x.| ^2 < 1 ^2 by SQUARE_1:16;
hence x ^2 < 1 by COMPLEX1:75; :: thesis: verum