let x be real number ; :: thesis: ( (x ^2 ) - 1 <= 0 implies ( - 1 <= x & x <= 1 ) )
assume (x ^2 ) - 1 <= 0 ; :: thesis: ( - 1 <= x & x <= 1 )
then ( 1 >= 0 & (x - 1) * (x + 1) <= 0 ) ;
hence ( - 1 <= x & x <= 1 ) by XREAL_1:95; :: thesis: verum