set T = TrivialTarskiSpace ;
a1: for a, b being POINT of TrivialTarskiSpace holds a,b equiv b,a
proof
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;
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; :: 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;
a3: for a, b, c being POINT of TrivialTarskiSpace st a,b equiv c,c holds
a = b
proof
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;
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; :: 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;
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; :: 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;
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