let MS be satisfying_equiv MusicStruct ; :: thesis: the Equidistance of MS is Equivalence_Relation of [: the carrier of MS, the carrier of MS:]
set R = the Equidistance of MS;
set C = [: the carrier of MS, the carrier of MS:];

now :: thesis: ( the Equidistance of MS is total & the Equidistance of MS is symmetric & the Equidistance of MS is transitive )

dom the Equidistance of MS = [: the carrier of MS, the carrier of MS:] by Th25, TAXONOM1:3;
hence the Equidistance of MS is total by PARTFUN1:def 2; :: thesis: ( the Equidistance of MS is symmetric & the Equidistance of MS is transitive )
( field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] & the Equidistance of MS is_symmetric_in [: the carrier of MS, the carrier of MS:] ) by Th25, Th26, PARTIT_2:9;
hence the Equidistance of MS is symmetric by RELAT_2:def 11; :: thesis: the Equidistance of MS is transitive
( field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] & the Equidistance of MS is_transitive_in [: the carrier of MS, the carrier of MS:] ) by Th25, Th27, PARTIT_2:9;
hence the Equidistance of MS is transitive by RELAT_2:def 16; :: thesis: verum

end;

hence the Equidistance of MS is Equivalence_Relation of [: the carrier of MS, the carrier of MS:] ; :: thesis: verum