let a be real number ; :: 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:11;
then (a - 1) * (a + 1) <= 0 ;
hence ( - 1 <= a & a <= 1 ) by XREAL_1:95; :: thesis: verum