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