for a, x being Real st a <= 0 & x < a holds
x ^2 > a ^2