let a, b be positive Real; :: thesis: 2 / ((1 / a) + (1 / b)) <= (a + b) / 2
A1: (a + b) / 2 >= sqrt (a * b) by SERIES_3:2;
2 / ((1 / a) + (1 / b)) <= sqrt (a * b) by Th7;
hence 2 / ((1 / a) + (1 / b)) <= (a + b) / 2 by A1, XXREAL_0:2; :: thesis: verum