let p, q be Rational; :: thesis: ( denominator p = denominator q & numerator p = numerator q implies p = q )
assume ( denominator p = denominator q & numerator p = numerator q ) ; :: thesis: p = q
hence p = (numerator q) / (denominator q) by Th37
.= q by Th37 ;
:: thesis: verum