let p be Rational; :: thesis: 1 <= denominator p
0 < denominator p by Th7;
then 0 + 1 <= denominator p by NAT_1:13;
hence 1 <= denominator p ; :: thesis: verum