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