:: {T}arski Geometry Axioms -- Part {III} :: by Roland Coghetto and Adam Grabowski :: :: Received November 29, 2017 :: Copyright (c) 2017-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies INCSP_1, GTARSKI1, GTARSKI2, GTARSKI3, ZFMISC_1, XXREAL_0, PROB_1, XBOOLE_0, TARSKI, SUBSET_1, STRUCT_0; notations GTARSKI1, GTARSKI2, TARSKI, ZFMISC_1, XBOOLE_0, STRUCT_0; constructors GTARSKI2; registrations GTARSKI1, GTARSKI2, STRUCT_0, ORDINAL1; requirements BOOLE, NUMERALS, SUBSET; begin :: Congruence properties reserve S for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct, a,b,c,d,e,f for POINT of S; ::\$N 2.1 Satz theorem :: GTARSKI3:1 ::EquivReflexive ::GTARSKI1:10 a,b equiv a,b; ::\$N 2.1 Satz bis theorem :: GTARSKI3:2 for S being satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct for a,b being POINT of S holds a,b equiv a,b; ::\$N 2.2 Satz theorem :: GTARSKI3:3 ::GTARSKI1:11 ::EquivSymmetric a,b equiv c,d implies c,d equiv a,b; ::\$N 2.2 Satz bis theorem :: 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; ::\$N 2.3 Satz theorem :: GTARSKI3:5 ::GTARSKI1:12 ::EquivTransitive a,b equiv c,d & c,d equiv e,f implies a,b equiv e,f; ::\$N 2.4 Satz theorem :: GTARSKI3:6 a,b equiv c,d implies b,a equiv c,d; ::\$N 2.5 Satz theorem :: GTARSKI3:7 a,b equiv c,d implies a,b equiv d,c; ::\$N 2.8 Satz theorem :: GTARSKI3:8 ::GTARSKI1:13 ::Baaa_2 for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct for a,b being POINT of S holds a,a equiv b,b; 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; theorem :: GTARSKI3:9 S is satisfying_SAS iff S is satisfying_SST_A5; registration cluster satisfying_SST_A5 -> satisfying_SAS for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; end; registration cluster satisfying_SAS -> satisfying_SST_A5 for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; end; definition let S be TarskiGeometryStruct; let a,b,c,d,a9,b9,c9,d9 being 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; theorem :: 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; reserve S for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct, q,a,b,c,a9,b9,c9,x1,x2 for POINT of S; ::\$N 2.11 Satz theorem :: GTARSKI3:11 ::GTARSKI1:24 between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 implies a,c equiv a9,c9; ::\$N 2.12 Satz theorem :: GTARSKI3:12 ::GTARSKI1:26 q <> a implies (for x1,x2 st between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c holds x1 = x2); begin :: Between properties ::\$N 3.1 Satz theorem :: GTARSKI3:13 ::Bqaa for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct for a,b being POINT of S holds between a,b,b; reserve S for satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct, a,b,c,d for POINT of S; ::\$N 3.2 Satz theorem :: GTARSKI3:14 between a,b,c implies between c,b,a; ::\$N 3.3 Satz theorem :: GTARSKI3:15 ::Baaa_1 between a,a,b; ::\$N 3.4 Satz theorem :: 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; reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d for POINT of S; ::\$N 3.5 Satz theorem :: GTARSKI3:17 between a,b,d & between b,c,d implies between a,b,c & between a,c,d; ::\$N 3.6 Satz theorem :: GTARSKI3:18 between a,b,c & between a,c,d implies between b,c,d & between a,b,d; ::\$N 3.7 Satz theorem :: GTARSKI3:19 between a,b,c & between b,c,d & b <> c implies between a,c,d & between a,b,d; ::\$N 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; ::\$N 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; reserve S for satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct, a,b,c,d,e for POINT of S; ::\$N 3.9 Satz (n = 3) theorem :: GTARSKI3:20 between a,b,c implies between c,b,a; ::\$N 3.9 Satz (n = 4) theorem :: GTARSKI3:21 between4 a,b,c,d implies between4 d,c,b,a; ::\$N 3.9 Satz (n = 5) theorem :: GTARSKI3:22 between5 a,b,c,d,e implies between5 e,d,c,b,a; ::\$N 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; ::\$N 3.10 Satz (n = 5) theorem :: GTARSKI3:24 between5 a,b,c,d,e implies 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; reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,p for POINT of S; ::\$N 3.11 Satz (n = 3, l = 1) theorem :: GTARSKI3:25 between a,b,c & between a,p,b implies between4 a,p,b,c; ::\$N 3.11 Satz (n = 3, l = 2) theorem :: GTARSKI3:26 between a,b,c & between b,p,c implies between4 a,b,p,c; ::\$N 3.11 Satz (n = 3, l = 1) theorem :: GTARSKI3:27 between4 a,b,c,d & between a,p,b implies between5 a,p,b,c,d; ::\$N 3.11 Satz (n = 3, l = 2) theorem :: GTARSKI3:28 between4 a,b,c,d & between b,p,c implies between5 a,b,p,c,d; ::\$N 3.11 Satz (n = 3, l = 3) theorem :: GTARSKI3:29 between4 a,b,c,d & between c,p,d implies between5 a,b,c,p,d; ::\$N 3.12 Satz (n = 3, l = 1) theorem :: GTARSKI3:30 between a,b,c & between a,c,p implies between4 a,b,c,p & (a <> c implies between4 a,b,c,p); ::\$N 3.12 Satz (n = 3, l = 2) theorem :: GTARSKI3:31 between a,b,c & between b,c,p implies between b,c,p & (b <> c implies between4 a,b,c,p); ::\$N 3.12 Satz (n = 4, l = 1) theorem :: GTARSKI3:32 between4 a,b,c,d & between a,d,p implies between5 a,b,c,d,p & (a <> d implies between5 a,b,c,d,p); ::\$N 3.12 Satz (n = 4, l = 2) theorem :: GTARSKI3:33 between4 a,b,c,d & between b,d,p implies between4 b,c,d,p & (b <> d implies between5 a,b,c,d,p); ::\$N 3.12 Satz (n = 4, l = 3) theorem :: GTARSKI3:34 between4 a,b,c,d & between c,d,p implies between c,d,p & (c <> d implies between5 a,b,c,d,p); registration cluster satisfying_Lower_Dimension_Axiom for satisfying_Tarski-model TarskiGeometryStruct; end; ::\$N 3.13 Satz theorem :: GTARSKI3:35 for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds 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; ::\$N 3.14 Satz theorem :: GTARSKI3:36 for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds for a,b being POINT of S ex c being POINT of S st between a,b,c & b <> c; ::\$N 3.15 Satz (n = 3) theorem :: GTARSKI3:37 for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds 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; ::\$N 3.15 Satz (n = 4) theorem :: GTARSKI3:38 for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds 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; ::\$N 3.15 Satz (n = 5) theorem :: GTARSKI3:39 for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds 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; ::\$N 3.17 Satz theorem :: 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; begin :: Collinearity 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; reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,a9,b9,c9,d9 for POINT of S; ::\$N 4.2 Satz theorem :: GTARSKI3:41 a,b,c,d IFS a9,b9,c9,d9 implies b,d equiv b9,d9; ::\$N 4.3 Satz theorem :: GTARSKI3:42 between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 implies a,b equiv a9,b9; ::\$N 4.5 Satz theorem :: GTARSKI3:43 between a,b,c & a,c equiv a9,c9 implies ex b9 st between a9,b9,c9 & a,b,c cong a9,b9,c9; ::\$N 4.6 Satz theorem :: GTARSKI3:44 between a,b,c & a,b,c cong a9,b9,c9 implies between a9,b9,c9; ::\$N 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; ::\$N 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; theorem :: 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; ::\$N 4.13 Satz theorem :: 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; theorem :: 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; theorem :: 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; reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,a9,b9,c9,d9,p,q for POINT of S; ::\$N 4.14 Satz theorem :: GTARSKI3:51 Collinear a,b,c & a,b equiv a9,b9 implies ex c9 being POINT of S st a,b,c cong a9,b9,c9; 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; ::\$N 4.16 Satz theorem :: GTARSKI3:52 a,b,c,d FS a9,b9,c9,d9 & a <> b implies c,d equiv c9,d9; ::\$N 4.17 Satz theorem :: GTARSKI3:53 a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q implies c,p equiv c,q; ::\$N 4.18 Satz theorem :: GTARSKI3:54 a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9; ::\$N 4.19 Satz theorem :: GTARSKI3:55 between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9; begin :: Between transitivity le reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,e,f,a9,b9,c9,d9 for POINT of S; ::\$N 5.1 Satz theorem :: GTARSKI3:56 ::GTARSKI1:37 a <> b & between a,b,c & between a,b,d implies between a,c,d or between a,d,c ; ::\$N 5.2 Satz theorem :: GTARSKI3:57 a <> b & between a,b,c & between a,b,d implies between b,c,d or between b,d,c ; ::\$N 5.3 Satz theorem :: GTARSKI3:58 between a,b,d & between a,c,d implies between a,b,c or between a,c,b; 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; ::\$N 5.5 Satz theorem :: GTARSKI3:59 a,b <= c,d iff (ex x being POINT of S st between a,b,x & a,x equiv c,d); ::\$N 5.6 Satz theorem :: GTARSKI3:60 a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 implies a9,b9 <= c9,d9; ::\$N 5.7 Satz theorem :: GTARSKI3:61 a,b <= a,b; ::\$N 5.8 Satz theorem :: GTARSKI3:62 a,b <= c,d & c,d <= e,f implies a,b <= e,f; ::\$N 5.9 Satz theorem :: GTARSKI3:63 a,b <= c,d & c,d <= a,b implies a,b equiv c,d; ::\$N 5.10 Satz theorem :: GTARSKI3:64 a,b <= c,d or c,d <= a,b; ::\$N 5.11 Satz theorem :: GTARSKI3:65 a,a <= b,c; ::\$N 5.12 Lemma 1 theorem :: GTARSKI3:66 for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct for a,b,c,d being POINT of S holds a,b <= c,d implies b,a <= c,d; ::\$N 5.12 Lemma 2 theorem :: GTARSKI3:67 a,b <= c,d implies a,b <= d,c; ::\$N 5.12 Lemma 3 theorem :: GTARSKI3:68 between a,b,c & a,c equiv a,b implies c = b; ::\$N METAMATH: endofsegidand theorem :: GTARSKI3:69 between a,c,b & a,b <= a,c implies b = c; ::\$N 5.12 Satz theorem :: GTARSKI3:70 Collinear a,b,c implies (between a,b,c iff (a,b <= a,c & b,c <= a,c)); begin :: Out lines 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; reserve p for POINT of S; ::\$N 6.2 Satz theorem :: GTARSKI3:71 a <> p & b <> p & c <> p & between a,p,c implies (between b,p,c iff p out a,b); ::\$N 6.3 Satz theorem :: GTARSKI3:72 p out a,b iff (a <> p & b <> p & (ex c st c <> p & between a,p,c & between b,p,c)); ::\$N 6.4 Satz theorem :: GTARSKI3:73 p out a,b iff (Collinear a,p,b & not between a,p,b); ::\$N 6.5 Satz theorem :: GTARSKI3:74 a <> p implies p out a,a; ::\$N 6.6 Satz theorem :: GTARSKI3:75 p out a,b implies p out b,a; ::\$N 6.7 Satz theorem :: GTARSKI3:76 p out a,b & p out b,c implies p out a,c; ::\$N METAMATH: segcon2 theorem :: GTARSKI3:77 ex x being POINT of S st (between p,a,x or between p,x,a) & p,x equiv b,c; reserve r for POINT of S; ::\$N 6.11 Satz a) theorem :: GTARSKI3:78 r <> a & b <> c implies ex x being POINT of S st (a out x,r & a,x equiv b,c); 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}; end; reserve x,y for POINT of S; ::\$N 6.11 Satz b) theorem :: GTARSKI3:79 r <> a & b <> c & (a out x,r & a,x equiv b,c) & (a out y,r & a,y equiv b,c) implies x = y; ::\$N 6.13 Satz theorem :: GTARSKI3:80 p out a,b implies (p,a <= p,b iff between p,a,b); ::\$N 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}; end; reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct; reserve p,q,r,s for POINT of S; ::\$N 6.15 Satz theorem :: GTARSKI3:81 p <> q & p <> r & between q,p,r implies Line(p,q) = halfline(p,q) \/ {p} \/ halfline(p,r); 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; ::\$N 6.16 Satz theorem :: GTARSKI3:82 :: GTARSKI1:45 p <> q & s <> p & s in Line(p,q) implies Line(p,q) = Line(p,s); reserve S for non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct, a,b,p,q for POINT of S; ::\$N 6.17 Satz theorem :: GTARSKI3:83 p in Line(p,q) & q in Line(p,q) & Line(p,q) = Line(q,p); reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct, A,B for Subset of S, a,b,c,p,q,r,s for POINT of S; theorem :: 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 :: GTARSKI3:85 for S being satisfying_Tarski-model non empty TarskiGeometryStruct for a,b,x,y being POINT of S st a,b equal_line x,y holds Line(a,b) = Line(x,y); theorem :: GTARSKI3:86 for S being satisfying_Tarski-model non empty 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; ::\$N 6.18 Satz theorem :: GTARSKI3:87 ::GTARSKI_1:46 A is_line & a <> b & a in A & b in A implies A = Line(a,b); ::\$N 6.19 Satz theorem :: GTARSKI3:88 a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B implies A = B; ::\$N 6.21 Satz theorem :: GTARSKI3:89 A is_line & B is_line & A <> B & a in A & a in B & b in A & b in B implies a = b; ::\$N 6.23 Satz theorem :: GTARSKI3:90 (ex p,q st p <> q) implies (Collinear a,b,c iff (ex A st A is_line & a in A & b in A & c in A)); ::\$N 6.24 Satz theorem :: GTARSKI3:91 for S being satisfying_A8 TarskiGeometryStruct ex a,b,c being POINT of S st not Collinear a,b,c; ::\$N 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; theorem :: 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; theorem :: 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; ::\$N 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; begin :: Midpoint definition let S be TarskiGeometryStruct; let a,b,m be POINT of S; pred Middle a,m,b means :: GTARSKI3:def 12 between a,m,b & m,a equiv m,b; end; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct, a,b,m for POINT of S; ::\$N 7.2 Satz theorem :: GTARSKI3:96 Middle a,m,b implies Middle b,m,a; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct, a,b,m for POINT of S; ::\$N 7.3 Satz theorem :: GTARSKI3:97 Middle a,m,a iff m = a; ::\$N 7.4 Existence theorem :: GTARSKI3:98 for p being POINT of S holds ex p9 being POINT of S st Middle p,a,p9; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct, a for POINT of S; ::\$N 7.4 Uniqueness theorem :: GTARSKI3:99 for p,p1,p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds p1 = p2; definition let S be satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct; let a,p be POINT of S; func reflection(a,p) -> POINT of S means :: GTARSKI3:def 13 Middle p,a,it; end; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct, a,p,p9 for POINT of S; ::\$N 7.6 Satz theorem :: GTARSKI3:100 reflection(a,p) = p9 iff Middle p,a,p9; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS satisfying_Pasch TarskiGeometryStruct, a,p,p9 for POINT of S; ::\$N 7.7 Satz theorem :: GTARSKI3:101 reflection(a,reflection(a,p)) = p; ::\$N 7.8 Satz theorem :: GTARSKI3:102 ex p st reflection(a,p) = p9; ::\$N 7.9 Satz theorem :: GTARSKI3:103 reflection(a,p) = reflection(a,p9) implies p = p9; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct, a,p for POINT of S; ::\$N 7.10 Satz theorem :: GTARSKI3:104 reflection(a,p) = p iff p = a; reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,m,p,p9,q,r,s for POINT of S; ::\$N 7.13 Satz theorem :: GTARSKI3:105 p,q equiv reflection(a,p),reflection(a,q); ::\$N 7.15 Satz theorem :: GTARSKI3:106 between p,q,r iff between reflection(a,p),reflection(a,q),reflection(a,r); ::\$N 7.16 Satz theorem :: GTARSKI3:107 p,q equiv r,s iff reflection(a,p),reflection(a,q) equiv reflection(a,r),reflection(a,s); ::\$N 7.17 Satz theorem :: GTARSKI3:108 Middle p,a,p9 & Middle p,b,p9 implies a = b; ::\$N 7.18 Satz theorem :: GTARSKI3:109 reflection(a,p) = reflection(b,p) implies a = b; ::\$N 7.19 Satz theorem :: GTARSKI3:110 reflection(b,reflection(a,p)) = reflection(a,reflection(b,p)) iff a = b; ::\$N 7.20 Satz theorem :: GTARSKI3:111 Collinear a,m,b & m,a equiv m,b implies a = b or Middle a,m,b; reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,p for POINT of S; ::\$N 7.21 Satz theorem :: GTARSKI3:112 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 implies Middle a,p,c & Middle b,p,d; reserve a1,a2,b1,b2,m1,m2 for POINT of S; ::\$N 7.22 Satz, part 1 theorem :: GTARSKI3:113 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 implies between m1,c,m2; ::\$N 7.22 Satz, part 2 theorem :: GTARSKI3:114 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 implies between m1,c,m2; ::\$N 7.22 Satz: Krippenlemma, (Gupta 1965, 3.45 Theorem) theorem :: GTARSKI3:115 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 implies between m1,c,m2; 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; ::\$N Krippenfigur theorem :: GTARSKI3:116 Krippenfigur a1,m1,b1,c,b2,m2,a2 implies between m1,c,m2; registration cluster non empty for satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct; end; reserve S for non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct, a,b,c,p,q,r for POINT of S; ::\$ 7.25 Satz theorem :: GTARSKI3:117 c,a equiv c,b implies ex x being POINT of S st Middle a,x,b; begin :: Note about Makarios's simplification of Tarski's axiom of geometry 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 holds between a,b,c or between b,c,a or 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; reserve S for TarskiGeometryStruct; theorem :: GTARSKI3:118 S is satisfying_CongruenceSymmetry iff S is (RE); theorem :: GTARSKI3:119 S is satisfying_CongruenceEquivalenceRelation iff S is (TE); theorem :: GTARSKI3:120 S is satisfying_CongruenceIdentity iff S is (IE); theorem :: GTARSKI3:121 S is satisfying_SegmentConstruction iff S is (SC); theorem :: GTARSKI3:122 S is satisfying_BetweennessIdentity iff S is (IB); theorem :: GTARSKI3:123 S is satisfying_Pasch iff S is (Pa); theorem :: GTARSKI3:124 S is satisfying_Lower_Dimension_Axiom iff S is (Lo2); theorem :: GTARSKI3:125 S is satisfying_Upper_Dimension_Axiom iff S is (Up2); theorem :: GTARSKI3:126 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); theorem :: GTARSKI3:128 for S being non empty TarskiGeometryStruct holds S is satisfying_Continuity_Axiom iff S is (Co); registration cluster (RE) -> satisfying_CongruenceSymmetry for TarskiGeometryStruct; cluster (TE) -> satisfying_CongruenceEquivalenceRelation for TarskiGeometryStruct; cluster (IE) -> satisfying_CongruenceIdentity for TarskiGeometryStruct; cluster (SC) -> satisfying_SegmentConstruction for TarskiGeometryStruct; cluster (IB) -> satisfying_BetweennessIdentity for TarskiGeometryStruct; cluster (Pa) -> satisfying_Pasch for TarskiGeometryStruct; cluster (Lo2) -> satisfying_Lower_Dimension_Axiom for TarskiGeometryStruct; cluster (Up2) -> satisfying_Upper_Dimension_Axiom for TarskiGeometryStruct; cluster (Eu) -> satisfying_Euclid_Axiom for TarskiGeometryStruct; cluster (Co) -> satisfying_Continuity_Axiom for TarskiGeometryStruct; end; registration cluster satisfying_CongruenceSymmetry -> (RE) for TarskiGeometryStruct; cluster satisfying_CongruenceEquivalenceRelation -> (TE) for TarskiGeometryStruct; cluster satisfying_CongruenceIdentity -> (IE) for TarskiGeometryStruct; cluster satisfying_SegmentConstruction -> (SC) for TarskiGeometryStruct; cluster satisfying_BetweennessIdentity -> (IB) for TarskiGeometryStruct; cluster satisfying_Pasch -> (Pa) for TarskiGeometryStruct; cluster satisfying_Lower_Dimension_Axiom -> (Lo2) for TarskiGeometryStruct; cluster satisfying_Upper_Dimension_Axiom -> (Up2) for TarskiGeometryStruct; cluster satisfying_Euclid_Axiom -> (Eu) for TarskiGeometryStruct; cluster satisfying_Continuity_Axiom -> (Co) for non empty TarskiGeometryStruct; end; registration cluster (RE) (TE) for TarskiGeometryStruct; end; theorem :: GTARSKI3:129 for S being (RE) (TE) TarskiGeometryStruct holds S is satisfying_SAS iff S is (FS); registration cluster (FS) -> satisfying_SAS for (RE) (TE) TarskiGeometryStruct; end; registration cluster (FS) for (RE) (TE) TarskiGeometryStruct; end; reserve S for TarskiGeometryStruct; ::\$N Makarios: Lemma 6 theorem :: GTARSKI3:130 for S being TarskiGeometryStruct st S is (RE) & S is (TE) holds (S is (FS) iff S is (FS')); theorem :: GTARSKI3:131 for S being (RE) (TE) TarskiGeometryStruct holds S is (FS) iff S is (FS'); registration cluster (FS') -> (FS) for (RE) (TE) TarskiGeometryStruct; end; registration cluster (TE) (SC) for TarskiGeometryStruct; end; registration cluster (FS') for (RE) (TE) TarskiGeometryStruct; end; registration cluster (SC) for (RE) (TE) (FS') TarskiGeometryStruct; end; theorem :: GTARSKI3:132 for S being (TE) (SC) TarskiGeometryStruct holds for a,b being POINT of S holds a,b equiv a,b; theorem :: GTARSKI3:133 for S being (IE) (SC) TarskiGeometryStruct holds for a,b being POINT of S holds between a,b,b; theorem :: GTARSKI3:134 for S being (TE) (SC) TarskiGeometryStruct holds for a,b,c,d being POINT of S st a,b equiv c,d holds c,d equiv a,b; theorem :: GTARSKI3:135 for S being (TE) (SC) (FS') TarskiGeometryStruct holds (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); 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; theorem :: GTARSKI3:136 for S being (TE) (SC) (FS') TarskiGeometryStruct holds S is (RE'); registration cluster (TE) (SC) (FS') -> (RE') for TarskiGeometryStruct; end; registration cluster (RE') for (IE) TarskiGeometryStruct; end; registration cluster (SC) for (RE') (IE) TarskiGeometryStruct; end; registration cluster trivial for (IE) non empty TarskiGeometryStruct; end; registration cluster trivial for (IE) (SC) non empty TarskiGeometryStruct; end; theorem :: GTARSKI3:137 for S being trivial (IE) (SC) non empty TarskiGeometryStruct holds S is (RE); registration cluster (RE') for (TE) (IE) (SC) non empty TarskiGeometryStruct; end; theorem :: GTARSKI3:138 for S being (RE') (TE) (IE) (SC) non empty TarskiGeometryStruct holds S is (RE); registration cluster (FS') for (TE) (IE) (SC) non empty TarskiGeometryStruct; end; theorem :: GTARSKI3:139 for S being (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds S is (RE); theorem :: GTARSKI3:140 for S being (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds S is (FS); begin :: Main results and Corollaries ::\$N Main results registration cluster (RE) (TE) (FS) -> (FS') for TarskiGeometryStruct; end; registration cluster (TE) (IE) (SC) (FS') -> (FS) for non empty TarskiGeometryStruct; end; registration cluster (TE) (IE) (SC) (FS') -> (RE) for non empty TarskiGeometryStruct; end; registration cluster (TE) (IE) (SC) (FS') -> satisfying_SAS for non empty TarskiGeometryStruct; end; registration cluster (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) for non empty TarskiGeometryStruct; end; definition mode Makarios_CE2 is (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) non empty TarskiGeometryStruct; end; definition mode Makarios_CE'2 is (TE) (IE) (SC) (FS') (IB) (Pa) (Lo2) (Up2) (Eu) (Co) non empty 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;