let x be real number ; :: thesis: ( x ^2 < 1 implies ((x ^2 ) + 1) / (1 - (x ^2 )) >= 0 )
assume x ^2 < 1 ; :: thesis: ((x ^2 ) + 1) / (1 - (x ^2 )) >= 0
then A1: 0 < 1 - (x ^2 ) by XREAL_1:52;
x ^2 >= 0 by XREAL_1:65;
then (x ^2 ) + 1 >= 0 + 1 by XREAL_1:8;
hence ((x ^2 ) + 1) / (1 - (x ^2 )) >= 0 by A1; :: thesis: verum