let a be Real; :: thesis: ( a ^2 < 1 implies ( - 1 < a & a < 1 ) )
assume a ^2 < 1 ; :: thesis: ( - 1 < a & a < 1 )
then (a ^2) - (1 ^2) < (1 ^2) - (1 ^2) by XREAL_1:9;
then (a - 1) * (a + 1) < 0 ;
hence ( - 1 < a & a < 1 ) by XREAL_1:94; :: thesis: verum