for a being positive Real
for x being Real st |.x.| >= a holds
x ^2 >= a ^2