theorem Th53: :: SQUARE_1:53

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