for x being Real st x ^2 < 1 holds
( x + 1 > 0 & 1 - x > 0 )