:: deftheorem Def22 defines satisfying_fourth_constructible MUSIC_S1:def 75 :
for S being MusicSpace holds
( S is satisfying_fourth_constructible iff for frequency being Element of S ex q being Element of S st [frequency,q] in fourth S );