:: deftheorem defines RATPLUS MUSIC_S1:def 1 :
RATPLUS = { r where r is positive Rational : verum } ;