let MS be satisfying_equiv MusicStruct ; 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 ( 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;
( 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;
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;
verum end;
hence
the Equidistance of MS is Equivalence_Relation of [: the carrier of MS, the carrier of MS:]
; verum