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