theorem Th33: :: RING_3:33

for p being Rational
for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds
( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) )