set T = TarskiSpace ;

a1: for a, b being POINT of TarskiSpace holds a,b equiv b,a

p,q equiv r,s

a = b

a4: for a, q, b, c being POINT of TarskiSpace ex x being POINT of TarskiSpace st

( between q,a,x & a,x equiv b,c )

a = b

a1: for a, b being POINT of TarskiSpace holds a,b equiv b,a

proof

a2:
for a, b, p, q, r, s being POINT of TarskiSpace st a,b equiv p,q & a,b equiv r,s holds
let a, b be POINT of TarskiSpace; :: thesis: a,b equiv b,a

dist (a,b) = dist (b,a) ;

hence a,b equiv b,a by NGDef; :: thesis: verum

end;dist (a,b) = dist (b,a) ;

hence a,b equiv b,a by NGDef; :: thesis: verum

p,q equiv r,s

proof

a3:
for a, b, c being POINT of TarskiSpace st a,b equiv c,c holds
let a, b, p, q, r, s be POINT of TarskiSpace; :: thesis: ( a,b equiv p,q & a,b equiv r,s implies p,q equiv r,s )

assume ( a,b equiv p,q & a,b equiv r,s ) ; :: thesis: p,q equiv r,s

then ( dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) ) by NGDef;

hence p,q equiv r,s by NGDef; :: thesis: verum

end;assume ( a,b equiv p,q & a,b equiv r,s ) ; :: thesis: p,q equiv r,s

then ( dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) ) by NGDef;

hence p,q equiv r,s by NGDef; :: thesis: verum

a = b

proof

xx:
MetrStruct(# the carrier of TarskiSpace, the distance of TarskiSpace #) = MetrStruct(# the carrier of RealSpace, the distance of RealSpace #)
by TADef;
let a, b, c be POINT of TarskiSpace; :: thesis: ( a,b equiv c,c implies a = b )

assume a,b equiv c,c ; :: thesis: a = b

then dist (a,b) = dist (c,c) by NGDef;

hence a = b by METRIC_1:2, METRIC_1:1; :: thesis: verum

end;assume a,b equiv c,c ; :: thesis: a = b

then dist (a,b) = dist (c,c) by NGDef;

hence a = b by METRIC_1:2, METRIC_1:1; :: thesis: verum

a4: for a, q, b, c being POINT of TarskiSpace ex x being POINT of TarskiSpace st

( between q,a,x & a,x equiv b,c )

proof

for a, b being POINT of TarskiSpace st between a,b,a holds
let a, q, b, c be POINT of TarskiSpace; :: thesis: ex x being POINT of TarskiSpace st

( between q,a,x & a,x equiv b,c )

set bc = dist (b,c);

set qa = dist (q,a);

end;( between q,a,x & a,x equiv b,c )

set bc = dist (b,c);

set qa = dist (q,a);

per cases
( q >= a or q <= a )
;

end;

suppose
q >= a
; :: thesis: ex x being POINT of TarskiSpace st

( between q,a,x & a,x equiv b,c )

( between q,a,x & a,x equiv b,c )

then z0:
q - a >= a - a
by XREAL_1:9;

Z2: q - a = |.(q - a).| by COMPLEX1:43, z0

.= dist (q,a) by xx, METRIC_1:def 12 ;

set x = a - (dist (b,c));

X1: dist (b,c) >= 0 by METRIC_1:5;

reconsider x = a - (dist (b,c)) as POINT of TarskiSpace by xx, XREAL_0:def 1;

take x ; :: thesis: ( between q,a,x & a,x equiv b,c )

X2: dist (a,x) = |.(a - x).| by METRIC_1:def 12, xx

.= dist (b,c) by METRIC_1:5, COMPLEX1:43 ;

dist (q,a) >= 0 by METRIC_1:5;

then X4: 0 <= (dist (q,a)) * (dist (b,c)) by X1;

X3: |.(q - a).| = dist (q,a) by xx, METRIC_1:def 12;

dist (q,x) = |.(q - x).| by xx, METRIC_1:def 12

.= |.((q - a) + (dist (b,c))).|

.= |.(q - a).| + |.(dist (b,c)).| by ABSVALUE:11, X4, Z2

.= (dist (q,a)) + (dist (b,c)) by X3, COMPLEX1:43, METRIC_1:5 ;

then a is_Between q,x by X2;

hence ( between q,a,x & a,x equiv b,c ) by NGDef, X2; :: thesis: verum

end;Z2: q - a = |.(q - a).| by COMPLEX1:43, z0

.= dist (q,a) by xx, METRIC_1:def 12 ;

set x = a - (dist (b,c));

X1: dist (b,c) >= 0 by METRIC_1:5;

reconsider x = a - (dist (b,c)) as POINT of TarskiSpace by xx, XREAL_0:def 1;

take x ; :: thesis: ( between q,a,x & a,x equiv b,c )

X2: dist (a,x) = |.(a - x).| by METRIC_1:def 12, xx

.= dist (b,c) by METRIC_1:5, COMPLEX1:43 ;

dist (q,a) >= 0 by METRIC_1:5;

then X4: 0 <= (dist (q,a)) * (dist (b,c)) by X1;

X3: |.(q - a).| = dist (q,a) by xx, METRIC_1:def 12;

dist (q,x) = |.(q - x).| by xx, METRIC_1:def 12

.= |.((q - a) + (dist (b,c))).|

.= |.(q - a).| + |.(dist (b,c)).| by ABSVALUE:11, X4, Z2

.= (dist (q,a)) + (dist (b,c)) by X3, COMPLEX1:43, METRIC_1:5 ;

then a is_Between q,x by X2;

hence ( between q,a,x & a,x equiv b,c ) by NGDef, X2; :: thesis: verum

suppose
q <= a
; :: thesis: ex x being POINT of TarskiSpace st

( between q,a,x & a,x equiv b,c )

( between q,a,x & a,x equiv b,c )

then Z2: a - q =
|.(a - q).|
by COMPLEX1:43, XREAL_1:48

.= |.(q - a).| by COMPLEX1:60

.= dist (q,a) by xx, METRIC_1:def 12 ;

set x = a + (dist (b,c));

X1: dist (b,c) >= 0 by METRIC_1:5;

reconsider x = a + (dist (b,c)) as POINT of TarskiSpace by xx, XREAL_0:def 1;

take x ; :: thesis: ( between q,a,x & a,x equiv b,c )

X2: dist (a,x) = |.(a - x).| by xx, METRIC_1:def 12

.= |.(- (dist (b,c))).|

.= |.(dist (b,c)).| by COMPLEX1:52

.= dist (b,c) by METRIC_1:5, COMPLEX1:43 ;

dist (q,a) >= 0 by METRIC_1:5;

then X4: 0 <= (dist (q,a)) * (dist (b,c)) by X1;

XX: |.((a - q) + (dist (b,c))).| = |.(a - q).| + |.(dist (b,c)).| by ABSVALUE:11, X4, Z2;

X3: |.(a - q).| = |.(q - a).| by COMPLEX1:60

.= dist (q,a) by xx, METRIC_1:def 12 ;

dist (q,x) = |.(q - x).| by METRIC_1:def 12, xx

.= |.(x - q).| by COMPLEX1:60

.= (dist (q,a)) + (dist (b,c)) by X3, XX, COMPLEX1:43, METRIC_1:5 ;

then a is_Between q,x by X2;

hence ( between q,a,x & a,x equiv b,c ) by NGDef, X2; :: thesis: verum

end;.= |.(q - a).| by COMPLEX1:60

.= dist (q,a) by xx, METRIC_1:def 12 ;

set x = a + (dist (b,c));

X1: dist (b,c) >= 0 by METRIC_1:5;

reconsider x = a + (dist (b,c)) as POINT of TarskiSpace by xx, XREAL_0:def 1;

take x ; :: thesis: ( between q,a,x & a,x equiv b,c )

X2: dist (a,x) = |.(a - x).| by xx, METRIC_1:def 12

.= |.(- (dist (b,c))).|

.= |.(dist (b,c)).| by COMPLEX1:52

.= dist (b,c) by METRIC_1:5, COMPLEX1:43 ;

dist (q,a) >= 0 by METRIC_1:5;

then X4: 0 <= (dist (q,a)) * (dist (b,c)) by X1;

XX: |.((a - q) + (dist (b,c))).| = |.(a - q).| + |.(dist (b,c)).| by ABSVALUE:11, X4, Z2;

X3: |.(a - q).| = |.(q - a).| by COMPLEX1:60

.= dist (q,a) by xx, METRIC_1:def 12 ;

dist (q,x) = |.(q - x).| by METRIC_1:def 12, xx

.= |.(x - q).| by COMPLEX1:60

.= (dist (q,a)) + (dist (b,c)) by X3, XX, COMPLEX1:43, METRIC_1:5 ;

then a is_Between q,x by X2;

hence ( between q,a,x & a,x equiv b,c ) by NGDef, X2; :: thesis: verum

a = b

proof

hence
( TarskiSpace is satisfying_CongruenceSymmetry & TarskiSpace is satisfying_CongruenceEquivalenceRelation & TarskiSpace is satisfying_CongruenceIdentity & TarskiSpace is satisfying_SegmentConstruction & TarskiSpace is satisfying_BetweennessIdentity )
by a1, a2, a3, a4; :: thesis: verum
let a, b be POINT of TarskiSpace; :: thesis: ( between a,b,a implies a = b )

assume between a,b,a ; :: thesis: a = b

then b is_Between a,a by NGDef;

then 0 = (dist (a,b)) + (dist (b,a)) by METRIC_1:1;

hence a = b by METRIC_1:2; :: thesis: verum

end;assume between a,b,a ; :: thesis: a = b

then b is_Between a,a by NGDef;

then 0 = (dist (a,b)) + (dist (b,a)) by METRIC_1:1;

hence a = b by METRIC_1:2; :: thesis: verum