for a, b being Real st - a <= b & b <= a holds
b ^2 <= a ^2