let a, b be positive Real; :: thesis: ( a < b implies a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) )
assume A1: a < b ; :: thesis: a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2)))
then A2: sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by Th5;
a / b < sqrt (a / b) by A1, Th4;
hence a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A2, XXREAL_0:2; :: thesis: verum