theorem :: SQUARE_1:52

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