let p be Rational; :: thesis: 0 < denominator p
0 <> denominator p by Def3;
hence 0 < denominator p ; :: thesis: verum