let a, b be real number ; :: thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies ( (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) & - (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) ) )
assume A1: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 ) ; :: thesis: ( (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) & - (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) )
a ^2 >= 0 by XREAL_1:65;
then A2: 1 + (a ^2 ) >= 1 + 0 by XREAL_1:9;
then A3: sqrt (1 + (a ^2 )) >= 0 by Def4;
b ^2 >= 0 by XREAL_1:65;
then 1 + (b ^2 ) >= 1 + 0 by XREAL_1:9;
then A4: sqrt (1 + (b ^2 )) >= 0 by Def4;

A5: now

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 ))

then - b <= 0 ;
hence (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) by A3, A4; :: thesis: verum

end;

suppose b < 0 ; :: thesis: (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 ))

then - b > 0 ;
then A6: (- b) * (sqrt (1 + (a ^2 ))) = sqrt (((- b) ^2 ) * (1 + (a ^2 ))) by A2, Th124;
(- b) ^2 >= 0 by XREAL_1:65;
then ((- b) ^2 ) * (1 + (a ^2 )) >= 0 by A2;
hence (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) by A1, A6, Lm7, Th94; :: thesis: verum

end;

end;

end;

then - ((- b) * (sqrt (1 + (a ^2 )))) >= - (sqrt (1 + (b ^2 ))) by XREAL_1:26;
hence ( (- b) * (sqrt (1 + (a ^2 ))) <= sqrt (1 + (b ^2 )) & - (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 ))) ) by A5; :: thesis: verum