let x be real number ; :: thesis: ( 0 < x & x < 1 implies (1 + (x ^2 )) / (1 - (x ^2 )) > 1 )
assume A1: ( 0 < x & x < 1 ) ; :: thesis: (1 + (x ^2 )) / (1 - (x ^2 )) > 1
then x ^2 < x by SQUARE_1:75;
then x ^2 < 1 by A1, XXREAL_0:2;
then A2: (x ^2 ) + (- (x ^2 )) < 1 + (- (x ^2 )) by XREAL_1:10;
0 * x < x * x by A1, XREAL_1:70;
then 0 * 2 < (x ^2 ) * 2 by XREAL_1:70;
then 0 + (- (x ^2 )) < (2 * (x ^2 )) + (- (x ^2 )) by XREAL_1:10;
then (- (x ^2 )) + 1 < (x ^2 ) + 1 by XREAL_1:10;
hence (1 + (x ^2 )) / (1 - (x ^2 )) > 1 by A2, XREAL_1:189; :: thesis: verum