let p be Rational; :: thesis: 0 < (denominator p) "
0 < denominator p by Th27;
hence 0 < (denominator p) " ; :: thesis: verum