theorem :: FUZZY_9:4

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) )