for S being satisfying_equiv satisfying_tonic MusicStruct
for a, b, c being Element of S st a,a equiv b,c holds
b = c