let p be Rational; :: thesis: 1 >= (denominator p) "
A1: 1 * ((denominator p) ") <= (denominator p) * ((denominator p) ") by Th29, XREAL_1:64;
0 <> denominator p by Def3;
hence 1 >= (denominator p) " by A1, XCMPLX_0:def 7; :: thesis: verum