theorem :: XREAL_1:166

for a, b being Real st a <= 0 & - 1 < a & - 1 <= b holds
a * b < 1