let a, b be real positive number ; :: 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: a / b < sqrt (a / b) by Th4;
sqrt (a / b) < (b + (sqrt (((a ^2 ) + (b ^2 )) / 2))) / (a + (sqrt (((a ^2 ) + (b ^2 )) / 2))) by A1, Th5;
hence a / b < (b + (sqrt (((a ^2 ) + (b ^2 )) / 2))) / (a + (sqrt (((a ^2 ) + (b ^2 )) / 2))) by A2, XXREAL_0:2; :: thesis: verum