theorem Th23: :: RING_3:23

for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) - (j / n)) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )