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:93; :: thesis: verum