let a, b be real positive number ; :: thesis: ( a < b implies sqrt (a / b) < (b + (sqrt (((a ^2 ) + (b ^2 )) / 2))) / (a + (sqrt (((a ^2 ) + (b ^2 )) / 2))) )
assume A1: a < b ; :: thesis: sqrt (a / b) < (b + (sqrt (((a ^2 ) + (b ^2 )) / 2))) / (a + (sqrt (((a ^2 ) + (b ^2 )) / 2)))
sqrt (((a ^2 ) + (b ^2 )) / 2) > 0 by SQUARE_1:93;
then A2: 1 < (b + (sqrt (((a ^2 ) + (b ^2 )) / 2))) / (a + (sqrt (((a ^2 ) + (b ^2 )) / 2))) by A1, Th3;
a / b < 1 by A1, XREAL_1:191;
then sqrt (a / b) < 1 by SQUARE_1:83, SQUARE_1:95;
hence sqrt (a / b) < (b + (sqrt (((a ^2 ) + (b ^2 )) / 2))) / (a + (sqrt (((a ^2 ) + (b ^2 )) / 2))) by A2, XXREAL_0:2; :: thesis: verum