:: by William Richter , Adam Grabowski and Jesse Alama

::

:: Received June 16, 2014

:: Copyright (c) 2014-2016 Association of Mizar Users

definition

attr c_{1} is strict ;

struct TarskiPlane -> 1-sorted ;

aggr TarskiPlane(# carrier, Betweenness, Equidistance #) -> TarskiPlane ;

sel Betweenness c_{1} -> Relation of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier of c_{1};

sel Equidistance c_{1} -> Relation of [: the carrier of c_{1}, the carrier of c_{1}:],[: the carrier of c_{1}, the carrier of c_{1}:];

end;
struct TarskiPlane -> 1-sorted ;

aggr TarskiPlane(# carrier, Betweenness, Equidistance #) -> TarskiPlane ;

sel Betweenness c

sel Equidistance c

:: deftheorem defines between GTARSKI1:def 1 :

for S being TarskiPlane

for a, b, c being POINT of S holds

( between a,b,c iff [[a,b],c] in the Betweenness of S );

for S being TarskiPlane

for a, b, c being POINT of S holds

( between a,b,c iff [[a,b],c] in the Betweenness of S );

:: deftheorem defines equiv GTARSKI1:def 2 :

for S being TarskiPlane

for a, b, c, d being POINT of S holds

( a,b equiv c,d iff [[a,b],[c,d]] in the Equidistance of S );

for S being TarskiPlane

for a, b, c, d being POINT of S holds

( a,b equiv c,d iff [[a,b],[c,d]] in the Equidistance of S );

:: deftheorem defines cong GTARSKI1:def 3 :

for S being TarskiPlane

for a, b, c, x, y, z being POINT of S holds

( a,b,c cong x,y,z iff ( a,b equiv x,y & a,c equiv x,z & b,c equiv y,z ) );

for S being TarskiPlane

for a, b, c, x, y, z being POINT of S holds

( a,b,c cong x,y,z iff ( a,b equiv x,y & a,c equiv x,z & b,c equiv y,z ) );

definition

let S be TarskiPlane ;

let a, b, c, d be POINT of S;

end;
let a, b, c, d be POINT of S;

pred a,b,c,d are_ordered means :: GTARSKI1:def 4

( between a,b,c & between a,b,d & between a,c,d & between b,c,d );

( between a,b,c & between a,b,d & between a,c,d & between b,c,d );

:: deftheorem defines are_ordered GTARSKI1:def 4 :

for S being TarskiPlane

for a, b, c, d being POINT of S holds

( a,b,c,d are_ordered iff ( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) );

for S being TarskiPlane

for a, b, c, d being POINT of S holds

( a,b,c,d are_ordered iff ( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) );

definition

let S be TarskiPlane ;

end;
attr S is satisfying_CongruenceSymmetry means :: GTARSKI1:def 5

for a, b being POINT of S holds a,b equiv b,a;

for a, b being POINT of S holds a,b equiv b,a;

attr S is satisfying_CongruenceEquivalenceRelation means :: GTARSKI1:def 6

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s;

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s;

attr S is satisfying_CongruenceIdentity means :: GTARSKI1:def 7

for a, b, c being POINT of S st a,b equiv c,c holds

a = b;

for a, b, c being POINT of S st a,b equiv c,c holds

a = b;

attr S is satisfying_SegmentConstruction means :: GTARSKI1:def 8

for a, q, b, c being POINT of S ex x being POINT of S st

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

for a, q, b, c being POINT of S ex x being POINT of S st

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

attr S is satisfying_SAS means :: GTARSKI1:def 9

for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds

c,x equiv c1,x1;

for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds

c,x equiv c1,x1;

attr S is satisfying_BetweennessIdentity means :: GTARSKI1:def 10

for a, b being POINT of S st between a,b,a holds

a = b;

for a, b being POINT of S st between a,b,a holds

a = b;

attr S is satisfying_Pasch means :: GTARSKI1:def 11

for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

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

for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

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

:: deftheorem defines satisfying_CongruenceSymmetry GTARSKI1:def 5 :

for S being TarskiPlane holds

( S is satisfying_CongruenceSymmetry iff for a, b being POINT of S holds a,b equiv b,a );

for S being TarskiPlane holds

( S is satisfying_CongruenceSymmetry iff for a, b being POINT of S holds a,b equiv b,a );

:: deftheorem defines satisfying_CongruenceEquivalenceRelation GTARSKI1:def 6 :

for S being TarskiPlane holds

( S is satisfying_CongruenceEquivalenceRelation iff for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s );

for S being TarskiPlane holds

( S is satisfying_CongruenceEquivalenceRelation iff for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s );

:: deftheorem defines satisfying_CongruenceIdentity GTARSKI1:def 7 :

for S being TarskiPlane holds

( S is satisfying_CongruenceIdentity iff for a, b, c being POINT of S st a,b equiv c,c holds

a = b );

for S being TarskiPlane holds

( S is satisfying_CongruenceIdentity iff for a, b, c being POINT of S st a,b equiv c,c holds

a = b );

:: deftheorem defines satisfying_SegmentConstruction GTARSKI1:def 8 :

for S being TarskiPlane holds

( S is satisfying_SegmentConstruction iff for a, q, b, c being POINT of S ex x being POINT of S st

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

for S being TarskiPlane holds

( S is satisfying_SegmentConstruction iff for a, q, b, c being POINT of S ex x being POINT of S st

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

:: deftheorem defines satisfying_SAS GTARSKI1:def 9 :

for S being TarskiPlane holds

( S is satisfying_SAS iff for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds

c,x equiv c1,x1 );

for S being TarskiPlane holds

( S is satisfying_SAS iff for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds

c,x equiv c1,x1 );

:: deftheorem defines satisfying_BetweennessIdentity GTARSKI1:def 10 :

for S being TarskiPlane holds

( S is satisfying_BetweennessIdentity iff for a, b being POINT of S st between a,b,a holds

a = b );

for S being TarskiPlane holds

( S is satisfying_BetweennessIdentity iff for a, b being POINT of S st between a,b,a holds

a = b );

:: deftheorem defines satisfying_Pasch GTARSKI1:def 11 :

for S being TarskiPlane holds

( S is satisfying_Pasch iff for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

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

for S being TarskiPlane holds

( S is satisfying_Pasch iff for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

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

definition

let S be TarskiPlane ;

end;
attr S is satisfying_Tarski-model means :: GTARSKI1:def 12

( S is satisfying_CongruenceSymmetry & S is satisfying_CongruenceEquivalenceRelation & S is satisfying_CongruenceIdentity & S is satisfying_SegmentConstruction & S is satisfying_SAS & S is satisfying_BetweennessIdentity & S is satisfying_Pasch );

( S is satisfying_CongruenceSymmetry & S is satisfying_CongruenceEquivalenceRelation & S is satisfying_CongruenceIdentity & S is satisfying_SegmentConstruction & S is satisfying_SAS & S is satisfying_BetweennessIdentity & S is satisfying_Pasch );

:: deftheorem defines satisfying_Tarski-model GTARSKI1:def 12 :

for S being TarskiPlane holds

( S is satisfying_Tarski-model iff ( S is satisfying_CongruenceSymmetry & S is satisfying_CongruenceEquivalenceRelation & S is satisfying_CongruenceIdentity & S is satisfying_SegmentConstruction & S is satisfying_SAS & S is satisfying_BetweennessIdentity & S is satisfying_Pasch ) );

for S being TarskiPlane holds

( S is satisfying_Tarski-model iff ( S is satisfying_CongruenceSymmetry & S is satisfying_CongruenceEquivalenceRelation & S is satisfying_CongruenceIdentity & S is satisfying_SegmentConstruction & S is satisfying_SAS & S is satisfying_BetweennessIdentity & S is satisfying_Pasch ) );

definition

attr c_{1} is strict ;

struct MetrTarskiStr -> MetrStruct , TarskiPlane ;

aggr MetrTarskiStr(# carrier, distance, Betweenness, Equidistance #) -> MetrTarskiStr ;

end;
struct MetrTarskiStr -> MetrStruct , TarskiPlane ;

aggr MetrTarskiStr(# carrier, distance, Betweenness, Equidistance #) -> MetrTarskiStr ;

definition

let M be MetrStruct ;

ex b_{1} being MetrTarskiStr st MetrStruct(# the carrier of b_{1}, the distance of b_{1} #) = MetrStruct(# the carrier of M, the distance of M #)

end;
mode TarskiExtension of M -> MetrTarskiStr means :TADef: :: GTARSKI1:def 13

MetrStruct(# the carrier of it, the distance of it #) = MetrStruct(# the carrier of M, the distance of M #);

existence MetrStruct(# the carrier of it, the distance of it #) = MetrStruct(# the carrier of M, the distance of M #);

ex b

proof end;

:: deftheorem TADef defines TarskiExtension GTARSKI1:def 13 :

for M being MetrStruct

for b_{2} being MetrTarskiStr holds

( b_{2} is TarskiExtension of M iff MetrStruct(# the carrier of b_{2}, the distance of b_{2} #) = MetrStruct(# the carrier of M, the distance of M #) );

for M being MetrStruct

for b

( b

registration

let M be non empty MetrStruct ;

coherence

for b_{1} being TarskiExtension of M holds not b_{1} is empty

end;
coherence

for b

proof end;

registration

let M be non empty Reflexive MetrStruct ;

coherence

for b_{1} being TarskiExtension of M holds b_{1} is Reflexive

end;
coherence

for b

proof end;

registration

let M be non empty discerning MetrStruct ;

coherence

for b_{1} being TarskiExtension of M holds b_{1} is discerning

end;
coherence

for b

proof end;

registration

let M be non empty symmetric MetrStruct ;

coherence

for b_{1} being TarskiExtension of M holds b_{1} is symmetric

end;
coherence

for b

proof end;

registration

let M be non empty triangle MetrStruct ;

coherence

for b_{1} being TarskiExtension of M holds b_{1} is triangle

end;
coherence

for b

proof end;

:: deftheorem defines is_Between GTARSKI1:def 14 :

for S being MetrStruct

for p, q, r being Element of S holds

( q is_Between p,r iff dist (p,r) = (dist (p,q)) + (dist (q,r)) );

for S being MetrStruct

for p, q, r being Element of S holds

( q is_Between p,r iff dist (p,r) = (dist (p,q)) + (dist (q,r)) );

definition

let M be MetrTarskiStr ;

end;
attr M is naturally_generated means :NGDef: :: GTARSKI1:def 15

( ( for a, b, c being POINT of M holds

( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds

( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) );

( ( for a, b, c being POINT of M holds

( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds

( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) );

:: deftheorem NGDef defines naturally_generated GTARSKI1:def 15 :

for M being MetrTarskiStr holds

( M is naturally_generated iff ( ( for a, b, c being POINT of M holds

( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds

( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) ) );

for M being MetrTarskiStr holds

( M is naturally_generated iff ( ( for a, b, c being POINT of M holds

( between a,b,c iff b is_Between a,c ) ) & ( for a, b, c, d being POINT of M holds

( a,b equiv c,d iff dist (a,b) = dist (c,d) ) ) ) );

theorem :: GTARSKI1:1

for M, N being MetrStruct

for x, y being Element of M

for a, b being Element of N st MetrStruct(# the carrier of M, the distance of M #) = MetrStruct(# the carrier of N, the distance of N #) & x = a & y = b holds

dist (x,y) = dist (a,b) ;

for x, y being Element of M

for a, b being Element of N st MetrStruct(# the carrier of M, the distance of M #) = MetrStruct(# the carrier of N, the distance of N #) & x = a & y = b holds

dist (x,y) = dist (a,b) ;

registration

let N be non empty MetrStruct ;

existence

ex b_{1} being TarskiExtension of N st b_{1} is naturally_generated

end;
existence

ex b

proof end;

registration
end;

definition

the naturally_generated TarskiExtension of the non empty trivial MetrSpace is MetrTarskiStr ;

end;

func TrivialTarskiSpace -> MetrTarskiStr equals :: GTARSKI1:def 16

the naturally_generated TarskiExtension of the non empty trivial MetrSpace;

coherence the naturally_generated TarskiExtension of the non empty trivial MetrSpace;

the naturally_generated TarskiExtension of the non empty trivial MetrSpace is MetrTarskiStr ;

:: deftheorem defines TrivialTarskiSpace GTARSKI1:def 16 :

TrivialTarskiSpace = the naturally_generated TarskiExtension of the non empty trivial MetrSpace;

TrivialTarskiSpace = the naturally_generated TarskiExtension of the non empty trivial MetrSpace;

registration
end;

registration

( 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 )
end;

cluster TrivialTarskiSpace -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch ;

coherence ( 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 )

proof end;

registration

existence

ex b_{1} being TarskiPlane st

( b_{1} is satisfying_Tarski-model & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

for b_{1} being TarskiPlane st b_{1} is satisfying_CongruenceSymmetry & b_{1} is satisfying_CongruenceEquivalenceRelation & b_{1} is satisfying_CongruenceIdentity & b_{1} is satisfying_SegmentConstruction & b_{1} is satisfying_SAS & b_{1} is satisfying_BetweennessIdentity & b_{1} is satisfying_Pasch holds

b_{1} is satisfying_Tarski-model
;

for b_{1} being TarskiPlane st b_{1} is satisfying_Tarski-model holds

( b_{1} is satisfying_CongruenceSymmetry & b_{1} is satisfying_CongruenceEquivalenceRelation & b_{1} is satisfying_CongruenceIdentity & b_{1} is satisfying_SegmentConstruction & b_{1} is satisfying_SAS & b_{1} is satisfying_BetweennessIdentity & b_{1} is satisfying_Pasch )
;

end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch -> satisfying_Tarski-model for TarskiPlane ;

coherence for b

b

cluster satisfying_Tarski-model -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch for TarskiPlane ;

coherence for b

( b

theorem A2: :: GTARSKI1:4

for S being satisfying_Tarski-model TarskiPlane

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s

proof end;

theorem A3: :: GTARSKI1:5

for S being satisfying_Tarski-model TarskiPlane

for a, b, c being POINT of S st a,b equiv c,c holds

a = b

for a, b, c being POINT of S st a,b equiv c,c holds

a = b

proof end;

theorem A4: :: GTARSKI1:6

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, q being POINT of S ex x being POINT of S st

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

for a, b, c, q being POINT of S ex x being POINT of S st

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

proof end;

theorem A5: :: GTARSKI1:7

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, x, a9, b9, c9, x9 being POINT of S st a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 holds

c,x equiv c9,x9

for a, b, c, x, a9, b9, c9, x9 being POINT of S st a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 holds

c,x equiv c9,x9

proof end;

theorem A6: :: GTARSKI1:8

for S being satisfying_Tarski-model TarskiPlane

for a, b being POINT of S st between a,b,a holds

a = b

for a, b being POINT of S st between a,b,a holds

a = b

proof end;

theorem A7: :: GTARSKI1:9

for S being satisfying_Tarski-model TarskiPlane

for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

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

for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

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

proof end;

theorem EquivSymmetric: :: GTARSKI1:11

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

proof end;

theorem EquivTransitive: :: GTARSKI1:12

for S being satisfying_Tarski-model TarskiPlane

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & p,q equiv r,s holds

a,b equiv r,s

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & p,q equiv r,s holds

a,b equiv r,s

proof end;

theorem Baaa: :: GTARSKI1:13

for S being satisfying_Tarski-model TarskiPlane

for a, b being POINT of S holds

( between a,a,a & a,a equiv b,b )

for a, b being POINT of S holds

( between a,a,a & a,a equiv b,b )

proof end;

theorem C1: :: GTARSKI1:15

for S being satisfying_Tarski-model TarskiPlane

for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & b,x equiv b,y holds

x = y

for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & b,x equiv b,y holds

x = y

proof end;

theorem Bsymmetry: :: GTARSKI1:16

for S being satisfying_Tarski-model TarskiPlane

for a, p, z being POINT of S st between a,p,z holds

between z,p,a

for a, p, z being POINT of S st between a,p,z holds

between z,p,a

proof end;

theorem Baaq: :: GTARSKI1:17

for S being satisfying_Tarski-model TarskiPlane

for a, q being POINT of S holds between a,a,q by Bsymmetry, Bqaa;

for a, q being POINT of S holds between a,a,q by Bsymmetry, Bqaa;

theorem BEquality: :: GTARSKI1:18

for S being satisfying_Tarski-model TarskiPlane

for a, b, c being POINT of S st between a,b,c & between b,a,c holds

a = b

for a, b, c being POINT of S st between a,b,c & between b,a,c holds

a = b

proof end;

theorem B124and234then123: :: GTARSKI1:19

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

between a,b,c

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

between a,b,c

proof end;

theorem BTransitivity: :: GTARSKI1:20

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds

between a,c,d

for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds

between a,c,d

proof end;

theorem BTransitivityOrdered: :: GTARSKI1:21

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds

a,b,c,d are_ordered

for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds

a,b,c,d are_ordered

proof end;

theorem :: GTARSKI1:22

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

a,b,c,d are_ordered

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

a,b,c,d are_ordered

proof end;

theorem B124and234Ordered: :: GTARSKI1:23

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

a,b,c,d are_ordered

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

a,b,c,d are_ordered

proof end;

theorem SegmentAddition: :: GTARSKI1:24

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 holds

a,c equiv a9,c9

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 holds

a,c equiv a9,c9

proof end;

theorem CongruenceDoubleSymmetry: :: GTARSKI1:25

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st a,b equiv c,d holds

b,a equiv d,c

for a, b, c, d being POINT of S st a,b equiv c,d holds

b,a equiv d,c

proof end;

theorem C1prime: :: GTARSKI1:26

for S being satisfying_Tarski-model TarskiPlane

for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & a,x equiv a,y holds

x = y

for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & a,x equiv a,y holds

x = y

proof end;

theorem :: GTARSKI1:27

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & a,c equiv a9,c9 holds

b,c equiv b9,c9

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & a,c equiv a9,c9 holds

b,c equiv b9,c9

proof end;

theorem EasyAngleTransport: :: GTARSKI1:28

for S being satisfying_Tarski-model TarskiPlane

for a, b, o being POINT of S st o <> a holds

ex x, y being POINT of S st

( between b,o,x & between a,o,y & x,y,o cong a,b,o )

for a, b, o being POINT of S st o <> a holds

ex x, y being POINT of S st

( between b,o,x & between a,o,y & x,y,o cong a,b,o )

proof end;

theorem B123and134Ordered: :: GTARSKI1:29

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds

a,b,c,d are_ordered

for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds

a,b,c,d are_ordered

proof end;

theorem BextendToLine: :: GTARSKI1:30

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d holds

ex x being POINT of S st

( a,b,c,x are_ordered & a,b,d,x are_ordered )

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d holds

ex x being POINT of S st

( a,b,c,x are_ordered & a,b,d,x are_ordered )

proof end;

theorem :: GTARSKI1:31

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & b <> c & b <> d holds

not between c,b,d

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & b <> c & b <> d holds

not between c,b,d

proof end;

theorem Inner5Segments: :: GTARSKI1:32

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, x, a9, b9, c9, x9 being POINT of S st a,b,c cong a9,b9,c9 & between a,x,c & between a9,x9,c9 & c,x equiv c9,x9 holds

b,x equiv b9,x9

for a, b, c, x, a9, b9, c9, x9 being POINT of S st a,b,c cong a9,b9,c9 & between a,x,c & between a9,x9,c9 & c,x equiv c9,x9 holds

b,x equiv b9,x9

proof end;

theorem RhombusDiagBisect: :: GTARSKI1:33

for S being satisfying_Tarski-model TarskiPlane

for b, c, d, c9, d9 being POINT of S st between b,c,d9 & between b,d,c9 & c,d9 equiv c,d & d,c9 equiv c,d & d9,c9 equiv c,d holds

ex e being POINT of S st

( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e )

for b, c, d, c9, d9 being POINT of S st between b,c,d9 & between b,d,c9 & c,d9 equiv c,d & d,c9 equiv c,d & d9,c9 equiv c,d holds

ex e being POINT of S st

( between c,e,c9 & between d,e,d9 & c,e equiv c9,e & d,e equiv d9,e )

proof end;

theorem FlatNormal: :: GTARSKI1:34

for S being satisfying_Tarski-model TarskiPlane

for c, d, e, d9 being POINT of S st between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e & c <> d & e <> d holds

ex p, r, q being POINT of S st

( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e )

for c, d, e, d9 being POINT of S st between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e & c <> d & e <> d holds

ex p, r, q being POINT of S st

( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e )

proof end;

theorem EqDist2PointsBetween: :: GTARSKI1:35

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, p, q being POINT of S st a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q holds

c,p equiv c,q

for a, b, c, p, q being POINT of S st a <> b & between a,b,c & a,p equiv a,q & b,p equiv b,q holds

c,p equiv c,q

proof end;

theorem EqDist2PointsInnerBetween: :: GTARSKI1:36

for S being satisfying_Tarski-model TarskiPlane

for a, c, p, q, x being POINT of S st between a,x,c & a,p equiv a,q & c,p equiv c,q holds

x,p equiv x,q

for a, c, p, q, x being POINT of S st between a,x,c & a,p equiv a,q & c,p equiv c,q holds

x,p equiv x,q

proof end;

theorem Gupta: :: GTARSKI1:37

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between b,d,c holds

between b,c,d

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between b,d,c holds

between b,c,d

proof end;

:: deftheorem defines Collinear GTARSKI1:def 17 :

for S being satisfying_Tarski-model TarskiPlane

for a, b, c being POINT of S holds

( Collinear a,b,c iff ( between a,b,c or between b,c,a or between c,a,b ) );

for S being satisfying_Tarski-model TarskiPlane

for a, b, c being POINT of S holds

( Collinear a,b,c iff ( between a,b,c or between b,c,a or between c,a,b ) );

:: deftheorem defines on_line GTARSKI1:def 18 :

for S being satisfying_Tarski-model TarskiPlane

for a, b, x being POINT of S holds

( x on_line a,b iff ( a <> b & ( between a,b,x or between b,x,a or between x,a,b ) ) );

for S being satisfying_Tarski-model TarskiPlane

for a, b, x being POINT of S holds

( x on_line a,b iff ( a <> b & ( between a,b,x or between b,x,a or between x,a,b ) ) );

definition

let S be satisfying_Tarski-model TarskiPlane ;

let a, b, x, y be POINT of S;

end;
let a, b, x, y be POINT of S;

pred a,b equal_line x,y means :: GTARSKI1:def 19

( a <> b & x <> y & ( for c being POINT of S holds

( c on_line a,b iff c on_line x,y ) ) );

( a <> b & x <> y & ( for c being POINT of S holds

( c on_line a,b iff c on_line x,y ) ) );

:: deftheorem defines equal_line GTARSKI1:def 19 :

for S being satisfying_Tarski-model TarskiPlane

for a, b, x, y being POINT of S holds

( a,b equal_line x,y iff ( a <> b & x <> y & ( for c being POINT of S holds

( c on_line a,b iff c on_line x,y ) ) ) );

for S being satisfying_Tarski-model TarskiPlane

for a, b, x, y being POINT of S holds

( a,b equal_line x,y iff ( a <> b & x <> y & ( for c being POINT of S holds

( c on_line a,b iff c on_line x,y ) ) ) );

theorem I1part1: :: GTARSKI1:38

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, x being POINT of S st a <> b & a <> x & x on_line a,b & c on_line a,b holds

c on_line a,x

for a, b, c, x being POINT of S st a <> b & a <> x & x on_line a,b & c on_line a,b holds

c on_line a,x

proof end;

theorem I1part2: :: GTARSKI1:39

for S being satisfying_Tarski-model TarskiPlane

for a, b, x being POINT of S st a <> b & a <> x & x on_line a,b holds

a,b equal_line a,x

for a, b, x being POINT of S st a <> b & a <> x & x on_line a,b holds

a,b equal_line a,x

proof end;

theorem :: GTARSKI1:40

for S being satisfying_Tarski-model TarskiPlane

for a, b being POINT of S st a <> b holds

a,b equal_line a,b ;

for a, b being POINT of S st a <> b holds

a,b equal_line a,b ;

theorem LineEqA1: :: GTARSKI1:41

for S being satisfying_Tarski-model TarskiPlane

for a, b being POINT of S st a <> b holds

a,b equal_line b,a

for a, b being POINT of S st a <> b holds

a,b equal_line b,a

proof end;

theorem :: GTARSKI1:42

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d being POINT of S st a <> b & c <> d & a,b equal_line c,d holds

c,d equal_line a,b ;

for a, b, c, d being POINT of S st a <> b & c <> d & a,b equal_line c,d holds

c,d equal_line a,b ;

theorem :: GTARSKI1:43

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d, e, f being POINT of S st a <> b & c <> d & e <> f & a,b equal_line c,d & c,d equal_line e,f holds

a,b equal_line e,f ;

for a, b, c, d, e, f being POINT of S st a <> b & c <> d & e <> f & a,b equal_line c,d & c,d equal_line e,f holds

a,b equal_line e,f ;

theorem :: GTARSKI1:44

for S being satisfying_Tarski-model TarskiPlane

for a, b, c, d, x being POINT of S st x on_line a,b & a,b equal_line c,d holds

x on_line c,d ;

for a, b, c, d, x being POINT of S st x on_line a,b & a,b equal_line c,d holds

x on_line c,d ;

theorem I1part2Reverse: :: GTARSKI1:45

for S being satisfying_Tarski-model TarskiPlane

for a, b, y being POINT of S st a <> b & b <> y & y on_line a,b holds

a,b equal_line y,b

for a, b, y being POINT of S st a <> b & b <> y & y on_line a,b holds

a,b equal_line y,b

proof end;

theorem :: GTARSKI1:46

for S being satisfying_Tarski-model TarskiPlane

for a, b, x, y being POINT of S st a <> b & x <> y & a on_line x,y & b on_line x,y holds

x,y equal_line a,b

for a, b, x, y being POINT of S st a <> b & x <> y & a on_line x,y & b on_line x,y holds

x,y equal_line a,b

proof end;

definition

the naturally_generated TarskiExtension of ZeroSpace is MetrTarskiStr ;

end;

func Tarski0Space -> MetrTarskiStr equals :: GTARSKI1:def 20

the naturally_generated TarskiExtension of ZeroSpace ;

coherence the naturally_generated TarskiExtension of ZeroSpace ;

the naturally_generated TarskiExtension of ZeroSpace is MetrTarskiStr ;

:: deftheorem defines Tarski0Space GTARSKI1:def 20 :

Tarski0Space = the naturally_generated TarskiExtension of ZeroSpace ;

Tarski0Space = the naturally_generated TarskiExtension of ZeroSpace ;

registration
end;

definition

let M be non empty MetrStruct ;

end;
attr M is close-everywhere means :Lem1: :: GTARSKI1:def 21

for a, b being Element of M holds dist (a,b) = 0 ;

for a, b being Element of M holds dist (a,b) = 0 ;

:: deftheorem Lem1 defines close-everywhere GTARSKI1:def 21 :

for M being non empty MetrStruct holds

( M is close-everywhere iff for a, b being Element of M holds dist (a,b) = 0 );

for M being non empty MetrStruct holds

( M is close-everywhere iff for a, b being Element of M holds dist (a,b) = 0 );

registration
end;

registration

( Tarski0Space is satisfying_CongruenceSymmetry & Tarski0Space is satisfying_CongruenceEquivalenceRelation & Tarski0Space is satisfying_SegmentConstruction & Tarski0Space is satisfying_SAS & Tarski0Space is satisfying_Pasch )
end;

cluster Tarski0Space -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_SAS satisfying_Pasch ;

coherence ( Tarski0Space is satisfying_CongruenceSymmetry & Tarski0Space is satisfying_CongruenceEquivalenceRelation & Tarski0Space is satisfying_SegmentConstruction & Tarski0Space is satisfying_SAS & Tarski0Space is satisfying_Pasch )

proof end;

definition

the naturally_generated TarskiExtension of RealSpace is MetrTarskiStr ;

end;

func TarskiSpace -> MetrTarskiStr equals :: GTARSKI1:def 22

the naturally_generated TarskiExtension of RealSpace ;

coherence the naturally_generated TarskiExtension of RealSpace ;

the naturally_generated TarskiExtension of RealSpace is MetrTarskiStr ;

:: deftheorem defines TarskiSpace GTARSKI1:def 22 :

TarskiSpace = the naturally_generated TarskiExtension of RealSpace ;

TarskiSpace = the naturally_generated TarskiExtension of RealSpace ;

registration
end;

registration

( TarskiSpace is satisfying_CongruenceSymmetry & TarskiSpace is satisfying_CongruenceEquivalenceRelation & TarskiSpace is satisfying_CongruenceIdentity & TarskiSpace is satisfying_SegmentConstruction & TarskiSpace is satisfying_BetweennessIdentity )
end;

cluster TarskiSpace -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity ;

coherence ( TarskiSpace is satisfying_CongruenceSymmetry & TarskiSpace is satisfying_CongruenceEquivalenceRelation & TarskiSpace is satisfying_CongruenceIdentity & TarskiSpace is satisfying_SegmentConstruction & TarskiSpace is satisfying_BetweennessIdentity )

proof end;