for a, b being Real st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(a ^2) * (b ^2) <= 1