let MS be satisfying_equiv MusicStruct ; the Equidistance of MS is_transitive_in [: 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 for x, y, z being object st x in [: the carrier of MS, the carrier of MS:] & y in [: the carrier of MS, the carrier of MS:] & z in [: the carrier of MS, the carrier of MS:] & [x,y] in the Equidistance of MS & [y,z] in the Equidistance of MS holds
[x,z] in the Equidistance of MSlet x,
y,
z be
object ;
( x in [: the carrier of MS, the carrier of MS:] & y in [: the carrier of MS, the carrier of MS:] & z in [: the carrier of MS, the carrier of MS:] & [x,y] in the Equidistance of MS & [y,z] in the Equidistance of MS implies [x,z] in the Equidistance of MS )assume that A1:
x in [: the carrier of MS, the carrier of MS:]
and A2:
y in [: the carrier of MS, the carrier of MS:]
and A3:
z in [: the carrier of MS, the carrier of MS:]
and A4:
[x,y] in the
Equidistance of
MS
and A5:
[y,z] in the
Equidistance of
MS
;
[x,z] in the Equidistance of MSconsider x1,
x2 being
object such that A6:
x1 in the
carrier of
MS
and A7:
x2 in the
carrier of
MS
and A8:
x = [x1,x2]
by A1, ZFMISC_1:def 2;
consider y1,
y2 being
object such that A9:
y1 in the
carrier of
MS
and A10:
y2 in the
carrier of
MS
and A11:
y = [y1,y2]
by A2, ZFMISC_1:def 2;
consider z1,
z2 being
object such that A12:
z1 in the
carrier of
MS
and A13:
z2 in the
carrier of
MS
and A14:
z = [z1,z2]
by A3, ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2,
y1 =
y1,
y2 =
y2,
z1 =
z1,
z2 =
z2 as
Element of
MS by A6, A7, A9, A10, A12, A13;
(
x1,
x2 equiv y1,
y2 &
y1,
y2 equiv z1,
z2 )
by A4, A5, A8, A11, A14;
then
x1,
x2 equiv z1,
z2
by Th23;
hence
[x,z] in the
Equidistance of
MS
by A8, A14;
verum end;
hence
the Equidistance of MS is_transitive_in [: the carrier of MS, the carrier of MS:]
by RELAT_2:def 8; verum