:: deftheorem Def11 defines satisfying_fifth_constructible MUSIC_S1:def 42 :
for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds
( S is satisfying_fifth_constructible iff for frequency being Element of S ex q being Element of S st [frequency,q] in fifth S );