let a, b be Real; :: thesis: ( - 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 ; :: thesis: (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; :: thesis: verum

assume that

A1: - 1 <= a and

A2: a <= 1 and

A3: - 1 <= b and

A4: b <= 1 ; :: thesis: (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; :: thesis: verum