theorem Th7: :: RAT_1:10

for p being Rational holds 0 < denominator p