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