:: deftheorem Def11bis defines Fifth MUSIC_S1:def 43 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct
for frequency, b₃ being Element of MS holds
( b₃ = Fifth (MS,frequency) iff [frequency,b₃] in fifth MS );