set T = TrivialTarskiSpace ;
a1:
for a, b being POINT of TrivialTarskiSpace holds a,b equiv b,a
a2:
for a, b, p, q, r, s being POINT of TrivialTarskiSpace st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s
proof
let a,
b,
p,
q,
r,
s be
POINT of
TrivialTarskiSpace;
( 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 )
;
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;
verum
end;
a3:
for a, b, c being POINT of TrivialTarskiSpace st a,b equiv c,c holds
a = b
a4:
for a, q, b, c being POINT of TrivialTarskiSpace ex x being POINT of TrivialTarskiSpace st
( between q,a,x & a,x equiv b,c )
proof
let a,
q,
b,
c be
POINT of
TrivialTarskiSpace;
ex x being POINT of TrivialTarskiSpace st
( between q,a,x & a,x equiv b,c )
take x =
a;
( 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;
verum
end;
W:
for a, b being POINT of TrivialTarskiSpace st between a,b,a holds
a = b
by STRUCT_0:def 10;
Z:
TrivialTarskiSpace is satisfying_SAS
by STRUCT_0:def 10;
TrivialTarskiSpace is satisfying_Pasch
proof
let a,
b,
p,
q,
z be
POINT of
TrivialTarskiSpace;
GTARSKI1:def 11 ( 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 )
;
ex x being POINT of TrivialTarskiSpace st
( between p,x,b & between q,x,a )
take x = the
POINT of
TrivialTarskiSpace;
( 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;
verum
end;
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; verum