:: deftheorem Def23 defines Fourth MUSIC_S1:def 76 :
for MS being satisfying_fourth_constructible MusicSpace
for frequency, b₃ being Element of MS holds
( b₃ = Fourth (MS,frequency) iff [frequency,b₃] in fourth MS );