theorem :: SERIES_3:24

for x, a being Real st |.x.| <= a holds
x ^2 <= a ^2