:: Tarski Geometry Axioms -- Part {II}
:: by Roland Coghetto and Adam Grabowski
::
:: Received June 30, 2016
:: Copyright (c) 2016-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 TARSKI, NUMBERS, SUBSET_1, COMPLEX1, REAL_1, RELAT_1, CARD_1,
ARYTM_1, SUPINF_2, XXREAL_2, NAT_1, ARYTM_3, SQUARE_1, XXREAL_0,
XBOOLE_0, RLTOPSP1, PRE_TOPC, MCART_1, EUCLID, INCSP_1, METRIC_1,
SIN_COS, COMPLEX2, PROJPL_1, GTARSKI1, PBOOLE, FINSEQ_2, QC_LANG1,
GTARSKI2, FUNCT_1, ROUGHS_4, RELAT_2, LATTICE3, EUCLIDLP, EUCLID12,
MEMBERED, ORDINAL2, ANALOAF, PASCH, RLVECT_1, ZFMISC_1, DIRAF, PENCIL_1,
PARSP_1;
notations XBOOLE_0, ORDINAL1, SUBSET_1, XXREAL_2, MEMBERED, TARSKI, XCMPLX_0,
NUMBERS, XREAL_0, COMPLEX1, METRIC_1, STRUCT_0, FINSEQ_2, SQUARE_1,
RVSUM_1, PRE_TOPC, XXREAL_0, RLVECT_1, SIN_COS, EUCLID_3, EUCLID_6,
GTARSKI1, EUCLID, BINOP_1, TOPREAL6, ANALOAF, DIRAF, PASCH, EUCLID12,
EUCLIDLP, EUCLID_4, RLTOPSP1;
constructors SQUARE_1, COMPLEX1, MONOID_0, SIN_COS, EUCLID_3, TOPREAL6,
GTARSKI1, SEQ_4, PASCH, DIRAF, EUCLID12, EUCLID_4;
registrations EUCLIDLP, RLTOPSP1, MONOID_0, RELSET_1, XXREAL_0, XREAL_0,
EUCLID, VALUED_0, SQUARE_1, ORDINAL1, SIN_COS, GTARSKI1, XCMPLX_0,
RLVECT_1, STRUCT_0, ZFMISC_1, ANALOAF, XXREAL_2, MEMBERED;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, GTARSKI1, MEMBERED, XXREAL_2;
equalities XBOOLE_0, EUCLID, VALUED_1, XCMPLX_0, RLVECT_1, ANALOAF;
expansions TARSKI, XBOOLE_0, GTARSKI1, SUBSET_1, ANALOAF, DIRAF, PASCH;
theorems XREAL_1, XXREAL_0, ZFMISC_1, XBOOLE_0, XBOOLE_1, EUCLID11, SQUARE_1,
XCMPLX_1, RVSUM_1, TARSKI, EUCLID, RLTOPSP1, EUCLID_6, SIN_COS, EUCLID10,
TOPREAL6, METRIC_1, COMPLEX1, GTARSKI1, TOPREAL3, EUCLID12, XCMPLX_0,
XXREAL_2, ANALOAF, PASCH, RLVECT_1, FINSEQ_1, DIRAF, XTUPLE_0, EUCLIDLP,
TOPREAL9;
begin :: Preliminaries
theorem Th1:
for r,s,t,u being Real st s <> 0 & t <> 0 &
r^2 = s^2 + t^2 - 2*s*t*u holds u = (r^2 - s^2 - t^2)/(-2*s*t)
proof
let r,s,t,u be Real;
assume that
A1: s <> 0 and
A2: t <> 0 and
A3: r^2 = s^2+t^2-2*s*t*u;
r^2-s^2-t^2 = u * (-2*s*t) by A3;
hence thesis by A1,A2,XCMPLX_1:89;
end;
theorem THJE:
for n being Nat
for u,v being Element of TOP-REAL n holds u + 0 * v = u
proof
let n be Nat;
let u,v be Element of TOP-REAL n;
0.TOP-REAL n = 0 * v by RLVECT_1:10;
hence thesis;
end;
theorem THJC:
for n being Nat
for r,s being Real, u,v,w being Element of TOP-REAL n st
r * u - r * v = s * w - s * u holds (r + s) * u = r * v + s * w
proof
let n be Nat;
let r,s be Real, u,v,w be Element of TOP-REAL n;
assume r * u - r * v = s * w - s * u;
then r * u - r * v + s * u = s * w + (- s * u + s * u) by RVSUM_1:15
.= s * w + ((- 1)* s * u + s * u) by RVSUM_1:49
.= s * w + (- s + s) * u by RVSUM_1:50
.= s * w by THJE;
then s * w + r * v = r * u + ((-1)* r * v) + s * u + r * v by RVSUM_1:49
.= r * u + s * u + ((-1)* r * v) + r * v by RVSUM_1:15
.= r * u + s * u + (((-1)* r * v) + r * v) by RVSUM_1:15
.= r * u + s * u + (- r + r) * v by RVSUM_1:50
.= (r * u + s * u) by THJE;
hence thesis by RVSUM_1:50;
end;
theorem THJD:
for r,s being Real st 0 < r & 0 < s holds 0 <= r / (r+s) <= 1
proof
let r,s be Real;
assume that
A1: 0 < r and
A2: 0 < s;
thus 0 <= r/(r+s) by A1,A2;
0 + r <= s + r by A2,XREAL_1:6;
then r / (r+s) <= (r+s) / (r+s) by A1,XREAL_1:72;
hence r / (r+s) <= 1 by A1,A2,XCMPLX_1:60;
end;
theorem Th2:
for a being Real holds cos (3*PI - a) = -cos a
proof
let a be Real;
cos(3*PI - a) = cos (2*PI + (PI -a))
.= cos (PI - a) by SIN_COS:79
.= - cos a by EUCLID10:2;
hence thesis;
end;
theorem THSD2:
for n being Nat
for a,b,c being Element of TOP-REAL n st a - c = b - c holds a = b
proof
let n be Nat;
let a,b,c be Element of TOP-REAL n;
assume a - c = b - c; then
a + (-c + c) = b - c + c by RLVECT_1:def 3; then
a + 0.TOP-REAL n = b - c + c by RLVECT_1:5; then
a = b + (- c + c) by RLVECT_1:def 3; then
a = b + 0.TOP-REAL n by RLVECT_1:5;
hence thesis;
end;
theorem ThWW:
for n being Nat
for a,b,c being Element of TOP-REAL n holds
c - a - (b - a) = c - b
proof
let n be Nat;
let a,b,c be Element of TOP-REAL n;
thus c - a - (b - a) = (c - a) - b + a by RLVECT_1:29
.= c - a + a + - b by RLVECT_1:def 3
.= c + (- a + a) + - b by RLVECT_1:def 3
.= c + 0.TOP-REAL n + - b by RLVECT_1:5
.= c - b;
end;
theorem THYQ:
for a,b,c,d being Real holds dist(|[a,b]|,|[c,d]|) = sqrt ((a-c)^2+(b-d)^2)
proof
let a,b,c,d be Real;
A1: |[a,b]|`1 = a & |[a,b]|`2 = b & |[c,d]|`1 = c & |[c,d]|`2 = d by EUCLID:52;
reconsider P = |[a,b]|,Q = |[c,d]| as Point of Euclid 2
by EUCLID:22;
dist(|[a,b]|,|[c,d]|) = dist(P,Q) by TOPREAL6:def 1
.= (Pitag_dist 2).(P,Q) by METRIC_1:def 1
.= sqrt ((a-c)^2+(b - d)^2) by A1,TOPREAL3:7;
hence thesis;
end;
theorem THY1:
dist(|[0,0]|,|[1,0]|) = 1
proof
dist(|[0,0]|,|[1,0]|) = sqrt ((0-1)^2+(0 - 0)^2) by THYQ
.= sqrt ((-1) * (-1) + 0^2) by SQUARE_1:def 1
.= sqrt (1 + 0 * 0) by SQUARE_1:def 1
.= 1;
hence thesis;
end;
theorem THY2:
dist(|[0,0]|,|[0,1]|) = 1
proof
dist(|[0,0]|,|[0,1]|) = sqrt ((0-0)^2+(0 - 1)^2) by THYQ
.= sqrt (0 * 0 + (-1)^2) by SQUARE_1:def 1
.= sqrt (0 + (-1) * (-1)) by SQUARE_1:def 1
.= 1;
hence thesis;
end;
theorem THY3:
dist(|[1,0]|,|[0,1]|) = sqrt 2
proof
dist(|[1,0]|,|[0,1]|) = sqrt ((1-0)^2+(0 - 1)^2) by THYQ
.= sqrt (1^2+(1)^2) by SQUARE_1:3
.= sqrt (1 * 1 + 1^2) by SQUARE_1:def 1
.= sqrt (1 * 1 + 1 * 1) by SQUARE_1:def 1
.= sqrt 2;
hence thesis;
end;
definition let n be Nat;
func TarskiEuclidSpace n -> MetrTarskiStr equals
the naturally_generated TarskiExtension of Euclid n;
coherence;
end;
definition
func TarskiEuclid2Space -> MetrTarskiStr equals
TarskiEuclidSpace 2;
:: the naturally_generated TarskiExtension of Euclid 2;
coherence;
end;
begin
registration let n be Nat;
cluster TarskiEuclidSpace n -> non empty;
coherence;
end;
registration
cluster TarskiEuclid2Space -> Reflexive symmetric discerning;
coherence;
end;
registration let n be Nat;
cluster TarskiEuclidSpace n -> Reflexive symmetric discerning;
coherence;
end;
definition
let n be Nat;
let P be POINT of TarskiEuclidSpace n;
func Tn2TR P -> Element of TOP-REAL n equals
P;
coherence
proof
the MetrStruct of TarskiEuclidSpace n = the MetrStruct of Euclid n
by GTARSKI1:def 13;
hence thesis by EUCLID:22;
end;
end;
definition
let P be POINT of TarskiEuclid2Space;
func Tn2TR P -> Element of TOP-REAL 2 equals
P;
coherence
proof
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
hence thesis by EUCLID:22;
end;
end;
definition
let P be POINT of TarskiEuclid2Space;
func Tn2E P -> Point of Euclid 2 equals
P;
coherence
proof
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
hence thesis;
end;
end;
definition
let P be POINT of TarskiEuclid2Space;
func Tn2R P -> Element of REAL 2 equals
P;
coherence
proof
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
hence thesis;
end;
end;
theorem ThEquiv:
for n being Nat
for p,q being POINT of TarskiEuclidSpace n,
p1,q1 being Element of TOP-REAL n st p = p1 & q = q1 holds
dist(p,q) = (Pitag_dist n).(p1, q1) & dist(p,q) = |. p1 - q1 .|
proof
let n be Nat;
let p,q be POINT of TarskiEuclidSpace n,
p1,q1 being Element of TOP-REAL n;
assume
A0: p = p1 & q = q1;
A1: the MetrStruct of TarskiEuclidSpace n = the MetrStruct of Euclid n
by GTARSKI1:def 13; then
(Pitag_dist n).(p1, q1) = |. p1 - q1 .| by A0,EUCLID:def 6;
hence thesis by A1,METRIC_1:def 1,A0;
end;
theorem ThLawOfCosines:
for a, b, c being POINT of TarskiEuclid2Space holds
(dist(c,a))^2 = (dist(a,b))^2 + (dist(b,c))^2 - 2 * dist(a,b) *
dist(b,c) * cos angle(Tn2TR a, Tn2TR b, Tn2TR c)
proof
let a, b, c be POINT of TarskiEuclid2Space;
set ta = |.Tn2TR a - Tn2TR b.|, tb = |. Tn2TR c - Tn2TR b .|,
tc = |.Tn2TR c - Tn2TR a.|;
|.Tn2TR a - Tn2TR b.| = dist(a,b) & |. Tn2TR c - Tn2TR b .| = dist(c,b) &
|.Tn2TR c - Tn2TR a.| = dist(c,a) by ThEquiv;
hence thesis by EUCLID_6:7;
end;
theorem
for a,b,c,e,f,g being POINT of TarskiEuclid2Space st
Tn2TR a, Tn2TR b, Tn2TR c is_a_triangle &
angle(Tn2TR a, Tn2TR b, Tn2TR c) < PI &
angle(Tn2TR e, Tn2TR c, Tn2TR a) = angle(Tn2TR b,Tn2TR c,Tn2TR a) / 3 &
angle(Tn2TR c, Tn2TR a, Tn2TR e) = angle(Tn2TR c, Tn2TR a, Tn2TR b) / 3 &
angle(Tn2TR a, Tn2TR b, Tn2TR f) = angle(Tn2TR a, Tn2TR b, Tn2TR c) / 3 &
angle(Tn2TR f, Tn2TR a, Tn2TR b) = angle(Tn2TR c, Tn2TR a, Tn2TR b) / 3 &
angle(Tn2TR b, Tn2TR c, Tn2TR g) = angle(Tn2TR b, Tn2TR c, Tn2TR a) / 3 &
angle(Tn2TR g, Tn2TR b, Tn2TR c) = angle(Tn2TR a, Tn2TR b, Tn2TR c) / 3
holds
dist(f,e) = dist(g,f) & dist(f,e) = dist(e,g) & dist(g,f) = dist(e,g)
proof
let a,b,c,e,f,g be POINT of TarskiEuclid2Space;
assume
A1: Tn2TR a, Tn2TR b, Tn2TR c is_a_triangle &
angle(Tn2TR a, Tn2TR b, Tn2TR c) < PI &
angle(Tn2TR e, Tn2TR c, Tn2TR a) = angle(Tn2TR b,Tn2TR c,Tn2TR a) / 3 &
angle(Tn2TR c, Tn2TR a, Tn2TR e) = angle(Tn2TR c, Tn2TR a, Tn2TR b) / 3 &
angle(Tn2TR a, Tn2TR b, Tn2TR f) = angle(Tn2TR a, Tn2TR b, Tn2TR c) / 3 &
angle(Tn2TR f, Tn2TR a, Tn2TR b) = angle(Tn2TR c, Tn2TR a, Tn2TR b) / 3 &
angle(Tn2TR b,Tn2TR c, Tn2TR g) = angle(Tn2TR b, Tn2TR c, Tn2TR a) / 3 &
angle(Tn2TR g, Tn2TR b, Tn2TR c) = angle(Tn2TR a, Tn2TR b, Tn2TR c) / 3;
|.Tn2TR f - Tn2TR e.| = dist(f,e) & |. Tn2TR g - Tn2TR f .| = dist(g,f) &
|.Tn2TR e - Tn2TR g.| = dist(e,g) by ThEquiv;
hence thesis by A1,EUCLID11:23;
end;
theorem ThConv:
for n being Nat
for p,q being Element of TarskiEuclidSpace n,
p1, q1 being Element of Euclid n st p = p1 & q = q1 holds
dist(p,q) = dist(p1, q1)
proof
let n be Nat;
let p,q be Element of TarskiEuclidSpace n;
let p1,q1 be Element of Euclid n;
assume
A1: p = p1 & q = q1;
thus dist(p,q) = (the distance of the MetrStruct of
TarskiEuclidSpace n).(p,q) by METRIC_1:def 1
.= (the distance of the MetrStruct of Euclid n).(p,q)
by GTARSKI1:def 13
.= dist(p1,q1) by METRIC_1:def 1,A1;
end;
theorem ThConv2:
for p,q being POINT of TarskiEuclid2Space holds
dist(p,q) =
sqrt(((Tn2TR p)`1-(Tn2TR q)`1)^2 + (((Tn2TR p)`2-(Tn2TR q)`2)^2))
proof
let p,q be POINT of TarskiEuclid2Space;
A1: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
(Pitag_dist 2).(Tn2E p, Tn2E q) =
sqrt(( (Tn2TR p)`1 - (Tn2TR q)`1)^2 + ( (Tn2TR p)`2
- (Tn2TR q)`2)^2) by TOPREAL3:7;
hence thesis by A1,METRIC_1:def 1;
end;
theorem ThConv3:
for A,B being POINT of TarskiEuclid2Space holds
dist(A,B) = |. Tn2TR A - Tn2TR B .| & dist(A,B) = |. Tn2R A - Tn2R B .|
proof
let A,B be POINT of TarskiEuclid2Space;
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
then dist(A,B) = (Pitag_dist 2).(Tn2TR A, Tn2TR B) by METRIC_1:def 1
.= |. Tn2R A - Tn2R B .| by EUCLID:def 6;
hence thesis;
end;
theorem ThConv4:
for a,b,c,d being POINT of TarskiEuclid2Space holds
|. Tn2TR a - Tn2TR b .| = |. Tn2TR c - Tn2TR d .| iff a,b equiv c,d
proof
let a,b,c,d be POINT of TarskiEuclid2Space;
A1: dist(a,b) = |. Tn2TR a - Tn2TR b .| &
dist(c,d) = |. Tn2TR c - Tn2TR d .| by ThConv3;
thus |. Tn2TR a - Tn2TR b .|= |. Tn2TR c - Tn2TR d .| implies a,b equiv c,d
by A1,GTARSKI1:def 15;
assume a,b equiv c,d;
hence thesis by A1,GTARSKI1:def 15;
end;
theorem ThConv5:
for p,q,r being POINT of TarskiEuclid2Space holds
p is_Between q,r iff Tn2TR p in LSeg(Tn2TR q, Tn2TR r)
proof
let p,q,r be POINT of TarskiEuclid2Space;
A1: dist(Tn2TR q,Tn2TR p) = dist(Tn2E q,Tn2E p) &
dist(Tn2TR p,Tn2TR r)=dist(Tn2E p,Tn2E r) & dist(Tn2TR q, Tn2TR r)
= dist(Tn2E q,Tn2E r) by TOPREAL6:def 1;
dist(q,p) = dist(Tn2E q,Tn2E p) & dist(p,r)=dist(Tn2E p,Tn2E r) &
dist(q,r)=dist(Tn2E q,Tn2E r) by ThConv;
hence thesis by A1,EUCLID12:12;
end;
reserve n for Nat;
theorem ThConv6:
for p,q,r being POINT of TarskiEuclid2Space holds
between p,q,r iff Tn2TR q in LSeg(Tn2TR p, Tn2TR r)
proof
let p,q,r be POINT of TarskiEuclid2Space;
hereby
assume between p,q,r;
then q is_Between p,r by GTARSKI1:def 15;
hence Tn2TR q in LSeg(Tn2TR p,Tn2TR r) by ThConv5;
end;
assume Tn2TR q in LSeg(Tn2TR p, Tn2TR r);
then q is_Between p,r by ThConv5;
hence thesis by GTARSKI1:def 15;
end;
theorem ThConv7:
for a,b being Point of TarskiEuclid2Space holds
between a,a,b & between a,b,b
proof
let a,b be Point of TarskiEuclid2Space;
Tn2TR a in LSeg(Tn2TR a,Tn2TR b) by RLTOPSP1:68;
hence between a,a,b by ThConv6;
Tn2TR b in LSeg(Tn2TR a,Tn2TR b) by RLTOPSP1:68;
hence between a,b,b by ThConv6;
end;
theorem ThConv7bis:
for a,b,c being Point of TarskiEuclid2Space st
between a,b,c holds between c,b,a
proof
let a,b,c be Point of TarskiEuclid2Space;
assume between a,b,c;
then Tn2TR b in LSeg(Tn2TR a,Tn2TR c) by ThConv6;
hence thesis by ThConv6;
end;
theorem ThConv7ter:
for a,b being Point of TarskiEuclid2Space st between a,b,a holds a = b
proof
let a,b be Point of TarskiEuclid2Space;
assume between a,b,a;
then Tn2TR b in LSeg(Tn2TR a,Tn2TR a) by ThConv6;
then Tn2TR b in { Tn2TR a } by RLTOPSP1:70;
hence thesis by TARSKI:def 1;
end;
theorem ThEgal:
for a, b being POINT of TarskiEuclid2Space holds a = b iff dist(a,b) = 0
proof
let a, b be POINT of TarskiEuclid2Space;
hereby
assume a = b;
then Tn2R a = Tn2R b;
then 0 = |. Tn2TR a - Tn2TR b .|;
hence dist(a,b) = 0 by ThEquiv;
end;
assume dist(a,b) = 0;
hence thesis by METRIC_1:2;
end;
theorem ThNull:
for a,b,c,d being POINT of TarskiEuclid2Space st
dist(a,b) + dist(c,d) = 0 holds a = b & c = d
proof
let a,b,c,d be POINT of TarskiEuclid2Space;
assume
A1: dist(a,b) + dist(c,d) = 0;
0 <= dist(a,b) & 0 <= dist(c,d) by METRIC_1:5;
then dist(a,b) = 0 & dist(c,d) = 0 by A1;
hence thesis by ThEgal;
end;
theorem
for a,b,c,a1,b1,c1 being POINT of TarskiEuclid2Space holds
a,b,c cong a1,b1,c1 iff (dist(a,b) = dist(a1,b1) &
dist(a,c) = dist(a1,c1) & dist(b,c) = dist(b1,c1)) by GTARSKI1:def 15;
theorem ThConv8:
for a,b,c being POINT of TarskiEuclid2Space holds
between a,b,c iff dist(a,c) = dist(a,b) + dist(b,c)
proof
let a,b,c be POINT of TarskiEuclid2Space;
hereby assume between a,b,c;
then b is_Between a,c by GTARSKI1:def 15;
hence dist(a,c) = dist(a,b) + dist(b,c);
end;
assume dist(a,c) = dist(a,b) + dist(b,c);
then b is_Between a,c;
hence thesis by GTARSKI1:def 15;
end;
theorem ThConv9:
for a,b,c,d being POINT of TarskiEuclid2Space holds
dist(a,b)^2 = dist(c,d)^2 iff a,b equiv c,d
proof
let a,b,c,d be POINT of TarskiEuclid2Space;
hereby
assume
A1: dist(a,b)^2 = dist(c,d)^2;
sqrt dist(a,b)^2 = dist(a,b) & sqrt dist(c,d)^2 = dist(c,d)
by METRIC_1:5,SQUARE_1:22;
hence a,b equiv c,d by A1,GTARSKI1:def 15;
end;
assume a,b equiv c,d;
hence thesis by GTARSKI1:def 15;
end;
theorem
for a being Point of TarskiEuclid2Space holds between a,a,a by ThConv7;
ThCongruenceSymmetry:
TarskiEuclid2Space is satisfying_CongruenceSymmetry
proof
for a,b being POINT of TarskiEuclid2Space holds a,b equiv b,a
proof
let a,b be POINT of TarskiEuclid2Space;
dist(a,b) = dist(b,a);
hence thesis by GTARSKI1:def 15;
end;
hence thesis;
end;
ThCongruenceEquivalenceRelation:
TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation
proof
let a, b, p, q, r, s be POINT of TarskiEuclid2Space;
assume a,b equiv p,q & a,b equiv r,s; then
dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) by GTARSKI1:def 15;
hence thesis by GTARSKI1:def 15;
end;
ThCongruenceIdentity:
TarskiEuclid2Space is satisfying_CongruenceIdentity
proof
let a, b, c be POINT of TarskiEuclid2Space;
assume a,b equiv c,c; then
dist (a,b) = dist (c,c) by GTARSKI1:def 15;
hence thesis by METRIC_1:2,1;
end;
ThSegmentConstruction:
TarskiEuclid2Space is satisfying_SegmentConstruction
proof
A1: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
let a, q, b, c be POINT of TarskiEuclid2Space;
per cases;
suppose
A1bis: a = q;
now
set alpha = |. Tn2TR b - Tn2TR c .|;
reconsider P = |[alpha,0]| as Element of TOP-REAL 2;
reconsider x = |[ (Tn2TR a)`1 + alpha, (Tn2TR a)`2 ]| as POINT of
TarskiEuclid2Space by A1,EUCLID:67;
A2: (Tn2TR x)`1 = (Tn2TR a)`1 + alpha & (Tn2TR x)`2 = (Tn2TR a)`2
by EUCLID:52;
A3: |. Tn2TR a - Tn2TR x .| = dist(a,x) by ThEquiv
.= sqrt(((Tn2TR a)`1 -
((Tn2TR a)`1 + alpha))^2 +
((Tn2TR a)`2 - (Tn2TR a)`2)^2) by A2,ThConv2
.= sqrt((0 - alpha)^2 + 0 * 0) by SQUARE_1:def 1
.= sqrt(alpha^2) by SQUARE_1:3
.= alpha by SQUARE_1:22;
take x;
thus between q,a,x by A1bis,ThConv7;
thus a,x equiv b,c by A3,ThConv4;
end;
hence thesis;
end;
suppose
A4: a <> q;
A5: b = c implies thesis
proof
assume
A6: b = c;
set x = a;
thus ex x being POINT of TarskiEuclid2Space st between q,a,x &
a,x equiv b,c
proof
take x;
A7: Tn2R a = Tn2R x;
Tn2R b = Tn2R c by A6;
then |. Tn2TR b - Tn2TR c .| = 0;
then |. Tn2TR a - Tn2TR x .| = |. Tn2TR b - Tn2TR c .| by A7;
hence thesis by ThConv7,ThConv4;
end;
end;
b <> c implies thesis
proof
assume b <> c;
then Tn2R b <> Tn2R c;
then reconsider alpha = |. Tn2TR b - Tn2TR c .| as positive Real
by EUCLID:17;
Tn2R a <> Tn2R q by A4;
then reconsider mu = |. Tn2TR a - Tn2TR q .| as positive Real
by EUCLID:17;
reconsider nu = alpha / mu as positive Real;
reconsider y = |[ (Tn2TR a)`1 + nu * ((Tn2TR a)`1 -
(Tn2TR q)`1), (Tn2TR a)`2 +
nu * ((Tn2TR a)`2 - (Tn2TR q)`2)]| as POINT of TarskiEuclid2Space
by A1,EUCLID:67;
reconsider x = Tn2TR a + nu * (Tn2TR a - Tn2TR q)
as POINT of TarskiEuclid2Space by A1,EUCLID:67;
ex x being POINT of TarskiEuclid2Space st between q,a,x &
a,x equiv b,c
proof
take x;
reconsider t1 = (-nu*(Tn2TR a -Tn2TR q)), t2 = Tn2TR a
as Element of 2-tuples_on REAL by EUCLID:22;
Tn2TR a - Tn2TR x = Tn2TR a + (-Tn2TR a + - nu * (Tn2TR a -
Tn2TR q)) by RVSUM_1:26
.= t1 + t2 - t2 by RVSUM_1:15
.= - nu * (Tn2TR a - Tn2TR q) by RVSUM_1:42; then
A8: |. Tn2TR a - Tn2TR x .| = |. nu * (Tn2TR a - Tn2TR q).|
by EUCLID:10
.= |. nu .| * |.Tn2TR a - Tn2TR q.| by EUCLID:11
.= alpha / mu * mu by COMPLEX1:43
.= alpha by XCMPLX_1:87;
reconsider aq = Tn2TR a - Tn2TR q, qa = Tn2TR q - Tn2TR a
as Element of 2-tuples_on REAL by EUCLID:22;
A9: Tn2TR q - Tn2TR x = Tn2TR q + ( - Tn2TR a +
- nu * (Tn2TR a - Tn2TR q)) by RVSUM_1:26
.= - nu *(Tn2TR a - Tn2TR q) + (--Tn2TR q + -Tn2TR a)
by RVSUM_1:15
.= - nu *(Tn2TR a - Tn2TR q) - (-Tn2TR q + Tn2TR a)
by RVSUM_1:26
.= ((-1) * nu) * aq + (-1) * aq by RVSUM_1:49
.= (-1 - nu) * (Tn2TR a - Tn2TR q) by RVSUM_1:50;
|. Tn2TR q - Tn2TR x .| =
|. -(1 + nu) .| * |. Tn2TR a - Tn2TR q.| by A9,EUCLID:11
.= |. 1 + nu .| * |. Tn2TR a - Tn2TR q.|
by COMPLEX1:52
.= (1 + nu) * |. Tn2TR a - Tn2TR q.| by COMPLEX1:43
.= mu + alpha / mu * mu
.= mu + alpha by XCMPLX_1:87; then
|. Tn2TR q - Tn2TR x .| =
|. Tn2R q - Tn2R a .| + |. Tn2TR a - Tn2TR x .|
by A8,EUCLID:18
.= |. Tn2TR q - Tn2TR a .| + |. Tn2TR a - Tn2TR x .|;
then
Tn2TR a in LSeg(Tn2TR q, Tn2TR x) by EUCLID12:11;
hence thesis by ThConv6,A8,ThConv4;
end;
hence thesis;
end;
hence thesis by A5;
end;
end;
ThSAS:
TarskiEuclid2Space is satisfying_SAS
proof
set TP = TarskiEuclid2Space;
let a, b, c, x, a1, b1, c1, x1 be POINT of TP;
assume that
A1: a <> b and
A2: a,b,c cong a1,b1,c1 and
A3: between a,b,x and
A4: between a1,b1,x1 and
A5: b,x equiv b1,x1;
A6: (dist(a,b) = dist(a1,b1) & dist(a,c) = dist(a1,c1) &
dist(b,c) = dist(b1,c1)) by A2,GTARSKI1:def 15;
A7: dist(a,x) = dist(a,b)+dist(b,x) by A3,ThConv8;
A8: dist(a1,x1) = dist(a1,b1)+dist(b1,x1) by A4,ThConv8;
A9: dist(b,x) = dist(b1,x1) by A5,GTARSKI1:def 15;
A10: (dist(c1,x1))^2 = (dist(x1,b1))^2 + (dist(c1,b1))^2 -
2 * dist(x1,b1) * dist(c1,b1) * cos angle(Tn2TR x1, Tn2TR b1, Tn2TR c1)
by ThLawOfCosines;
dist(c,x)^2 = dist(c1,x1)^2
proof
per cases;
suppose x = b; then
A11: 0 = dist(x,b) by ThEgal; then
A12: dist(x1,b1) = 0 by A5,GTARSKI1:def 15;
A12bis: dist(c,x)^2 = 0^2 + dist(c,b)^2 - 2 * 0 * dist(c,b) *
cos angle(Tn2TR x,Tn2TR b,Tn2TR c) by A11,ThLawOfCosines
.= 0 * 0 + dist(c,b)^2 by SQUARE_1:def 1;
dist(c1,x1)^2 = 0^2 + dist(c1,b1)^2 - 2 * 0 * dist(c1,b1) *
cos angle(Tn2TR x1,Tn2TR b1,Tn2TR c1) by ThLawOfCosines,A12
.= 0 * 0 + dist(c1,b1)^2 by SQUARE_1:def 1;
hence thesis by A12bis,A2,GTARSKI1:def 15;
end;
suppose
A13: c = b;
then 0 = dist(c,b) by ThEgal;
then dist(c1,b1) = 0 by A2,GTARSKI1:def 15;
then dist(c1,x1)^2 = 0 * 0 + dist(x1,b1)^2 by A10,SQUARE_1:def 1;
hence thesis by A13,A5,GTARSKI1:def 15;
end;
suppose
A14: x <> b & c <> b;
A15: a <> x
proof
assume a = x;
then dist(a,b) + dist(b,x) = 0 by A7,ThEgal;
hence contradiction by A1,ThNull;
end;
dist(a,b) <> 0 & dist(a,x) <>0 & dist(b,x) <>0 by A1,A14,A15,ThEgal;
then
A16: Tn2TR a1 <> Tn2TR b1 & Tn2TR a1 <> Tn2TR x1 & Tn2TR b1 <> Tn2TR x1
by ThEgal,A6,A7,A8,A9;
Tn2TR b in LSeg(Tn2TR a,Tn2TR x ) by A3,ThConv6;
then angle(Tn2TR a,Tn2TR b,Tn2TR c ) +
angle(Tn2TR c,Tn2TR b,Tn2TR x ) = PI or
angle(Tn2TR a,Tn2TR b,Tn2TR c ) + angle(Tn2TR c,Tn2TR b,Tn2TR x ) =
3 * PI by A1,A14,EUCLID_6:13;
then cos angle (Tn2TR a,Tn2TR b,Tn2TR c ) =
cos (PI - angle(Tn2TR c,Tn2TR b,Tn2TR x))
or cos angle (Tn2TR a,Tn2TR b,Tn2TR c ) =
cos (3 * PI - angle(Tn2TR c,Tn2TR b,Tn2TR x)); then
A17: cos angle (Tn2TR a,Tn2TR b,Tn2TR c ) =
- cos (angle(Tn2TR c,Tn2TR b,Tn2TR x))
by Th2,EUCLID10:2;
Tn2TR b1 in LSeg(Tn2TR a1,Tn2TR x1 ) by A4,ThConv6;
then angle(Tn2TR a1,Tn2TR b1,Tn2TR c1 ) +
angle(Tn2TR c1,Tn2TR b1,Tn2TR x1 ) = PI or
angle(Tn2TR a1,Tn2TR b1,Tn2TR c1 ) +
angle(Tn2TR c1,Tn2TR b1,Tn2TR x1 ) = 3 * PI
by A16,EUCLID_6:13;
then cos angle (Tn2TR a1,Tn2TR b1,Tn2TR c1 ) =
cos (PI - angle(Tn2TR c1,Tn2TR b1,Tn2TR x1))
or cos angle (Tn2TR a1,Tn2TR b1,Tn2TR c1 ) =
cos (3 * PI - angle(Tn2TR c1,Tn2TR b1,Tn2TR x1));
then
A18: cos angle (Tn2TR a1,Tn2TR b1,Tn2TR c1 ) =
- cos (angle(Tn2TR c1,Tn2TR b1,Tn2TR x1)) by Th2,EUCLID10:2;
A19: dist(a,b) <> 0 & dist(c,b) <> 0 by A1,A14,ThEgal;
A20: dist(c,a)^2 = dist(a,b)^2+dist(c,b)^2 - 2*dist(a,b)*dist(c,b) *
cos angle(Tn2TR a,Tn2TR b,Tn2TR c) by ThLawOfCosines;
A21: dist(a1,b1) <> 0 & dist(c1,b1) <> 0 by A1,A6,A14,ThEgal;
dist(c1,a1)^2 = dist(a1,b1)^2+dist(c1,b1)^2 -
2*dist(a1,b1)*dist(c1,b1) *
cos angle(Tn2TR a1,Tn2TR b1,Tn2TR c1) by ThLawOfCosines; then
A22: cos angle(Tn2TR a1,Tn2TR b1,Tn2TR c1)
= (dist(c,a)^2-dist(a,b)^2-dist(c,b)^2)/(-2*dist(a,b)*dist(c,b))
by A6,Th1,A21
.= cos angle(Tn2TR a,Tn2TR b,Tn2TR c) by A20,A19,Th1;
(dist(c,x))^2 = (dist(x,b))^2 + (dist(c,b))^2 - 2 * dist(x,b) *
dist(c,b) * cos angle(Tn2TR x, Tn2TR b, Tn2TR c)
by ThLawOfCosines
.= (dist(x1,b1))^2 + (dist(c1,b1))^2 - 2 * dist(x1,b1) *
dist(c1,b1) *
(-cos angle(Tn2TR a1, Tn2TR b1, Tn2TR c1))
by A17,EUCLID_6:3,A6,A9,A22
.= (dist(x1,b1))^2 + (dist(c1,b1))^2 - 2 * dist(x1,b1) *
dist(c1,b1) *
cos angle(Tn2TR x1, Tn2TR b1, Tn2TR c1)
by A18,EUCLID_6:3
.= (dist(c1,x1))^2 by ThLawOfCosines;
hence thesis;
end;
end;
hence thesis by ThConv9;
end;
ThBetweennessIdentity:
TarskiEuclid2Space is satisfying_BetweennessIdentity
proof
let a,b be POINT of TarskiEuclid2Space;
assume between a,b,a;
then Tn2TR b in LSeg(Tn2TR a,Tn2TR a) by ThConv6;
then Tn2TR b in { Tn2TR a} by RLTOPSP1:70;
hence thesis by TARSKI:def 1;
end;
begin :: Ordered Affine Space Generated by TOP-REAL 2
theorem THQQ:
OASpace TOP-REAL 2 is OAffinSpace
proof
(ex u,v be VECTOR of TOP-REAL 2 st
for a,b being Real st a*u + b*v = 0.(TOP-REAL 2) holds a=0 & b=0)
proof
reconsider u = |[1,0]|, v = |[0,1]| as VECTOR of TOP-REAL 2;
now
let a,b be Real;
assume
A1: a * u + b * v = 0.(TOP-REAL 2);
A2: a * u + b * v = |[a * 1,a * 0]| + b * v by EUCLID:58
.= |[a * 1,a * 0]| + |[b * 0, b * 1]| by EUCLID:58
.= |[a + 0,0 + b]| by EUCLID:56
.= |[a,b]|;
|[a,b]|`1 = a & |[a,b]|`2 = b & |[0,0]|`1 = 0 & |[0,0]|`2 = 0
by EUCLID:52;
hence a = 0 & b = 0 by A1,A2,EUCLID:54;
end;
hence thesis;
end;
hence thesis by ANALOAF:26;
end;
theorem THSS:
for a,b,c being Element of OASpace(TOP-REAL 2) holds
Mid a,b,c iff a = b or b = c or
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v))
proof
let a,b,c be Element of OASpace(TOP-REAL 2);
A1: now
assume Mid a,b,c;
then a,b // b,c;
then consider u,v,w,y be VECTOR of TOP-REAL 2 such that
A2: [a,b] = [u,v] and
A3: [b,c] = [w,y] and
A4: u,v // w,y by ANALOAF:def 3;
A5: a = u & b = v & b = w & c = y by A2,A3,XTUPLE_0:1;
per cases by A4;
suppose u = v;
hence a = b or b = c or
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v))
by A5;
end;
suppose w = y;
hence a = b or b = c or
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v))
by A5;
end;
suppose ex r,s be Real st 0 < r & 0 < s & r * (v-u) = s * (y - w);
then consider r,s be Real such that
A6: 0 < r and
A7: 0 < s and
A8: r * (v - u) = s * (y - w);
r * v - r * u = r * (v - u) by RLVECT_1:34
.= s * y - s * v by A5,A8,RLVECT_1:34; then
A9: (r + s) * v = r * u + s * y by THJC;
reconsider t = 1/(r+s) as Real;
A10: 1 - s/(r+s) = (r+s)/(r+s) - s/(r+s) by A6,A7,XCMPLX_1:60
.= r/(r+s);
A11: 1/(r+s)*(r+s) = (r+s)/(r+s)
.= 1 by A6,A7,XCMPLX_1:60;
A12: v = 1 * v by RVSUM_1:52
.= t * ((r+s) * v) by A11,RVSUM_1:49
.= t * (r * u) + t *(s * y) by RVSUM_1:51,A9
.= (t * r) * u + t * (s * y) by RVSUM_1:49
.= (1-s/(r+s)) * u + s/(r+s) * y by A10,RVSUM_1:49;
reconsider l = s/(r+s) as Real;
0 <= l <= 1 & v = (1-l) * u + l * y by A12,A6,A7,THJD;
then v in {(1-l) * u + l * y where l is Real : 0 <= l & l <= 1};
then b in LSeg(u,y) by A5,RLTOPSP1:def 2;
hence a = b or b = c or
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v))
by A5;
end;
end;
now
assume
A13: a = b or b = c or
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v));
reconsider OAS = OASpace(TOP-REAL 2) as OAffinSpace by THQQ;
per cases by A13;
suppose
A14: a = b;
a is Element of OAS & b is Element of OAS;
hence Mid a,b,c by A14,DIRAF:10;
end;
suppose
A15: b = c;
b is Element of OAS & c is Element of OAS;
hence Mid a,b,c by A15,DIRAF:10;
end;
suppose
ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v);
then consider u,v be Point of TOP-REAL 2 such that
A16: u = a and
A17: v = c and
A18: b in LSeg(u,v);
b in {(1-l) * u + l * v where l is Real: 0 <= l & l <= 1}
by RLTOPSP1:def 2,A18;
then consider l be Real such that
A19: b = (1-l) * u + l * v and
A20: 0 <= l and
A21: l <= 1;
reconsider w = b,y = b as Point of TOP-REAL 2;
now
take u,w,y,v;
thus [a,b] = [u,w] & [b,c] = [y,v] by A16,A17;
A22: w - (1-l)*u = l * v + (1-l) * u + ((-1)*(1-l)) * u by A19,RVSUM_1:49
.= l * v + ((1-l) * u + (-(1-l)) * u) by RVSUM_1:15
.= l * v + ((1-l) + (-(1-l))) * u by RVSUM_1:50
.= l * v by THJE;
|[l * v`1,l * v`2]| = l * v by EUCLID:57
.= |[w`1,w`2]| - (1-l)*u by A22,EUCLID:53
.= |[w`1,w`2]| - |[ (1-l)*u`1,(1-l)*u`2]|
by EUCLID:57
.= |[w`1-(1-l)*u`1,w`2-(1-l)*u`2]| by EUCLID:62;
then
A23: l * v`1 = w`1-(1-l)*u`1 & l * v`2 = w`2-(1-l)*u`2 by FINSEQ_1:77;
A24: (1-l) * w - (1-l) * u = l * v - l * w
proof
A25: (1-l) * w - (1-l) * u = (1-l) * |[w`1,w`2]| - (1-l)* u by EUCLID:53
.= (1-l) * |[w`1,w`2]| - (1-l)*|[u`1,u`2]| by EUCLID:53
.= |[(1-l) * w`1,(1-l)*w`2]| - (1-l)*|[u`1,u`2]| by EUCLID:58
.= |[(1-l) * w`1,(1-l)*w`2]| - |[(1-l)*u`1,(1-l)*u`2]|
by EUCLID:58
.= |[(1-l)*w`1-(1-l)*u`1,(1-l)*w`2-(1-l)*u`2]| by EUCLID:62
.= |[l*v`1 - l*w`1,l*v`2 - l*w`2]| by A23;
l * v - l * w = l * |[v`1,v`2]| - l * w by EUCLID:53
.= l * |[v`1,v`2]| - l * |[w`1,w`2]| by EUCLID:53
.= |[l * v`1,l * v`2]| - l * |[w`1,w`2]| by EUCLID:58
.= |[l * v`1,l * v`2]| - |[l * w`1,l * w`2]| by EUCLID:58
.= |[l * v`1 - l * w`1,l * v`2 - l * w`2]| by EUCLID:62;
hence thesis by A25;
end;
A26: (1-l)*(w - u) = (1-l) * w + (1-l) * (-u) by RVSUM_1:51
.= (1-l) * w + ((1-l) * (-1)) * u by RVSUM_1:49
.= (1-l) * w - (1-l) * u by RVSUM_1:49
.= l * v + ((-1) * l) * w by A24,RVSUM_1:49
.= l * v + l * ((-1)*w) by RVSUM_1:49
.= l * (v - w) by RVSUM_1:51;
per cases by A20,A21,XXREAL_0:1;
suppose l = 1;
then w = v + 0 * u by A19,RVSUM_1:52
.= v by THJE;
hence u,w // y,v;
end;
suppose l = 0;
then w = u + 0 * v by A19,RVSUM_1:52
.= u by THJE;
hence u,w // y,v;
end;
suppose
A27: 0 < l < 1;
then l - l < 1 - l by XREAL_1:9;
hence u,w // y,v by A27,A26;
end;
end;
then a,b // b,c by ANALOAF:def 3;
hence Mid a,b,c;
end;
end;
hence thesis by A1;
end;
theorem THSS2:
for a,b,c being Element of OASpace(TOP-REAL 2) holds
Mid a,b,c iff
(ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v))
proof
let a,b,c be Element of OASpace(TOP-REAL 2);
hereby
assume Mid a,b,c;
then per cases by THSS;
suppose
A1: a = b;
reconsider u = a, v = c as Point of TOP-REAL 2;
u in LSeg(u,v) by RLTOPSP1:68;
hence ex u,v be Point of TOP-REAL 2 st u = a & v = c &
b in LSeg(u,v) by A1;
end;
suppose
A2: b = c;
reconsider u = a, v = c as Point of TOP-REAL 2;
v in LSeg(u,v) by RLTOPSP1:68;
hence ex u,v be Point of TOP-REAL 2 st
u = a & v = c & b in LSeg(u,v) by A2;
end;
suppose ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v);
hence ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v);
end;
end;
assume ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v);
hence Mid a,b,c by THSS;
end;
theorem THSS3:
for a,b,c being Element of OASpace(TOP-REAL 2),
ap,bp,cp being POINT of TarskiEuclid2Space st
a = ap & b = bp & c = cp holds Mid a,b,c iff between ap,bp,cp
proof
let a,b,c be Element of OASpace(TOP-REAL 2),
ap,bp,cp be POINT of TarskiEuclid2Space;
assume that
A1: a = ap and
A2: b = bp and
A3: c = cp;
hereby
assume Mid a,b,c;
then ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)
by THSS2;
then Tn2TR bp in LSeg(Tn2TR ap, Tn2TR cp) by A1,A2,A3;
hence between ap,bp,cp by ThConv6;
end;
assume between ap,bp,cp;
then Tn2TR bp in LSeg(Tn2TR ap, Tn2TR cp) by ThConv6;
hence Mid a,b,c by A1,A2,A3,THSS2;
end;
begin
theorem THORANGE:
for A,B,C,D being Element of TOP-REAL 2 st
B in LSeg(A,C) & C in LSeg(A,D) holds B in LSeg(A,D)
proof
let A,B,C,D be Element of TOP-REAL 2;
assume that
A1: B in LSeg(A,C) and
A2: C in LSeg(A,D);
B in {(1-r)*A+r*C where r is Real : 0 <= r & r <= 1} by A1,RLTOPSP1:def 2;
then consider r be Real such that
A3: B = (1-r)*A+r*C and
A4: 0 <= r and
A5: r <= 1;
C in {(1-r)*A+r*D where r is Real : 0 <= r & r <= 1} by A2,RLTOPSP1:def 2;
then consider s be Real such that
A6: C = (1-s)*A+s*D and
A7: 0 <= s and
A8: s <= 1;
reconsider t = r * s as Real;
A9: r * s <= 1 * 1 by A4,A5,A7,A8,XREAL_1:66;
s * D = |[s*D`1,s*D`2]| by EUCLID:57; then
A10: r*((1-s)*A+s*D) = r * ( |[(1-s)*A`1,(1-s)*A`2]| + |[s*D`1,s*D`2]| )
by EUCLID:57
.= r * ( |[(1-s)*A`1 + s * D`1,(1-s)*A`2 + s * D`2]| ) by EUCLID:56
.= ( |[ r * ((1-s)*A`1 + s * D`1), r * ((1-s)*A`2 + s * D`2)]| )
by EUCLID:58;
B = |[(1-r)*A`1,(1-r)*A`2]| +
|[ r * ((1-s)*A`1 + s * D`1), r * ((1-s)*A`2 + s * D`2)]|
by A3,A6,A10,EUCLID:57
.= |[(1-r)*A`1 + r * ((1-s)*A`1 + s * D`1),
(1-r)*A`2 + r * ((1-s)*A`2 + s * D`2)]| by EUCLID:56
.= |[ (1-r*s)*A`1+r*s*D`1,(1-r*s)*A`2+r*s*D`2]|
.= |[ (1-r*s)*A`1,(1-r*s)*A`2]| +|[r*s*D`1,r*s*D`2]| by EUCLID:56
.= (1-r*s)*A + |[r*s*D`1,r*s*D`2]| by EUCLID:57
.= (1-t)*A+t*D by EUCLID:57;
then B in {(1-r)*A+r*D where r is Real:0 <= r & r <= 1} by A9,A4,A7;
hence thesis by RLTOPSP1:def 2;
end;
theorem THORANGE2:
for A,B,C,D being Element of TOP-REAL 2 st
B <> C & B in LSeg(A,C) & C in LSeg(B,D) holds C in LSeg(A,D)
proof
let A,B,C,D be Element of TOP-REAL 2;
assume that
A1: B <> C and
A2: B in LSeg(A,C) and
A3: C in LSeg(B,D);
reconsider OAS = OASpace(TOP-REAL 2) as OAffinSpace by THQQ;
reconsider ta = A,tb = B,tc = C,td = D as Element of OAS;
Mid ta,tb,tc & Mid tb,tc,td by A2,A3,THSS2;
then ex u,v be Point of TOP-REAL 2 st
u = ta & v = td & tc in LSeg(u,v) by A1,DIRAF:12,THSS2;
hence thesis;
end;
theorem THPOIRE:
for p,q,r,s being Point of TarskiEuclid2Space st
between p,q,r & between p,r,s holds between p,q,s
proof
let p,q,r,s be Point of TarskiEuclid2Space;
assume that
A1: between p,q,r and
A2: between p,r,s;
Tn2TR q in LSeg(Tn2TR p, Tn2TR r) &
Tn2TR r in LSeg(Tn2TR p, Tn2TR s) by A1,A2,ThConv6;
hence thesis by ThConv6,THORANGE;
end;
theorem THNOIX:
for A,B,C,D being Point of TOP-REAL 2 st
B in LSeg(A,C) & D in LSeg(A,B) holds
B in LSeg(D,C)
proof
let A,B,C,D be Point of TOP-REAL 2;
assume that
A1: B in LSeg(A,C) and
A2: D in LSeg(A,B);
A3: dist(A,D) + dist(D,C) = dist(A,C) by A1,A2,THORANGE,EUCLID12:12;
A4: dist(A,B) + dist(B,C) = dist(A,C) by A1,EUCLID12:12;
dist(A,D) + dist(D,B) = dist(A,B) by A2,EUCLID12:12;
then dist(D,B) + dist(B,C)= dist(D,C) by A3,A4;
hence thesis by EUCLID12:12;
end;
theorem THNOIX2:
for p,q,r,s being Point of TarskiEuclid2Space st
between p,q,r & between p,s,q holds between s,q,r
proof
let p,q,r,s be Point of TarskiEuclid2Space;
assume that
A1: between p,q,r and
A2: between p,s,q;
A3: Tn2TR q in LSeg (Tn2TR p, Tn2TR r) by A1,ThConv6;
Tn2TR s in LSeg (Tn2TR p, Tn2TR q) by A2,ThConv6;
then Tn2TR q in LSeg(Tn2TR s, Tn2TR r) by A3,THNOIX;
hence thesis by ThConv6;
end;
theorem THNOIX3:
for p,q,r,s being Point of TarskiEuclid2Space st
q <> r & between p,q,r & between q,r,s holds between p,q,s
proof
let p,q,r,s be Point of TarskiEuclid2Space;
assume that
A1: q <> r and
A2: between p,q,r and
A3: between q,r,s;
A4: Tn2TR q in LSeg(Tn2TR p,Tn2TR r) by A2,ThConv6; then
A5: dist(Tn2TR p, Tn2TR q)+dist(Tn2TR q, Tn2TR r)=
dist(Tn2TR p, Tn2TR r) by EUCLID12:12;
A6: Tn2TR r in LSeg(Tn2TR q,Tn2TR s) by A3,ThConv6;
A7: Tn2TR r in LSeg(Tn2TR p, Tn2TR s) by A1,A4,A6,THORANGE2;
dist(Tn2TR p, Tn2TR q) + dist(Tn2TR q, Tn2TR s)
= dist(Tn2TR p, Tn2TR r) - dist(Tn2TR q, Tn2TR r) +
(dist(Tn2TR q, Tn2TR r) + dist(Tn2TR r, Tn2TR s))
by A5,A6,EUCLID12:12
.= dist(Tn2TR p, Tn2TR r) + dist(Tn2TR r, Tn2TR s)
.= dist(Tn2TR p, Tn2TR s) by A7,EUCLID12:12;
then Tn2TR q in LSeg(Tn2TR p, Tn2TR s) by EUCLID12:12;
hence thesis by ThConv6;
end;
theorem
for p,q,r,s being Point of TarskiEuclid2Space st
q <> r & between p,q,r & between q,r,s holds between p,r,s
proof
let p,q,r,s be Point of TarskiEuclid2Space;
assume that
A1: q <> r and
A2: between p,q,r and
A3: between q,r,s;
A4: Tn2TR q in LSeg(Tn2TR p,Tn2TR r) by A2,ThConv6;
A6: Tn2TR r in LSeg(Tn2TR q,Tn2TR s) by A3,ThConv6;
Tn2TR r in LSeg(Tn2TR p, Tn2TR s) by A1,A4,A6,THORANGE2;
hence thesis by ThConv6;
end;
ThPasch:
TarskiEuclid2Space is satisfying_Pasch
proof
set S = TarskiEuclid2Space;
now
let a, b, p, q, z be POINT of S;
assume that
A1: between a,p,z and
A2: between b,q,z;
reconsider OAS = OASpace(TOP-REAL 2) as OAffinSpace by THQQ;
A3: OAS is satisfying_Int_Bet_Pasch by PASCH:30;
Tn2TR a is Element of REAL 2 & Tn2TR b is Element of REAL 2 &
Tn2TR p is Element of REAL 2 & Tn2TR z is Element of REAL 2 &
Tn2TR q is Element of REAL 2 by EUCLID:22;
then reconsider a1 = a,b1 = b,p1 = p,z1 = z,q1 = q as Element of OAS;
Mid a1,p1,z1 by A1,THSS3; then
A4: Mid z1,p1,a1 by DIRAF:9;
Mid b1,q1,z1 by A2,THSS3; then
A5: Mid z1,q1,b1 by DIRAF:9;
per cases;
suppose z1,p1,b1 are_collinear;
then z1,p1 '||' z1,b1;
then per cases by DIRAF:2;
suppose z1,p1 // z1,b1;
then consider u,v,w,y be VECTOR of TOP-REAL 2 such that
A6: [z1,p1] = [u,v] and
A7: [z1,b1] = [w,y] and
A8: u,v // w,y by ANALOAF:def 3;
A9: u = z1 & p1 = v & z1 = w & b1 = y by A6,A7,XTUPLE_0:1;
then per cases by A8;
suppose u = v; then
A10: between p,q,b by A9,A2,ThConv7bis;
between q,q,a by ThConv7;
hence ex x being POINT of S st between p,x,b & between q,x,a
by A10;
end;
suppose u = y; then
A11: b = q by A2,A9,ThConv7ter;
A12: between p,b,b by ThConv7;
between q,b,a by A11,ThConv7;
hence ex x being POINT of S st between p,x,b & between q,x,a
by A12;
end;
suppose ex a,b be Real st 0 < a & 0 < b & a * (v-u)= b*(y-u);
then consider r,s be Real such that
A13: 0 < r and
A14: 0 < s and
A15: r * (v - u) = s * (y - u);
per cases by XXREAL_0:1;
suppose r = s;
then v - u = y - u by A13,A15,RLVECT_1:36; then
A16: v = y by THSD2;
A17: between p,p,b by ThConv7;
Tn2TR p in LSeg (Tn2TR z,Tn2TR a) by A1,ThConv6; then
A18: between z,b,a by A16,A9,ThConv6;
Tn2TR q in LSeg (Tn2TR b,Tn2TR z) by A2,ThConv6; then
A19: between z,q,b by ThConv6;
between q,p,a by A16,A9,A18,A19,THNOIX2;
hence ex x being POINT of S st between p,x,b & between q,x,a
by A17;
end;
suppose
A20: r < s;
reconsider t = r / s as Real;
A21: r / s < s / s by A13,A20,XREAL_1:74;
A22: t * v - t * u = |[t * v`1,t * v`2]| - t * u by EUCLID:57
.= |[t * v`1,t * v`2]| - |[t * u`1,t * u`2]| by EUCLID:57
.= |[ 1/s * r * v`1 -1/s * r * u`1,t * v`2 - t * u`2]|
by EUCLID:62
.= |[(1/s) * (r * v`1 - r * u`1),(1/s) * (r * v`2-r*u`2)]|
.= (1/s) *|[r * v`1 - r * u`1,r * v`2-r*u`2]| by EUCLID:58;
A23: |[r * v`1-r*u`1,r*v`2-r*u`2]| = |[r*(v`1-u`1),r*(v`2-u`2)]|
.= r*|[v`1-u`1,v`2-u`2]| by EUCLID:58
.= s * (y-u) by A15,EUCLID:61;
A24: t * v - t * u = (1/s) * |[ s*(y-u)`1,s*(y-u)`2]|
by A23,A22,EUCLID:57
.= |[ (1/s)*(s*(y-u)`1),(1/s)*(s*(y-u)`2)]|
by EUCLID:58
.= |[ s*(1/s)*(y-u)`1,s*(1/s)*(y-u)`2]|
.= |[ 1*(y-u)`1,s*(1/s)*(y-u)`2]|
by XCMPLX_1:106,A14
.= |[(y-u)`1,1 * (y-u)`2]| by XCMPLX_1:106,A14
.= y - u by EUCLID:53;
y = |[y`1-u`1+u`1,y`2-u`2+u`2]| by EUCLID:53
.= |[y`1-u`1,y`2-u`2]| + |[u`1,u`2]| by EUCLID:56
.= |[y`1,y`2]| - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:62
.= y - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:53
.= y - u + |[u`1,u`2]| by EUCLID:53
.= y - u + u by EUCLID:53
.= |[t*v`1,t*v`2]| - t * u + u by A24,EUCLID:57
.= (|[t*v`1,t*v`2]| - |[t*u`1,t*u`2]|) + u by EUCLID:57
.= (|[t*v`1,t*v`2]| - |[t*u`1,t*u`2]|) + |[u`1,u`2]|
by EUCLID:53
.= |[t*v`1-t*u`1,t*v`2-t*u`2]| + |[u`1,u`2]| by EUCLID:62
.= |[t*v`1-t*u`1+u`1,t*v`2-t*u`2+u`2]| by EUCLID:56
.= |[t*v`1+ (1-t)*u`1,t*v`2+ (1-t)*u`2]|
.= |[(1-t)*u`1,(1-t)*u`2]| + |[t*v`1,t*v`2]| by EUCLID:56
.= (1-t) * u + |[t*v`1,t*v`2]| by EUCLID:57
.= (1-t) * u + t * v by EUCLID:57;
then (1-t) * u + t * v = y & 0 < t & t < 1
by A21,A13,A14,XCMPLX_1:60;
then y in {(1-t)*u+t*v where t is Real: 0 <= t & t <= 1};
then Tn2TR b in LSeg(Tn2TR z, Tn2TR p) by A9,RLTOPSP1:def 2; then
A25: between z,b,p by ThConv6;
A26: between z,p,a by A1,ThConv7bis;
A27: between z,q,b by A2,ThConv7bis; then
A28: between z,q,p by A25,THPOIRE;
Tn2TR p in LSeg(Tn2TR z,Tn2TR a) by A1,ThConv6; then
A29: dist(Tn2TR z,Tn2TR p) + dist(Tn2TR p,Tn2TR a) =
dist(Tn2TR z,Tn2TR a) by EUCLID12:12;
Tn2TR q in LSeg(Tn2TR z,Tn2TR p) by A27,A25,THPOIRE,ThConv6;
then
A30: dist(Tn2TR z,Tn2TR q) + dist(Tn2TR q,Tn2TR p) =
dist(Tn2TR z,Tn2TR p) by EUCLID12:12;
Tn2TR q in LSeg(Tn2TR z,Tn2TR a) by A28,A26,THPOIRE,ThConv6; then
dist(Tn2TR z,Tn2TR q) + dist(Tn2TR q,Tn2TR a) =
dist(Tn2TR z,Tn2TR a) by EUCLID12:12;
then dist(Tn2TR q,Tn2TR p) + dist(Tn2TR p,Tn2TR a) =
dist(Tn2TR q, Tn2TR a) by A29,A30; then
A31: Tn2TR p in LSeg(Tn2TR q,Tn2TR a) by EUCLID12:12;
A32: between p,p,b by ThConv7;
between q,p,a by A31,ThConv6;
hence ex x being POINT of S st between p,x,b & between q,x,a
by A32;
end;
suppose
A33: s < r;
set t = s / r;
t < r / r by A33,A13,XREAL_1:74; then
A34: t < 1 by A13,XCMPLX_1:60;
A35: t * y - t * u = |[t * y`1,t * y`2]| - t * u by EUCLID:57
.= |[t * y`1,t * y`2]| - |[t * u`1,t * u`2]| by EUCLID:57
.= |[ 1/r * s * y`1 -1/r * s * u`1,
(1/r)*s * y`2 - (1/r)*s * u`2]| by EUCLID:62
.= |[(1/r) * (s * y`1 - s * u`1),(1/r) * (s * y`2-s*u`2)]|
.= (1/r) *|[s * y`1 - s * u`1,s * y`2-s*u`2]| by EUCLID:58;
A36: |[s * y`1-s*u`1,s*y`2-s*u`2]| = |[s*(y`1-u`1),s*(y`2-u`2)]|
.= s*|[y`1-u`1,y`2-u`2]| by EUCLID:58
.= r * (v-u) by A15,EUCLID:61;
A37: t * y - t * u = (1/r) * |[ r*(v-u)`1,r*(v-u)`2]|
by A36,A35,EUCLID:57
.= |[ (1/r)*(r*(v-u)`1),(1/r)*(r*(v-u)`2)]| by EUCLID:58
.= |[ r*(1/r)*(v-u)`1,r*(1/r)*(v-u)`2]|
.= |[ 1*(v-u)`1,r*(1/r)*(v-u)`2]| by XCMPLX_1:106,A13
.= |[(v-u)`1,1 * (v-u)`2]| by XCMPLX_1:106,A13
.= v - u by EUCLID:53;
v = |[v`1-u`1+u`1,v`2-u`2+u`2]| by EUCLID:53
.= |[v`1-u`1,v`2-u`2]| + |[u`1,u`2]| by EUCLID:56
.= |[v`1,v`2]| - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:62
.= v - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:53
.= v - u + |[u`1,u`2]| by EUCLID:53
.= t * y - t * u + u by A37,EUCLID:53
.= |[t*y`1,t*y`2]| - t * u + u by EUCLID:57
.= (|[t*y`1,t*y`2]| - |[t*u`1,t*u`2]|) + u by EUCLID:57
.= (|[t*y`1,t*y`2]| - |[t*u`1,t*u`2]|) + |[u`1,u`2]|
by EUCLID:53
.= |[t*y`1-t*u`1,t*y`2-t*u`2]| + |[u`1,u`2]| by EUCLID:62
.= |[t*y`1-t*u`1+u`1,t*y`2-t*u`2+u`2]| by EUCLID:56
.= |[t*y`1+ (1-t)*u`1,t*y`2+ (1-t)*u`2]|
.= |[(1-t)*u`1,(1-t)*u`2]| + |[t*y`1,t*y`2]| by EUCLID:56
.= (1-t) * u + |[t*y`1,t*y`2]| by EUCLID:57
.= (1-t) * u + t * y by EUCLID:57;
then v in {(1-t)*u+t*y where t is Real: 0 <= t & t <= 1}
by A13,A14,A34;
then Tn2TR p in LSeg(Tn2TR z, Tn2TR b) by A9,RLTOPSP1:def 2; then
A38: between z,p,b by ThConv6;
A39: between z,p,a by A1,ThConv7bis;
A40: between z,q,b by A2,ThConv7bis;
A41: Mid z1,p1,b1 & Mid z1,q1,b1 by A38,A40,THSS3;
per cases;
suppose
A42: z <> p;
Mid z1,p1,b1 & Mid z1,p1,a1 by A38,A39,THSS3;
then per cases by A42,DIRAF:15;
suppose Mid p1,b1,a1;
per cases by A41,DIRAF:17;
suppose Mid z1,p1,q1;
then between z,p,q by THSS3; then
A43: between p,q,b by A40,THNOIX2;
between q,q,a by ThConv7;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A43;
end;
suppose Mid z1,q1,p1;
then between z,q,p by THSS3; then
A44: between q,p,a by A39,THNOIX2;
between p,p,b by ThConv7;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A44;
end;
end;
suppose Mid p1,a1,b1;
per cases by A41,DIRAF:17;
suppose Mid z1,p1,q1;
then between z,p,q by THSS3; then
A45: between p,q,b by A40,THNOIX2;
between q,q,a by ThConv7;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A45;
end;
suppose Mid z1,q1,p1;
then between z,q,p by THSS3; then
A46: between q,p,a by A39,THNOIX2;
between p,p,b by ThConv7;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A46;
end;
end;
end;
suppose
A47: z = p;
between q,q,a by ThConv7;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A47,A40;
end;
end;
end;
end;
suppose b1,z1 // z1,p1;
then Mid b1,z1,p1;
then Mid p1,z1,b1 by DIRAF:9; then
A48: between p,z,b by THSS3; then
A49: between b,z,p by ThConv7bis;
A50: between q,z,p by A2,A49,THNOIX2;
A51: between z,p,a by A1,ThConv7bis;
per cases;
suppose z = p; then
A52: between p,q,b by A2,ThConv7bis;
between q,q,a by ThConv7;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A52;
end;
suppose z <> p;
then between q,z,a by A50,A51,THNOIX3;
hence ex x being POINT of S st
between p,x,b & between q,x,a by A48;
end;
end;
end;
suppose
A53: not z1,p1,b1 are_collinear;
consider y be Element of OAS such that
A54: Mid p1,y,b1 and
A55: Mid q1,y,a1 by A3,A53,A4,A5;
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
then reconsider yt = y as POINT of S by EUCLID:22;
A56: between p,yt,b by A54,THSS3;
between q,yt,a by A55,THSS3;
hence ex x being POINT of S st between p,x,b & between q,x,a by A56;
end;
end;
hence thesis;
end;
registration
cluster TarskiEuclid2Space -> satisfying_CongruenceSymmetry
satisfying_CongruenceEquivalenceRelation
satisfying_CongruenceIdentity
satisfying_SegmentConstruction
satisfying_SAS
satisfying_BetweennessIdentity
satisfying_Pasch;
coherence by ThCongruenceSymmetry,
ThCongruenceEquivalenceRelation,
ThCongruenceIdentity,
ThSegmentConstruction,
ThSAS,
ThBetweennessIdentity,
ThPasch;
end;
registration
cluster TarskiEuclid2Space -> satisfying_Tarski-model;
coherence;
end;
begin :: Preparatory Work for The Rest of Tarski's Axioms
theorem ThAZ9:
for P,Q,R being Point of TOP-REAL 2, L being Element of line_of_REAL 2
st P in L & Q in L & R in L holds P in LSeg(Q,R) or
Q in LSeg(R,P) or R in LSeg(P,Q)
proof
let P,Q,R be Point of TOP-REAL 2, L be Element of line_of_REAL 2;
assume that
A1: P in L and
A2: Q in L and
A3: R in L;
L in line_of_REAL 2;
then L in the set of all Line(x1,x2) where x1,x2 is Element of REAL 2
by EUCLIDLP:def 4;
then consider x1,x2 be Element of REAL 2 such that
A4: L = Line(x1,x2);
reconsider tx1 = x1,tx2 = x2 as Element of TOP-REAL 2 by EUCLID:22;
P in Line(tx1,tx2) & Q in Line(tx1,tx2) & R in Line(tx1,tx2)
by A1,A2,A3,A4,EUCLID12:4;
hence thesis by RLTOPSP1:def 16,TOPREAL9:67;
end;
theorem ThConvAG:
for a,b,c being Element of TarskiEuclid2Space holds
Tn2TR b in LSeg (Tn2TR a,Tn2TR c) implies
ex jj being Real st 0 <= jj & jj <= 1 &
Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a)
proof
let a,b,c be Element of TarskiEuclid2Space;
assume Tn2TR b in LSeg (Tn2TR a,Tn2TR c); then
consider jj being Real such that
G2: 0 <= jj & jj <= 1 & Tn2TR b = (1-jj)*Tn2TR a + jj*Tn2TR c by RLTOPSP1:76;
set v = Tn2TR a, w = Tn2TR c;
Tn2TR b - Tn2TR a = (1-jj)*v - v + jj*w by RVSUM_1:15,G2
.= (1-jj+(-1))*v + jj*w by RVSUM_1:50
.= jj*w + (jj*(-1))*v
.= jj*w + jj*((-1)*v) by RVSUM_1:49
.= jj * (w - v) by RVSUM_1:51;
hence thesis by G2;
end;
theorem
for n being Nat
for a,b,c being Element of TarskiEuclidSpace n holds
Tn2TR b in LSeg (Tn2TR a, Tn2TR c) implies
ex jj being Real st 0 <= jj <= 1 &
Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a)
proof
let n be Nat;
let a,b,c be Element of TarskiEuclidSpace n;
assume Tn2TR b in LSeg (Tn2TR a, Tn2TR c); then
consider jj being Real such that
G2: 0 <= jj <= 1 & Tn2TR b = (1-jj)*Tn2TR a + jj*Tn2TR c by RLTOPSP1:76;
set v = Tn2TR a, w = Tn2TR c;
Tn2TR b - Tn2TR a = (1-jj)*v - v + jj*w by RVSUM_1:15,G2
.= (1-jj+(-1))*v + jj*w by RVSUM_1:50
.= jj*w + (jj*(-1))*v
.= jj*w + jj*((-1)*v) by RVSUM_1:49
.= jj * (w - v) by RVSUM_1:51;
hence thesis by G2;
end;
theorem ThConvAGI:
for a,b,c being Element of TarskiEuclid2Space holds
(ex jj being Real st 0 <= jj & jj <= 1 &
Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a))
implies
Tn2TR b in LSeg (Tn2TR a,Tn2TR c)
proof
let a,b,c be Element of TarskiEuclid2Space;
given jj being Real such that
G2: 0 <= jj <= 1 & Tn2TR b - Tn2TR a = jj * (Tn2TR c - Tn2TR a);
set v = Tn2TR a, w = Tn2TR c;
SS: Tn2TR b + (v - v) = Tn2TR b + 0.TOP-REAL 2 by RLVECT_1:5
.= Tn2TR b;
G3: v = 1 * v by RVSUM_1:52;
Tn2TR b + (- v + v) = jj * (Tn2TR c - Tn2TR a) + v by G2,RVSUM_1:15; then
Tn2TR b = jj*w + jj * (-v) + v by RVSUM_1:51,SS
.= jj*w + (jj * (-1))*v + v by RVSUM_1:49
.= jj*w + (-1) * (jj*v) + v by RVSUM_1:49
.= jj*w + (- jj*v + 1*v) by RVSUM_1:15,G3
.= jj*w + (((-1) * jj)*v + 1*v) by RVSUM_1:49
.= ((1 - jj)*v) + jj*w by RVSUM_1:50; then
Tn2TR b in {(1-r)*v + r*w where r is Real : 0 <= r & r <= 1 } by G2;
hence thesis by RLTOPSP1:def 2;
end;
begin :: Four Remaining Axioms of Tarski
definition let S be TarskiGeometryStruct;
attr S is satisfying_A8 means ::: Axiom A8
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 satisfying_A9 means ::: Axiom A9
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 satisfying_A10 means ::: Axiom A10
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 satisfying_A11 means ::: Axiom A11
for X,Y being Subset of S 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);
end;
notation let S be TarskiGeometryStruct;
synonym S is satisfying_Lower_Dimension_Axiom for S is satisfying_A8;
synonym S is satisfying_Upper_Dimension_Axiom for S is satisfying_A9;
synonym S is satisfying_Euclid_Axiom for S is satisfying_A10;
synonym S is satisfying_Continuity_Axiom for S is satisfying_A11;
end;
:: Axiom A8 -- Lower Dimension Axiom
::$N Lower dimension axiom
theorem AxiomA8: :: Axiom A8
ex a,b,c being Point of TarskiEuclid2Space st
not between a,b,c & not between b,c,a & not between c,a,b
proof
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
then reconsider a = |[0,0]|, b = |[1,0]|, c = |[0,1]|
as Point of TarskiEuclid2Space by EUCLID:22;
take a,b,c;
thus not between a,b,c
proof
assume between a,b,c;
then Tn2TR b in LSeg(Tn2TR a,Tn2TR c) by ThConv6;
then dist(Tn2TR a,Tn2TR b) + dist(Tn2TR b,Tn2TR c) =
dist(Tn2TR a,Tn2TR c) by EUCLID12:12;
hence thesis by SQUARE_1:19,THY1,THY2,THY3;
end;
thus not between b,c,a
proof
assume between b,c,a;
then Tn2TR c in LSeg(Tn2TR b,Tn2TR a) by ThConv6;
then dist(Tn2TR b,Tn2TR c) + dist(Tn2TR c,Tn2TR a) =
dist(Tn2TR b,Tn2TR a) by EUCLID12:12;
hence thesis by SQUARE_1:19,THY1,THY2,THY3;
end;
assume between c,a,b;
then Tn2TR a in LSeg(Tn2TR c,Tn2TR b) by ThConv6;
then dist(Tn2TR c,Tn2TR a) + dist(Tn2TR a,Tn2TR b) =
dist(Tn2TR c,Tn2TR b) by EUCLID12:12;
hence thesis by SQUARE_1:21,THY1,THY2,THY3;
end;
:: Axiom A9 -- Upper Dimension Axiom
::$N Upper dimension axiom
theorem AxiomA9: :: Axiom A9
for a,b,c,p,q being Point of TarskiEuclid2Space 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
proof
let a,b,c,p,q be Point of TarskiEuclid2Space;
assume that
A1: p <> q and
A2: a,p equiv a,q and
A3: b,p equiv b,q and
A4: c,p equiv c,q;
|. Tn2TR a - Tn2TR p.| = |. Tn2TR a - Tn2TR q.| by A2,ThConv4; then
A5: Tn2TR a in the_perpendicular_bisector(Tn2TR p,Tn2TR q) by A1,EUCLID12:60;
|. Tn2TR b - Tn2TR p.| = |. Tn2TR b - Tn2TR q.| by A3,ThConv4; then
A6: Tn2TR b in the_perpendicular_bisector(Tn2TR p,Tn2TR q) by A1,EUCLID12:60;
|. Tn2TR c - Tn2TR p.| = |. Tn2TR c - Tn2TR q.| by A4,ThConv4;
then Tn2TR c in the_perpendicular_bisector(Tn2TR p,Tn2TR q)
by A1,EUCLID12:60;
then Tn2TR a in LSeg(Tn2TR b,Tn2TR c) or
Tn2TR b in LSeg(Tn2TR c,Tn2TR a) or Tn2TR c in LSeg(Tn2TR a,Tn2TR b)
by A5,A6,ThAZ9;
hence thesis by ThConv6;
end;
:: Axiom A10 -- Axiom of Euclid
::$N Axiom of Euclid
theorem AxiomA10: :: Axiom A10 -- Axiom of Euclid
for a,b,c,d,t being Element of TarskiEuclid2Space st
between a,d,t & between b,d,c & a <> d holds
ex x,y being Element of TarskiEuclid2Space st
between a,b,x & between a,c,y & between x,t,y
proof
let a,b,c,d,t be Element of TarskiEuclid2Space;
assume that
A1: between a,d,t and
A2: between b,d,c and
A3: a <> d;
G0: Tn2TR d in LSeg(Tn2TR a, Tn2TR t ) by A1,ThConv6;
set v = Tn2TR a, w = Tn2TR t;
consider jj being Real such that
G2: 0 <= jj & jj <= 1 & Tn2TR d = (1-jj)*v + jj*w by RLTOPSP1:76,G0;
g1: Tn2TR d - Tn2TR a = (1-jj)*v - v + jj*w by RVSUM_1:15,G2
.= (1-jj + (-1)) * v + jj*w by RVSUM_1:50
.= jj*w + (jj * (-1))*v
.= jj*w + jj * ((-1)*v) by RVSUM_1:49
.= jj * (w - v) by RVSUM_1:51;
set jt = 1 / jj;
JJ: jj <> 0
proof
assume jj = 0; then
Tn2TR d - Tn2TR a = 0.TOP-REAL 2 by g1,RLVECT_1:10;
hence thesis by A3,RLVECT_1:21;
end;
set xxx = jt * (Tn2TR b - Tn2TR a) + Tn2TR a;
ww: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by
GTARSKI1:def 13; then
reconsider xx = xxx as Element of TarskiEuclid2Space by EUCLID:22;
jj * (xxx - Tn2TR a) =
jj * (jt * (Tn2TR b - Tn2TR a) + (Tn2TR a - Tn2TR a)) by RLVECT_1:28
.= jj * ((1 / jj) * (Tn2TR b - Tn2TR a) + 0.TOP-REAL 2) by RLVECT_1:15
.= (jj * (1 / jj)) * (Tn2TR b - Tn2TR a) by RLVECT_1:def 7
.= 1 * (Tn2TR b - Tn2TR a) by XCMPLX_0:def 7,JJ
.= Tn2TR b - Tn2TR a by RVSUM_1:52; then
Tn2TR b in LSeg (Tn2TR a, Tn2TR xx) by G2,ThConvAGI; then
T1: between a,b,xx by ThConv6;
set yyy = jt * (Tn2TR c - Tn2TR a) + Tn2TR a;
reconsider yy = yyy as Element of TarskiEuclid2Space by ww,EUCLID:22;
jj * (yyy - Tn2TR a) = jj * (jt * (Tn2TR c - Tn2TR a) +
(Tn2TR a - Tn2TR a)) by RLVECT_1:28
.= jj * (jt * (Tn2TR c - Tn2TR a) + 0.TOP-REAL 2) by RLVECT_1:15
.= (jj * jt) * (Tn2TR c - Tn2TR a) by RLVECT_1:def 7
.= 1 * (Tn2TR c - Tn2TR a) by XCMPLX_0:def 7,JJ
.= (Tn2TR c - Tn2TR a) by RVSUM_1:52; then
Tn2TR c in LSeg (Tn2TR a, Tn2TR yy) by G2,ThConvAGI; then
T2: between a,c,yy by ThConv6;
Tn2TR d in LSeg (Tn2TR b, Tn2TR c) by A2,ThConv6; then
consider kk being Real such that
Y1: 0 <= kk & kk <= 1 & Tn2TR d - Tn2TR b = kk * (Tn2TR c - Tn2TR b)
by ThConvAG;
jt * (Tn2TR d - Tn2TR a) = (1 / jj) * jj * (Tn2TR t - Tn2TR a)
by g1,RLVECT_1:def 7
.= 1 * (Tn2TR t - Tn2TR a) by JJ,XCMPLX_0:def 7
.= Tn2TR t - Tn2TR a by RVSUM_1:52; then
w1: jt * (Tn2TR d - Tn2TR a) + Tn2TR a =
Tn2TR t + (- Tn2TR a + Tn2TR a) by RLVECT_1:def 3
.= Tn2TR t + 0.TOP-REAL 2 by RLVECT_1:5;
W2: Tn2TR yy - Tn2TR xx =
(1 / jj) * (Tn2TR c - Tn2TR a) + Tn2TR a -
Tn2TR a - (1 / jj) * (Tn2TR b - Tn2TR a)
by RLVECT_1:27
.= jt * (Tn2TR c - Tn2TR a) + (Tn2TR a - Tn2TR a) -
(1 / jj) * (Tn2TR b - Tn2TR a)
by RLVECT_1:28
.= jt * (Tn2TR c - Tn2TR a) + 0.TOP-REAL 2 -
(1 / jj) * (Tn2TR b - Tn2TR a)
by RLVECT_1:15
.= jt * ((Tn2TR c - Tn2TR a) - (Tn2TR b - Tn2TR a)) by RLVECT_1:34
.= jt * (Tn2TR c - Tn2TR b) by ThWW;
Tn2TR t - Tn2TR xx = jt * (Tn2TR d - Tn2TR a) + Tn2TR a -
Tn2TR a - (1 / jj) * (Tn2TR b - Tn2TR a)
by RLVECT_1:27,w1
.= jt * (Tn2TR d - Tn2TR a) + (Tn2TR a - Tn2TR a) -
(1 / jj) * (Tn2TR b - Tn2TR a)
by RLVECT_1:def 3
.= jt * (Tn2TR d - Tn2TR a) + 0.TOP-REAL 2 - (1 / jj) *
(Tn2TR b - Tn2TR a) by RLVECT_1:5
.= jt * ((Tn2TR d - Tn2TR a) - (Tn2TR b - Tn2TR a)) by RLVECT_1:34
.= jt * (Tn2TR d - Tn2TR b) by ThWW
.= jt * kk * (Tn2TR c - Tn2TR b) by RLVECT_1:def 7,Y1
.= kk * (Tn2TR yy - Tn2TR xx) by W2,RLVECT_1:def 7; then
Tn2TR t in LSeg (Tn2TR xx, Tn2TR yy) by Y1,ThConvAGI; then
between xx,t,yy by ThConv6;
hence thesis by T1,T2;
end;
begin :: Axiom A11 -- Axiom Schema of Continuity
::$N Axiom schema of continuity
theorem AxiomA11: :: Axiom A11
for X,Y being Subset of TarskiEuclid2Space st
(ex a being Element of TarskiEuclid2Space st
for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y) holds
(ex b being Element of TarskiEuclid2Space st
for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between x,b,y)
proof
let X,Y being Subset of TarskiEuclid2Space;
given a be Element of TarskiEuclid2Space such that
A1: for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between a,x,y;
per cases;
suppose
SS: X c= {a} or Y = {};
ex b being Element of TarskiEuclid2Space st
for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between x,b,y
proof
take b = a;
let x,y be Element of TarskiEuclid2Space;
assume x in X & y in Y; then
x = a by SS,TARSKI:def 1;
hence thesis by GTARSKI1:17;
end;
hence thesis;
end;
suppose
SSS: not X c= {a} & Y <> {};
X \ {a} <> {} by XBOOLE_1:37,SSS; then
consider c being object such that
G9: c in X \ {a} by XBOOLE_0:def 1;
reconsider c as Element of TarskiEuclid2Space by G9;
su: X \ {a} c= X by XBOOLE_1:36;
set S = { j where j is Real : j >= 1 &
Tn2TR a + j * (Tn2TR c - Tn2TR a) in Y };
S is real-membered
proof
let w be object;
assume w in S; then
consider j1 being Real such that
G1: w = j1 & j1 >= 1 & Tn2TR a + j1 * (Tn2TR c - Tn2TR a) in Y;
thus thesis by G1;
end; then
reconsider S as real-membered set;
gg: 1 is LowerBound of S
proof
let x be ExtReal;
assume x in S; then
consider j1 being Real such that
G1: x = j1 & j1 >= 1 & Tn2TR a + j1 * (Tn2TR c - Tn2TR a) in Y;
thus thesis by G1;
end;
consider d being object such that
G2: d in Y by XBOOLE_0:def 1,SSS;
reconsider d as Element of TarskiEuclid2Space by G2;
Tn2TR c in LSeg (Tn2TR a,Tn2TR d) by ThConv6,su,G9,A1,G2; then
consider jda being Real such that
G0: 0 <= jda & jda <= 1 & Tn2TR c - Tn2TR a =
jda * (Tn2TR d - Tn2TR a) by ThConvAG;
set jd = 1 / jda;
hh: jda <> 0
proof
assume jda = 0; then
Tn2TR c - Tn2TR a = 0.TOP-REAL 2 + 0 * (Tn2TR d - Tn2TR a) by G0
.= 0.TOP-REAL 2 by THJE;
hence thesis by G9,ZFMISC_1:56,RLVECT_1:21;
end;
Lem: for y being Element of TarskiEuclid2Space st y in Y holds
ex j1 being Real st j1 >= 1 & Tn2TR y - Tn2TR a =
j1 * (Tn2TR c - Tn2TR a)
proof
let y be Element of TarskiEuclid2Space;
assume y in Y; then
Tn2TR c in LSeg (Tn2TR a,Tn2TR y) by A1,su,G9,ThConv6; then
consider j being Real such that
H1: 0 <= j & j <= 1 & Tn2TR c - Tn2TR a = j * (Tn2TR y - Tn2TR a)
by ThConvAG;
set j1 = 1 / j;
H2: j <> 0
proof
assume j = 0; then
Tn2TR c - Tn2TR a = 0.TOP-REAL 2 + 0 * (Tn2TR y - Tn2TR a) by H1
.= 0.TOP-REAL 2 by THJE;
hence thesis by G9,ZFMISC_1:56,RLVECT_1:21;
end; then
H5: j1 >= 1 by H1,XREAL_1:181;
j1 * (Tn2TR c - Tn2TR a) = j1 * j * (Tn2TR y - Tn2TR a)
by RLVECT_1:def 7,H1
.= 1 * (Tn2TR y - Tn2TR a) by H2,XCMPLX_0:def 7
.= Tn2TR y - Tn2TR a by RVSUM_1:52;
hence thesis by H5;
end;
Gy: jd * (Tn2TR c - Tn2TR a) = jd * jda * (Tn2TR d - Tn2TR a)
by RLVECT_1:def 7,G0
.= 1 * (Tn2TR d - Tn2TR a) by hh,XCMPLX_0:def 7
.= Tn2TR d - Tn2TR a by RVSUM_1:52;
J2: jd >= 1 by XREAL_1:181,G0,hh;
jd * (Tn2TR c - Tn2TR a) + Tn2TR a = Tn2TR d + (- Tn2TR a + Tn2TR a)
by RLVECT_1:def 3,Gy
.= Tn2TR d + 0.TOP-REAL 2 by RLVECT_1:5; then
J1: jd in S by J2,G2;
reconsider S as non empty bounded_below real-membered set
by J1,gg,XXREAL_2:def 9;
set k = inf S;
set bb = Tn2TR a + k * (Tn2TR c - Tn2TR a);
p2: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
reconsider bb as Element of TarskiEuclid2Space by p2,EUCLID:67;
ex b being Element of TarskiEuclid2Space st
for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between x,b,y
proof
take b = bb;
let x,y be Element of TarskiEuclid2Space;
assume
T1: x in X & y in Y; then
consider j1 being Real such that
HH: j1 >= 1 & Tn2TR y - Tn2TR a = j1 * (Tn2TR c - Tn2TR a) by Lem;
Tn2TR y + (- Tn2TR a + Tn2TR a) = Tn2TR a + j1 * (Tn2TR c - Tn2TR a)
by HH,RLVECT_1:def 3; then
hH: Tn2TR y + 0.TOP-REAL 2 = Tn2TR a + j1 * (Tn2TR c - Tn2TR a)
by RLVECT_1:5;
Tn2TR x in LSeg (Tn2TR a,Tn2TR d) by T1,A1,G2,ThConv6; then
consider l being Real such that
z1: 0 <= l & l <= 1 & Tn2TR x - Tn2TR a = l * (Tn2TR d - Tn2TR a)
by ThConvAG;
z2: Tn2TR x - Tn2TR a = l * jd * (Tn2TR c - Tn2TR a)
by RLVECT_1:def 7,z1,Gy;
set i = l * jd;
Tn2TR x + (- Tn2TR a + Tn2TR a) = i * (Tn2TR c - Tn2TR a) + Tn2TR a
by z2,RLVECT_1:def 3; then
E3: Tn2TR x + 0.TOP-REAL 2 = i * (Tn2TR c - Tn2TR a) + Tn2TR a
by RLVECT_1:5;
for h being ExtReal st h in S holds i <= h
proof
let h be ExtReal;
assume h in S; then
consider j1 being Real such that
G1: h = j1 & j1 >= 1 & Tn2TR a + j1 * (Tn2TR c - Tn2TR a) in Y;
set z = Tn2TR a + j1 * (Tn2TR c - Tn2TR a);
reconsider z as Element of TarskiEuclid2Space by EUCLID:67,p2;
Tn2TR x in LSeg (Tn2TR a,Tn2TR z) by T1,A1,G1,ThConv6; then
consider ll being Real such that
z1: 0 <= ll & ll <= 1 & Tn2TR x - Tn2TR a = ll * (Tn2TR z - Tn2TR a)
by ThConvAG;
z0: Tn2TR c - Tn2TR a <> 0.TOP-REAL 2
proof
assume Tn2TR c - Tn2TR a = 0.TOP-REAL 2; then
Tn2TR c + (-Tn2TR a + Tn2TR a) = 0.TOP-REAL 2 + Tn2TR a
by RLVECT_1:def 3; then
Tn2TR c + 0.TOP-REAL 2 = 0.TOP-REAL 2 + Tn2TR a by RLVECT_1:5;
hence thesis by G9,ZFMISC_1:56;
end;
Tn2TR z - Tn2TR a = j1 * (Tn2TR c - Tn2TR a) +
(Tn2TR a + -Tn2TR a) by RLVECT_1:def 3
.= j1 * (Tn2TR c - Tn2TR a) + 0.TOP-REAL 2 by RLVECT_1:5
.= j1 * (Tn2TR c - Tn2TR a); then
Tn2TR x - Tn2TR a = ll * j1 * (Tn2TR c - Tn2TR a)
by z1,RLVECT_1:def 7; then
ll * j1 = i by RLVECT_1:37,z0,z2;
hence thesis by G1,XREAL_1:153,z1;
end; then
fF: i is LowerBound of S by XXREAL_2:def 2; then
f1: i <= k by XXREAL_2:def 4;
j1 in S by hH,HH,T1; then
F0: k <= j1 by XXREAL_2:3; then
f2: i <= j1 by f1,XXREAL_0:2;
ff: Tn2TR b - Tn2TR x = Tn2TR a + k * (Tn2TR c - Tn2TR a) +
(-i * (Tn2TR c - Tn2TR a) + -Tn2TR a)
by E3,RLVECT_1:31
.= (k * (Tn2TR c - Tn2TR a) + Tn2TR a) +- Tn2TR a +
-i * (Tn2TR c - Tn2TR a) by RLVECT_1:def 3
.= k * (Tn2TR c - Tn2TR a) + (Tn2TR a +- Tn2TR a) +
-i * (Tn2TR c - Tn2TR a) by RLVECT_1:def 3
.= k * (Tn2TR c - Tn2TR a) + 0.TOP-REAL 2 +
-i * (Tn2TR c - Tn2TR a) by RLVECT_1:5
.= k * (Tn2TR c - Tn2TR a) - i * (Tn2TR c - Tn2TR a)
.= (k - i) * (Tn2TR c - Tn2TR a) by RLVECT_1:35;
set l = (k - i) / (j1 - i);
per cases;
suppose i = j1; then
k = i by F0,f1,XXREAL_0:1; then
Tn2TR b - Tn2TR x = 0.TOP-REAL 2 + 0 * (Tn2TR c - Tn2TR a) by ff
.= 0.TOP-REAL 2 by THJE; then
Tn2TR b + (- Tn2TR x + Tn2TR x) = 0.TOP-REAL 2 + Tn2TR x
by RLVECT_1:def 3; then
Tn2TR b + 0.TOP-REAL 2 = 0.TOP-REAL 2 + Tn2TR x by RLVECT_1:5;
hence thesis by GTARSKI1:17;
end;
suppose i <> j1; then
i < j1 by f2,XXREAL_0:1; then
R1: j1 - i > 0 by XREAL_1:50;
Tn2TR y - Tn2TR x = (Tn2TR a + j1 * (Tn2TR c - Tn2TR a)) +
(- i * (Tn2TR c - Tn2TR a) + -Tn2TR a)
by RLVECT_1:31,E3,hH
.= (j1 * (Tn2TR c - Tn2TR a) + Tn2TR a) +- Tn2TR a -
i * (Tn2TR c - Tn2TR a)
by RLVECT_1:def 3
.= j1 * (Tn2TR c - Tn2TR a) + (Tn2TR a +- Tn2TR a) -
i * (Tn2TR c - Tn2TR a)
by RLVECT_1:def 3
.= j1 * (Tn2TR c - Tn2TR a) + 0.TOP-REAL 2 -
i * (Tn2TR c - Tn2TR a)
by RLVECT_1:5
.= (j1 - i) * (Tn2TR c - Tn2TR a) by RLVECT_1:35; then
(1 / (j1 - i)) * (Tn2TR y - Tn2TR x) =
(1 / (j1 - i)) * (j1 - i) * (Tn2TR c - Tn2TR a)
by RLVECT_1:def 7; then
(1 / (j1 - i)) * (Tn2TR y - Tn2TR x) =
1 * (Tn2TR c - Tn2TR a) by XCMPLX_0:def 7,R1; then
Tn2TR c - Tn2TR a = (1 / (j1 - i)) * (Tn2TR y - Tn2TR x)
by RVSUM_1:52; then
S2: Tn2TR b - Tn2TR x = l * (Tn2TR y - Tn2TR x) by RLVECT_1:def 7,ff;
R4: k - i <= j1 - i by XREAL_1:13,F0;
k - i >= 0 by fF,XREAL_1:48,XXREAL_2:def 4; then
Tn2TR b in LSeg (Tn2TR x,Tn2TR y) by S2,ThConvAGI,R4,XREAL_1:183;
hence thesis by ThConv6;
end;
end;
hence thesis;
end;
end;
registration
cluster TarskiEuclid2Space ->
satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom
satisfying_Euclid_Axiom satisfying_Continuity_Axiom;
coherence by AxiomA8,AxiomA9,AxiomA10,AxiomA11;
end;
begin :: Corrolaries
reserve X,Y for Subset of TarskiEuclid2Space;
theorem
for a being Element of TarskiEuclid2Space st
(for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y) & a in Y holds X = {a} or X is empty
proof
let a be Element of TarskiEuclid2Space;
assume that
A1: for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between a,x,y and
A2: a in Y;
M1: X c= {a}
proof
let x be object;
assume
L1: x in X;
then reconsider x as Element of TarskiEuclid2Space;
a = x by GTARSKI1:def 10,A1,A2,L1;
hence thesis by TARSKI:def 1;
end;
per cases;
suppose X is empty;
hence thesis;
end;
suppose X is non empty;
then consider x be object such that A3: x in X;
reconsider x as Element of TarskiEuclid2Space by A3;
a = x by GTARSKI1:def 10,A1,A2,A3;
then {a} c= X by TARSKI:def 1,A3;
hence thesis by M1;
end;
end;
theorem
for a being Element of TarskiEuclid2Space st
(for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y) & X is non empty & Y is non empty &
(X is trivial implies X <> {a}) holds
ex b being Element of TarskiEuclid2Space st
X c= Line(Tn2TR a, Tn2TR b) & Y c= Line(Tn2TR a, Tn2TR b)
proof
let a be Element of TarskiEuclid2Space such that
A1: for x,y being Element of TarskiEuclid2Space st
x in X & y in Y holds between a,x,y and
A1A: X is non empty and
A1B: Y is non empty and
A3: X is trivial implies X <> {a};
consider x0 be object such that
K1: x0 in X by A1A;
reconsider x0 as Element of TarskiEuclid2Space by K1;
consider c be object such that
MM: c in Y by A1B;
reconsider c as Element of TarskiEuclid2Space by MM;
V1: X c= LSeg(Tn2TR a,Tn2TR c)
proof
let x be object;
assume
DA: x in X;
then reconsider x1 = x as Element of TarskiEuclid2Space;
Tn2TR x1 in LSeg(Tn2TR a,Tn2TR c) by ThConv6,A1,DA,MM;
hence x in LSeg(Tn2TR a,Tn2TR c);
end;
t2: LSeg(Tn2TR a,Tn2TR c) c= Line(Tn2TR a,Tn2TR c) by RLTOPSP1:73; then
T1: X c= Line(Tn2TR a, Tn2TR c) by V1;
T2: x0 in Line(Tn2TR a, Tn2TR c) by t2,V1,K1;
Y c= Line(Tn2TR a, Tn2TR c)
proof
let y be object;
assume
V2: y in Y; then
reconsider y0 = y as Element of TarskiEuclid2Space;
per cases;
suppose
MU: x0 = a;
per cases;
suppose X is trivial;
then consider xx be object such that
KL: X = {xx} by A1A,ZFMISC_1:131;
thus thesis by MU,K1,KL,TARSKI:def 1,A3;
end;
suppose X is non trivial;
then consider a0,b0 be object such that
LO1: a0 in X and
LO2: b0 in X and
LO3: a0 <> b0;
ex x1 be object st x1 in X & x1 <> a
proof
assume
AA: for x1 be object holds not x1 in X or x1 = a;
a0 <> a or b0 <> a by LO3;
hence contradiction by LO1,LO2,AA;
end; then
consider x1 be object such that
K1: x1 in X and
VAL: x1 <> a;
reconsider x1 as Element of TarskiEuclid2Space by K1;
N1: Tn2TR x1 in LSeg(Tn2TR a,Tn2TR y0) by ThConv6,V2,K1,A1;
n2: LSeg(Tn2TR a,Tn2TR y0) c= Line(Tn2TR a,Tn2TR y0) by RLTOPSP1:73;
Tn2TR a in Line(Tn2TR a,Tn2TR y0) by RLTOPSP1:72; then
ff: Line(Tn2TR x1,Tn2TR a) = Line(Tn2TR a,Tn2TR y0)
by N1,n2,VAL,RLTOPSP1:75;
Tn2TR a in Line(Tn2TR a,Tn2TR c) by RLTOPSP1:72;
then Line(Tn2TR a,Tn2TR x1) c= Line(Tn2TR a,Tn2TR c)
by K1,T1,RLTOPSP1:74;
hence thesis by ff,RLTOPSP1:72;
end;
end;
suppose
VAL: x0 <> a;
N1: Tn2TR x0 in LSeg(Tn2TR a,Tn2TR y0) by ThConv6,V2,K1,A1;
n2: LSeg(Tn2TR a,Tn2TR y0) c= Line(Tn2TR a,Tn2TR y0) by RLTOPSP1:73;
Tn2TR a in Line(Tn2TR a,Tn2TR y0) by RLTOPSP1:72; then
ff: Line(Tn2TR x0,Tn2TR a) = Line(Tn2TR a,Tn2TR y0)
by N1,n2,VAL,RLTOPSP1:75;
Tn2TR a in Line(Tn2TR a,Tn2TR c) by RLTOPSP1:72;
then Line(Tn2TR a,Tn2TR x0) c= Line(Tn2TR a,Tn2TR c) by T2,RLTOPSP1:74;
hence thesis by ff,RLTOPSP1:72;
end;
end;
hence thesis by T1;
end;