let a, b be positive Real; :: thesis: 2 / ((1 / a) + (1 / b)) <= sqrt (((a ^2) + (b ^2)) / 2)
A1: 2 / ((1 / a) + (1 / b)) <= (a + b) / 2 by Th10;
(a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) by Th8;
hence 2 / ((1 / a) + (1 / b)) <= sqrt (((a ^2) + (b ^2)) / 2) by A1, XXREAL_0:2; :: thesis: verum