let a, b be Real; ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (a ^2) * (b ^2) <= 1 )
assume that
A1:
- 1 <= a
and
A2:
a <= 1
and
A3:
- 1 <= b
and
A4:
b <= 1
; (a ^2) * (b ^2) <= 1
A5:
0 <= b ^2
by XREAL_1:63;
a ^2 <= 1 ^2
by A1, A2, Th49;
then A6:
(a ^2) * (b ^2) <= 1 * (b ^2)
by A5, XREAL_1:64;
b ^2 <= 1 ^2
by A3, A4, Th49;
hence
(a ^2) * (b ^2) <= 1
by A6, XXREAL_0:2; verum