theorem Th5: :: RING_3:5

multrat || INT = multint