let p, q, s, t be Real; :: thesis: ( p > 0 & p * s < 0 implies ( t > q iff (t - q) / (p - s) > 0 ) )
assume that
A1: p > 0 and
A2: p * s < 0 ; :: thesis: ( t > q iff (t - q) / (p - s) > 0 )
A5s: s < 0 / p by A1, A2;
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 t - q > q - q by XREAL_1:9;
hence (t - q) / (p - s) > 0 by A5s, A1; :: thesis: verum

end;

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