let MS be satisfying_equiv MusicStruct ; :: thesis: the Equidistance of MS is_reflexive_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 being object st x in [: the carrier of MS, the carrier of MS:] holds
[x,x] in the Equidistance of MS

let x be object ; :: thesis: ( x in [: the carrier of MS, the carrier of MS:] implies [x,x] in the Equidistance of MS )
assume x in [: the carrier of MS, the carrier of MS:] ; :: thesis: [x,x] in the Equidistance of MS
then consider y, z being object such that
A1: y in the carrier of MS and
A2: z in the carrier of MS and
A3: x = [y,z] by ZFMISC_1:def 2;
reconsider y = y, z = z as Element of MS by A1, A2;
y,z equiv y,z by Th21;
hence [x,x] in the Equidistance of MS by A3; :: thesis: verum

end;

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