let x be Real; :: thesis: ( 0 < x & x < 1 implies (2 * x) / (1 - (x ^2)) > 0 )

assume that

A1: 0 < x and

A2: x < 1 ; :: thesis: (2 * x) / (1 - (x ^2)) > 0

x ^2 < x by A1, A2, SQUARE_1:13;

then x ^2 < 1 by A2, XXREAL_0:2;

then A3: (x ^2) + (- (x ^2)) < 1 + (- (x ^2)) by XREAL_1:8;

0 * 2 < x * 2 by A1;

hence (2 * x) / (1 - (x ^2)) > 0 by A3; :: thesis: verum

assume that

A1: 0 < x and

A2: x < 1 ; :: thesis: (2 * x) / (1 - (x ^2)) > 0

x ^2 < x by A1, A2, SQUARE_1:13;

then x ^2 < 1 by A2, XXREAL_0:2;

then A3: (x ^2) + (- (x ^2)) < 1 + (- (x ^2)) by XREAL_1:8;

0 * 2 < x * 2 by A1;

hence (2 * x) / (1 - (x ^2)) > 0 by A3; :: thesis: verum