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