theorem Th3: :: MUSIC_S1:4

NATPLUS c= RATPLUS