theorem :: MUSIC_S1:34

for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is Equivalence_Relation of [: the carrier of MS, the carrier of MS:]