let MS be satisfying_equiv MusicStruct ; 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 for x being object st x in [: the carrier of MS, the carrier of MS:] holds
[x,x] in the Equidistance of MSlet x be
object ;
( 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:]
;
[x,x] in the Equidistance of MSthen 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;
verum end;
hence
the Equidistance of MS is_reflexive_in [: the carrier of MS, the carrier of MS:]
by RELAT_2:def 1; verum