theorem :: FUZZY_9:3

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