let x be Real; :: thesis: ( x ^2 < 1 implies ( x + 1 > 0 & 1 - x > 0 ) )
assume x ^2 < 1 ; :: thesis: ( x + 1 > 0 & 1 - x > 0 )
then ( - 1 < x & x < 1 ) by SQUARE_1:52;
hence ( x + 1 > 0 & 1 - x > 0 ) by XREAL_1:148, XREAL_1:149; :: thesis: verum