theorem Th36: :: MUSIC_S1:43
for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = (3 / 2) * fr & [fr,qr] in fifth RAT_Music )