theorem :: SQUARE_1:43

for x being Real st (x ^2) - 1 <= 0 holds
( - 1 <= x & x <= 1 )