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