for MS being MusicSpace st MS = REAL_Music holds
for frequency being Element of MS ex fr, qr being positive Real st
( fr = frequency & qr = (4 / 3) * fr & [fr,qr] in fourth MS )