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 S_{1}[ object , object ] means ex x1, x2, y1, y2 being Element of N st

( [x1,x2] = N & [y1,y2] = c_{2} & 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 S_{1}[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) )_{2}[ object , object ] means ex x1, x2, x3 being Element of N st

( [x1,x2] = N & x3 = c_{2} & 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 S_{2}[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)) )

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 )

( a,b equiv c,d iff dist (a,b) = dist (c,d) )

set X = the carrier of N;

set F = the distance of N;

set A = [: the carrier of N, the carrier of N:];

defpred S

( [x1,x2] = N & [y1,y2] = c

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 S

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

defpred S
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 )

end;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

thus
( dist (x1,x2) = dist (y1,y2) implies [[x1,x2],[y1,y2]] in E )
by t2; :: thesis: verum
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;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

( [x1,x2] = N & x3 = c

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 S

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

set M = MetrTarskiStr(# the carrier of N, the distance of N,B,E #);
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 )

end;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

thus
( dist (x1,x3) = (dist (x1,x2)) + (dist (x2,x3)) implies [[x1,x2],x3] in B )
by t0; :: thesis: verum
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;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

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

for a, b, c, d being POINT of MetrTarskiStr(# the carrier of N, the distance of N,B,E #) holds
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 )

then dist (aa,cc) = (dist (aa,bb)) + (dist (bb,cc)) ;

hence between a,b,c by T0; :: thesis: verum

end;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
b is_Between a,c
; :: thesis: between a,b,c
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;then dist (aa,cc) = (dist (aa,bb)) + (dist (bb,cc)) by T0;

hence b is_Between a,c ; :: thesis: verum

then dist (aa,cc) = (dist (aa,bb)) + (dist (bb,cc)) ;

hence between a,b,c by T0; :: thesis: verum

( a,b equiv c,d iff dist (a,b) = dist (c,d) )

proof

hence
T is naturally_generated
by T1; :: thesis: verum
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 ;

then dist (aa,bb) = dist (cc,dd) ;

hence a,b equiv c,d by T2; :: thesis: verum

end;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
dist (a,b) = dist (c,d)
; :: thesis: a,b equiv c,dassume 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;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

then dist (aa,bb) = dist (cc,dd) ;

hence a,b equiv c,d by T2; :: thesis: verum