theorem Th34: :: MUSIC_S1:41

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