set T = TarskiSpace ;
a1: for a, b being POINT of TarskiSpace holds a,b equiv b,a
proof
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;
a2: for a, b, p, q, r, s being POINT of TarskiSpace 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 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;
a3: for a, b, c being POINT of TarskiSpace st a,b equiv c,c holds
a = b
proof
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;
xx: MetrStruct(# the carrier of TarskiSpace, the distance of TarskiSpace #) = MetrStruct(# the carrier of RealSpace, the distance of RealSpace #) by TADef;
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
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);
per cases ( q >= a or q <= a ) ;
suppose q >= a ; :: thesis: ex x being POINT of TarskiSpace st
( 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;
suppose q <= a ; :: thesis: ex x being POINT of TarskiSpace st
( 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;
end;
end;
for a, b being POINT of TarskiSpace st between a,b,a holds
a = b
proof
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;
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