:: Tarski Geometry Axioms
:: by William Richter , Adam Grabowski and Jesse Alama
::
:: Received June 16, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct TarskiGeometryStruct -> 1-sorted ;
aggr TarskiGeometryStruct(# carrier, Betweenness, Equidistance #) -> TarskiGeometryStruct ;
sel Betweenness c₁ -> Relation of [: the carrier of c₁, the carrier of c₁:], the carrier of c₁;
sel Equidistance c₁ -> Relation of [: the carrier of c₁, the carrier of c₁:],[: the carrier of c₁, the carrier of c₁:];

end;

definition

let S be TarskiGeometryStruct ;
mode POINT of S is Element of S;

end;

definition

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

pred between a,b,c means :: GTARSKI1:def 1
[[a,b],c] in the Betweenness of S;

end;

:: deftheorem defines between GTARSKI1:def 1 :
for S being TarskiGeometryStruct
for a, b, c being POINT of S holds
( between a,b,c iff [[a,b],c] in the Betweenness of S );

definition

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

pred a,b equiv c,d means :: GTARSKI1:def 2
[[a,b],[c,d]] in the Equidistance of S;

end;

:: deftheorem defines equiv GTARSKI1:def 2 :
for S being TarskiGeometryStruct
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 );

definition

let S be TarskiGeometryStruct ;
let a, b, c, x, y, z be POINT of S;

pred a,b,c cong x,y,z means :: GTARSKI1:def 3
( a,b equiv x,y & a,c equiv x,z & b,c equiv y,z );

end;

:: deftheorem defines cong GTARSKI1:def 3 :
for S being TarskiGeometryStruct
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 TarskiGeometryStruct ;
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 );

end;

:: deftheorem defines are_ordered GTARSKI1:def 4 :
for S being TarskiGeometryStruct
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 TarskiGeometryStruct ;

attr S is satisfying_CongruenceSymmetry means :: GTARSKI1:def 5
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;

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;

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

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;

attr S is satisfying_BetweennessIdentity means :: GTARSKI1:def 10
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 );

end;

:: deftheorem defines satisfying_CongruenceSymmetry GTARSKI1:def 5 :
for S being TarskiGeometryStruct 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 TarskiGeometryStruct 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 TarskiGeometryStruct 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 TarskiGeometryStruct 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 TarskiGeometryStruct 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 TarskiGeometryStruct 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 TarskiGeometryStruct 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 TarskiGeometryStruct ;

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

end;

:: deftheorem defines satisfying_Tarski-model GTARSKI1:def 12 :
for S being TarskiGeometryStruct 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₁ is strict ;
struct MetrTarskiStr -> MetrStruct , TarskiGeometryStruct ;
aggr MetrTarskiStr(# carrier, distance, Betweenness, Equidistance #) -> MetrTarskiStr ;

end;

definition

let M be MetrStruct ;

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
ex b₁ being MetrTarskiStr st MetrStruct(# the carrier of b₁, the distance of b₁ #) = MetrStruct(# the carrier of M, the distance of M #)

proof end;

end;

:: deftheorem TADef defines TarskiExtension GTARSKI1:def 13 :
for M being MetrStruct
for b₂ being MetrTarskiStr holds
( b₂ is TarskiExtension of M iff MetrStruct(# the carrier of b₂, the distance of b₂ #) = MetrStruct(# the carrier of M, the distance of M #) );

registration

let M be non empty MetrStruct ;

cluster -> non empty for TarskiExtension of M;

coherence
for b₁ being TarskiExtension of M holds not b₁ is empty

proof end;

end;

registration

let M be non empty Reflexive MetrStruct ;

cluster -> Reflexive for TarskiExtension of M;

coherence
for b₁ being TarskiExtension of M holds b₁ is Reflexive

proof end;

end;

registration

let M be non empty discerning MetrStruct ;

cluster -> discerning for TarskiExtension of M;

coherence
for b₁ being TarskiExtension of M holds b₁ is discerning

proof end;

end;

registration

let M be non empty symmetric MetrStruct ;

cluster -> symmetric for TarskiExtension of M;

coherence
for b₁ being TarskiExtension of M holds b₁ is symmetric

proof end;

end;

registration

let M be non empty triangle MetrStruct ;

cluster -> triangle for TarskiExtension of M;

coherence
for b₁ being TarskiExtension of M holds b₁ is triangle

proof end;

end;

definition

let S be MetrStruct ;
let p, q, r be Element of S;

pred q is_Between p,r means :: GTARSKI1:def 14
dist (p,r) = (dist (p,q)) + (dist (q,r));

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

definition

let M be MetrTarskiStr ;

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

end;

:: 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) ) ) ) );

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

registration

let N be non empty MetrStruct ;

cluster non empty naturally_generated for TarskiExtension of N;

existence
ex b₁ being TarskiExtension of N st b₁ is naturally_generated

proof end;

end;

registration

cluster non empty trivial Reflexive discerning symmetric triangle for MetrStruct ;

existence
ex b₁ being MetrSpace st
( b₁ is trivial & not b₁ is empty )

proof end;

end;

definition

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 is MetrTarskiStr ;

end;

:: deftheorem defines TrivialTarskiSpace GTARSKI1:def 16 :
TrivialTarskiSpace = the naturally_generated TarskiExtension of the non empty trivial MetrSpace;

registration

cluster TrivialTarskiSpace -> non empty trivial ;

coherence
( TrivialTarskiSpace is trivial & not TrivialTarskiSpace is empty )

proof end;

end;

theorem TrivialBetween: :: GTARSKI1:2

for M being non empty trivial MetrSpace
for a, b, c being Element of M holds a is_Between b,c

proof end;

registration

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;

end;

registration

cluster TrivialTarskiSpace -> satisfying_Tarski-model ;

coherence
TrivialTarskiSpace is satisfying_Tarski-model ;

end;

registration

cluster non empty satisfying_Tarski-model for TarskiGeometryStruct ;

existence
ex b₁ being TarskiGeometryStruct st
( b₁ is satisfying_Tarski-model & not b₁ is empty )

proof end;

end;

registration

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

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_CongruenceSymmetry & b₁ is satisfying_CongruenceEquivalenceRelation & b₁ is satisfying_CongruenceIdentity & b₁ is satisfying_SegmentConstruction & b₁ is satisfying_SAS & b₁ is satisfying_BetweennessIdentity & b₁ is satisfying_Pasch holds
b₁ is satisfying_Tarski-model ;

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

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_Tarski-model holds
( b₁ is satisfying_CongruenceSymmetry & b₁ is satisfying_CongruenceEquivalenceRelation & b₁ is satisfying_CongruenceIdentity & b₁ is satisfying_SegmentConstruction & b₁ is satisfying_SAS & b₁ is satisfying_BetweennessIdentity & b₁ is satisfying_Pasch ) ;

end;

theorem A1: :: GTARSKI1:3

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv b,a

proof end;

theorem A2: :: GTARSKI1:4

for S being satisfying_Tarski-model TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 EquivReflexive: :: GTARSKI1:10

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b

proof end;

theorem EquivSymmetric: :: GTARSKI1:11

for S being satisfying_Tarski-model TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
for a, b being POINT of S holds
( between a,a,a & a,a equiv b,b )

proof end;

theorem Bqaa: :: GTARSKI1:14

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, q being POINT of S holds between q,a,a

proof end;

theorem C1: :: GTARSKI1:15

for S being satisfying_Tarski-model TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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;

definition

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

pred Collinear a,b,c means :: GTARSKI1:def 17
( between a,b,c or between b,c,a or between c,a,b );

end;

:: deftheorem defines Collinear GTARSKI1:def 17 :
for S being TarskiGeometryStruct
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 ) );

definition

let S be satisfying_Tarski-model TarskiGeometryStruct ;
let a, b, x be POINT of S;

pred x on_line a,b means :: GTARSKI1:def 18
( a <> b & ( between a,b,x or between b,x,a or between x,a,b ) );

end;

:: deftheorem defines on_line GTARSKI1:def 18 :
for S being satisfying_Tarski-model TarskiGeometryStruct
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 TarskiGeometryStruct ;
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 ) ) );

end;

:: deftheorem defines equal_line GTARSKI1:def 19 :
for S being satisfying_Tarski-model TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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 TarskiGeometryStruct
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

func Tarski0Space -> MetrTarskiStr equals :: GTARSKI1:def 20
the naturally_generated TarskiExtension of ZeroSpace ;

coherence
the naturally_generated TarskiExtension of ZeroSpace is MetrTarskiStr ;

end;

:: deftheorem defines Tarski0Space GTARSKI1:def 20 :
Tarski0Space = the naturally_generated TarskiExtension of ZeroSpace ;

registration

cluster Tarski0Space -> non empty Reflexive symmetric ;

coherence
( Tarski0Space is Reflexive & Tarski0Space is symmetric & not Tarski0Space is empty ) ;

end;

definition

let M be non empty MetrStruct ;

attr M is close-everywhere means :Lem1: :: GTARSKI1:def 21
for a, b being Element of M holds dist (a,b) = 0 ;

end;

:: 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 );

registration

cluster Tarski0Space -> close-everywhere ;

coherence
Tarski0Space is close-everywhere

proof end;

end;

registration

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;

end;

definition

func TarskiSpace -> MetrTarskiStr equals :: GTARSKI1:def 22
the naturally_generated TarskiExtension of RealSpace ;

coherence
the naturally_generated TarskiExtension of RealSpace is MetrTarskiStr ;

end;

:: deftheorem defines TarskiSpace GTARSKI1:def 22 :
TarskiSpace = the naturally_generated TarskiExtension of RealSpace ;

registration

cluster TarskiSpace -> non empty ;

coherence
not TarskiSpace is empty ;

end;

registration

cluster TarskiSpace -> Reflexive discerning symmetric ;

coherence
( TarskiSpace is Reflexive & TarskiSpace is symmetric & TarskiSpace is discerning ) ;

end;

registration

cluster -> real for Element of the carrier of TarskiSpace;

coherence
for b₁ being Element of TarskiSpace holds b₁ is real

proof end;

end;

registration

cluster -> real for Element of the carrier of RealSpace;

coherence
for b₁ being Element of RealSpace holds b₁ is real ;

end;

theorem :: GTARSKI1:47

for a, b, c being Element of RealSpace st b in [.a,c.] holds
b is_Between a,c

proof end;

registration

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;

end;