for S being satisfying_equiv satisfying_interval MusicStruct
for a, b, c being Element of S holds
( a,b equiv a,c iff b = c )