let p, q, s, t be Real; :: thesis: ( p > 0 & p * s < 0 implies ( t < q iff (t - q) / (p - s) < 0 ) )
assume that
A0: p > 0 and
A1: p * s < 0 ; :: thesis: ( t < q iff (t - q) / (p - s) < 0 )
thus ( t < q implies (t - q) / (p - s) < 0 ) :: thesis: ( (t - q) / (p - s) < 0 implies t < q )

proof

assume t < q ; :: thesis: (t - q) / (p - s) < 0
then (q - t) / (p - s) > 0 by Th101, A0, A1;
then - ((q - t) / (p - s)) < 0 ;
then (- (q - t)) / (p - s) < 0 by XCMPLX_1:187;
hence (t - q) / (p - s) < 0 ; :: thesis: verum

end;

assume A2: (t - q) / (p - s) < 0 ; :: thesis: t < q
s < 0 / p by A0, A1;
then t - q < 0 by A0, A2;
then (t - q) + q < 0 + q by XREAL_1:6;
hence t < q ; :: thesis: verum