let p, q, s, t be Real; ( p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 implies ( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) & - (q / p) < - (t / s) ) )
assume A2:
( p * s < 0 & p > 0 )
; ( not ((p * t) - (q * s)) / (p - s) > 0 or ( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) & - (q / p) < - (t / s) ) )
then A7:
p - s <> 0
;
assume A3:
((p * t) - (q * s)) / (p - s) > 0
; ( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) & - (q / p) < - (t / s) )
A8: ((t - q) / (p - s)) + (q / p) =
(((t - q) * p) + (q * (p - s))) / ((p - s) * p)
by XCMPLX_1:116, A7, A2
.=
(1 / p) * (((t * p) - (q * s)) / (p - s))
by XCMPLX_1:103
;
A5s:
(((t - q) / (p - s)) + (q / p)) - (q / p) > 0 - (q / p)
by XREAL_1:9, A8, A3, A2;
A9:
s < 0
by A2;
then A10: ((t - q) / (p - s)) + (t / s) =
(((t - q) * s) + (t * (p - s))) / ((p - s) * s)
by A2, XCMPLX_1:116
.=
(1 / s) * (((t * p) - (q * s)) / (p - s))
by XCMPLX_1:103
;
(((t - q) / (p - s)) + (t / s)) - (t / s) < 0 - (t / s)
by XREAL_1:9, A10, A3, A9;
hence
( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) & - (q / p) < - (t / s) )
by A5s, XXREAL_0:2; verum