theorem :: RAT_1:37

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