let p be Rational; :: thesis: ( p < 0 iff numerator p < 0 )
A1: 0 < denominator p by Th27;

A4: now

assume p < 0 ; :: thesis: numerator p < 0
then (numerator p) / (denominator p) < 0 by Th37;
then ((numerator p) / (denominator p)) * (denominator p) < 0 * (denominator p) by A1, XREAL_1:70;
hence numerator p < 0 ; :: thesis: verum

end;

thus ( p < 0 iff numerator p < 0 ) by A4; :: thesis: verum