let x be Real; :: 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:50;
x ^2 >= 0 by XREAL_1:63;
hence ((x ^2) + 1) / (1 - (x ^2)) >= 0 by A1; :: thesis: verum