let MS be satisfying_equiv MusicStruct ; the Equidistance of MS is_symmetric_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 being object st x in [: the carrier of MS, the carrier of MS:] & y in [: the carrier of MS, the carrier of MS:] & [x,y] in the Equidistance of MS holds
[y,x] in the Equidistance of MSlet x,
y be
object ;
( x in [: the carrier of MS, the carrier of MS:] & y in [: the carrier of MS, the carrier of MS:] & [x,y] in the Equidistance of MS implies [y,x] 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:
[x,y] in the
Equidistance of
MS
;
[y,x] in the Equidistance of MSconsider x1,
x2 being
object such that A4:
x1 in the
carrier of
MS
and A5:
x2 in the
carrier of
MS
and A6:
x = [x1,x2]
by A1, ZFMISC_1:def 2;
consider y1,
y2 being
object such that A7:
y1 in the
carrier of
MS
and A8:
y2 in the
carrier of
MS
and A9:
y = [y1,y2]
by A2, ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2,
y1 =
y1,
y2 =
y2 as
Element of
MS by A4, A5, A7, A8;
x1,
x2 equiv y1,
y2
by A3, A6, A9;
then
y1,
y2 equiv x1,
x2
by Th22;
hence
[y,x] in the
Equidistance of
MS
by A6, A9;
verum end;
hence
the Equidistance of MS is_symmetric_in [: the carrier of MS, the carrier of MS:]
by RELAT_2:def 3; verum