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