set T = TrivialTarskiSpace ;

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

p,q equiv r,s

a = b

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

a = b by STRUCT_0:def 10;

Z: TrivialTarskiSpace is satisfying_SAS by STRUCT_0:def 10;

TrivialTarskiSpace is satisfying_Pasch

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

proof

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

a = b by STRUCT_0:def 10;

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

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

end;a = b by STRUCT_0:def 10;

then 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 TrivialTarskiSpace st a,b equiv c,c holds
let a, b, p, q, r, s be POINT of TrivialTarskiSpace; :: 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

a4:
for a, q, b, c being POINT of TrivialTarskiSpace ex x being POINT of TrivialTarskiSpace st
let a, b, c be POINT of TrivialTarskiSpace; :: 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

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

proof

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

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

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

b = c by STRUCT_0:def 10;

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

then dist (a,x) = dist (b,c) by METRIC_1:1;

then T1: a,x equiv b,c by NGDef;

a is_Between q,x by TrivialBetween;

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

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

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

b = c by STRUCT_0:def 10;

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

then dist (a,x) = dist (b,c) by METRIC_1:1;

then T1: a,x equiv b,c by NGDef;

a is_Between q,x by TrivialBetween;

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

a = b by STRUCT_0:def 10;

Z: TrivialTarskiSpace is satisfying_SAS by STRUCT_0:def 10;

TrivialTarskiSpace is satisfying_Pasch

proof

hence
( TrivialTarskiSpace is satisfying_CongruenceSymmetry & TrivialTarskiSpace is satisfying_CongruenceEquivalenceRelation & TrivialTarskiSpace is satisfying_CongruenceIdentity & TrivialTarskiSpace is satisfying_SegmentConstruction & TrivialTarskiSpace is satisfying_SAS & TrivialTarskiSpace is satisfying_BetweennessIdentity & TrivialTarskiSpace is satisfying_Pasch )
by a1, a2, a3, a4, W, Z; :: thesis: verum
let a, b, p, q, z be POINT of TrivialTarskiSpace; :: according to GTARSKI1:def 11 :: thesis: ( between a,p,z & between b,q,z implies ex x being POINT of TrivialTarskiSpace st

( between p,x,b & between q,x,a ) )

assume ( between a,p,z & between b,q,z ) ; :: thesis: ex x being POINT of TrivialTarskiSpace st

( between p,x,b & between q,x,a )

take x = the POINT of TrivialTarskiSpace; :: thesis: ( between p,x,b & between q,x,a )

S1: x is_Between p,b by TrivialBetween;

x is_Between q,a by TrivialBetween;

hence ( between p,x,b & between q,x,a ) by NGDef, S1; :: thesis: verum

end;( between p,x,b & between q,x,a ) )

assume ( between a,p,z & between b,q,z ) ; :: thesis: ex x being POINT of TrivialTarskiSpace st

( between p,x,b & between q,x,a )

take x = the POINT of TrivialTarskiSpace; :: thesis: ( between p,x,b & between q,x,a )

S1: x is_Between p,b by TrivialBetween;

x is_Between q,a by TrivialBetween;

hence ( between p,x,b & between q,x,a ) by NGDef, S1; :: thesis: verum