theorem Th15: :: FUZZY_9:15

for p, q, s, t, x being Real st p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 & not x in ].(- (q / p)),(- (t / s)).[ holds
(((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x <= 0