theorem Th4: :: RING_3:4

addrat || INT = addint