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