:: {T}arski Geometry Axioms -- Part {III}
:: by Roland Coghetto and Adam Grabowski
::
:: Received November 29, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

:: 2.1 Satz

theorem Satz2p1: :: GTARSKI3:1

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b

proof end;

:: 2.1 Satz bis

theorem Satz2p1bis: :: GTARSKI3:2

for S being satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b

proof end;

:: 2.2 Satz

theorem Satz2p2: :: GTARSKI3:3

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

proof end;

:: 2.2 Satz bis

theorem Satz2p2bis: :: GTARSKI3:4

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

proof end;

:: 2.3 Satz

theorem Satz2p3: :: GTARSKI3:5

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct
for a, b, c, d, e, f being POINT of S st a,b equiv c,d & c,d equiv e,f holds
a,b equiv e,f

proof end;

:: 2.4 Satz

theorem Satz2p4: :: GTARSKI3:6

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

proof end;

:: 2.5 Satz

theorem Satz2p5: :: GTARSKI3:7

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

proof end;

:: 2.8 Satz

theorem Satz2p8: :: GTARSKI3:8

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct
for a, b being POINT of S holds a,a equiv b,b

proof end;

definition

let S be TarskiGeometryStruct ;

attr S is satisfying_SST_A5 means :: GTARSKI3:def 1
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
c,d equiv c9,d9;

end;

:: deftheorem defines satisfying_SST_A5 GTARSKI3:def 1 :
for S being TarskiGeometryStruct holds
( S is satisfying_SST_A5 iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
c,d equiv c9,d9 );

theorem EQUIV1: :: GTARSKI3:9

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds
( S is satisfying_SAS iff S is satisfying_SST_A5 )

proof end;

registration

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SST_A5 -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS for TarskiGeometryStruct ;

coherence
for b₁ being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct st b₁ is satisfying_SST_A5 holds
b₁ is satisfying_SAS by EQUIV1;

end;

registration

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SST_A5 for TarskiGeometryStruct ;

coherence
for b₁ being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct st b₁ is satisfying_SAS holds
b₁ is satisfying_SST_A5 by EQUIV1;

end;

definition

let S be TarskiGeometryStruct ;
let a, b, c, d, a9, b9, c9, d9 be POINT of S;

pred a,b,c,d AFS a9,b9,c9,d9 means :: GTARSKI3:def 2
( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 );

end;

:: deftheorem defines AFS GTARSKI3:def 2 :
for S being TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S holds
( a,b,c,d AFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );

theorem Axiom5AFS: :: GTARSKI3:10

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d AFS a9,b9,c9,d9 & a <> b holds
c,d equiv c9,d9

proof end;

:: 2.11 Satz

theorem Satz2p11: :: GTARSKI3:11

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS 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;

:: 2.12 Satz

theorem Satz2p12: :: GTARSKI3:12

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct
for q, a, b, c being POINT of S st q <> a holds
for x1, x2 being POINT of S st between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c holds
x1 = x2

proof end;

:: 3.1 Satz

theorem Satz3p1: :: GTARSKI3:13

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct
for a, b being POINT of S holds between a,b,b

proof end;

:: 3.2 Satz

theorem Satz3p2: :: GTARSKI3:14

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c being POINT of S st between a,b,c holds
between c,b,a

proof end;

:: 3.3 Satz

theorem :: GTARSKI3:15

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b being POINT of S holds between a,a,b by Satz3p1, Satz3p2;

:: 3.4 Satz

theorem Satz3p4: :: GTARSKI3:16

for S being satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c being POINT of S st between a,b,c & between b,a,c holds
a = b

proof end;

Satz3p5p1: for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch 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;

Satz3p6p1: for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds
between b,c,d

proof end;

Satz3p7p1: for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds
between a,c,d

proof end;

Satz3p5p2: 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,c,d

proof end;

Satz3p6p2: 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
between a,b,d

proof end;

Satz3p7p2: for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds
between a,b,d

proof end;

:: 3.5 Satz

theorem :: GTARSKI3:17

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 & between a,c,d ) by Satz3p5p1, Satz3p5p2;

:: 3.6 Satz

theorem :: GTARSKI3:18

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
( between b,c,d & between a,b,d ) by Satz3p6p1, Satz3p6p2;

:: 3.7 Satz

theorem :: GTARSKI3:19

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds
( between a,c,d & between a,b,d ) by Satz3p7p1, Satz3p7p2;

:: 3.8 Definition (n = 4)

definition

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

pred between4 a,b,c,d means :: GTARSKI3:def 3
( between a,b,c & between a,b,d & between a,c,d & between b,c,d );

end;

:: deftheorem defines between4 GTARSKI3:def 3 :
for S being TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( between4 a,b,c,d iff ( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) );

:: 3.8 Definition (n = 5)

definition

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

pred between5 a,b,c,d,e means :: GTARSKI3:def 4
( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e );

end;

:: deftheorem defines between5 GTARSKI3:def 4 :
for S being TarskiGeometryStruct
for a, b, c, d, e being POINT of S holds
( between5 a,b,c,d,e iff ( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e ) );

:: 3.9 Satz (n = 3)

theorem :: GTARSKI3:20

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c being POINT of S st between a,b,c holds
between c,b,a by Satz3p2;

:: 3.9 Satz (n = 4)

theorem :: GTARSKI3:21

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d being POINT of S st between4 a,b,c,d holds
between4 d,c,b,a by Satz3p2;

:: 3.9 Satz (n = 5)

theorem :: GTARSKI3:22

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds
between5 e,d,c,b,a by Satz3p2;

:: 3.10 Satz (n = 4)

theorem :: GTARSKI3:23

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d being POINT of S st between4 a,b,c,d holds
( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) ;

:: 3.10 Satz (n = 5)

theorem :: GTARSKI3:24

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds
( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e & between4 a,b,c,d & between4 a,b,c,e & between4 a,c,d,e & between4 b,c,d,e ) ;

:: 3.11 Satz (n = 3, l = 1)

theorem :: GTARSKI3:25

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,b,c & between a,p,b holds
between4 a,p,b,c by Satz3p6p1, Satz3p6p2;

:: 3.11 Satz (n = 3, l = 2)

theorem Satz3p11p3pb: :: GTARSKI3:26

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,b,c & between b,p,c holds
between4 a,b,p,c by Satz3p5p1, Satz3p5p2;

:: 3.11 Satz (n = 3, l = 1)

theorem :: GTARSKI3:27

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,p,b holds
between5 a,p,b,c,d

proof end;

:: 3.11 Satz (n = 3, l = 2)

theorem Satz3p11p4pb: :: GTARSKI3:28

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,p,c holds
between5 a,b,p,c,d

proof end;

:: 3.11 Satz (n = 3, l = 3)

theorem :: GTARSKI3:29

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,p,d holds
between5 a,b,c,p,d

proof end;

:: 3.12 Satz (n = 3, l = 1)

theorem :: GTARSKI3:30

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,b,c & between a,c,p holds
( between4 a,b,c,p & ( a <> c implies between4 a,b,c,p ) ) by Satz3p6p1, Satz3p6p2;

:: 3.12 Satz (n = 3, l = 2)

theorem :: GTARSKI3:31

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,b,c & between b,c,p holds
( between b,c,p & ( b <> c implies between4 a,b,c,p ) ) by Satz3p7p1, Satz3p7p2;

:: 3.12 Satz (n = 4, l = 1)

theorem :: GTARSKI3:32

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,d,p holds
( between5 a,b,c,d,p & ( a <> d implies between5 a,b,c,d,p ) )

proof end;

:: 3.12 Satz (n = 4, l = 2)

theorem :: GTARSKI3:33

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,d,p holds
( between4 b,c,d,p & ( b <> d implies between5 a,b,c,d,p ) )

proof end;

:: 3.12 Satz (n = 4, l = 3)

theorem :: GTARSKI3:34

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,d,p holds
( between c,d,p & ( c <> d implies between5 a,b,c,d,p ) )

proof end;

registration

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

existence
ex b₁ being satisfying_Tarski-model TarskiGeometryStruct st b₁ is satisfying_Lower_Dimension_Axiom

proof end;

end;

:: 3.13 Satz

theorem Satz3p13: :: GTARSKI3:35

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )

proof end;

:: 3.14 Satz

theorem Satz3p14: :: GTARSKI3:36

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S ex c being POINT of S st
( between a,b,c & b <> c )

proof end;

:: 3.15 Satz (n = 3)

theorem Satz3p15p3: :: GTARSKI3:37

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a1, a2 being POINT of S st a1 <> a2 holds
ex a3 being POINT of S st
( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct )

proof end;

:: 3.15 Satz (n = 4)

theorem Satz3p15p4: :: GTARSKI3:38

for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a1, a2 being POINT of S st a1 <> a2 holds
ex a3, a4 being POINT of S st
( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )

proof end;

:: 3.15 Satz (n = 5)

theorem :: GTARSKI3:39

for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a1, a2 being POINT of S st a1 <> a2 holds
ex a3, a4, a5 being POINT of S st
( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )

proof end;

:: 3.17 Satz

theorem Satz3p17: :: GTARSKI3:40

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c & between a,p,a9 holds
ex q being POINT of S st
( between p,q,c & between b,q,b9 )

proof end;

definition

let S be TarskiGeometryStruct ;
let a, b, c, d, a9, b9, c9, d9 be POINT of S;

pred a,b,c,d IFS a9,b9,c9,d9 means :: GTARSKI3:def 5
( between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 & a,d equiv a9,d9 & c,d equiv c9,d9 );

end;

:: deftheorem defines IFS GTARSKI3:def 5 :
for S being TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S holds
( a,b,c,d IFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 & a,d equiv a9,d9 & c,d equiv c9,d9 ) );

:: 4.2 Satz

theorem Satz4p2: :: GTARSKI3:41

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d IFS a9,b9,c9,d9 holds
b,d equiv b9,d9

proof end;

:: 4.3 Satz

theorem Satz4p3: :: GTARSKI3:42

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,c equiv a9,c9 & b,c equiv b9,c9 holds
a,b equiv a9,b9

proof end;

:: 4.5 Satz

theorem Satz4p5: :: GTARSKI3:43

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, c9 being POINT of S st between a,b,c & a,c equiv a9,c9 holds
ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 )

proof end;

:: 4.6 Satz

theorem Satz4p6: :: GTARSKI3:44

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & a,b,c cong a9,b9,c9 holds
between a9,b9,c9

proof end;

:: 4.11 Satz

theorem :: GTARSKI3:45

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c being POINT of S st Collinear a,b,c holds
( Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b ) by Satz3p2;

:: 4.12 Sazz

theorem :: GTARSKI3:46

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct
for a, b being POINT of S holds Collinear a,a,b by Satz3p1;

theorem Lm4p13p1: :: GTARSKI3:47

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st a,b,c cong a9,b9,c9 holds
b,c,a cong b9,c9,a9

proof end;

:: 4.13 Satz

theorem Satz4p13: :: GTARSKI3:48

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st Collinear a,b,c & a,b,c cong a9,b9,c9 holds
Collinear a9,b9,c9

proof end;

theorem Lm4p14p1: :: GTARSKI3:49

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st b,a,c cong b9,a9,c9 holds
a,b,c cong a9,b9,c9

proof end;

theorem Lm4p14p2: :: GTARSKI3:50

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct
for a, b, c, a9, b9, c9 being POINT of S st a,c,b cong a9,c9,b9 holds
a,b,c cong a9,b9,c9

proof end;

:: 4.14 Satz

theorem Satz4p14: :: GTARSKI3:51

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a9, b9 being POINT of S st Collinear a,b,c & a,b equiv a9,b9 holds
ex c9 being POINT of S st a,b,c cong a9,b9,c9

proof end;

definition

let S be TarskiGeometryStruct ;
let a, b, c, d, a9, b9, c9, d9 be POINT of S;

pred a,b,c,d FS a9,b9,c9,d9 means :: GTARSKI3:def 6
( Collinear a,b,c & a,b,c cong a9,b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 );

end;

:: deftheorem defines FS GTARSKI3:def 6 :
for S being TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S holds
( a,b,c,d FS a9,b9,c9,d9 iff ( Collinear a,b,c & a,b,c cong a9,b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );

:: 4.16 Satz

theorem Satz4p16: :: GTARSKI3:52

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d FS a9,b9,c9,d9 & a <> b holds
c,d equiv c9,d9

proof end;

:: 4.17 Satz

theorem Satz4p17: :: GTARSKI3:53

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p, q being POINT of S st a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q holds
c,p equiv c,q

proof end;

:: 4.18 Satz

theorem Satz4p18: :: GTARSKI3:54

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, c9 being POINT of S st a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 holds
c = c9

proof end;

:: 4.19 Satz

theorem Satz4p19: :: GTARSKI3:55

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, c9 being POINT of S st between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 holds
c = c9

proof end;

:: 5.1 Satz

theorem Satz5p1: :: GTARSKI3:56

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 a,c,d holds
between a,d,c

proof end;

:: 5.2 Satz

theorem Satz5p2: :: GTARSKI3:57

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,c,d holds
between b,d,c

proof end;

:: 5.3 Satz

theorem Satz5p3: :: GTARSKI3:58

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,d & between a,c,d & not between a,b,c holds
between a,c,b

proof end;

definition

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

pred a,b <= c,d means :: GTARSKI3:def 7
ex y being POINT of S st
( between c,y,d & a,b equiv c,y );

end;

:: deftheorem defines <= GTARSKI3:def 7 :
for S being TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b <= c,d iff ex y being POINT of S st
( between c,y,d & a,b equiv c,y ) );

:: 5.5 Satz

theorem Satz5p5: :: GTARSKI3:59

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )

proof end;

:: 5.6 Satz

theorem Satz5p6: :: GTARSKI3:60

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 holds
a9,b9 <= c9,d9

proof end;

:: 5.7 Satz

theorem :: GTARSKI3:61

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

proof end;

:: 5.8 Satz

theorem :: GTARSKI3:62

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, e, f being POINT of S st a,b <= c,d & c,d <= e,f holds
a,b <= e,f

proof end;

:: 5.9 Satz

theorem :: GTARSKI3:63

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b <= c,d & c,d <= a,b holds
a,b equiv c,d

proof end;

:: 5.10 Satz

theorem Satz5p10: :: GTARSKI3:64

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b <= c,d or c,d <= a,b )

proof end;

:: 5.11 Satz

theorem :: GTARSKI3:65

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S holds a,a <= b,c

proof end;

:: 5.12 Lemma 1

theorem :: GTARSKI3:66

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b <= c,d holds
b,a <= c,d by Satz2p4;

:: 5.12 Lemma 2

theorem Lemma5p12p2: :: GTARSKI3:67

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b <= c,d holds
a,b <= d,c

proof end;

:: 5.12 Lemma 3

theorem Lemma5p12p3: :: GTARSKI3:68

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st between a,b,c & a,c equiv a,b holds
c = b

proof end;

:: METAMATH: endofsegidand

theorem Lemma5p12p4: :: GTARSKI3:69

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st between a,c,b & a,b <= a,c holds
b = c

proof end;

:: 5.12 Satz

theorem Satz5p12: :: GTARSKI3:70

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st Collinear a,b,c holds
( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) )

proof end;

definition

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

pred p out a,b means :: GTARSKI3:def 8
( p <> a & p <> b & ( between p,a,b or between p,b,a ) );

end;

:: deftheorem defines out GTARSKI3:def 8 :
for S being TarskiGeometryStruct
for a, b, p being POINT of S holds
( p out a,b iff ( p <> a & p <> b & ( between p,a,b or between p,b,a ) ) );

:: 6.2 Satz

theorem Satz6p2: :: GTARSKI3:71

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st a <> p & b <> p & c <> p & between a,p,c holds
( between b,p,c iff p out a,b )

proof end;

:: 6.3 Satz

theorem Satz6p3: :: GTARSKI3:72

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S holds
( p out a,b iff ( a <> p & b <> p & ex c being POINT of S st
( c <> p & between a,p,c & between b,p,c ) ) )

proof end;

:: 6.4 Satz

theorem :: GTARSKI3:73

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S holds
( p out a,b iff ( Collinear a,p,b & not between a,p,b ) )

proof end;

:: 6.5 Satz

theorem :: GTARSKI3:74

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p being POINT of S st a <> p holds
p out a,a by Satz3p1;

:: 6.6 Satz

theorem :: GTARSKI3:75

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S st p out a,b holds
p out b,a ;

:: 6.7 Satz

theorem :: GTARSKI3:76

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st p out a,b & p out b,c holds
p out a,c by Satz3p6p2, Satz5p3, Satz5p1;

:: METAMATH: segcon2

theorem Lemmapsegcon2: :: GTARSKI3:77

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S ex x being POINT of S st
( ( between p,a,x or between p,x,a ) & p,x equiv b,c )

proof end;

:: 6.11 Satz a)

theorem :: GTARSKI3:78

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, r being POINT of S st r <> a & b <> c holds
ex x being POINT of S st
( a out x,r & a,x equiv b,c )

proof end;

definition

let S be TarskiGeometryStruct ;
let a, p be POINT of S;

func halfline (p,a) -> set equals :: GTARSKI3:def 9
{ x where x is POINT of S : p out x,a } ;

coherence
{ x where x is POINT of S : p out x,a } is set ;

end;

:: deftheorem defines halfline GTARSKI3:def 9 :
for S being TarskiGeometryStruct
for a, p being POINT of S holds halfline (p,a) = { x where x is POINT of S : p out x,a } ;

:: 6.11 Satz b)

theorem Satz6p11pb: :: GTARSKI3:79

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, r, x, y being POINT of S st r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c holds
x = y

proof end;

:: 6.13 Satz

theorem Satz6p13: :: GTARSKI3:80

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S st p out a,b holds
( p,a <= p,b iff between p,a,b )

proof end;

:: 6.14 Definition

definition

let S be non empty TarskiGeometryStruct ;
let p, q be POINT of S;

func Line (p,q) -> Subset of S equals :: GTARSKI3:def 10
{ x where x is POINT of S : Collinear p,q,x } ;

coherence
{ x where x is POINT of S : Collinear p,q,x } is Subset of S

proof end;

end;

:: deftheorem defines Line GTARSKI3:def 10 :
for S being non empty TarskiGeometryStruct
for p, q being POINT of S holds Line (p,q) = { x where x is POINT of S : Collinear p,q,x } ;

:: 6.15 Satz

theorem :: GTARSKI3:81

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for p, q, r being POINT of S st p <> q & p <> r & between q,p,r holds
Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))

proof end;

definition

let S be non empty TarskiGeometryStruct ;
let A be Subset of S;

pred A is_line means :: GTARSKI3:def 11
ex p, q being POINT of S st
( p <> q & A = Line (p,q) );

end;

:: deftheorem defines is_line GTARSKI3:def 11 :
for S being non empty TarskiGeometryStruct
for A being Subset of S holds
( A is_line iff ex p, q being POINT of S st
( p <> q & A = Line (p,q) ) );

:: 6.16 Satz

theorem :: GTARSKI3:82

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for p, q, s being POINT of S st p <> q & s <> p & s in Line (p,q) holds
Line (p,q) = Line (p,s)

proof end;

:: 6.17 Satz

theorem Satz6p17: :: GTARSKI3:83

for S being non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for p, q being POINT of S holds
( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )

proof end;

theorem Thequiv1: :: GTARSKI3:84

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being Element of S holds
( ( a <> b & Collinear a,b,c ) iff c on_line a,b ) ;

theorem Thequiv2: :: GTARSKI3:85

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S st a,b equal_line x,y holds
Line (a,b) = Line (x,y)

proof end;

theorem :: GTARSKI3:86

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S st a <> b & x <> y & Line (a,b) = Line (x,y) holds
a,b equal_line x,y

proof end;

:: 6.18 Satz

theorem Satz6p18: :: GTARSKI3:87

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A being Subset of S
for a, b being POINT of S st A is_line & a <> b & a in A & b in A holds
A = Line (a,b)

proof end;

:: 6.19 Satz

theorem Satz6p19: :: GTARSKI3:88

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, B being Subset of S
for a, b being POINT of S st a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B holds
A = B

proof end;

:: 6.21 Satz

theorem :: GTARSKI3:89

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, B being Subset of S
for a, b being POINT of S st A is_line & B is_line & A <> B & a in A & a in B & b in A & b in B holds
a = b by Satz6p19;

:: 6.23 Satz

theorem :: GTARSKI3:90

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st ex p, q being POINT of S st p <> q holds
( Collinear a,b,c iff ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) )

proof end;

:: 6.24 Satz

theorem Satz6p24: :: GTARSKI3:91

for S being satisfying_A8 TarskiGeometryStruct holds
not for a, b, c being POINT of S holds Collinear a,b,c

proof end;

:: 6.25 Satz

theorem :: GTARSKI3:92

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S st S is satisfying_A8 & a <> b holds
ex c being POINT of S st not Collinear a,b,c

proof end;

theorem Satz6p28Lem01: :: GTARSKI3:93

for S being satisfying_Tarski-model TarskiGeometryStruct
for p, a, b being POINT of S st p out a,b & p,a <= p,b holds
between p,a,b by Satz6p13;

theorem Satz6p28Lem02: :: GTARSKI3:94

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, e, f, g, h being Element of S st not c,d <= a,b & a,b equiv e,f & c,d equiv g,h holds
e,f <= g,h

proof end;

:: 6.28 Satz, introduced by Beeson

theorem :: GTARSKI3:95

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, a1, b1, c1 being Element of S st b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 holds
a,c equiv a1,c1

proof end;

definition

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

pred Middle a,m,b means :DEFM: :: GTARSKI3:def 12
( between a,m,b & m,a equiv m,b );

end;

:: deftheorem DEFM defines Middle GTARSKI3:def 12 :
for S being TarskiGeometryStruct
for a, b, m being POINT of S holds
( Middle a,m,b iff ( between a,m,b & m,a equiv m,b ) );

:: 7.2 Satz

theorem :: GTARSKI3:96

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, m being POINT of S st Middle a,m,b holds
Middle b,m,a by Satz3p2, Satz2p2;

:: 7.3 Satz

theorem Satz7p3: :: GTARSKI3:97

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct
for a, m being POINT of S holds
( Middle a,m,a iff m = a ) by GTARSKI1:def 10, Satz3p1, Satz2p1;

:: 7.4 Existence

theorem Satz7p4existence: :: GTARSKI3:98

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct
for a, p being POINT of S ex p9 being POINT of S st Middle p,a,p9

proof end;

:: 7.4 Uniqueness

theorem Satz7p4uniqueness: :: GTARSKI3:99

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct
for a, p, p1, p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds
p1 = p2

proof end;

definition

let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct ;
let a, p be POINT of S;

func reflection (a,p) -> POINT of S means :DEFR: :: GTARSKI3:def 13
Middle p,a,it;

existence
ex b₁ being POINT of S st Middle p,a,b₁ by Satz7p4existence;
uniqueness
for b₁, b₂ being POINT of S st Middle p,a,b₁ & Middle p,a,b₂ holds
b₁ = b₂ by Satz7p4uniqueness;

end;

:: deftheorem DEFR defines reflection GTARSKI3:def 13 :
for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct
for a, p, b₄ being POINT of S holds
( b₄ = reflection (a,p) iff Middle p,a,b₄ );

:: 7.6 Satz

theorem :: GTARSKI3:100

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct
for a, p, p9 being POINT of S holds
( reflection (a,p) = p9 iff Middle p,a,p9 ) by DEFR;

:: 7.7 Satz

theorem Satz7p7: :: GTARSKI3:101

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, p being POINT of S holds reflection (a,(reflection (a,p))) = p

proof end;

:: 7.8 Satz

theorem :: GTARSKI3:102

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, p9 being POINT of S ex p being POINT of S st reflection (a,p) = p9

proof end;

:: 7.9 Satz

theorem Satz7p9: :: GTARSKI3:103

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, p, p9 being POINT of S st reflection (a,p) = reflection (a,p9) holds
p = p9

proof end;

:: 7.10 Satz

theorem Satz7p10: :: GTARSKI3:104

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct
for a, p being POINT of S holds
( reflection (a,p) = p iff p = a )

proof end;

:: 7.13 Satz

theorem Satz7p13: :: GTARSKI3:105

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, q being POINT of S holds p,q equiv reflection (a,p), reflection (a,q)

proof end;

Lemma7p15a: for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, q, r being POINT of S st between p,q,r holds
between reflection (a,p), reflection (a,q), reflection (a,r)

proof end;

:: 7.15 Satz

theorem Satz7p15: :: GTARSKI3:106

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, q, r being POINT of S holds
( between p,q,r iff between reflection (a,p), reflection (a,q), reflection (a,r) )

proof end;

Lemma7p16a: for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, q, r, s being POINT of S st p,q equiv r,s holds
reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s)

proof end;

:: 7.16 Satz

theorem Satz7p16: :: GTARSKI3:107

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, q, r, s being POINT of S holds
( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )

proof end;

:: 7.17 Satz

theorem Satz7p17: :: GTARSKI3:108

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p, p9 being POINT of S st Middle p,a,p9 & Middle p,b,p9 holds
a = b

proof end;

:: 7.18 Satz

theorem :: GTARSKI3:109

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S st reflection (a,p) = reflection (b,p) holds
a = b

proof end;

:: 7.19 Satz

theorem :: GTARSKI3:110

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S holds
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )

proof end;

:: 7.20 Satz

theorem Satz7p20: :: GTARSKI3:111

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, m being POINT of S st Collinear a,m,b & m,a equiv m,b & not a = b holds
Middle a,m,b

proof end;

:: 7.21 Satz

theorem :: GTARSKI3:112

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st not Collinear a,b,c & b <> d & a,b equiv c,d & b,c equiv d,a & Collinear a,p,c & Collinear b,p,d holds
( Middle a,p,c & Middle b,p,d )

proof end;

:: 7.22 Satz, part 1

theorem Satz7p22part1: :: GTARSKI3:113

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a1 <= c,a2 holds
between m1,c,m2

proof end;

:: 7.22 Satz, part 2

theorem Satz7p22part2: :: GTARSKI3:114

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a2 <= c,a1 holds
between m1,c,m2

proof end;

:: 7.22 Satz: Krippenlemma, (Gupta 1965, 3.45 Theorem)

theorem Satz7p22: :: GTARSKI3:115

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 holds
between m1,c,m2

proof end;

definition

let S be TarskiGeometryStruct ;
let a1, a2, b1, b2, c, m1, m2 be POINT of S;

pred Krippenfigur a1,m1,b1,c,b2,m2,a2 means :: GTARSKI3:def 14
( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 );

end;

:: deftheorem defines Krippenfigur GTARSKI3:def 14 :
for S being TarskiGeometryStruct
for a1, a2, b1, b2, c, m1, m2 being POINT of S holds
( Krippenfigur a1,m1,b1,c,b2,m2,a2 iff ( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 ) );

:: Krippenfigur

theorem :: GTARSKI3:116

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for c, a1, a2, b1, b2, m1, m2 being POINT of S st Krippenfigur a1,m1,b1,c,b2,m2,a2 holds
between m1,c,m2 by Satz7p22;

registration

cluster non empty satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch satisfying_Tarski-model satisfying_Lower_Dimension_Axiom satisfying_SST_A5 for TarskiGeometryStruct ;

existence
not for b₁ being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds b₁ is empty by GTARSKI2:def 2;

end;

::$ 7.25 Satz

theorem :: GTARSKI3:117

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st c,a equiv c,b holds
ex x being POINT of S st Middle a,x,b

proof end;

definition

let S be TarskiGeometryStruct ;

attr S is (RE) means :: GTARSKI3:def 15
for a, b being POINT of S holds a,b equiv b,a;

attr S is (TE) means :: GTARSKI3:def 16
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 (IE) means :: GTARSKI3:def 17
for a, b, c being POINT of S st a,b equiv c,c holds
a = b;

attr S is (SC) means :: GTARSKI3:def 18
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 );

attr S is (FS) means :: GTARSKI3:def 19
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
c,d equiv c9,d9;

attr S is (IB) means :: GTARSKI3:def 20
for a, b being POINT of S st between a,b,a holds
a = b;

attr S is (Pa) means :: GTARSKI3:def 21
for a, b, c, p, q being POINT of S st between a,p,c & between b,q,c holds
ex x being POINT of S st
( between p,x,b & between q,x,a );

attr S is (Lo2) means :: GTARSKI3:def 22
ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b );

attr S is (Up2) means :: GTARSKI3:def 23
for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds
between c,a,b;

attr S is (Eu) means :: GTARSKI3:def 24
for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds
ex x, y being POINT of S st
( between a,b,x & between a,c,y & between x,t,y );

attr S is (Co) means :: GTARSKI3:def 25
for X, Y being set st ex a being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between a,x,y holds
ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y;

attr S is (FS') means :: GTARSKI3:def 26
for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
d,c equiv c9,d9;

end;

:: deftheorem defines (RE) GTARSKI3:def 15 :
for S being TarskiGeometryStruct holds
( S is (RE) iff for a, b being POINT of S holds a,b equiv b,a );

:: deftheorem defines (TE) GTARSKI3:def 16 :
for S being TarskiGeometryStruct holds
( S is (TE) 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 (IE) GTARSKI3:def 17 :
for S being TarskiGeometryStruct holds
( S is (IE) iff for a, b, c being POINT of S st a,b equiv c,c holds
a = b );

:: deftheorem defines (SC) GTARSKI3:def 18 :
for S being TarskiGeometryStruct holds
( S is (SC) iff 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 ) );

:: deftheorem defines (FS) GTARSKI3:def 19 :
for S being TarskiGeometryStruct holds
( S is (FS) iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
c,d equiv c9,d9 );

:: deftheorem defines (IB) GTARSKI3:def 20 :
for S being TarskiGeometryStruct holds
( S is (IB) iff for a, b being POINT of S st between a,b,a holds
a = b );

:: deftheorem defines (Pa) GTARSKI3:def 21 :
for S being TarskiGeometryStruct holds
( S is (Pa) iff for a, b, c, p, q being POINT of S st between a,p,c & between b,q,c holds
ex x being POINT of S st
( between p,x,b & between q,x,a ) );

:: deftheorem defines (Lo2) GTARSKI3:def 22 :
for S being TarskiGeometryStruct holds
( S is (Lo2) iff ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b ) );

:: deftheorem defines (Up2) GTARSKI3:def 23 :
for S being TarskiGeometryStruct holds
( S is (Up2) iff for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds
between c,a,b );

:: deftheorem defines (Eu) GTARSKI3:def 24 :
for S being TarskiGeometryStruct holds
( S is (Eu) iff for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds
ex x, y being POINT of S st
( between a,b,x & between a,c,y & between x,t,y ) );

:: deftheorem defines (Co) GTARSKI3:def 25 :
for S being TarskiGeometryStruct holds
( S is (Co) iff for X, Y being set st ex a being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between a,x,y holds
ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y );

:: deftheorem defines (FS') GTARSKI3:def 26 :
for S being TarskiGeometryStruct holds
( S is (FS') iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
d,c equiv c9,d9 );

theorem :: GTARSKI3:118

for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceSymmetry iff S is (RE) ) ;

theorem :: GTARSKI3:119

for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceEquivalenceRelation iff S is (TE) ) ;

theorem :: GTARSKI3:120

for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceIdentity iff S is (IE) ) ;

theorem :: GTARSKI3:121

for S being TarskiGeometryStruct holds
( S is satisfying_SegmentConstruction iff S is (SC) ) ;

theorem :: GTARSKI3:122

for S being TarskiGeometryStruct holds
( S is satisfying_BetweennessIdentity iff S is (IB) ) ;

theorem :: GTARSKI3:123

for S being TarskiGeometryStruct holds
( S is satisfying_Pasch iff S is (Pa) ) ;

theorem :: GTARSKI3:124

for S being TarskiGeometryStruct holds
( S is satisfying_Lower_Dimension_Axiom iff S is (Lo2) ) ;

theorem :: GTARSKI3:125

for S being TarskiGeometryStruct holds
( S is satisfying_Upper_Dimension_Axiom iff S is (Up2) ) ;

theorem :: GTARSKI3:126

for S being TarskiGeometryStruct holds
( S is satisfying_Euclid_Axiom iff S is (Eu) ) ;

theorem :: GTARSKI3:127

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds
( S is satisfying_SAS iff S is (FS) )

proof end;

theorem ThMak1: :: GTARSKI3:128

for S being non empty TarskiGeometryStruct holds
( S is satisfying_Continuity_Axiom iff S is (Co) )

proof end;

registration

cluster (RE) -> satisfying_CongruenceSymmetry for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (RE) holds
b₁ is satisfying_CongruenceSymmetry ;

cluster (TE) -> satisfying_CongruenceEquivalenceRelation for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (TE) holds
b₁ is satisfying_CongruenceEquivalenceRelation ;

cluster (IE) -> satisfying_CongruenceIdentity for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (IE) holds
b₁ is satisfying_CongruenceIdentity ;

cluster (SC) -> satisfying_SegmentConstruction for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (SC) holds
b₁ is satisfying_SegmentConstruction ;

cluster (IB) -> satisfying_BetweennessIdentity for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (IB) holds
b₁ is satisfying_BetweennessIdentity ;

cluster (Pa) -> satisfying_Pasch for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (Pa) holds
b₁ is satisfying_Pasch ;

cluster (Lo2) -> satisfying_Lower_Dimension_Axiom for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (Lo2) holds
b₁ is satisfying_Lower_Dimension_Axiom ;

cluster (Up2) -> satisfying_Upper_Dimension_Axiom for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (Up2) holds
b₁ is satisfying_Upper_Dimension_Axiom ;

cluster (Eu) -> satisfying_Euclid_Axiom for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (Eu) holds
b₁ is satisfying_Euclid_Axiom ;

cluster (Co) -> satisfying_Continuity_Axiom for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (Co) holds
b₁ is satisfying_Continuity_Axiom ;

end;

registration

cluster satisfying_CongruenceSymmetry -> (RE) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_CongruenceSymmetry holds
b₁ is (RE) ;

cluster satisfying_CongruenceEquivalenceRelation -> (TE) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_CongruenceEquivalenceRelation holds
b₁ is (TE) ;

cluster satisfying_CongruenceIdentity -> (IE) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_CongruenceIdentity holds
b₁ is (IE) ;

cluster satisfying_SegmentConstruction -> (SC) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_SegmentConstruction holds
b₁ is (SC) ;

cluster satisfying_BetweennessIdentity -> (IB) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_BetweennessIdentity holds
b₁ is (IB) ;

cluster satisfying_Pasch -> (Pa) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_Pasch holds
b₁ is (Pa) ;

cluster satisfying_Lower_Dimension_Axiom -> (Lo2) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_Lower_Dimension_Axiom holds
b₁ is (Lo2) ;

cluster satisfying_Upper_Dimension_Axiom -> (Up2) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_Upper_Dimension_Axiom holds
b₁ is (Up2) ;

cluster satisfying_Euclid_Axiom -> (Eu) for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is satisfying_Euclid_Axiom holds
b₁ is (Eu) ;

cluster non empty satisfying_Continuity_Axiom -> non empty (Co) for TarskiGeometryStruct ;

coherence
for b₁ being non empty TarskiGeometryStruct st b₁ is satisfying_Continuity_Axiom holds
b₁ is (Co) by ThMak1;

end;

registration

cluster (RE) (TE) for TarskiGeometryStruct ;

existence
ex b₁ being TarskiGeometryStruct st
( b₁ is (RE) & b₁ is (TE) )

proof end;

end;

theorem ThMak2: :: GTARSKI3:129

for S being (RE) (TE) TarskiGeometryStruct holds
( S is satisfying_SAS iff S is (FS) )

proof end;

registration

cluster (RE) (TE) (FS) -> satisfying_SAS (RE) (TE) for TarskiGeometryStruct ;

coherence
for b₁ being (RE) (TE) TarskiGeometryStruct st b₁ is (FS) holds
b₁ is satisfying_SAS by ThMak2;

end;

registration

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation (RE) (TE) (FS) for TarskiGeometryStruct ;

existence
ex b₁ being (RE) (TE) TarskiGeometryStruct st b₁ is (FS)

proof end;

end;

:: Makarios: Lemma 6

theorem ThMak3: :: GTARSKI3:130

for S being TarskiGeometryStruct st S is (RE) & S is (TE) holds
( S is (FS) iff S is (FS') )

proof end;

theorem :: GTARSKI3:131

for S being (RE) (TE) TarskiGeometryStruct holds
( S is (FS) iff S is (FS') ) by ThMak3;

registration

cluster (RE) (TE) (FS') -> (RE) (TE) (FS) for TarskiGeometryStruct ;

coherence
for b₁ being (RE) (TE) TarskiGeometryStruct st b₁ is (FS') holds
b₁ is (FS) by ThMak3;

end;

registration

cluster (TE) (SC) for TarskiGeometryStruct ;

existence
ex b₁ being TarskiGeometryStruct st
( b₁ is (TE) & b₁ is (SC) )

proof end;

end;

registration

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation (RE) (TE) (FS') for TarskiGeometryStruct ;

existence
ex b₁ being (RE) (TE) TarskiGeometryStruct st b₁ is (FS')

proof end;

end;

registration

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS satisfying_SST_A5 (RE) (TE) (SC) (FS) (FS') for TarskiGeometryStruct ;

existence
ex b₁ being (RE) (TE) (FS') TarskiGeometryStruct st b₁ is (SC)

proof end;

end;

theorem :: GTARSKI3:132

for S being (TE) (SC) TarskiGeometryStruct
for a, b being POINT of S holds a,b equiv a,b by Satz2p1bis;

theorem :: GTARSKI3:133

for S being (IE) (SC) TarskiGeometryStruct
for a, b being POINT of S holds between a,b,b by Satz3p1;

theorem :: GTARSKI3:134

for S being (TE) (SC) TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b equiv c,d holds
c,d equiv a,b by Satz2p2bis;

theorem ThMak4: :: GTARSKI3:135

for S being (TE) (SC) (FS') TarskiGeometryStruct
for a, b, c, d, e, f being POINT of S st a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f holds
f,c equiv e,f

proof end;

definition

let S be TarskiGeometryStruct ;

attr S is (RE') means :: GTARSKI3:def 27
for a, b, c, d being POINT of S st a <> b & between b,a,c holds
d,c equiv c,d;

end;

:: deftheorem defines (RE') GTARSKI3:def 27 :
for S being TarskiGeometryStruct holds
( S is (RE') iff for a, b, c, d being POINT of S st a <> b & between b,a,c holds
d,c equiv c,d );

theorem ThMak5: :: GTARSKI3:136

for S being (TE) (SC) (FS') TarskiGeometryStruct holds S is (RE')

proof end;

registration

cluster (TE) (SC) (FS') -> (RE') for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (TE) & b₁ is (SC) & b₁ is (FS') holds
b₁ is (RE') by ThMak5;

end;

registration

cluster satisfying_CongruenceIdentity (IE) (RE') for TarskiGeometryStruct ;

existence
ex b₁ being (IE) TarskiGeometryStruct st b₁ is (RE')

proof end;

end;

registration

cluster satisfying_CongruenceIdentity (IE) (SC) (RE') for TarskiGeometryStruct ;

existence
ex b₁ being (IE) (RE') TarskiGeometryStruct st b₁ is (SC)

proof end;

end;

registration

cluster non empty trivial satisfying_CongruenceIdentity (IE) for TarskiGeometryStruct ;

existence
ex b₁ being non empty (IE) TarskiGeometryStruct st b₁ is trivial

proof end;

end;

registration

cluster non empty trivial satisfying_CongruenceIdentity satisfying_SegmentConstruction (IE) (SC) for TarskiGeometryStruct ;

existence
ex b₁ being non empty (IE) (SC) TarskiGeometryStruct st b₁ is trivial

proof end;

end;

theorem :: GTARSKI3:137

for S being non empty trivial (IE) (SC) TarskiGeometryStruct holds S is (RE)

proof end;

registration

cluster non empty satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction (TE) (IE) (SC) (RE') for TarskiGeometryStruct ;

existence
ex b₁ being non empty (TE) (IE) (SC) TarskiGeometryStruct st b₁ is (RE')

proof end;

end;

theorem ThMak6: :: GTARSKI3:138

for S being non empty (TE) (IE) (SC) (RE') TarskiGeometryStruct holds S is (RE)

proof end;

registration

cluster non empty satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction (TE) (IE) (SC) (FS') for TarskiGeometryStruct ;

existence
ex b₁ being non empty (TE) (IE) (SC) TarskiGeometryStruct st b₁ is (FS')

proof end;

end;

theorem :: GTARSKI3:139

for S being non empty (TE) (IE) (SC) (FS') TarskiGeometryStruct holds S is (RE) by ThMak6;

theorem ThMak7: :: GTARSKI3:140

for S being non empty (TE) (IE) (SC) (FS') TarskiGeometryStruct holds S is (FS)

proof end;

:: Main results

registration

cluster (RE) (TE) (FS) -> (FS') for TarskiGeometryStruct ;

coherence
for b₁ being TarskiGeometryStruct st b₁ is (RE) & b₁ is (TE) & b₁ is (FS) holds
b₁ is (FS') by ThMak3;

end;

registration

cluster non empty (TE) (IE) (SC) (FS') -> non empty (FS) for TarskiGeometryStruct ;

coherence
for b₁ being non empty TarskiGeometryStruct st b₁ is (TE) & b₁ is (IE) & b₁ is (SC) & b₁ is (FS') holds
b₁ is (FS) by ThMak7;

end;

registration

cluster non empty (TE) (IE) (SC) (FS') -> non empty (RE) for TarskiGeometryStruct ;

coherence
for b₁ being non empty TarskiGeometryStruct st b₁ is (TE) & b₁ is (IE) & b₁ is (SC) & b₁ is (FS') holds
b₁ is (RE) by ThMak6;

end;

registration

cluster non empty (TE) (IE) (SC) (FS') -> non empty satisfying_SAS for TarskiGeometryStruct ;

coherence
for b₁ being non empty TarskiGeometryStruct st b₁ is (TE) & b₁ is (IE) & b₁ is (SC) & b₁ is (FS') holds
b₁ is satisfying_SAS ;

end;

registration

cluster non empty (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) for TarskiGeometryStruct ;

existence
ex b₁ being non empty TarskiGeometryStruct st
( b₁ is (RE) & b₁ is (TE) & b₁ is (IE) & b₁ is (SC) & b₁ is (FS) & b₁ is (IB) & b₁ is (Pa) & b₁ is (Lo2) & b₁ is (Up2) & b₁ is (Eu) & b₁ is (Co) )

proof end;

end;

definition

mode Makarios_CE2 is non empty (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) TarskiGeometryStruct ;

end;

definition

mode Makarios_CE'2 is non empty (TE) (IE) (SC) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) (FS') TarskiGeometryStruct ;

end;

theorem :: GTARSKI3:141

for TP being Makarios_CE2 holds TP is Makarios_CE'2 ;

theorem :: GTARSKI3:142

for TP being Makarios_CE'2 holds TP is Makarios_CE2 ;

theorem :: GTARSKI3:143

for TP being Makarios_CE2 holds
( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;

theorem :: GTARSKI3:144

for TP being Makarios_CE'2 holds
( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;