let a, b be negative Real; :: thesis: ((a / b) + (b / a)) / 2 >= 1
A1: ( (a * a) / (a * b) = a / b & (b * b) / (a * b) = b / a ) by XCMPLX_1:91;
not (a - b) * (a - b) is negative ;
then (((a * a) - ((2 * a) * b)) + (b * b)) + ((2 * a) * b) >= 0 + ((2 * a) * b) by XREAL_1:6;
then ((a * a) + (b * b)) / ((2 * a) * b) >= ((2 * a) * b) / ((2 * a) * b) by XREAL_1:72;
then ((a * a) + (b * b)) / (2 * (a * b)) >= 1 by XCMPLX_1:60;
then (((a * a) + (b * b)) / (a * b)) / 2 >= 1 by XCMPLX_1:78;
hence ((a / b) + (b / a)) / 2 >= 1 by A1; :: thesis: verum