theorem :: RAT_1:12

for p being Rational holds 0 < (denominator p) " ;