theorem Th4: :: MUSIC_S1:5

NATPLUS c= REALPLUS