let a, b be Real; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (1 + (a ^2)) * (b ^2) <= 1 + (b ^2) )

assume that

A1: - 1 <= a and

A2: a <= 1 and

A3: - 1 <= b and

A4: b <= 1 ; :: thesis: (1 + (a ^2)) * (b ^2) <= 1 + (b ^2)

(a ^2) * (b ^2) <= 1 by A1, A2, A3, A4, Th53;

then (1 * (b ^2)) + ((a ^2) * (b ^2)) <= 1 + (b ^2) by XREAL_1:7;

hence (1 + (a ^2)) * (b ^2) <= 1 + (b ^2) ; :: thesis: verum

assume that

A1: - 1 <= a and

A2: a <= 1 and

A3: - 1 <= b and

A4: b <= 1 ; :: thesis: (1 + (a ^2)) * (b ^2) <= 1 + (b ^2)

(a ^2) * (b ^2) <= 1 by A1, A2, A3, A4, Th53;

then (1 * (b ^2)) + ((a ^2) * (b ^2)) <= 1 + (b ^2) by XREAL_1:7;

hence (1 + (a ^2)) * (b ^2) <= 1 + (b ^2) ; :: thesis: verum