:: deftheorem Def24 defines classical_fourth MUSIC_S1:def 77 :
for MS being satisfying_fourth_constructible MusicSpace holds
( MS is classical_fourth iff for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr ) );