theorem Th1: :: MUSIC_S1:1

for r being object holds
( r in REAL+ \ {0} iff r is positive Real )