for p, q being Rational
for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds
( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) )