let p be Rational; :: thesis: ( p < 0 iff numerator p < 0 )

now :: thesis: ( p < 0 implies numerator p < 0 )

assume p < 0 ; :: thesis: numerator p < 0
then (numerator p) / (denominator p) < 0 by Th12;
hence numerator p < 0 ; :: thesis: verum

end;

hence ( p < 0 iff numerator p < 0 ) ; :: thesis: verum