let a be positive light Real; :: thesis: 1 + a < 1 / (1 - a)
1 - (a * a) < 1 - 0 by XREAL_1:10;
then ( (1 + a) * (1 - a) < 1 & 1 - a > 0 ) ;
hence 1 + a < 1 / (1 - a) by XREAL_1:81; :: thesis: verum