theorem Th47: :: MUSIC_S1:58

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