let a be positive heavy Real; (1 / (a + 1)) + (1 / (a - 1)) > 2 / a
A1:
( (1 * (a + 1)) / ((a - 1) * (a + 1)) = 1 / (a - 1) & (1 * (a - 1)) / ((a - 1) * (a + 1)) = 1 / (a + 1) & (2 * a) / (a * a) = 2 / a )
by XCMPLX_1:91;
( 1 - 1 < (a * a) - 1 & (a * a) - 1 < (a * a) - 0 )
by XREAL_1:6;
then
((a + 1) + (a - 1)) / ((a + 1) * (a - 1)) > ((a + 1) + (a - 1)) / (a * a)
by XREAL_1:76;
hence
(1 / (a + 1)) + (1 / (a - 1)) > 2 / a
by A1; verum