let a, b be real number ; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (a ^2 ) * (b ^2 ) <= 1 )
assume A1: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 ) ; :: thesis: (a ^2 ) * (b ^2 ) <= 1
then A2: a ^2 <= 1 ^2 by Th119;
A3: b ^2 <= 1 ^2 by A1, Th119;
0 <= b ^2 by XREAL_1:65;
then (a ^2 ) * (b ^2 ) <= 1 * (b ^2 ) by A2, XREAL_1:66;
hence (a ^2 ) * (b ^2 ) <= 1 by A3, XXREAL_0:2; :: thesis: verum