for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct
for frequency being Element of MS holds fifth (MS,frequency) = fifth MS