let x be Real; :: thesis: ( x ^2 < 1 implies (x + 1) / (1 - x) > 0 )
assume x ^2 < 1 ; :: thesis: (x + 1) / (1 - x) > 0
then ( x + 1 > 0 & 1 - x > 0 ) by Th11;
hence (x + 1) / (1 - x) > 0 ; :: thesis: verum