theorem Th49: :: MUSIC_S1:60

for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave RAT_Music )