for MS being satisfying_fourth_constructible MusicSpace st MS = REAL_Music holds
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr )