theorem :: SQUARE_1:51

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