theorem Th2: :: MUSIC_S1:2

for r being object holds
( r is Element of RATPLUS iff r is positive Rational )