for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed MusicStruct
for frequency being Element of MS holds 1 -harmonique (MS,frequency) = frequency