theorem :: SQUARE_1:57

for a, b being Real st a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))