theorem :: FUZZY_9:2

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