let MS be satisfying_equiv MusicStruct ; :: thesis: 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 :: thesis: 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 MS

let x, y be object ; :: thesis: ( 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 ; :: thesis: [y,x] in the Equidistance of MS
consider 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; :: thesis: verum

end;

hence the Equidistance of MS is_symmetric_in [: the carrier of MS, the carrier of MS:] by RELAT_2:def 3; :: thesis: verum