theorem Th43: :: MUSIC_S1:54

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