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

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