for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p - q) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )