let p be Rational; :: thesis: 1 #Q p = 1
thus 1 #Q p = (denominator p) -Root 1 by Th37
.= 1 by Th20, RAT_1:11 ; :: thesis: verum