let a, b be positive Real; :: 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)))
then a / b < 1 by XREAL_1:189;
then A2: sqrt (a / b) < 1 by SQUARE_1:18, SQUARE_1:27;
sqrt (((a ^2) + (b ^2)) / 2) > 0 by SQUARE_1:25;
then 1 < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A1, Th3;
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