set C = the carrier of N;
set X = the carrier of N;
set F = the distance of N;
set A = [: the carrier of N, the carrier of N:];
defpred S1[ object , object ] means ex x1, x2, y1, y2 being Element of N st
( [x1,x2] = N & [y1,y2] = c2 & dist (x1,x2) = dist (y1,y2) );
consider E being Relation of [: the carrier of N, the carrier of N:],[: the carrier of N, the carrier of N:] such that
t2: for xx, yy being Element of [: the carrier of N, the carrier of N:] holds
( [xx,yy] in E iff S1[xx,yy] ) from RELSET_1:sch 2();
 T2: for x1, x2, y1, y2 being Element of the carrier of N holds
( [[x1,x2],[y1,y2]] in E iff dist (x1,x2) = dist (y1,y2) )
proof
let x1, x2, y1, y2 be Element of the carrier of N; :: thesis: ( [[x1,x2],[y1,y2]] in E iff dist (x1,x2) = dist (y1,y2) )
reconsider xx = [x1,x2], yy = [y1,y2] as Element of [: the carrier of N, the carrier of N:] ;
thus ( [[x1,x2],[y1,y2]] in E implies dist (x1,x2) = dist (y1,y2) ) :: thesis: ( dist (x1,x2) = dist (y1,y2) implies [[x1,x2],[y1,y2]] in E )
proof
assume [[x1,x2],[y1,y2]] in E ; :: thesis: dist (x1,x2) = dist (y1,y2)
then consider w1, w2, v1, v2 being Element of N such that
k1: ( [w1,w2] = xx & [v1,v2] = yy & dist (w1,w2) = dist (v1,v2) ) by t2;
( x1 = w1 & x2 = w2 & v1 = y1 & v2 = y2 ) by k1, XTUPLE_0:1;
hence dist (x1,x2) = dist (y1,y2) by k1; :: thesis: verum
end;
thus ( dist (x1,x2) = dist (y1,y2) implies [[x1,x2],[y1,y2]] in E ) by t2; :: thesis: verum
end;
defpred S2[ object , object ] means ex x1, x2, x3 being Element of N st
( [x1,x2] = N & x3 = c2 & dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) );
consider B being Relation of [: the carrier of N, the carrier of N:], the carrier of N such that
t0: for xx being Element of [: the carrier of N, the carrier of N:]
for x3 being Element of the carrier of N holds
( [xx,x3] in B iff S2[xx,x3] ) from RELSET_1:sch 2();
 T0: for x1, x2, x3 being Element of the carrier of N holds
( [[x1,x2],x3] in B iff dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) )
proof
let x1, x2, x3 be Element of the carrier of N; :: thesis: ( [[x1,x2],x3] in B iff dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) )
thus ( [[x1,x2],x3] in B implies dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) ) :: thesis: ( dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) implies [[x1,x2],x3] in B )
proof
assume [[x1,x2],x3] in B ; :: thesis: dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3))
then consider y1, y2, y3 being Element of N such that
H1: ( [y1,y2] = [x1,x2] & y3 = x3 & dist (y1,y3) = (dist (y1,y2)) + (dist (y2,y3)) ) by t0;
( y1 = x1 & y2 = x2 ) by H1, XTUPLE_0:1;
hence dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) by H1; :: thesis: verum
end;
thus ( dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) implies [[x1,x2],x3] in B ) by t0; :: thesis: verum
end;
set M = MetrTarskiStr(# the carrier of N, the distance of N,B,E #);
Z1: MetrStruct(# the carrier of MetrTarskiStr(# the carrier of N, the distance of N,B,E #), the distance of MetrTarskiStr(# the carrier of N, the distance of N,B,E #) #) = MetrStruct(# the carrier of N, the distance of N #) ;
reconsider T = MetrTarskiStr(# the carrier of N, the distance of N,B,E #) as TarskiExtension of N by Z1, TADef;
take T ; :: thesis: T is naturally_generated
T1: for a, b, c being POINT of MetrTarskiStr(# the carrier of N, the distance of N,B,E #) holds
( between a,b,c iff b is_Between a,c )
proof
let a, b, c be POINT of MetrTarskiStr(# the carrier of N, the distance of N,B,E #); :: thesis: ( between a,b,c iff b is_Between a,c )
reconsider aa = a, bb = b, cc = c as Element of N ;
thus ( between a,b,c implies b is_Between a,c ) :: thesis: ( b is_Between a,c implies between a,b,c )
proof
assume between a,b,c ; :: thesis: b is_Between a,c
then dist (aa,cc) = (dist (aa,bb)) + (dist (bb,cc)) by T0;
hence b is_Between a,c ; :: thesis: verum
end;
assume b is_Between a,c ; :: thesis: between a,b,c
then dist (aa,cc) = (dist (aa,bb)) + (dist (bb,cc)) ;
hence between a,b,c by T0; :: thesis: verum
end;
for a, b, c, d being POINT of MetrTarskiStr(# the carrier of N, the distance of N,B,E #) holds
( a,b equiv c,d iff dist (a,b) = dist (c,d) )
proof
let a, b, c, d be POINT of MetrTarskiStr(# the carrier of N, the distance of N,B,E #); :: thesis: ( a,b equiv c,d iff dist (a,b) = dist (c,d) )
reconsider aa = a, bb = b, cc = c, dd = d as Element of the carrier of N ;
hereby :: thesis: ( dist (a,b) = dist (c,d) implies a,b equiv c,d )
assume s1: a,b equiv c,d ; :: thesis: dist (a,b) = dist (c,d)
S2: ( [[aa,bb],[cc,dd]] in E iff dist (aa,bb) = dist (cc,dd) ) by T2;
thus dist (a,b) = dist (c,d) by s1, S2; :: thesis: verum
end;
assume dist (a,b) = dist (c,d) ; :: thesis: a,b equiv c,d
then dist (aa,bb) = dist (cc,dd) ;
hence a,b equiv c,d by T2; :: thesis: verum
end;
hence T is naturally_generated by T1; :: thesis: verum