let p, q be Rational; :: thesis: ( denominator p = denominator q & numerator p = numerator q implies p = q )
assume that
A1: denominator p = denominator q and
A2: numerator p = numerator q ; :: thesis: p = q
thus p = (numerator q) / (denominator q) by A1, A2, Th12
.= q by Th12 ; :: thesis: verum