theorem Th5: :: MUSIC_S1:6

RATPLUS c= REALPLUS