let a, b be real number ; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 ) )
assume ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 ) ; :: thesis: (1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 )
then (a ^2 ) * (b ^2 ) <= 1 by Th123;
then (1 * (b ^2 )) + ((a ^2 ) * (b ^2 )) <= 1 + (b ^2 ) by XREAL_1:9;
hence (1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 ) ; :: thesis: verum