theorem Th13: :: FUZZY_9:8

for p, q, s, t being Real st p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 holds
( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) & - (q / p) < - (t / s) )