for MS being satisfying_equiv MusicStruct st not MS is empty holds
( the Equidistance of MS is reflexive & field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] )