let a be positive light Real; :: thesis: (1 / (1 + a)) + (1 / (1 - a)) > 2
A1: 1 - (a * a) < 1 - 0 by XREAL_1:10;
A2: ( (1 * (1 - a)) / ((1 - a) * (1 + a)) = 1 / (1 + a) & (1 * (1 + a)) / ((1 + a) * (1 - a)) = 1 / (1 - a) ) by XCMPLX_1:91;
((1 - a) + (1 + a)) / ((1 - a) * (1 + a)) > ((1 - a) + (1 + a)) / 1 by A1, XREAL_1:76;
hence (1 / (1 + a)) + (1 / (1 - a)) > 2 by A2; :: thesis: verum