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


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

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

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

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

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

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

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

:: WP: 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 b1 being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct st b1 is satisfying_SST_A5 holds
b1 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 b1 being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct st b1 is satisfying_SAS holds
b1 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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

:: WP: 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 b1 being satisfying_Tarski-model TarskiGeometryStruct st b1 is satisfying_Lower_Dimension_Axiom
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

:: WP: 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 } ;

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

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

:: WP: 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 } ;

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

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

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

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

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

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

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

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

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

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

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

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

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

:: WP: 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 b1 being POINT of S st Middle p,a,b1 by Satz7p4existence;
uniqueness
for b1, b2 being POINT of S st Middle p,a,b1 & Middle p,a,b2 holds
b1 = b2 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, b4 being POINT of S holds
( b4 = reflection (a,p) iff Middle p,a,b4 );

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

:: WP: 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 b1 being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds b1 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 b1 being TarskiGeometryStruct st b1 is (RE) holds
b1 is satisfying_CongruenceSymmetry ;
cluster (TE) -> satisfying_CongruenceEquivalenceRelation for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (TE) holds
b1 is satisfying_CongruenceEquivalenceRelation ;
cluster (IE) -> satisfying_CongruenceIdentity for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (IE) holds
b1 is satisfying_CongruenceIdentity ;
cluster (SC) -> satisfying_SegmentConstruction for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (SC) holds
b1 is satisfying_SegmentConstruction ;
cluster (IB) -> satisfying_BetweennessIdentity for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (IB) holds
b1 is satisfying_BetweennessIdentity ;
cluster (Pa) -> satisfying_Pasch for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (Pa) holds
b1 is satisfying_Pasch ;
cluster (Lo2) -> satisfying_Lower_Dimension_Axiom for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (Lo2) holds
b1 is satisfying_Lower_Dimension_Axiom ;
cluster (Up2) -> satisfying_Upper_Dimension_Axiom for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (Up2) holds
b1 is satisfying_Upper_Dimension_Axiom ;
cluster (Eu) -> satisfying_Euclid_Axiom for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (Eu) holds
b1 is satisfying_Euclid_Axiom ;
cluster (Co) -> satisfying_Continuity_Axiom for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (Co) holds
b1 is satisfying_Continuity_Axiom ;
end;

registration
cluster satisfying_CongruenceSymmetry -> (RE) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_CongruenceSymmetry holds
b1 is (RE) ;
cluster satisfying_CongruenceEquivalenceRelation -> (TE) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_CongruenceEquivalenceRelation holds
b1 is (TE) ;
cluster satisfying_CongruenceIdentity -> (IE) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_CongruenceIdentity holds
b1 is (IE) ;
cluster satisfying_SegmentConstruction -> (SC) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_SegmentConstruction holds
b1 is (SC) ;
cluster satisfying_BetweennessIdentity -> (IB) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_BetweennessIdentity holds
b1 is (IB) ;
cluster satisfying_Pasch -> (Pa) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_Pasch holds
b1 is (Pa) ;
cluster satisfying_Lower_Dimension_Axiom -> (Lo2) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_Lower_Dimension_Axiom holds
b1 is (Lo2) ;
cluster satisfying_Upper_Dimension_Axiom -> (Up2) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_Upper_Dimension_Axiom holds
b1 is (Up2) ;
cluster satisfying_Euclid_Axiom -> (Eu) for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is satisfying_Euclid_Axiom holds
b1 is (Eu) ;
cluster non empty satisfying_Continuity_Axiom -> non empty (Co) for TarskiGeometryStruct ;
coherence
for b1 being non empty TarskiGeometryStruct st b1 is satisfying_Continuity_Axiom holds
b1 is (Co) by ThMak1;
end;

registration
cluster (RE) (TE) for TarskiGeometryStruct ;
existence
ex b1 being TarskiGeometryStruct st
( b1 is (RE) & b1 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 b1 being (RE) (TE) TarskiGeometryStruct st b1 is (FS) holds
b1 is satisfying_SAS by ThMak2;
end;

registration
cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation (RE) (TE) (FS) for TarskiGeometryStruct ;
existence
ex b1 being (RE) (TE) TarskiGeometryStruct st b1 is (FS)
proof end;
end;

:: WP: 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 b1 being (RE) (TE) TarskiGeometryStruct st b1 is (FS') holds
b1 is (FS) by ThMak3;
end;

registration
cluster (TE) (SC) for TarskiGeometryStruct ;
existence
ex b1 being TarskiGeometryStruct st
( b1 is (TE) & b1 is (SC) )
proof end;
end;

registration
cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation (RE) (TE) (FS') for TarskiGeometryStruct ;
existence
ex b1 being (RE) (TE) TarskiGeometryStruct st b1 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 b1 being (RE) (TE) (FS') TarskiGeometryStruct st b1 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 b1 being TarskiGeometryStruct st b1 is (TE) & b1 is (SC) & b1 is (FS') holds
b1 is (RE') by ThMak5;
end;

registration
cluster satisfying_CongruenceIdentity (IE) (RE') for TarskiGeometryStruct ;
existence
ex b1 being (IE) TarskiGeometryStruct st b1 is (RE')
proof end;
end;

registration
cluster satisfying_CongruenceIdentity (IE) (SC) (RE') for TarskiGeometryStruct ;
existence
ex b1 being (IE) (RE') TarskiGeometryStruct st b1 is (SC)
proof end;
end;

registration
cluster non empty trivial satisfying_CongruenceIdentity (IE) for TarskiGeometryStruct ;
existence
ex b1 being non empty (IE) TarskiGeometryStruct st b1 is trivial
proof end;
end;

registration
cluster non empty trivial satisfying_CongruenceIdentity satisfying_SegmentConstruction (IE) (SC) for TarskiGeometryStruct ;
existence
ex b1 being non empty (IE) (SC) TarskiGeometryStruct st b1 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 b1 being non empty (TE) (IE) (SC) TarskiGeometryStruct st b1 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 b1 being non empty (TE) (IE) (SC) TarskiGeometryStruct st b1 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;

:: WP: Main results
registration
cluster (RE) (TE) (FS) -> (FS') for TarskiGeometryStruct ;
coherence
for b1 being TarskiGeometryStruct st b1 is (RE) & b1 is (TE) & b1 is (FS) holds
b1 is (FS') by ThMak3;
end;

registration
cluster non empty (TE) (IE) (SC) (FS') -> non empty (FS) for TarskiGeometryStruct ;
coherence
for b1 being non empty TarskiGeometryStruct st b1 is (TE) & b1 is (IE) & b1 is (SC) & b1 is (FS') holds
b1 is (FS) by ThMak7;
end;

registration
cluster non empty (TE) (IE) (SC) (FS') -> non empty (RE) for TarskiGeometryStruct ;
coherence
for b1 being non empty TarskiGeometryStruct st b1 is (TE) & b1 is (IE) & b1 is (SC) & b1 is (FS') holds
b1 is (RE) by ThMak6;
end;

registration
cluster non empty (TE) (IE) (SC) (FS') -> non empty satisfying_SAS for TarskiGeometryStruct ;
coherence
for b1 being non empty TarskiGeometryStruct st b1 is (TE) & b1 is (IE) & b1 is (SC) & b1 is (FS') holds
b1 is satisfying_SAS ;
end;

registration
cluster non empty (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) for TarskiGeometryStruct ;
existence
ex b1 being non empty TarskiGeometryStruct st
( b1 is (RE) & b1 is (TE) & b1 is (IE) & b1 is (SC) & b1 is (FS) & b1 is (IB) & b1 is (Pa) & b1 is (Lo2) & b1 is (Up2) & b1 is (Eu) & b1 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 ) ;