theorem Th25: :: MUSIC_S1:30

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