set T = TarskiSpace ;
a1:
for a, b being POINT of TarskiSpace holds a,b equiv b,a
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;
( 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 TarskiSpace st a,b equiv c,c holds
a = b
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;
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
;
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
;
( 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;
verum end; suppose
q <= a
;
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
;
( 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;
verum end; end;
end;
for a, b being POINT of TarskiSpace st between a,b,a holds
a = b
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; verum