let MS be satisfying_equiv MusicStruct ; :: thesis: ( not MS is empty implies ( the Equidistance of MS is reflexive & field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] ) )
assume A1: not MS is empty ; :: thesis: ( the Equidistance of MS is reflexive & field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] )
the Equidistance of MS is_reflexive_in [: the carrier of MS, the carrier of MS:] by Th25;
hence ( the Equidistance of MS is reflexive & field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] ) by A1, PARTIT_2:21; :: thesis: verum