:: deftheorem defines REALPLUS MUSIC_S1:def 2 :
REALPLUS = REAL+ \ {0};