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

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

assume A1: numerator p <= 0 ; :: thesis: p <= 0

per cases ( numerator p = 0 or numerator p < 0 ) by A1;

suppose numerator p = 0 ; :: thesis: p <= 0

hence p <= 0 by Th11; :: thesis: verum

end;

suppose numerator p < 0 ; :: thesis: p <= 0

hence p <= 0 ; :: thesis: verum

end;

end;

end;

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