:: {T}arski Geometry Axioms -- Part {III}
:: by Roland Coghetto and Adam Grabowski
::
:: Received November 29, 2017
:: Copyright (c) 2017-2026 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 Sazz
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 being POINT of S 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;
::$N 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;