theorem Th35: :: RAT_1:38

for p being Rational holds
( p <= 0 iff numerator p <= 0 )