:: {T}arski Geometry Axioms -- Part {III} :: by Roland Coghetto and Adam Grabowski :: :: Received November 29, 2017 :: Copyright (c) 2017 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; definitions TARSKI, XBOOLE_0; expansions XBOOLE_0, ZFMISC_1, GTARSKI1, GTARSKI2; theorems GTARSKI1, GTARSKI2, TARSKI, XBOOLE_0, ZFMISC_1, XBOOLE_1; 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 Satz2p1: ::EquivReflexive ::GTARSKI1:10 a,b equiv a,b proof b,a equiv a,b by GTARSKI1:def 5; hence thesis by GTARSKI1:def 6; end; ::\$N 2.1 Satz bis theorem Satz2p1bis: for S being satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct for a,b being POINT of S holds a,b equiv a,b proof let S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct; let a,b be POINT of S; ex c be POINT of S st between a,a,c & a,c equiv a,b by GTARSKI1:def 8; hence thesis by GTARSKI1:def 6; end; ::\$N 2.2 Satz theorem Satz2p2: ::GTARSKI1:11 ::EquivSymmetric a,b equiv c,d implies c,d equiv a,b proof assume A1: a,b equiv c,d; a,b equiv a,b by Satz2p1; hence thesis by A1,GTARSKI1:def 6; end; ::\$N 2.2 Satz bis theorem Satz2p2bis: 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 let S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct; let a,b,c,d be POINT of S; assume A1: a,b equiv c,d; a,b equiv a,b by Satz2p1bis; hence thesis by A1,GTARSKI1:def 6; end; ::\$N 2.3 Satz theorem Satz2p3: ::GTARSKI1:12 ::EquivTransitive a,b equiv c,d & c,d equiv e,f implies a,b equiv e,f proof assume A1: a,b equiv c,d & c,d equiv e,f; then c,d equiv a,b by Satz2p2; hence thesis by A1,GTARSKI1:def 6; end; ::\$N 2.4 Satz theorem Satz2p4: a,b equiv c,d implies b,a equiv c,d proof assume A1: a,b equiv c,d; b,a equiv a,b by GTARSKI1:def 5; hence thesis by A1,Satz2p3; end; ::\$N 2.5 Satz theorem Satz2p5: a,b equiv c,d implies a,b equiv d,c proof assume A1: a,b equiv c,d; c,d equiv d,c by GTARSKI1:def 5; hence thesis by A1,Satz2p3; end; ::\$N 2.8 Satz theorem Satz2p8: ::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 proof let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct; let a,b be POINT of S; ex c be POINT of S st between a,a,c & a,c equiv b,b by GTARSKI1:def 8; hence thesis by GTARSKI1:def 7; end; definition let S be TarskiGeometryStruct; attr S is satisfying_SST_A5 means 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 EQUIV1: S is satisfying_SAS iff S is satisfying_SST_A5 proof thus S is satisfying_SAS implies S is satisfying_SST_A5 proof assume A1: S is satisfying_SAS; now let a,b,c,d,a9,b9,c9,d9 be POINT of S; assume A2: 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; then a,b,d cong a9,b9,d9; then d,c equiv d9,c9 by A1,A2; then c,d equiv d9,c9 by Satz2p4; hence c,d equiv c9,d9 by Satz2p5; end; hence thesis; end; thus S is satisfying_SST_A5 implies S is satisfying_SAS proof assume A3: S is satisfying_SST_A5; now let a, b, c, x, a1, b1, c1, x1 be POINT of S; assume a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1; then x,c equiv x1,c1 by A3; then c,x equiv x1,c1 by Satz2p4; hence c,x equiv c1,x1 by Satz2p5; end; hence thesis; end; end; registration cluster satisfying_SST_A5 -> satisfying_SAS for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; coherence by EQUIV1; end; registration cluster satisfying_SAS -> satisfying_SST_A5 for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; coherence by EQUIV1; 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 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 Axiom5AFS: 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 let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS TarskiGeometryStruct; let a,b,c,d,a9,b9,c9,d9 be POINT of S; assume A1: a,b,c,d AFS a9,b9,c9,d9 & a <> b; S is satisfying_SST_A5; hence thesis by A1; end; 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 Satz2p11: ::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 proof assume A1: between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9; A2: S is satisfying_SST_A5; b,a equiv a9,b9 by A1,Satz2p4; then A3: a,b,c,a AFS a9,b9,c9,a9 by A1,Satz2p5,Satz2p8; per cases; suppose a = b; hence thesis by A1,Satz2p2,GTARSKI1:def 7; end; suppose a <> b; then c,a equiv c9,a9 by A3,A2; then a,c equiv c9,a9 by Satz2p4; hence thesis by Satz2p5; end; end; ::\$N 2.12 Satz theorem Satz2p12: ::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) proof assume A1: q <> a; A2: S is satisfying_SST_A5; hereby let x1,x2; assume A3: between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c; then b,c equiv a,x2 by Satz2p2; then A4: a,x1 equiv a,x2 by A3,Satz2p3; q,a equiv q,a & a,x1 equiv a,x1 by Satz2p1; then q,a,x1,x1 AFS q,a,x1,x2 by A3,A4,Satz2p11; then x1,x1 equiv x1,x2 by A1,A2; hence x1 = x2 by Satz2p2,GTARSKI1:def 7; end; end; begin :: Between properties ::\$N 3.1 Satz theorem Satz3p1: ::Bqaa for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct for a,b being POINT of S holds between a,b,b proof let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct; let a,b be POINT of S; ex x be POINT of S st between a,b,x & b,x equiv b,b by GTARSKI1:def 8; hence thesis by GTARSKI1:def 7; end; 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 Satz3p2: between a,b,c implies between c,b,a proof assume A1: between a,b,c; between b,c,c by Satz3p1; then ex x be POINT of S st between b,x,b & between c,x,a by A1,GTARSKI1:def 11; hence thesis by GTARSKI1:def 10; end; ::\$N 3.3 Satz theorem ::Baaa_1 between a,a,b by Satz3p1,Satz3p2; ::\$N 3.4 Satz theorem Satz3p4: 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 let S be satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct; let a,b,c be POINT of S; assume between a,b,c & between b,a,c; then consider x be POINT of S such that A1: between b,x,b & between a,x,a by GTARSKI1:def 11; x = a & x = b by A1,GTARSKI1:def 10; hence thesis; end; Satz3p5p1: between a,b,d & between b,c,d implies between a,b,c proof assume between a,b,d & between b,c,d; then consider x be POINT of S such that A1: between b,x,b & between c,x,a by GTARSKI1:def 11; b = x by A1,GTARSKI1:def 10; hence thesis by A1,Satz3p2; end; Satz3p6p1: between a,b,c & between a,c,d implies between b,c,d proof assume between a,b,c & between a,c,d; then between c,b,a & between d,c,a by Satz3p2; then between d,c,b by Satz3p5p1; hence thesis by Satz3p2; end; reserve S for satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d for POINT of S; Satz3p7p1: between a,b,c & between b,c,d & b <> c implies between a,c,d proof assume A1: between a,b,c & between b,c,d & b <> c; consider x be POINT of S such that A2: between a,c,x & c,x equiv c,d by GTARSKI1:def 8; A3: between b,c,x by A1,A2,Satz3p6p1; c,d equiv c,d by Satz2p1; hence thesis by A1,A2,A3,Satz2p12; end; Satz3p5p2: between a,b,d & between b,c,d implies between a,c,d proof assume A1: between a,b,d & between b,c,d; then between a,b,c by Satz3p5p1; hence thesis by A1,Satz3p7p1; end; Satz3p6p2: between a,b,c & between a,c,d implies between a,b,d proof assume between a,b,c & between a,c,d; then between c,b,a & between d,c,a by Satz3p2; then between d,b,a by Satz3p5p2; hence thesis by Satz3p2; end; Satz3p7p2: between a,b,c & between b,c,d & b <> c implies between a,b,d proof assume A1: between a,b,c & between b,c,d & b <> c; then between c,b,a & between d,c,b by Satz3p2; then between d,b,a by A1,Satz3p7p1; hence thesis by Satz3p2; end; ::\$N 3.5 Satz theorem between a,b,d & between b,c,d implies between a,b,c & between a,c,d by Satz3p5p1,Satz3p5p2; ::\$N 3.6 Satz theorem between a,b,c & between a,c,d implies between b,c,d & between a,b,d by Satz3p6p1,Satz3p6p2; ::\$N 3.7 Satz theorem between a,b,c & between b,c,d & b <> c implies between a,c,d & between a,b,d by Satz3p7p1,Satz3p7p2; ::\$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 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 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 between a,b,c implies between c,b,a by Satz3p2; ::\$N 3.9 Satz (n = 4) theorem between4 a,b,c,d implies between4 d,c,b,a by Satz3p2; ::\$N 3.9 Satz (n = 5) theorem between5 a,b,c,d,e implies between5 e,d,c,b,a by Satz3p2; ::\$N 3.10 Satz (n = 4) theorem 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 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 between a,b,c & between a,p,b implies between4 a,p,b,c by Satz3p6p1,Satz3p6p2; ::\$N 3.11 Satz (n = 3, l = 2) theorem Satz3p11p3pb: between a,b,c & between b,p,c implies between4 a,b,p,c by Satz3p5p1,Satz3p5p2; ::\$N 3.11 Satz (n = 3, l = 1) theorem between4 a,b,c,d & between a,p,b implies between5 a,p,b,c,d proof assume A1: between4 a,b,c,d & between a,p,b; then between a,p,b & between a,p,c & between a,p,d & between p,b,c & between p,b,d by Satz3p6p1,Satz3p6p2; hence thesis by A1,Satz3p5p2; end; ::\$N 3.11 Satz (n = 3, l = 2) theorem Satz3p11p4pb: between4 a,b,c,d & between b,p,c implies between5 a,b,p,c,d proof assume A1: between4 a,b,c,d & between b,p,c; then between a,b,p & between p,c,d & between b,p,c & between b,p,d & between a,p,c by Satz3p5p1,Satz3p5p2,Satz3p6p1,Satz3p6p2; hence thesis by A1,Satz3p5p2; end; ::\$N 3.11 Satz (n = 3, l = 3) theorem between4 a,b,c,d & between c,p,d implies between5 a,b,c,p,d proof assume A1: between4 a,b,c,d & between c,p,d; then between a,p,d & between a,c,p & between b,c,p & between b,p,d & between c,p,d by Satz3p5p1,Satz3p5p2; hence thesis by A1,Satz3p5p1; end; ::\$N 3.12 Satz (n = 3, l = 1) theorem between a,b,c & between a,c,p implies between4 a,b,c,p & (a <> c implies between4 a,b,c,p) by Satz3p6p1,Satz3p6p2; ::\$N 3.12 Satz (n = 3, l = 2) theorem between a,b,c & between b,c,p implies between b,c,p & (b <> c implies between4 a,b,c,p) by Satz3p7p1,Satz3p7p2; ::\$N 3.12 Satz (n = 4, l = 1) theorem 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) proof assume A1: between4 a,b,c,d & between a,d,p; then between a,b,p & between a,c,p & between a,d,p & between c,d,p & between b,d,p by Satz3p6p1,Satz3p6p2; hence thesis by A1,Satz3p6p1; end; ::\$N 3.12 Satz (n = 4, l = 2) theorem between4 a,b,c,d & between b,d,p implies between4 b,c,d,p & (b <> d implies between5 a,b,c,d,p) proof assume A1: between4 a,b,c,d & between b,d,p; hence between4 b,c,d,p by Satz3p6p1,Satz3p6p2; thus b <> d implies between5 a,b,c,d,p proof assume b <> d; then between a,b,p & between a,d,p by A1,Satz3p7p1,Satz3p7p2; hence thesis by A1,Satz3p6p1,Satz3p6p2; end; end; ::\$N 3.12 Satz (n = 4, l = 3) theorem between4 a,b,c,d & between c,d,p implies between c,d,p & (c <> d implies between5 a,b,c,d,p) proof assume A1: between4 a,b,c,d & between c,d,p; hence between c,d,p; hereby assume c <> d; then between b,c,p & between b,d,p & between a,c,p & between a,d,p by A1,Satz3p7p1,Satz3p7p2; hence between5 a,b,c,d,p by A1,Satz3p7p2; end; end; registration cluster satisfying_Lower_Dimension_Axiom for satisfying_Tarski-model TarskiGeometryStruct; existence proof take TarskiEuclid2Space; thus thesis; end; end; ::\$N 3.13 Satz theorem Satz3p13: 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 proof let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct; consider a,b,c be POINT of S such that A1: not between a,b,c & not between b,c,a & not between c,a,b by GTARSKI2:def 7; take a,b,c; thus thesis by A1,Satz3p1; end; ::\$N 3.14 Satz theorem Satz3p14: 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 proof let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct; let a,b be POINT of S; consider u,v,w be POINT of S such that A1: not between u,v,w & not between v,w,u & not between w,u,v & u <> v & v <> w & w <> u by Satz3p13; consider x be POINT of S such that A2: between a,b,x & b,x equiv u,v by GTARSKI1:def 8; b <> x by A1,A2,Satz2p2,GTARSKI1:def 7; hence thesis by A2; end; ::\$N 3.15 Satz (n = 3) theorem Satz3p15p3: 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 proof let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct; let a1,a2 be POINT of S; assume A1: a1 <> a2; consider a3 be POINT of S such that A2: between a1,a2,a3 & a2 <> a3 by Satz3p14; a1 <> a3 by A2,GTARSKI1:def 10; hence thesis by A1,A2,ZFMISC_1:def 5; end; ::\$N 3.15 Satz (n = 4) theorem Satz3p15p4: 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 proof let S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct; let a1,a2 be POINT of S; assume a1 <> a2; then consider a3 be POINT of S such that A1: between a1,a2,a3 & a1,a2,a3 are_mutually_distinct by Satz3p15p3; consider a4 be POINT of S such that A2: between a2,a3,a4 & a2,a3,a4 are_mutually_distinct by A1,Satz3p15p3; take a3,a4; thus between4 a1,a2,a3,a4 by A1,A2,Satz3p7p1,Satz3p7p2; thus a1,a2,a3,a4 are_mutually_distinct by A1,Satz3p7p1,GTARSKI1:def 10,A2; end; ::\$N 3.15 Satz (n = 5) theorem 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 proof let S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct; let a1,a2 be POINT of S; assume a1 <> a2; then consider a3,a4 be POINT of S such that A1: between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct by Satz3p15p4; consider a5 be POINT of S such that A2: between a3,a4,a5 & a3,a4,a5 are_mutually_distinct by A1,Satz3p15p3; take a3,a4,a5; between a1,a3,a5 & between a1,a4,a5 & between a2,a3,a5 & between a2,a4,a5 by A1,A2,Satz3p7p1,Satz3p7p2; hence between5 a1,a2,a3,a4,a5 by A1,A2,Satz3p6p2; thus a1,a2,a3,a4,a5 are_mutually_distinct by A1,A2,Satz3p7p1,GTARSKI1:def 10; end; ::\$N 3.17 Satz theorem Satz3p17: 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 let S be satisfying_Tarski-model TarskiGeometryStruct; let a,b,c,p,a9,b9,c9 be POINT of S; assume A1: between a,b,c & between a9,b9,c & between a,p,a9; then between c,b9,a9 by Satz3p2; then consider x be POINT of S such that A2: between b9,x,a & between p,x,c by A1,GTARSKI1:def 11; between c,b,a by A1,Satz3p2; then consider q be POINT of S such that A3: between x,q,c & between b,q,b9 by A2,GTARSKI1:def 11; between p,q,c by A2,A3,Satz3p5p2; hence thesis by A3; end; 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 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 Satz4p2: a,b,c,d IFS a9,b9,c9,d9 implies b,d equiv b9,d9 proof assume A1: a,b,c,d IFS a9,b9,c9,d9; per cases; suppose A2: a = c; now thus c = b by A1,A2,GTARSKI1:def 10; a9 = c9 by A1,A2,Satz2p2,GTARSKI1:def 7; hence c9 = b9 by A1,GTARSKI1:def 10; end; hence thesis by A1; end; suppose A3: a <> c; consider e be POINT of S such that A4: between a,c,e & c,e equiv a,c by GTARSKI1:def 8; A5: c <> e by A3,A4,Satz2p2,GTARSKI1:def 7; consider e9 be POINT of S such that A6: between a9,c9,e9 & c9,e9 equiv c,e by GTARSKI1:def 8; A7: c,e equiv c9,e9 by A6,Satz2p2; S is satisfying_SST_A5; then A8: e,d equiv e9,d9 by A3,A4,A6,A1,A7; c,b equiv b9,c9 by A1,Satz2p4; then A9: c,b equiv c9,b9 by Satz2p5; e9,c9 equiv c,e by A6,Satz2p4; then e9,c9 equiv e,c by Satz2p5; then A17: e,c equiv e9,c9 by Satz2p2; A18: between e,c,b proof between b,c,e & between a,b,e by A1,A4,Satz3p6p1,Satz3p6p2; hence thesis by Satz3p2; end; A19: between e9,c9,b9 proof between b9,c9,e9 & between a9,b9,e9 by A1,A6,Satz3p6p1,Satz3p6p2; hence thesis by Satz3p2; end; S is satisfying_SST_A5; hence thesis by A19,A18,A8,A9,A17,A1,A5; end; end; ::\$N 4.3 Satz theorem Satz4p3: between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 implies a,b equiv a9,b9 proof assume A1: between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9; then c,a equiv a9,c9 by Satz2p4; then a,b,c,a IFS a9,b9,c9,a9 by A1,Satz2p8,Satz2p5; then a,b equiv b9,a9 by Satz4p2,Satz2p4; hence thesis by Satz2p5; end; ::\$N 4.5 Satz theorem Satz4p5: between a,b,c & a,c equiv a9,c9 implies ex b9 st between a9,b9,c9 & a,b,c cong a9,b9,c9 proof assume A1: between a,b,c & a,c equiv a9,c9; consider d9 be POINT of S such that A2: between c9,a9,d9 & a9,d9 equiv c9,a9 by GTARSKI1:def 8; per cases; suppose a9 = d9; then c9 = a9 by A2,Satz2p2,GTARSKI1:def 7; then a = c by A1,GTARSKI1:def 7; then A2BIS: a = b by A1,GTARSKI1:def 10; take a9; thus thesis by A2BIS,Satz2p8,A1,Satz3p1,Satz3p2; end; suppose A2TER: a9 <> d9; consider b9 be POINT of S such that A3: between d9,a9,b9 & a9,b9 equiv a,b by GTARSKI1:def 8; consider c99 be POINT of S such that A4: between d9,b9,c99 & b9,c99 equiv b,c by GTARSKI1:def 8; A5: between a9,b9,c99 & between d9,a9,c99 by A3,A4,Satz3p6p1,Satz3p6p2; A6: a,b equiv a9,b9 by A3,Satz2p2; A7: b,c equiv b9,c99 by A4,Satz2p2; then A8: a,c equiv a9,c99 by A1,A5,A6,Satz2p11; A9: c99 = c9 proof A10: between d9,a9,c9 by A2,Satz3p2; A11: between d9,a9,c99 by A3,A4,Satz3p6p2; A12: a9,c9 equiv a,c by A1,Satz2p2; a9,c99 equiv a,c by A8,Satz2p2; hence thesis by A2TER,A10,A11,A12,Satz2p12; end; between a9,b9,c9 by A3,A4,Satz3p6p1,A9; hence thesis by A6,A7,A1,A9,GTARSKI1:def 3; end; end; ::\$N 4.6 Satz theorem Satz4p6: between a,b,c & a,b,c cong a9,b9,c9 implies between a9,b9,c9 proof assume A1: between a,b,c & a,b,c cong a9,b9,c9; consider b99 be POINT of S such that A3: between a9,b99,c9 & a,b,c cong a9,b99,c9 by A1,Satz4p5; A5: a9,b99 equiv a,b & b99,c9 equiv b,c by A3,Satz2p2; then a9,b99 equiv a9,b9 & b99,c9 equiv b9,c9 by A1,Satz2p3; then c9,b99 equiv b9,c9 by Satz2p4; then a9,b99,c9,b99 IFS a9,b99,c9,b9 by A5,A3,A1,Satz2p1,Satz2p3,Satz2p5; then b99,b9 equiv b99,b99 by Satz2p2,Satz4p2; hence thesis by A3,GTARSKI1:def 7; end; ::\$N 4.11 Satz theorem 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; ::\$N 4.12 Satz theorem for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct for a,b being POINT of S holds Collinear a,a,b by Satz3p1; theorem Lm4p13p1: 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 let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; let a,b,c,a9,b9,c9 be POINT of S; assume A1: a,b,c cong a9,b9,c9; then b,a equiv a9,b9 & c,a equiv a9,c9 by Satz2p4; hence b,c,a cong b9,c9,a9 by A1,Satz2p5; end; ::\$N 4.13 Satz theorem Satz4p13: 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 let S be satisfying_Tarski-model TarskiGeometryStruct; let a,b,c,a9,b9,c9 be POINT of S; assume A1: Collinear a,b,c & a,b,c cong a9,b9,c9; A4: between b,c,a implies between b9,c9,a9 proof assume A5: between b,c,a; b,c,a cong b9,c9,a9 by A1,Lm4p13p1; hence between b9,c9,a9 by A5,Satz4p6; end; between c,a,b implies between c9,a9,b9 proof assume A8: between c,a,b; b,c,a cong b9,c9,a9 by A1,Lm4p13p1; then c,a,b cong c9,a9,b9 by Lm4p13p1; hence between c9,a9,b9 by A8,Satz4p6; end; hence thesis by A1,A4,Satz4p6; end; theorem Lm4p14p1: 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 let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; let a,b,c,a9,b9,c9 be POINT of S; assume A1: b,a,c cong b9,a9,c9; then a,b equiv b9,a9 by Satz2p4; hence a,b,c cong a9,b9,c9 by A1,Satz2p5; end; theorem Lm4p14p2: 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 let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; let a,b,c,a9,b9,c9 be POINT of S; assume A1: a,c,b cong a9,c9,b9; then b,c equiv c9,b9 by Satz2p4; hence thesis by A1,Satz2p5; end; 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 Satz4p14: Collinear a,b,c & a,b equiv a9,b9 implies ex c9 being POINT of S st a,b,c cong a9,b9,c9 proof assume A1: Collinear a,b,c & a,b equiv a9,b9; then per cases; suppose A2: between a,b,c; consider c9 be POINT of S such that A3: between a9,b9,c9 & b9,c9 equiv b,c by GTARSKI1:def 8; A4: b,c equiv b9,c9 by A3,Satz2p2; then a,c equiv a9,c9 by A1,A3,A2,Satz2p11; hence thesis by A1,A4,GTARSKI1:def 3; end; suppose between c,a,b; then A5: between b,a,c by Satz3p2; consider c9 be POINT of S such that A6: between b9,a9,c9 & a9,c9 equiv a,c by GTARSKI1:def 8; b,a equiv a9,b9 by A1,Satz2p4; then A7: b,a equiv b9,a9 by Satz2p5; a,c equiv a9,c9 by A6,Satz2p2; then b,a,c cong b9,a9,c9 by A5,A6,A7,Satz2p11; hence thesis by Lm4p14p1; end; suppose between b,c,a; then ex y be POINT of S st between a9,y,b9 & a,c,b cong a9,y,b9 by A1,Satz3p2,Satz4p5; hence thesis by Lm4p14p2; end; 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 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 Satz4p16: a,b,c,d FS a9,b9,c9,d9 & a <> b implies c,d equiv c9,d9 proof assume A1: a,b,c,d FS a9,b9,c9,d9 & a <> b; then Collinear a,b,c; then per cases; suppose A2: between a,b,c; then A3: between a9,b9,c9 by A1,Satz4p6; A4: a,b equiv a9,b9 & a,c equiv a9,c9 & b,c equiv b9,c9 by A1,GTARSKI1:def 3; S is satisfying_SST_A5; hence thesis by A1,A4,A2,A3; end; suppose A5: between b,c,a; b,c,a cong b9,c9,a9 by A1,Lm4p13p1; then b,c,a,d IFS b9,c9,a9,d9 by A5,Satz4p6,A1; hence thesis by Satz4p2; end; suppose between c,a,b; then A6: between b,a,c by Satz3p2; A7: b,a,c cong b9,a9,c9 by A1,Lm4p14p1; A8: between b9,a9,c9 by A6,A7,Satz4p6; S is satisfying_SST_A5; hence thesis by A1,A8,A6,A7; end; end; ::\$N 4.17 Satz theorem Satz4p17: a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q implies c,p equiv c,q proof assume A1: a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q; a,b,c,p FS a,b,c,q proof a,b equiv a,b & a,c equiv a,c & b,c equiv b,c by Satz2p1; hence thesis by A1,GTARSKI1:def 3; end; hence c,p equiv c,q by A1,Satz4p16; end; ::\$N 4.18 Satz theorem Satz4p18: a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9 proof assume a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9; then c,c equiv c,c9 by Satz4p17; hence thesis by Satz2p2,GTARSKI1:def 7; end; ::\$N 4.19 Satz theorem Satz4p19: between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9 proof assume A1: between a,c,b & a,c equiv a,c9 & b,c equiv b,c9; A2: a = b implies c = c9 proof assume a = b; then a = c by A1,GTARSKI1:def 10; hence thesis by A1,Satz2p2,GTARSKI1:def 7; end; a <> b implies c = c9 proof assume A3: a <> b; Collinear a,b,c by A1,Satz3p2; hence thesis by A1,A3,Satz4p18; end; hence thesis by A2; end; 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 Satz5p1: ::GTARSKI1:37 a <> b & between a,b,c & between a,b,d implies between a,c,d or between a,d,c proof assume A1: a <> b & between a,b,c & between a,b,d; then between b,d,c or between b,c,d by GTARSKI1:37; hence thesis by A1,Satz3p5p2; end; ::\$N 5.2 Satz theorem Satz5p2: a <> b & between a,b,c & between a,b,d implies between b,c,d or between b,d,c proof assume A1: a <> b & between a,b,c & between a,b,d; then between a,c,d or between a,d,c by Satz5p1; hence thesis by A1,Satz3p6p1; end; ::\$N 5.3 Satz theorem Satz5p3: between a,b,d & between a,c,d implies between a,b,c or between a,c,b proof assume A1: between a,b,d & between a,c,d; per cases; suppose a = b; hence thesis by Satz3p1,Satz3p2; end; suppose A2: a <> b; consider p be POINT of S such that A3: between d,a,p & a,p equiv a,b by GTARSKI1:def 8; A4: a <> p by A3,Satz2p2,A2,GTARSKI1:def 7; between p,a,d by A3,Satz3p2; then between p,a,b & between p,a,c by A1,Satz3p5p1; hence thesis by A4,Satz5p2; end; end; definition let S be TarskiGeometryStruct; let a,b,c,d be POINT of S; pred a,b <= c,d means ex y being POINT of S st between c,y,d & a,b equiv c,y; end; ::\$N 5.5 Satz theorem Satz5p5: a,b <= c,d iff (ex x being POINT of S st between a,b,x & a,x equiv c,d) proof A1: a,b <= c,d implies (ex x be POINT of S st between a,b,x & a,x equiv c,d) proof assume a,b <= c,d; then consider y be POINT of S such that A2: between c,y,d & a,b equiv c,y; Collinear c,y,d by A2; then consider x be POINT of S such that A3: c,y,d cong a,b,x by A2,Satz2p2,Satz4p14; a,x equiv c,d by A3,Satz2p2; hence thesis by A2,A3,Satz4p6; end; (ex x be POINT of S st between a,b,x & a,x equiv c,d) implies a,b <= c,d proof assume ex x be POINT of S st between a,b,x & a,x equiv c,d; then consider x be POINT of S such that A4: between a,b,x & a,x equiv c,d; A5: Collinear x,a,b by A4; x,a equiv c,d by A4,Satz2p4; then consider y be POINT of S such that A6: x,a,b cong d,c,y by A5,Satz2p5,Satz4p14; a,b,x cong c,y,d proof A9: a,x equiv c,d proof a,x equiv d,c by A6,Satz2p4; hence thesis by Satz2p5; end; b,x equiv y,d proof b,x equiv d,y by A6,Satz2p4; hence thesis by Satz2p5; end; hence thesis by A6,A9; end; hence thesis by A4,Satz4p6; end; hence thesis by A1; end; ::\$N 5.6 Satz theorem Satz5p6: a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 implies a9,b9 <= c9,d9 proof assume A1: a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9; then consider x be POINT of S such that A2: between a,b,x & a,x equiv c,d by Satz5p5; Collinear a,b,x by A2; then consider y be POINT of S such that A3: a,b,x cong a9,b9,y by A1,Satz4p14; a9,y equiv c9,d9 proof a9,y equiv a,x by A3,Satz2p2; then a9,y equiv c,d by A2,Satz2p3; hence thesis by A1,Satz2p3; end; hence a9,b9 <= c9,d9 by A2,A3,Satz4p6,Satz5p5; end; ::\$N 5.7 Satz theorem a,b <= a,b proof between a,b,b by Satz3p1; hence thesis by Satz2p1; end; ::\$N 5.8 Satz theorem a,b <= c,d & c,d <= e,f implies a,b <= e,f proof assume A1: a,b <= c,d & c,d <= e,f; then consider x be POINT of S such that A2: between a,b,x & a,x equiv c,d by Satz5p5; consider y be POINT of S such that A3: between c,d,y & c,y equiv e,f by A1,Satz5p5; Collinear c,d,y by A3; then consider q be POINT of S such that A4: c,d,y cong a,x,q by A2,Satz2p2,Satz4p14; A5: between a,b,q proof between a,x,q by A3,A4,Satz4p6; hence thesis by A2,Satz3p6p2; end; a,q equiv e,f proof a,q equiv c,y by A4,Satz2p2; hence thesis by A3,Satz2p3; end; hence thesis by A5,Satz5p5; end; ::\$N 5.9 Satz theorem a,b <= c,d & c,d <= a,b implies a,b equiv c,d proof assume A1: a,b <= c,d & c,d <= a,b; then consider y be POINT of S such that A2: between c,y,d & a,b equiv c,y; consider p be POINT of S such that A3: between c,d,p & c,p equiv a,b by A1,Satz5p5; consider q be POINT of S such that A4: between a,q,b & c,d equiv a,q by A1; consider r be POINT of S such that A5: between d,c,r & c,r equiv a,b by GTARSKI1:def 8; A6: c = y implies a,b equiv c,d proof assume A7: c = y; then a = b by A2,GTARSKI1:def 7; then a = q by A4,GTARSKI1:def 10; hence thesis by A7,A2,A4,GTARSKI1:def 7; end; c <> y implies a,b equiv c,d proof assume A8: c <> y; A9: between d,y,c & between p,d,c by A2,A3,Satz3p2; A10: r <> c proof assume r = c; then a = b by A5,Satz2p2,GTARSKI1:def 7; hence contradiction by A2,Satz2p2,A8,GTARSKI1:def 7; end; A11: between r,c,y proof between y,c,r by A5,A9,Satz3p6p1; hence thesis by Satz3p2; end; A12: c <> d by A2,A8,GTARSKI1:def 10; A13: between r,c,p proof between r,c,d by A5,Satz3p2; hence thesis by A3,A12,Satz3p7p2; end; c,y equiv a,b by A2,Satz2p2; then y = p by A3,A10,A11,A13,Satz2p12; then between d,p,c & between p,d,c by A2,A3,Satz3p2; then p = d by Satz3p4; hence thesis by A3,Satz2p2; end; hence thesis by A6; end; ::\$N 5.10 Satz theorem Satz5p10: a,b <= c,d or c,d <= a,b proof consider x be POINT of S such that A1: between b,a,x & a,x equiv c,d by GTARSKI1:def 8; consider y be POINT of S such that A2: between x,a,y & a,y equiv c,d by GTARSKI1:def 8; A3: x = a implies a,b <= c,d or c,d <= a,b proof assume x = a; then A4: c = d by A1,Satz2p2,GTARSKI1:def 7; ex q be POINT of S st between c,c,q & c,q equiv a,b by GTARSKI1:def 8; hence thesis by A4,Satz5p5; end; x <> a implies a,b <= c,d or c,d <= a,b proof assume A5: x <> a; A6: between x,a,b by A1,Satz3p2; then A7: between x,y,b or between x,b,y by A2,A5,Satz5p1; between x,y,b implies c,d <= a,b proof assume between x,y,b; then between a,y,b by A2,Satz3p6p1; hence thesis by A2,Satz2p2; end; hence thesis by A2,A6,A7,Satz3p6p1,Satz5p5; end; hence thesis by A3; end; ::\$N 5.11 Satz theorem a,a <= b,c proof ex x be POINT of S st between a,a,x & a,x equiv b,c by GTARSKI1:def 8; hence thesis by Satz5p5; end; ::\$N 5.12 Lemma 1 theorem 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 by Satz2p4; ::\$N 5.12 Lemma 2 theorem Lemma5p12p2: a,b <= c,d implies a,b <= d,c proof assume a,b <= c,d; then ex x be POINT of S st between a,b,x & a,x equiv c,d by Satz5p5; hence thesis by Satz2p5,Satz5p5; end; ::\$N 5.12 Lemma 3 theorem Lemma5p12p3: between a,b,c & a,c equiv a,b implies c = b proof assume A1: between a,b,c & a,c equiv a,b; then A2: between c,b,a by Satz3p2; A3: c,b,a cong b,c,a proof A4: c,a equiv a,b by A1,Satz2p4; a,b equiv a,c by A1,Satz2p2; then b,a equiv a,c by Satz2p4; hence thesis by A4,Satz2p5,GTARSKI1:def 5; end; between b,c,a by A2,A3,Satz4p6; hence thesis by A2,Satz3p4; end; ::\$N METAMATH: endofsegidand theorem Lemma5p12p4: between a,c,b & a,b <= a,c implies b = c proof assume A1: between a,c,b & a,b <= a,c; then consider x be POINT of S such that A2: between a,b,x & a,x equiv a,c by Satz5p5; c = x by A1,A2,Lemma5p12p3,Satz3p6p2; hence thesis by A1,A2,Satz3p6p1,GTARSKI1:def 10; end; ::\$N 5.12 Satz theorem Satz5p12: Collinear a,b,c implies (between a,b,c iff (a,b <= a,c & b,c <= a,c)) proof assume A1: Collinear a,b,c; thus between a,b,c implies a,b <= a,c & b,c <= a,c proof assume A2: between a,b,c; hence a,b <= a,c by Satz2p1; thus b,c <= a,c proof between c,b,a by A2,Satz3p2; then c,b <= c,a by Satz2p1; then b,c <= c,a by Satz2p4; hence thesis by Lemma5p12p2; end; end; thus a,b <= a,c & b,c <= a,c implies between a,b,c proof assume A3: a,b <= a,c & b,c <= a,c; A4: between c,a,b implies between a,b,c proof assume A5: between c,a,b; c,b <= a,c by A3,Satz2p4; then a = b by A5,Lemma5p12p2,Lemma5p12p4; hence thesis by Satz3p1,Satz3p2; end; between b,c,a implies between a,b,c proof assume between b,c,a; then b = c by A3,Satz3p2,Lemma5p12p4; hence thesis by Satz3p1; end; hence thesis by A1,A4; end; end; begin :: Out lines definition let S be TarskiGeometryStruct; let a,b,p be POINT of S; pred p out a,b means 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 Satz6p2: a <> p & b <> p & c <> p & between a,p,c implies (between b,p,c iff p out a,b) proof assume A1: a <> p & b <> p & c <> p & between a,p,c; thus between b,p,c implies p out a,b proof assume between b,p,c; then between c,p,b & between c,p,a by A1,Satz3p2; hence thesis by A1,Satz5p2; end; thus p out a,b implies between b,p,c proof assume A2: p out a,b; A3: between p,a,b implies between b,p,c proof assume between p,a,b; then between b,a,p by Satz3p2; hence thesis by A1,Satz3p7p1; end; between p,b,a implies between b,p,c proof assume between p,b,a; then between a,b,p by Satz3p2; hence thesis by A1,Satz3p6p1; end; hence thesis by A2,A3; end; end; ::\$N 6.3 Satz theorem Satz6p3: p out a,b iff (a <> p & b <> p & (ex c st c <> p & between a,p,c & between b,p,c)) proof thus p out a,b implies (a <> p & b <> p & (ex c st (c <> p & between a,p,c & between b,p,c))) proof assume A1: p out a,b; consider c be POINT of S such that A2: between a,p,c & p,c equiv p,a by GTARSKI1:def 8; A3: p <> c by A1,A2,Satz2p2,GTARSKI1:def 7; A4: between p,a,b implies (ex c st (c <> p & between a,p,c & between b,p,c)) proof assume between p,a,b; between b,p,c by A1,A2,A3,Satz6p2; hence thesis by A2,A3; end; between p,b,a implies (ex c st (c <> p & between a,p,c & between b,p,c)) proof assume between p,b,a; between b,p,c by A1,A2,A3,Satz6p2; hence thesis by A2,A3; end; hence thesis by A1,A4; end; thus a <> p & b <> p & (ex c st (c <> p & between a,p,c & between b,p,c)) implies p out a,b by Satz6p2; end; ::\$N 6.4 Satz theorem p out a,b iff (Collinear a,p,b & not between a,p,b) proof p out a,b implies (Collinear a,p,b & not between a,p,b) proof assume A1: p out a,b; between p,b,a implies Collinear a,p,b & not between a,p,b proof assume between p,b,a; hence Collinear a,p,b; thus not between a,p,b proof assume A2: between a,p,b; then between b,p,a by Satz3p2; hence contradiction by A1,A2,Satz3p4; end; end; hence thesis by Satz3p2,Satz3p4,A1; end; hence thesis by Satz3p1,Satz3p2; end; ::\$N 6.5 Satz theorem a <> p implies p out a,a by Satz3p1; ::\$N 6.6 Satz theorem p out a,b implies p out b,a; ::\$N 6.7 Satz theorem p out a,b & p out b,c implies p out a,c by Satz3p6p2,Satz5p3,Satz5p1; ::\$N METAMATH: segcon2 theorem Lemmapsegcon2: ex x being POINT of S st (between p,a,x or between p,x,a) & p,x equiv b,c proof set q = p; consider r be POINT of S such that A1: between a,q,r & q,r equiv a,q by GTARSKI1:def 8; consider x be POINT of S such that A2: between r,q,x & q,x equiv b,c by GTARSKI1:def 8; A3: r = q implies ((between q,a,x or between q,x,a) & q,x equiv b,c) by A1,A2,Satz2p2,GTARSKI1:def 7; r <> q implies ((between q,a,x or between q,x,a) & q,x equiv b,c) proof assume A4: r <> q; between r,q,a by A1,Satz3p2; hence thesis by A2,A4,Satz5p2; end; hence thesis by A3; end; reserve r for POINT of S; ::\$N 6.11 Satz a) theorem r <> a & b <> c implies ex x being POINT of S st (a out x,r & a,x equiv b,c) proof assume A1: r <> a & b <> c; consider x be POINT of S such that A2: (between a,r,x or between a,x,r) & a,x equiv b,c by Lemmapsegcon2; a out x,r by A1,A2,Satz2p2,GTARSKI1:def 7; hence thesis by A2; end; definition let S be TarskiGeometryStruct; let a,p be POINT of S; func halfline(p,a) -> set equals {x where x is POINT of S: p out x,a}; coherence; end; reserve x,y for POINT of S; ::\$N 6.11 Satz b) theorem Satz6p11pb: 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 proof assume A1: r <> a & b <> c & (a out x,r & a,x equiv b,c) & (a out y,r & a,y equiv b,c); consider s be POINT of S such that A2: s <> a & between x,a,s & between r,a,s by A1,Satz6p3; consider t be POINT of S such that A3: t <> a & between y,a,t & between r,a,t by A1,Satz6p3; A4: between a,s,t implies x = y proof assume between a,s,t; then between x,s,t & between x,a,t by A2,Satz3p7p1,Satz3p7p2; then between t,a,x & between t,a,y by A3,Satz3p2; hence thesis by A1,A3,Satz2p12; end; between a,t,s implies x = y proof assume between a,t,s; then between y,t,s & between y,a,s by A3,Satz3p7p1,Satz3p7p2; then between s,a,y & between s,a,x by A2,Satz3p2; hence thesis by A1,A2,Satz2p12; end; hence thesis by A4,A1,A2,A3,Satz5p2; end; ::\$N 6.13 Satz theorem Satz6p13: p out a,b implies (p,a <= p,b iff between p,a,b) proof assume A1: p out a,b; A2: p,a <= p,b implies between p,a,b proof assume A3: p,a <= p,b; consider y be POINT of S such that A4: between p,y,b & p,a equiv p,y by A3; A5: p out y,b by A1,A4,GTARSKI1:def 7; p,y equiv p,y by Satz2p1; hence thesis by A4,A1,A5,Satz6p11pb; end; between p,a,b implies p,a <= p,b proof assume A6: between p,a,b; then Collinear p,a,b; hence thesis by A6,Satz5p12; end; hence thesis by A2; end; ::\$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 {x where x is POINT of S: Collinear p,q,x}; coherence proof set X = {x where x is POINT of S: Collinear p,q,x}; X c= the carrier of S proof let x be object; assume x in X; then ex y be POINT of S st x = y & Collinear p,q,y; hence thesis; end; hence thesis; end; end; reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct; reserve p,q,r,s for POINT of S; ::\$N 6.15 Satz theorem p <> q & p <> r & between q,p,r implies Line(p,q) = halfline(p,q) \/ {p} \/ halfline(p,r) proof assume that A1A: p <> q and A1B: p <> r and A1C: between q,p,r; thus Line(p,q) c= halfline(p,q) \/ {p} \/ halfline(p,r) proof let t be object; assume t in Line(p,q); then consider x be Element of S such that A2: t = x & Collinear p,q,x; A3: between q,x,p & p <> x implies x in halfline(p,q) proof assume between q,x,p & p <> x; then p out x,q by A1A,Satz3p2; hence thesis; end; A4: between x,p,q & x = q implies p = x by GTARSKI1:def 10; A5: between x,p,q & p <> x & x <> q implies x in halfline(p,r) proof assume A6: between x,p,q & p <> x & x <> q; then between q,p,r & between q,p,x by A1C,Satz3p2; then p out x,r by A1A,A1B,A6,Satz5p2; hence thesis; end; between p,q,x & p <> x implies x in halfline(p,q) proof assume between p,q,x & p <> x; then p out x,q by A1A; hence thesis; end; then (x in halfline(p,q) or x in {p}) or x in halfline(p,r) by A2,A3,A5,A4,TARSKI:def 1; then (x in halfline(p,q) \/ {p}) or x in halfline(p,r) by XBOOLE_0:def 3; hence thesis by A2,XBOOLE_0:def 3; end; thus halfline(p,q) \/ {p} \/ halfline(p,r) c= Line(p,q) proof let t be object; assume t in halfline(p,q) \/ {p} \/ halfline(p,r); then t in halfline(p,q) \/ {p} or t in halfline(p,r) by XBOOLE_0:def 3; then t in halfline(p,q) or t in {p} or t in halfline(p,r) by XBOOLE_0:def 3; then per cases by TARSKI:def 1; suppose t in halfline(p,q); then consider x be POINT of S such that A7: t = x & p out x,q; Collinear p,q,x by A7,Satz3p2; hence thesis by A7; end; suppose A8: t = p; then reconsider x = t as POINT of S; Collinear p,q,p by Satz3p1; hence thesis by A8; end; suppose t in halfline(p,r); then consider x be POINT of S such that A9: t = x & p out x,r; A10: between p,x,r implies between p,q,x or between q,x,p or between x,p,q proof assume between p,x,r; then between q,p,x by A1C,Satz3p5p1; hence thesis by Satz3p2; end; between p,r,x implies between p,q,x or between q,x,p or between x,p,q proof assume between p,r,x; then between q,p,x by A1B,A1C,Satz3p7p2; hence thesis by Satz3p2; end; then Collinear p,q,x by A9,A10; hence thesis by A9; end; end; end; definition let S be non empty TarskiGeometryStruct; let A be Subset of S; pred A is_line means ex p,q being POINT of S st p <> q & A = Line(p,q); end; ::\$N 6.16 Satz theorem :: GTARSKI1:45 p <> q & s <> p & s in Line(p,q) implies Line(p,q) = Line(p,s) proof assume that A1A: p <> q and A1B: s <> p and A1C: s in Line(p,q); consider x be POINT of S such that A2: s = x & Collinear p,q,x by A1C; thus Line(p,q) c= Line(p,s) proof let t be object; assume t in Line(p,q); then consider y be POINT of S such that A3: t = y & Collinear p,q,y; A4: between p,q,y implies between p,s,y or between s,y,p or between y,p,s proof assume A5: between p,q,y; A6: between p,q,s implies between p,s,y or between s,y,p or between y,p,s proof assume between p,q,s; then between p,y,s or between p,s,y by A1A,A5,Satz5p1; hence thesis by Satz3p2; end; A7: between q,s,p implies between p,s,y or between s,y,p or between y,p,s proof assume between q,s,p; then between p,s,q by Satz3p2; hence thesis by A5,Satz3p6p2; end; between s,p,q implies between p,s,y or between s,y,p or between y,p,s proof assume between s,p,q; then between s,p,y by A1A,A5,Satz3p7p2; hence thesis by Satz3p2; end; hence thesis by A2,A6,A7; end; A8: between q,y,p implies between p,s,y or between s,y,p or between y,p,s proof assume between q,y,p; then A9: between p,y,q by Satz3p2; A10: between p,q,s implies between p,s,y or between s,y,p or between y,p,s proof assume between p,q,s; then between p,y,s by A9,Satz3p6p2; hence thesis by Satz3p2; end; A11: between q,s,p implies between p,s,y or between s,y,p or between y,p,s proof assume between q,s,p; then between p,s,q by Satz3p2; then between p,s,y or between p,y,s by A9,Satz5p3; hence thesis by Satz3p2; end; between s,p,q implies between p,s,y or between s,y,p or between y,p,s proof assume between s,p,q; then between s,p,y by A9,Satz3p5p1; hence thesis by Satz3p2; end; hence thesis by A2,A10,A11; end; between y,p,q implies between p,s,y or between s,y,p or between y,p,s proof assume A12: between y,p,q; A13: between q,s,p implies between p,s,y or between s,y,p or between y,p,s proof assume A14: between q,s,p; between q,p,y by A12,Satz3p2; then between s,p,y by A14,Satz3p6p1; hence thesis by Satz3p2; end; between s,p,q implies between p,s,y or between s,y,p or between y,p,s proof assume between s,p,q; then between q,p,s & between q,p,y by A12,Satz3p2; then between p,s,y or between p,y,s by A1A,Satz5p2; hence thesis by Satz3p2; end; hence thesis by A2,A12,A1A,Satz3p7p2,A13; end; then Collinear p,s,y by A4,A8,A3; hence thesis by A3; end; thus Line(p,s) c= Line(p,q) proof let t be object; assume t in Line(p,s); then consider y be POINT of S such that A15: t = y & Collinear p,s,y; A16: between p,s,y implies between p,q,y or between q,y,p or between y,p,q proof assume A17: between p,s,y; A18: between q,s,p implies between p,q,y or between q,y,p or between y,p,q proof assume between q,s,p; then between p,s,q by Satz3p2; then between p,q,y or between p,y,q by A17,A1B,Satz5p1; hence thesis by Satz3p2; end; between s,p,q implies between p,q,y or between q,y,p or between y,p,q proof assume between s,p,q; then between q,p,s by Satz3p2; then between q,p,y by A1B,A17,Satz3p7p2; hence thesis by Satz3p2; end; hence thesis by A17,Satz3p6p2,A18,A2; end; A19: between s,y,p implies between p,q,y or between q,y,p or between y,p,q proof assume A20: between s,y,p; A21: between p,q,s implies between p,q,y or between q,y,p or between y,p,q proof assume A22: between p,q,s; between p,y,s by A20,Satz3p2; then between p,q,y or between p,y,q by A22,Satz5p3; hence thesis by Satz3p2; end; A23: between q,s,p implies between p,q,y or between q,y,p or between y,p,q proof assume between q,s,p; then A25: between p,s,q by Satz3p2; between p,y,s by A20,Satz3p2; then between p,y,q by A25,Satz3p6p2; hence thesis by Satz3p2; end; between s,p,q implies between p,q,y or between q,y,p or between y,p,q proof assume between s,p,q; then A26: between q,p,s by Satz3p2; between p,y,s by A20,Satz3p2; then between q,p,y by A26,Satz3p5p1; hence thesis by Satz3p2; end; hence thesis by A21,A23,A2; end; between y,p,s implies between p,q,y or between q,y,p or between y,p,q proof assume A27: between y,p,s; A28: between q,s,p implies between p,q,y or between q,y,p or between y,p,q proof assume between q,s,p; then between p,s,q by Satz3p2; hence thesis by A27,A1B,Satz3p7p2; end; between s,p,q implies between p,q,y or between q,y,p or between y,p,q proof assume A29: between s,p,q; between s,p,y by A27,Satz3p2; then between p,q,y or between p,y,q by Satz5p2,A29,A1B; hence thesis by Satz3p2; end; hence thesis by A27,Satz3p5p1,A28,A2; end; then Collinear p,q,y by A15,A16,A19; hence thesis by A15; end; end; 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 Satz6p17: p in Line(p,q) & q in Line(p,q) & Line(p,q) = Line(q,p) proof thus p in Line(p,q) proof Collinear p,q,p by Satz3p1; hence thesis; end; Collinear p,q,q by Satz3p1; hence q in Line(p,q); thus Line(p,q)=Line(q,p) proof A2: Line(p,q) c= Line(q,p) proof let x be object; assume x in Line(p,q); then consider y be POINT of S such that A3: y = x and A4: Collinear p,q,y; Collinear q,p,y by A4,Satz3p2; hence thesis by A3; end; Line(q,p) c= Line(p,q) proof let x be object; assume x in Line(q,p); then consider y be POINT of S such that A5: y = x and A6: Collinear q,p,y; Collinear p,q,y by A6,Satz3p2; hence thesis by A5; end; hence thesis by A2; end; end; 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 Thequiv1: 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: 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) proof let S be satisfying_Tarski-model non empty TarskiGeometryStruct; let a,b,x,y be POINT of S; assume A1: a,b equal_line x,y; Line(a,b) = Line(x,y) proof A2: Line(a,b) c= Line(x,y) proof let z be object; assume z in Line(a,b); then consider z9 be POINT of S such that A3: z = z9 and A4: Collinear a,b,z9; z9 on_line x,y by A1,A4,Thequiv1; then Collinear x,y,z9; hence z in Line(x,y) by A3; end; Line(x,y) c= Line(a,b) proof let z be object; assume z in Line(x,y); then consider z9 be POINT of S such that A5: z = z9 and A6: Collinear x,y,z9; z9 on_line a,b by A6,A1,Thequiv1; then Collinear a,b,z9; hence thesis by A5; end; hence thesis by A2; end; hence thesis; end; theorem 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 proof let S be satisfying_Tarski-model non empty TarskiGeometryStruct; let a,b,x,y be POINT of S; assume that A1: a <> b and A1A: x <> y and A2: Line(a,b) = Line(x,y); for c be POINT of S holds c on_line a,b iff c on_line x,y proof let c be POINT of S; hereby assume c on_line a,b; then Collinear a,b,c; then c in Line(x,y) by A2; then ex z be POINT of S st c = z & Collinear x,y,z; hence c on_line x,y by A1A; end; assume c on_line x,y; then Collinear x,y,c; then c in Line(a,b) by A2; then ex z be POINT of S st c = z & Collinear a,b,z; hence c on_line a,b by A1; end; hence thesis by A1,A1A; end; ::\$N 6.18 Satz theorem Satz6p18: ::GTARSKI_1:46 A is_line & a <> b & a in A & b in A implies A = Line(a,b) proof assume that A1: A is_line and A2: a <> b and A3: a in A and A4: b in A; consider p,q such that A5: p <> q and A6: A = Line(p,q) by A1; consider xa be POINT of S such that A7: a = xa and A8: Collinear p,q,xa by A3,A6; consider xb be POINT of S such that A9: b = xb and A10: Collinear p,q,xb by A4,A6; a on_line p,q & b on_line p,q by A5,A7,A8,A9,A10; hence thesis by A2,A6,Thequiv2,GTARSKI1:46; end; ::\$N 6.19 Satz theorem Satz6p19: a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B implies A = B proof assume that A1: a <> b and A2: A is_line and A3: a in A and A4: b in A and A5: B is_line and A6: a in B and A7: b in B; consider pa,qa be POINT of S such that pa <> qa and A8: A = Line(pa,qa) by A2; consider pb,qb be POINT of S such that pb <> qb and A9: B = Line(pb,qb) by A5; Line(pa,qa) = Line(a,b) & Line(pb,qb) = Line(a,b) by A1,A3,A4,A8,A2,A6,A7,A9,A5,Satz6p18; hence thesis by A8,A9; end; ::\$N 6.21 Satz theorem A is_line & B is_line & A <> B & a in A & a in B & b in A & b in B implies a = b by Satz6p19; ::\$N 6.23 Satz theorem (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)) proof assume ex p,q st p <> q; then consider p,q such that A1: p <> q; A2: (ex A st A is_line & a in A & b in A & c in A) implies Collinear a,b,c proof assume ex A st A is_line & a in A & b in A & c in A; then consider A such that A3: A is_line and A4: a in A and A5: b in A and A6: c in A; per cases; suppose a <> b; then c in Line(a,b) by A3,A4,A5,A6,Satz6p18; then ex x st c = x & Collinear a,b,x; hence thesis; end; suppose a = b; hence thesis by Satz3p1; end; end; Collinear a,b,c implies (ex A st A is_line & a in A & b in A & c in A) proof assume A8: Collinear a,b,c; per cases; suppose A9: a = b; per cases; suppose A10: a = c; per cases by A1; suppose A11: a <> p; set A = Line(a,p); now thus A is_line by A11; Collinear a,p,a by Satz3p1; hence a in A & b in A & c in A by A9,A10; end; hence ex A st A is_line & a in A & b in A & c in A; end; suppose A12: a <> q; set A = Line(a,q); now thus A is_line by A12; Collinear a,q,a by Satz3p1; hence a in A & b in A & c in A by A9,A10; end; hence ex A st A is_line & a in A & b in A & c in A; end; end; suppose A13: a <> c; set A = Line(a,c); now thus A is_line by A13; Collinear a,c,a & Collinear a,c,c by Satz3p1; hence a in A & b in A & c in A by A9; end; hence ex A st A is_line & a in A & b in A & c in A; end; end; suppose A14: a <> b; Collinear a,b,a & Collinear a,b,b by Satz3p1; then A15: a in Line(a,b) & b in Line(a,b) & c in Line(a,b) by A8; reconsider A = Line(a,b) as Subset of S; A is_line by A14; hence ex A st A is_line & a in A & b in A & c in A by A15; end; end; hence thesis by A2; end; ::\$N 6.24 Satz theorem Satz6p24: for S being satisfying_A8 TarskiGeometryStruct ex a,b,c being POINT of S st not Collinear a,b,c proof let S be satisfying_A8 TarskiGeometryStruct; consider a,b,c being POINT of S such that A1: not between a,b,c and A2: not between b,c,a and A3: not between c,a,b by GTARSKI2:def 7; not Collinear a,b,c by A1,A2,A3; hence thesis; end; ::\$N 6.25 Satz theorem 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 let S be non empty satisfying_Tarski-model TarskiGeometryStruct; let a,b be POINT of S; assume that A1: S is satisfying_A8 and A2: a <> b; assume A3: for c be POINT of S holds Collinear a,b,c; consider a9,b9,c9 be POINT of S such that A4: not Collinear a9,b9,c9 by A1,Satz6p24; A5: a9 <> b9 by A4,Satz3p1; set A = Line(a,b); Collinear a,b,a9 & Collinear a,b,b9 by A3; then A is_line & a9 in A & b9 in A by A2; then A6: Line(a9,b9) = A by A5,Satz6p18; Collinear a,b,c9 by A3; then c9 in Line(a9,b9) by A6; then ex x be POINT of S st c9 = x & Collinear a9,b9,x; hence contradiction by A4; end; theorem Satz6p28Lem01: 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: 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 let S be satisfying_Tarski-model TarskiGeometryStruct; let a,b,c,d,e,f,g,h be Element of S; a,b <= c,d or c,d <= a,b by Satz5p10; hence thesis by Satz5p6; end; ::\$N 6.28 Satz, introduced by Beeson theorem 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 let S be satisfying_Tarski-model TarskiGeometryStruct; let a,b,c,a1,b1,c1 be Element of S; assume that A1: b out a,c and A2: b1 out a1,c1 and A3: b,a equiv b1,a1 and A4: b,c equiv b1,c1 and A5: not a,c equiv a1,c1; now thus b out c,a by A1; thus b1 out c1,a1 by A2; b,a equiv a1,b1 & b,c equiv c1,b1 & not a,c equiv c1,a1 by Satz2p5,A3,A4,A5; hence not c,a equiv c1,a1 & a,b equiv a1,b1 & c,b equiv c1,b1 by Satz2p4; hence not (between c,a,b & between c1,a1,b1) & not (between a,c,b & between a1,c1,b1) by Satz4p3,A5; thus (b,a <= b,c or b1,c1 <= b1,a1) & (b,c <= b,a or b1,a1 <= b1,c1) by A3,Satz6p28Lem02,A4; end; hence contradiction by Satz6p28Lem01,A1,A2,Satz3p2; end; begin :: Midpoint definition let S be TarskiGeometryStruct; let a,b,m be POINT of S; pred Middle a,m,b means :DEFM: 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 Middle a,m,b implies Middle b,m,a by Satz3p2,Satz2p2; 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 Satz7p3: Middle a,m,a iff m = a by GTARSKI1:def 10,Satz3p1,Satz2p1; ::\$N 7.4 Existence theorem Satz7p4existence: for p being POINT of S holds ex p9 being POINT of S st Middle p,a,p9 proof let p be POINT of S; per cases; suppose p <> a; consider x be POINT of S such that A1: between p,a,x & a,x equiv p,a by GTARSKI1:def 8; a,x equiv a,p by A1,Satz2p5; then a,p equiv a,x by Satz2p2; hence thesis by A1,DEFM; end; suppose p = a; hence thesis by Satz7p3; end; end; reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct, a for POINT of S; ::\$N 7.4 Uniqueness theorem Satz7p4uniqueness: for p,p1,p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds p1 = p2 proof let p,p1,p2 be POINT of S; assume A1: Middle p,a,p1 & Middle p,a,p2; per cases; suppose A2: p <> a; a,p1 equiv a,p & a,p2 equiv a,p by A1,Satz2p2; hence thesis by A1,A2,Satz2p12; end; suppose p = a; then a = p1 & a = p2 by A1,Satz2p2,GTARSKI1:def 7; hence thesis; end; end; 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 :DEFR: Middle p,a,it; existence by Satz7p4existence; uniqueness by Satz7p4uniqueness; 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 reflection(a,p) = p9 iff Middle p,a,p9 by DEFR; 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 Satz7p7: reflection(a,reflection(a,p)) = p proof Middle p,a,reflection(a,p) by DEFR; then Middle reflection(a,p),a,p by Satz3p2,Satz2p2; hence thesis by DEFR; end; ::\$N 7.8 Satz theorem ex p st reflection(a,p) = p9 proof set p = reflection(a,p9); take p; thus thesis by Satz7p7; end; ::\$N 7.9 Satz theorem Satz7p9: reflection(a,p) = reflection(a,p9) implies p = p9 proof assume reflection(a,p) = reflection(a,p9); then reflection(a,reflection(a,p)) = p9 by Satz7p7; hence thesis by Satz7p7; end; 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 Satz7p10: reflection(a,p) = p iff p = a proof hereby assume reflection(a,p) = p; then Middle p,a,p by DEFR; hence p = a by GTARSKI1:def 10; end; assume p = a; then Middle p,a,p by Satz3p1,Satz2p1; hence thesis by DEFR; end; 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 Satz7p13: p,q equiv reflection(a,p),reflection(a,q) proof reconsider p9 = reflection(a,p), q9 = reflection(a,q) as POINT of S; per cases; suppose A1: p = a; Middle q,a,reflection(a,q) by DEFR; hence thesis by A1,Satz7p10; end; suppose A2: p <> a; A3: Middle p,a,p9 by DEFR; A4: Middle q,a,q9 by DEFR; consider x be POINT of S such that A5: between p9,p,x and A6: p,x equiv q,a by GTARSKI1:def 8; consider y be POINT of S such that A7: between q9,q,y and A8: q,y equiv p,a by GTARSKI1:def 8; consider x9 be POINT of S such that A9: between x,p9,x9 and A10: p9,x9 equiv q,a by GTARSKI1:def 8; consider y9 be POINT of S such that A11: between y,q9,y9 and A12: q9,y9 equiv p,a by GTARSKI1:def 8; A13: between5 x,p,a,p9,x9 & between5 y,q,a,q9,y9 proof A14: between x9,p9,x by A9,Satz3p2; between p9,a,p by A3,Satz3p2; then between5 x9,p9,a,p,x by A5,A14,Satz3p11p3pb,Satz3p11p4pb; hence between5 x,p,a,p9,x9 by Satz3p2; A15: between y9,q9,y by A11,Satz3p2; between q9,a,q by A4,Satz3p2; then between5 y9,q9,a,q,y by A7,A15,Satz3p11p3pb,Satz3p11p4pb; hence between5 y,q,a,q9,y9 by Satz3p2; end; A16: a,x equiv a,y proof A17: p,a equiv q,y by A8,Satz2p2; x,p equiv q,a by A6,Satz2p4; then A18: x,p equiv a,q by Satz2p5; between x,p,a & between a,q,y by A13,Satz3p2; then x,a equiv a,y by A17,A18,Satz2p11; hence thesis by Satz2p4; end; A19: a,y equiv a,x9 proof q,a equiv p9,x9 by A10,Satz2p2; then a,q equiv p9,x9 by Satz2p4; then A20: a,q equiv x9,p9 by Satz2p5; q,y equiv a,p by A8,Satz2p5; then q,y equiv a,p9 by A3,Satz2p3; then A21: q,y equiv p9,a by Satz2p5; between a,q,y & between x9,p9,a by A13,Satz3p2; then a,y equiv x9,a by A20,A21,Satz2p11; hence thesis by Satz2p5; end; A22: a,x9 equiv a,y9 proof q,a equiv a,q9 by A4,Satz2p4; then p9,x9 equiv a,q9 by A10,Satz2p3; then A23: x9,p9 equiv a,q9 by Satz2p4; p,a equiv a,p9 by A3,Satz2p4; then q9,y9 equiv a,p9 by A12,Satz2p3; then a,p9 equiv q9,y9 by Satz2p2; then A24: p9,a equiv q9,y9 by Satz2p4; between x9,p9,a & between a,q9,y9 by A13,Satz3p2; then x9,a equiv a,y9 by A23,A24,Satz2p11; hence thesis by Satz2p4; end; A25: x,a,x9,y9 AFS y9,a,y,x proof now thus between x,a,x9 by A13; thus between y9,a,y by A13,Satz3p2; a,x equiv a,x9 by A16,A19,Satz2p3; then A26: a,x equiv a,y9 by A22,Satz2p3; hence a,y9 equiv a,x by Satz2p2; a,x equiv y9,a by A26,Satz2p5; hence x,a equiv y9,a by Satz2p4; thus a,x9 equiv a,y by A19,Satz2p2; thus x,y9 equiv y9,x by Satz2p1,Satz2p5; end; hence thesis; end; A27: S is satisfying_SST_A5; x <> a by A13,A2,GTARSKI1:def 10; then A28: x9,y9 equiv y,x by A27,A25; A29: y,q,a,x IFS y9,q9,a,x9 proof now thus between y,q,a & between y9,q9,a by A13,Satz3p2; a,y equiv a,y9 by A19,A22,Satz2p3; then a,y equiv y9,a by Satz2p5; hence y,a equiv y9,a by Satz2p4; a,q equiv q9,a by A4,Satz2p5; hence q,a equiv q9,a by Satz2p4; y,x equiv x9,y9 by A28,Satz2p2; hence y,x equiv y9,x9 by Satz2p5; thus a,x equiv a,x9 by A16,A19,Satz2p3; end; hence thesis; end; x,p,a,q IFS x9,p9,a,q9 proof now thus between x,p,a & between x9,p9,a by A13,Satz3p2; a,x equiv a,x9 by A16,A19,Satz2p3; then a,x equiv x9,a by Satz2p5; hence x,a equiv x9,a by Satz2p4; a,p equiv p9,a by A3,Satz2p5; hence p,a equiv p9,a by Satz2p4; q,x equiv x9,q9 by A29,Satz4p2,Satz2p5; hence x,q equiv x9,q9 by Satz2p4; thus a,q equiv a,q9 by A4; end; hence thesis; end; hence thesis by Satz4p2; end; end; Lemma7p15a: between p,q,r implies between reflection(a,p),reflection(a,q),reflection(a,r) proof assume A1: between p,q,r; p,q,r cong reflection(a,p),reflection(a,q),reflection(a,r) by Satz7p13; hence between reflection(a,p),reflection(a,q),reflection(a,r) by A1,Satz4p6; end; ::\$N 7.15 Satz theorem Satz7p15: between p,q,r iff between reflection(a,p),reflection(a,q),reflection(a,r) proof now assume C1: between reflection(a,p),reflection(a,q),reflection(a,r); reflection(a,reflection(a,p)) = p & reflection(a,reflection(a,q)) = q & reflection(a,reflection(a,r)) = r by Satz7p7; hence between p,q,r by C1,Lemma7p15a; end; hence thesis by Lemma7p15a; end; Lemma7p16a: p,q equiv r,s implies reflection(a,p),reflection(a,q) equiv reflection(a,r),reflection(a,s) proof assume A1: p,q equiv r,s; A2: r,s equiv reflection(a,r),reflection(a,s) by Satz7p13; p,q equiv reflection(a,p),reflection(a,q) by Satz7p13; then r,s equiv reflection(a,p),reflection(a,q) by A1,GTARSKI1:def 6; hence thesis by A2,GTARSKI1:def 6; end; ::\$N 7.16 Satz theorem Satz7p16: p,q equiv r,s iff reflection(a,p),reflection(a,q) equiv reflection(a,r),reflection(a,s) proof now assume reflection(a,p),reflection(a,q) equiv reflection(a,r),reflection(a,s); reflection(a,reflection(a,p)) = p & reflection(a,reflection(a,q)) = q & reflection(a,reflection(a,r)) = r & reflection(a,reflection(a,s)) = s by Satz7p7; hence thesis by Lemma7p16a; end; hence thesis by Lemma7p16a; end; ::\$N 7.17 Satz theorem Satz7p17: Middle p,a,p9 & Middle p,b,p9 implies a = b proof assume that A1: Middle p,a,p9 and A2: Middle p,b,p9; now thus between p,b,p9 by A2; reflection(a,p) = p9 by A1,DEFR; then b,p9 equiv reflection(a,b),reflection(a,reflection(a,p)) by Satz7p13; then b,p9 equiv reflection(a,b),p by Satz7p7; then b,p equiv reflection(a,b),p by A2,Satz2p3; hence p,b equiv reflection(a,b),p by Satz2p4; hence p,b equiv p,reflection(a,b) by Satz2p5; b,p equiv reflection(a,b),reflection(a,p) by Satz7p13; then b,p equiv reflection(a,b),p9 by A1,DEFR; then b,p9 equiv reflection(a,b),p9 by A2,GTARSKI1:def 6; then p9,b equiv reflection(a,b),p9 by Satz2p4; hence p9,b equiv p9,reflection(a,b) by Satz2p5; end; then reflection(a,b) = b by Satz4p19; hence thesis by Satz7p10; end; ::\$N 7.18 Satz theorem reflection(a,p) = reflection(b,p) implies a = b proof assume A1: reflection(a,p) = reflection(b,p); Middle p,a,reflection(a,p) & Middle p,b,reflection(b,p) by DEFR; hence thesis by A1,Satz7p17; end; ::\$N 7.19 Satz theorem reflection(b,reflection(a,p)) = reflection(a,reflection(b,p)) iff a = b proof reflection(b,reflection(a,p)) = reflection(a,reflection(b,p)) implies a = b proof assume A1: reflection(b,reflection(a,p)) = reflection(a,reflection(b,p)); set p9 = reflection(a,p); A2: Middle p,a,p9 by DEFR; Middle reflection(b,p),a,reflection(b,p9) by A1,DEFR; then Middle reflection(b,reflection(b,p)),reflection(b,a), reflection(b,reflection(b,p9)) by Satz7p15,Satz7p16; then Middle p,reflection(b,a),reflection(b,reflection(b,p9)) by Satz7p7; then Middle p,reflection(b,a),p9 by Satz7p7; hence thesis by A2,Satz7p17,Satz7p10; end; hence thesis; end; ::\$N 7.20 Satz theorem Satz7p20: Collinear a,m,b & m,a equiv m,b implies a = b or Middle a,m,b proof assume that A1: Collinear a,m,b and A2: m,a equiv m,b; assume A3: a <> b; per cases by A1; suppose between a,m,b; hence thesis by A2; end; suppose between m,b,a; then A4: between a,b,m by Satz3p2; A5: between b,b,m by Satz3p1,Satz3p2; m,a equiv b,m by A2,Satz2p5; then A6: a,m equiv b,m by Satz2p4; b,m equiv b,m by Satz2p1; hence thesis by A3,A4,A5,A6,Satz4p3,GTARSKI1:def 7; end; suppose A7: between b,a,m; A8: between a,a,m by Satz3p1,Satz3p2; m,a equiv b,m by A2,Satz2p5; then a,m equiv b,m by Satz2p4; then A9: b,m equiv a,m by Satz2p2; a,m equiv a,m by Satz2p1; hence thesis by A3,A7,A8,A9,Satz4p3,GTARSKI1:def 7; end; end; reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct, a,b,c,d,p for POINT of S; ::\$N 7.21 Satz theorem 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 proof assume that A1: not Collinear a,b,c and A2: b <> d and A3: a,b equiv c,d and A4: b,c equiv d,a and A5: Collinear a,p,c and A6: Collinear b,p,d; A7: Collinear b,d,p by A6,Satz3p2; then consider p9 being POINT of S such that A8: b,d,p cong d,b,p9 by GTARSKI1:def 5,Satz4p14; A9: Collinear d,b,p9 by A7,A8,Satz4p13; now thus Collinear b,d,p by A6,Satz3p2; thus b,d,p cong d,b,p9 by A8; a,b equiv d,c by A3,Satz2p5; hence b,a equiv d,c by Satz2p4; thus d,a equiv b,c by A4,Satz2p2; end; then A10: b,d,p,a FS d,b,p9,c; then p,a equiv c,p9 by A2,Satz4p16,Satz2p5; then A11: a,p equiv c,p9 by Satz2p4; A12: a,c equiv c,a by GTARSKI1:def 5; now thus Collinear b,d,p by A6,Satz3p2; thus b,d,p cong d,b,p9 by A8; thus b,c equiv d,a by A4; a,b equiv d,c by A3,Satz2p5; then b,a equiv d,c by Satz2p4; hence d,c equiv b,a by Satz2p2; end; then b,d,p,c FS d,b,p9,a; then p,c equiv p9,a by A2,Satz4p16; then A13: Collinear c,p9,a by A5,Satz4p13,A11,A12,GTARSKI1:def 3; A14: a <> c by A1,Satz3p1; A15: Line(a,c) <> Line(b,d) proof assume Line(a,c) = Line(b,d); then b in Line(a,c) by Satz6p17; then ex x be POINT of S st b = x & Collinear a,c,x; hence contradiction by A1,Satz3p2; end; now thus Line(a,c) <> Line(b,d) by A15; thus Line(a,c) is_line by A14; thus Line(b,d) is_line by A2; Collinear a,c,p9 by A13; hence p9 in Line(a,c); Collinear b,d,p9 by A9,Satz3p2; hence p9 in Line(b,d); Collinear a,c,p by A5,Satz3p2; hence p in Line(a,c); Collinear b,d,p by A6,Satz3p2; hence p in Line(b,d); end; then A16: p9 = p by Satz6p19; now thus Middle a,p,c by A14,Satz7p20,A10,A2,Satz4p16,A16,A5; b,p equiv p,d by A16,A8,Satz2p5; hence Middle b,p,d by A2,Satz7p20,A6,Satz2p4; end; hence thesis; end; reserve a1,a2,b1,b2,m1,m2 for POINT of S; ::\$N 7.22 Satz, part 1 theorem Satz7p22part1: 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 proof assume that A1: between a1,c,a2 and A2: between b1,c,b2 and A3: c,a1 equiv c,b1 and A4: c,a2 equiv c,b2 and A5: Middle a1,m1,b1 and A6: Middle a2,m2,b2 and A7: c,a1 <= c,a2; per cases; suppose A8: a2 = c; a1 = c proof consider x be POINT of S such that A9: between c,a1,x and A10: c,x equiv c,c by A7,A8,Satz5p5; c = x by A10,GTARSKI1:def 7; hence thesis by A9,GTARSKI1:def 10; end; then Middle a1,m1,a1 & Middle a2,m2,a2 by A5,A6,A8,A3,A4,Satz2p2,GTARSKI1:def 7; then m1 = a1 & m2 = a2 by GTARSKI1:def 10; hence thesis by A8,Satz3p1; end; suppose A11: a2 <> c; set a = reflection(c,a2), b = reflection(c,b2), m = reflection(c,m2); now thus c,a1 equiv c,a1 by Satz2p1; c,a2 equiv reflection(c,c),reflection(c,a2) by Satz7p13; hence c,a2 equiv c,a by Satz7p10; end; then A12: c,a1 <= c,a by A7,Satz5p6; per cases; suppose A13: a1 = c; then a1 = b1 by A3,Satz2p2,GTARSKI1:def 7; then m1 = a1 by A5,GTARSKI1:def 10; hence thesis by A13,Satz3p1,Satz3p2; end; suppose A14: a1 <> c; A15: between c,a1,a proof c out a1,a proof now thus c <> a1 by A14; thus c <> a proof assume c = a; then reflection(c,a2) = reflection(c,c) by Satz7p10; hence contradiction by A11,Satz7p9; end; thus between c,a1,a or between c,a,a1 proof A16: Middle a2,c,a by DEFR; A17: between a2,c,a1 by A1,Satz3p2; then per cases by A11,A16,Satz5p1; suppose between a2,a,a1; hence thesis by A16,Satz3p6p1; end; suppose between a2,a1,a; hence thesis by A17,Satz3p6p1; end; end; end; hence thesis; end; hence thesis by A12,Satz6p13; end; A18: between c,b1,b proof per cases; suppose c = b1; hence thesis by A14,A3,GTARSKI1:def 7; end; suppose A19: c <> b1; A20: c,b1 <= c,b2 by A3,A4,A7,Satz5p6; c,b2 equiv reflection(c,c),reflection(c,b2) by Satz7p13; then c,b2 equiv c,b & c,b1 equiv c,b1 by Satz2p1,Satz7p10; then A21: c,b1 <= c,b by A20,Satz5p6; A22: b2 <> c by A11,A4,GTARSKI1:def 7; c out b1,b proof now thus c <> b1 by A19; thus c <> b proof assume c = b; then reflection(c,b2) = reflection(c,c) by Satz7p10; hence contradiction by A22,Satz7p9; end; thus between c,b1,b or between c,b,b1 proof A23: Middle b2,c,b by DEFR; A24: between b2,c,b1 by A2,Satz3p2; then between b2,b,b1 or between b2,b1,b by A22,A23,Satz5p1; hence thesis by A23,A24,Satz3p6p1; end; end; hence thesis; end; hence thesis by A21,Satz6p13; end; end; between a,a1,c & between b,b1,c & between a,m,b by A18,Satz3p2,A15,A6,Satz7p15; then consider q be POINT of S such that A25: between m,q,c and A26: between a1,q,b1 by Satz3p17; A27: between m,c,m2 proof Middle m2,c,m by DEFR; hence thesis by Satz3p2; end; q = m1 proof a,a1,c,m IFS b,b1,c,m proof now thus between a,a1,c by A15,Satz3p2; thus between b,b1,c by A18,Satz3p2; reflection(c,c),reflection(c,a2) equiv reflection(c,c),reflection(c,b2) by A4,Satz7p16; then c,reflection(c,a2) equiv reflection(c,c),reflection(c,b2) by Satz7p10; then c,a equiv c,b by Satz7p10; then c,a equiv b,c by Satz2p5; hence a,c equiv b,c by Satz2p4; c,a1 equiv b1,c by A3,Satz2p5; hence a1,c equiv b1,c by Satz2p4; m2,a2 equiv b2,m2 by A6,Satz2p5; then a2,m2 equiv b2,m2 by Satz2p4; hence a,m equiv b,m by Satz7p16; thus c,m equiv c,m by Satz2p1; end; hence thesis; end; then a1,m equiv b1,m by Satz4p2; then A28: a1,m equiv m,b1 by Satz2p5; then A29: m,a1 equiv m,b1 by Satz2p4; q,a1 equiv q,b1 proof per cases; suppose A30: m <> c; Collinear c,m,q by A25; hence thesis by A3,A29,A30,Satz4p17; end; suppose m = c; then q = m by A25,GTARSKI1:def 10; hence thesis by A28,Satz2p4; end; end; then Middle a1,q,b1 by A26; hence thesis by A5,Satz7p17; end; hence thesis by A27,A25,Satz3p6p1; end; end; end; ::\$N 7.22 Satz, part 2 theorem Satz7p22part2: 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 proof assume that A1: between a1,c,a2 and A2: between b1,c,b2 and A3: c,a1 equiv c,b1 and A4: c,a2 equiv c,b2 and A5: Middle a1,m1,b1 and A6: Middle a2,m2,b2 and A7: c,a2 <= c,a1; per cases; suppose A8: a1 = c; a2 = c proof consider x be POINT of S such that A9: between c,a2,x and A10: c,x equiv c,c by A7,A8,Satz5p5; c = x by A10,GTARSKI1:def 7; hence thesis by A9,GTARSKI1:def 10; end; then Middle a1,m1,a1 & Middle a2,m2,a2 by A5,A6,A8,A3,A4,Satz2p2,GTARSKI1:def 7; then m1 = a1 & m2 = a2 by GTARSKI1:def 10; hence thesis by A8,Satz3p1,Satz3p2; end; suppose A11: a1 <> c; set a = reflection(c,a1), b = reflection(c,b1), m = reflection(c,m1); now thus c,a2 equiv c,a2 by Satz2p1; c,a1 equiv reflection(c,c),reflection(c,a1) by Satz7p13; hence c,a1 equiv c,a by Satz7p10; end; then A12: c,a2 <= c,a by A7,Satz5p6; per cases; suppose A13: a2 = c; then a2 = b2 by A4,Satz2p2,GTARSKI1:def 7; then m2 = a2 by A6,GTARSKI1:def 10; hence thesis by A13,Satz3p1; end; suppose A14: a2 <> c; A15: between c,a2,a proof c out a2,a proof now thus c <> a2 by A14; thus c <> a proof assume c = a; then reflection(c,a1) = reflection(c,c) by Satz7p10; hence contradiction by A11,Satz7p9; end; thus between c,a2,a or between c,a,a2 proof A16: Middle a1,c,a by DEFR; then between a1,a,a2 or between a1,a2,a by A1,A11,Satz5p1; hence thesis by A1,A16,Satz3p6p1; end; end; hence thesis; end; hence thesis by A12,Satz6p13; end; A17: between c,b2,b proof per cases; suppose c = b2; hence thesis by A14,A4,GTARSKI1:def 7; end; suppose A18: c <> b2; A19: c,b2 <= c,b1 by A3,A4,A7,Satz5p6; c,b1 equiv reflection(c,c),reflection(c,b1) by Satz7p13; then c,b1 equiv c,b & c,b2 equiv c,b2 by Satz2p1,Satz7p10; then A20: c,b2 <= c,b by A19,Satz5p6; A21: b1 <> c by A11,A3,GTARSKI1:def 7; c out b2,b proof now thus c <> b2 by A18; thus c <> b proof assume c = b; then reflection(c,b1) = reflection(c,c) by Satz7p10; hence contradiction by A21,Satz7p9; end; thus (between c,b2,b or between c,b,b2) proof A22: Middle b1,c,b by DEFR; then per cases by A2,A21,Satz5p1; suppose between b1,b,b2; hence thesis by A22,Satz3p6p1; end; suppose between b1,b2,b; hence thesis by A2,Satz3p6p1; end; end; end; hence thesis; end; hence thesis by A20,Satz6p13; end; end; between a,a2,c & between b,b2,c & between a,m,b by A5,Satz7p15,A15,Satz3p2,A17; then consider q be POINT of S such that A23: between m,q,c and A24: between a2,q,b2 by Satz3p17; A25: between m,c,m1 proof Middle m1,c,m by DEFR; hence thesis by Satz3p2; end; q = m2 proof a,a2,c,m IFS b,b2,c,m proof now thus between a,a2,c by A15,Satz3p2; thus between b,b2,c by A17,Satz3p2; reflection(c,c),reflection(c,a1) equiv reflection(c,c),reflection(c,b1) by A3,Satz7p16; then c,reflection(c,a1) equiv reflection(c,c),reflection(c,b1) by Satz7p10; then c,a equiv c,b by Satz7p10; then c,a equiv b,c by Satz2p5; hence a,c equiv b,c by Satz2p4; c,a2 equiv b2,c by A4,Satz2p5; hence a2,c equiv b2,c by Satz2p4; m1,a1 equiv b1,m1 by A5,Satz2p5; then a1,m1 equiv b1,m1 by Satz2p4; hence a,m equiv b,m by Satz7p16; thus c,m equiv c,m by Satz2p1; end; hence thesis; end; then a2,m equiv b2,m by Satz4p2; then A26: a2,m equiv m,b2 by Satz2p5; then A27: m,a2 equiv m,b2 by Satz2p4; q,a2 equiv q,b2 proof per cases; suppose A28: m <> c; Collinear c,m,q by A23; hence thesis by A4,A27,A28,Satz4p17; end; suppose m = c; then q = m by A23,GTARSKI1:def 10; hence thesis by A26,Satz2p4; end; end; then Middle a2,q,b2 by A24; hence thesis by A6,Satz7p17; end; then between m2,c,m1 by A25,A23,Satz3p6p1; hence thesis by Satz3p2; end; end; end; ::\$N 7.22 Satz: Krippenlemma, (Gupta 1965, 3.45 Theorem) theorem Satz7p22: 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 proof assume that A1: between a1,c,a2 and A2: between b1,c,b2 and A3: c,a1 equiv c,b1 and A4: c,a2 equiv c,b2 and A5: Middle a1,m1,b1 and A6: Middle a2,m2,b2; per cases by Satz5p10; suppose c,a1 <= c,a2; hence thesis by A1,A2,A3,A4,A5,A6,Satz7p22part1; end; suppose c,a2 <= c,a1; hence thesis by A1,A2,A3,A4,A5,A6,Satz7p22part2; end; 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 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 Krippenfigur a1,m1,b1,c,b2,m2,a2 implies between m1,c,m2 by Satz7p22; registration cluster non empty for satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct; existence by GTARSKI2:def 2; 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 c,a equiv c,b implies ex x being POINT of S st Middle a,x,b proof assume A1: c,a equiv c,b; per cases; suppose Collinear a,b,c; then Collinear a,c,b by Satz3p2; then per cases by A1,Satz7p20; suppose A2: a = b; take a; thus thesis by A2,Satz3p1,Satz2p1; end; suppose Middle a,c,b; hence thesis; end; end; suppose A3: not Collinear a,b,c; consider p such that A4: between c,a,p and A5: a <> p by Satz3p14; consider q such that A6: between c,b,q and A7: b,q equiv a,p by GTARSKI1:def 8; between p,a,c & between q,b,c by A4,A6,Satz3p2; then consider r such that A8: between a,r,q and A9: between b,r,p by GTARSKI1:def 11; consider x be POINT of S such that A10: between a,x,b and A11: between r,x,c by A4,A9,GTARSKI1:def 11; take x; x,a equiv x,b proof A12: r,a equiv r,b proof A13: c,a,p,b AFS c,b,q,a by A4,A6,A1,A7,GTARSKI1:def 5,Satz2p2; c <> a by A3,Satz3p1; then A15: p,b equiv a,q by Satz2p5,A13,Axiom5AFS; thesis proof consider r9 be POINT of S such that A19: between a,r9,q and A20: b,r,p cong a,r9,q by A15,Satz2p4,A9,Satz4p5; A21: now b,q equiv p,a by A7,Satz2p5; then q,b equiv p,a by Satz2p4; hence b,r,p,a IFS a,r9,q,b by A9,A19,A20,Satz2p2,GTARSKI1:def 5; thus b,r,p,q IFS a,r9,q,p by A9,A19,A20,GTARSKI1:def 5,A7; end; then r,a equiv b,r9 by Satz2p5,Satz4p2; then A23: a,r,q cong b,r9,p by A21,Satz2p4,Satz2p2,Satz4p2; now thus Collinear a,r,q by A8; hence Collinear b,r9,p by A23,Satz4p13; end; then Collinear a,q,r & Collinear b,p,r9 by Satz3p2; then A24: r in Line(a,q) & r9 in Line(b,p); A25: r9 in Line(a,q) & r in Line(b,p) proof Collinear a,q,r9 by A19,Satz3p2; hence r9 in Line(a,q); Collinear b,p,r by A9,Satz3p2; hence r in Line(b,p); end; A26: a = q iff b = p by A15,Satz2p2,GTARSKI1:def 7; r = r9 proof per cases; suppose A27: a = q or b = p; then A28: a = r by A8,A26,GTARSKI1:def 10; between a,r9,a by A19,A27,A15,Satz2p2,GTARSKI1:def 7; hence thesis by A28,GTARSKI1:def 10; end; suppose A29: a <> q & b <> p; assume A30: r <> r9; reconsider A = Line(a,q), B = Line(b,p) as Subset of S; A31: A is_line & B is_line by A29; then A32: A = B by A30,A24,A25,Satz6p19; A33: a <> b by A3,Satz3p1; A34: A = Line(a,b) proof b in A & a in A & A is_line by A29,A32,Satz6p17; hence thesis by A33,Satz6p18; end; A35: Line(a,p) = A proof A36: a in A by Satz6p17; p in B by Satz6p17; then p in A & A is_line by A31,A30,A24,A25,Satz6p19; hence Line(a,p) = A by A36,A5,Satz6p18; end; c in A proof Collinear a,p,c by A4; hence thesis by A35; end; then ex y be POINT of S st c = y & Collinear a,b,y by A34; hence contradiction by A3; end; end; hence thesis by A21,Satz4p2; end; hence thesis; end; per cases; suppose r = c; then r = x by A11,GTARSKI1:def 10; hence thesis by A12; end; suppose A37: r <> c; Collinear c,r,x & c,a equiv c,b & r,a equiv r,b by A11,A1,A12; hence thesis by A37,Satz4p17; end; end; hence thesis by A10; end; end; begin :: Note about Makarios's simplification of Tarski's axiom of geometry definition let S be TarskiGeometryStruct; attr S is (RE) means for a,b being POINT of S holds a,b equiv b,a; attr S is (TE) means 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 for a,b,c being POINT of S st a,b equiv c,c holds a = b; attr S is (SC) means 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 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 for a,b being POINT of S st between a,b,a holds a = b; attr S is (Pa) means 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 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 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 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 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 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 S is satisfying_CongruenceSymmetry iff S is (RE); theorem S is satisfying_CongruenceEquivalenceRelation iff S is (TE); theorem S is satisfying_CongruenceIdentity iff S is (IE); theorem S is satisfying_SegmentConstruction iff S is (SC); theorem S is satisfying_BetweennessIdentity iff S is (IB); theorem S is satisfying_Pasch iff S is (Pa); theorem S is satisfying_Lower_Dimension_Axiom iff S is (Lo2); theorem S is satisfying_Upper_Dimension_Axiom iff S is (Up2); theorem S is satisfying_Euclid_Axiom iff S is (Eu); theorem for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds S is satisfying_SAS iff S is (FS) proof let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct; hereby assume S is satisfying_SAS; then S is satisfying_SST_A5; hence S is (FS); end; assume S is (FS); then S is satisfying_SST_A5; hence S is satisfying_SAS; end; theorem ThMak1: for S being non empty TarskiGeometryStruct holds S is satisfying_Continuity_Axiom iff S is (Co) proof let S be non empty TarskiGeometryStruct; hereby assume A1: S is satisfying_Continuity_Axiom; now let X,Y be set; reconsider X9 = X /\ the carrier of S, Y9 = Y /\ the carrier of S as Subset of S by XBOOLE_1:17; assume 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); then consider a be POINT of S such that A3: (for x,y being POINT of S st x in X & y in Y holds between a,x,y); for x,y be POINT of S st x in X9 & y in Y9 holds between a,x,y proof let x,y be POINT of S; assume x in X9 & y in Y9; then x in X & y in Y by XBOOLE_0:def 4; hence thesis by A3; end; then consider b be POINT of S such that A4: for x,y be POINT of S st x in X9 & y in Y9 holds between x,b,y by A1; for x,y be POINT of S st x in X & y in Y holds between x,b,y proof let x,y be POINT of S; assume x in X & y in Y; then x in X9 & y in Y9 by XBOOLE_0:def 4; hence thesis by A4; end; hence 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); end; hence S is (Co); end; assume S is (Co); hence S is satisfying_Continuity_Axiom; end; registration cluster (RE) -> satisfying_CongruenceSymmetry for TarskiGeometryStruct; coherence; cluster (TE) -> satisfying_CongruenceEquivalenceRelation for TarskiGeometryStruct; coherence; cluster (IE) -> satisfying_CongruenceIdentity for TarskiGeometryStruct; coherence; cluster (SC) -> satisfying_SegmentConstruction for TarskiGeometryStruct; coherence; cluster (IB) -> satisfying_BetweennessIdentity for TarskiGeometryStruct; coherence; cluster (Pa) -> satisfying_Pasch for TarskiGeometryStruct; coherence; cluster (Lo2) -> satisfying_Lower_Dimension_Axiom for TarskiGeometryStruct; coherence; cluster (Up2) -> satisfying_Upper_Dimension_Axiom for TarskiGeometryStruct; coherence; cluster (Eu) -> satisfying_Euclid_Axiom for TarskiGeometryStruct; coherence; cluster (Co) -> satisfying_Continuity_Axiom for TarskiGeometryStruct; coherence; end; registration cluster satisfying_CongruenceSymmetry -> (RE) for TarskiGeometryStruct; coherence; cluster satisfying_CongruenceEquivalenceRelation -> (TE) for TarskiGeometryStruct; coherence; cluster satisfying_CongruenceIdentity -> (IE) for TarskiGeometryStruct; coherence; cluster satisfying_SegmentConstruction -> (SC) for TarskiGeometryStruct; coherence; cluster satisfying_BetweennessIdentity -> (IB) for TarskiGeometryStruct; coherence; cluster satisfying_Pasch -> (Pa) for TarskiGeometryStruct; coherence; cluster satisfying_Lower_Dimension_Axiom -> (Lo2) for TarskiGeometryStruct; coherence; cluster satisfying_Upper_Dimension_Axiom -> (Up2) for TarskiGeometryStruct; coherence; cluster satisfying_Euclid_Axiom -> (Eu) for TarskiGeometryStruct; coherence; cluster satisfying_Continuity_Axiom -> (Co) for non empty TarskiGeometryStruct; coherence by ThMak1; end; registration cluster (RE) (TE) for TarskiGeometryStruct; existence proof TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation; hence thesis; end; end; theorem ThMak2: for S being (RE) (TE) TarskiGeometryStruct holds S is satisfying_SAS iff S is (FS) proof let S be (RE) (TE) TarskiGeometryStruct; hereby assume S is satisfying_SAS; then S is satisfying_SST_A5; hence S is (FS); end; assume S is (FS); then S is satisfying_SST_A5; hence S is satisfying_SAS; end; registration cluster (FS) -> satisfying_SAS for (RE) (TE) TarskiGeometryStruct; coherence by ThMak2; end; registration cluster (FS) for (RE) (TE) TarskiGeometryStruct; existence proof TarskiEuclid2Space is (FS) by ThMak2; hence thesis; end; end; reserve S for TarskiGeometryStruct; ::\$N Makarios: Lemma 6 theorem ThMak3: for S being TarskiGeometryStruct st S is (RE) & S is (TE) holds (S is (FS) iff S is (FS')) proof let S be TarskiGeometryStruct; assume that A1: S is (RE) and A2: S is (TE); hereby assume A3: S is (FS); thus S is (FS') proof let a,b,c,d,a9,b9,c9,d9 be POINT of S; assume 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; then c,d equiv c9,d9 & c,d equiv d,c by A1,A3; hence d,c equiv c9,d9 by A2; end; end; assume A4: S is (FS'); let a,b,c,d,a9,b9,c9,d9 be POINT of S; assume 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; then d,c equiv c9,d9 & d,c equiv c,d by A1,A4; hence c,d equiv c9,d9 by A2; end; theorem for S being (RE) (TE) TarskiGeometryStruct holds S is (FS) iff S is (FS') by ThMak3; registration cluster (FS') -> (FS) for (RE) (TE) TarskiGeometryStruct; coherence by ThMak3; end; registration cluster (TE) (SC) for TarskiGeometryStruct; existence proof TarskiEuclid2Space is (SC); hence thesis; end; end; registration cluster (FS') for (RE) (TE) TarskiGeometryStruct; existence proof TarskiEuclid2Space is (FS) by ThMak2; then TarskiEuclid2Space is (FS') by ThMak3; hence thesis; end; end; registration cluster (SC) for (RE) (TE) (FS') TarskiGeometryStruct; existence proof TarskiEuclid2Space is (FS) by ThMak2; then TarskiEuclid2Space is (RE) (TE) (FS') by ThMak3; hence thesis; end; end; theorem for S being (TE) (SC) TarskiGeometryStruct holds for a,b being POINT of S holds a,b equiv a,b by Satz2p1bis; theorem for S being (IE) (SC) TarskiGeometryStruct holds for a,b being POINT of S holds between a,b,b by Satz3p1; theorem 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 by Satz2p2bis; theorem ThMak4: 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) proof let S be (TE) (SC) (FS') TarskiGeometryStruct; let a,b,c,d,e,f be POINT of S; assume A1: 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; A2: a,f equiv a,f by Satz2p1bis; S is (FS'); hence thesis by A1,A2; end; definition let S be TarskiGeometryStruct; attr S is (RE') means for a,b,c,d being POINT of S st a <> b & between b,a,c holds d,c equiv c,d; end; theorem ThMak5: for S being (TE) (SC) (FS') TarskiGeometryStruct holds S is (RE') proof let S be (TE) (SC) (FS') TarskiGeometryStruct; let a,b,c,d be POINT of S; assume A1: a <> b & between b,a,c; a,c equiv a,c & b,a equiv b,a & b,d equiv b,d by Satz2p1bis; hence thesis by A1,ThMak4; end; registration cluster (TE) (SC) (FS') -> (RE') for TarskiGeometryStruct; coherence by ThMak5; end; registration cluster (RE') for (IE) TarskiGeometryStruct; existence proof TarskiEuclid2Space is (FS) by ThMak2; then TarskiEuclid2Space is (RE) (TE) (FS') by ThMak3; hence thesis; end; end; registration cluster (SC) for (RE') (IE) TarskiGeometryStruct; existence proof TarskiEuclid2Space is (FS) by ThMak2; then TarskiEuclid2Space is (RE) (TE) (FS') by ThMak3; hence thesis; end; end; registration cluster trivial for (IE) non empty TarskiGeometryStruct; existence proof TrivialTarskiSpace is (IE); hence thesis; end; end; registration cluster trivial for (IE) (SC) non empty TarskiGeometryStruct; existence proof TrivialTarskiSpace is (IE); hence thesis; end; end; theorem for S being trivial (IE) (SC) non empty TarskiGeometryStruct holds S is (RE) proof let S be trivial (IE) (SC) non empty TarskiGeometryStruct; let a,b be POINT of S; a = b by ZFMISC_1:def 10; hence thesis by Satz2p8; end; registration cluster (RE') for (TE) (IE) (SC) non empty TarskiGeometryStruct; existence proof now TrivialTarskiSpace is (FS) by ThMak2; hence TrivialTarskiSpace is (RE) (TE) (FS') by ThMak3; thus TrivialTarskiSpace is non empty; end; hence thesis; end; end; theorem ThMak6: for S being (RE') (TE) (IE) (SC) non empty TarskiGeometryStruct holds S is (RE) proof let S be (RE') (TE) (IE) (SC) non empty TarskiGeometryStruct; let a,b be POINT of S; per cases; suppose a = b; hence thesis by Satz2p8; end; suppose A1: a <> b; between b,a,a & S is (RE') by Satz3p1; hence thesis by A1,Satz2p2bis; end; end; registration cluster (FS') for (TE) (IE) (SC) non empty TarskiGeometryStruct; existence proof now TrivialTarskiSpace is (FS) by ThMak2; hence TrivialTarskiSpace is (RE) (TE) (FS') by ThMak3; thus TrivialTarskiSpace is non empty; end; hence thesis; end; end; theorem for S being (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds S is (RE) by ThMak6; theorem ThMak7: for S being (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds S is (FS) proof let S be (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct; S is (RE) by ThMak6; hence thesis; end; begin :: Main results and Corollaries ::\$N Main results registration cluster (RE) (TE) (FS) -> (FS') for TarskiGeometryStruct; coherence by ThMak3; end; registration cluster (TE) (IE) (SC) (FS') -> (FS) for non empty TarskiGeometryStruct; coherence by ThMak7; end; registration cluster (TE) (IE) (SC) (FS') -> (RE) for non empty TarskiGeometryStruct; coherence by ThMak6; end; registration cluster (TE) (IE) (SC) (FS') -> satisfying_SAS for non empty TarskiGeometryStruct; coherence; end; registration cluster (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) for non empty TarskiGeometryStruct; existence proof TarskiEuclid2Space is (FS) & TarskiEuclid2Space is (Co) by GTARSKI2:def 2,ThMak2; hence thesis by GTARSKI2:def 2; end; 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 for TP being Makarios_CE2 holds TP is Makarios_CE'2; theorem for TP being Makarios_CE'2 holds TP is Makarios_CE2; theorem 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 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;