theorem Th27: :: MUSIC_S1:33

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