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