let x be real number ; ( 0 < x & x < 1 implies (2 * x) / (1 - (x ^2 )) > 0 )
assume that
A1:
0 < x
and
A2:
x < 1
; (2 * x) / (1 - (x ^2 )) > 0
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 * 2 < x * 2
by A1, XREAL_1:70;
hence
(2 * x) / (1 - (x ^2 )) > 0
by A3, XREAL_1:141; verum