for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_harmonique_stable MusicStruct
for a, b being Element of MS holds a,a equiv b,b