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