theorem Th41: :: MUSIC_S1:52

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