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