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