set S = TarskiEuclid2Space ;
now for a, b, p, q, z being POINT of TarskiEuclid2Space st between a,p,z & between b,q,z holds
ex x being POINT of TarskiEuclid2Space st
( between p,x,b & between q,x,a )let a,
b,
p,
q,
z be
POINT of
TarskiEuclid2Space;
( between a,p,z & between b,q,z implies ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x ) )assume that A1:
between a,
p,
z
and A2:
between b,
q,
z
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
( z1,p1,b1 are_collinear or not z1,p1,b1 are_collinear )
;
suppose
z1,
p1,
b1 are_collinear
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )then
z1,
p1 '||' z1,
b1
;
per cases then
( z1,p1 // z1,b1 or b1,z1 // z1,p1 )
by DIRAF:2;
suppose
z1,
p1 // z1,
b1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )then consider u,
v,
w,
y being
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;
per cases then
( u = v or u = y or ex a, b being Real st
( 0 < a & 0 < b & a * (v - u) = b * (y - u) ) )
by A8;
suppose
u = v
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )then A10:
between p,
q,
b
by A9, A2, ThConv7bis;
between q,
q,
a
by ThConv7;
hence
ex
x being
POINT of
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A10;
verum end; suppose
u = y
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A12;
verum end; suppose
ex
a,
b being
Real st
(
0 < a &
0 < b &
a * (v - u) = b * (y - u) )
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )then consider r,
s being
Real such that A13:
0 < r
and A14:
0 < s
and A15:
r * (v - u) = s * (y - u)
;
per cases
( r = s or r < s or s < r )
by XXREAL_0:1;
suppose
r = s
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A17;
verum end; suppose A20:
r < s
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A32;
verum end; suppose A33:
s < r
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )set t =
s / r;
s / r < r / r
by A33, A13, XREAL_1:74;
then A34:
s / r < 1
by A13, XCMPLX_1:60;
A35:
((s / r) * y) - ((s / r) * u) =
|[((s / r) * (y `1)),((s / r) * (y `2))]| - ((s / r) * u)
by EUCLID:57
.=
|[((s / r) * (y `1)),((s / r) * (y `2))]| - |[((s / r) * (u `1)),((s / r) * (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:
((s / r) * y) - ((s / r) * 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
.=
(((s / r) * y) - ((s / r) * u)) + u
by A37, EUCLID:53
.=
(|[((s / r) * (y `1)),((s / r) * (y `2))]| - ((s / r) * u)) + u
by EUCLID:57
.=
(|[((s / r) * (y `1)),((s / r) * (y `2))]| - |[((s / r) * (u `1)),((s / r) * (u `2))]|) + u
by EUCLID:57
.=
(|[((s / r) * (y `1)),((s / r) * (y `2))]| - |[((s / r) * (u `1)),((s / r) * (u `2))]|) + |[(u `1),(u `2)]|
by EUCLID:53
.=
|[(((s / r) * (y `1)) - ((s / r) * (u `1))),(((s / r) * (y `2)) - ((s / r) * (u `2)))]| + |[(u `1),(u `2)]|
by EUCLID:62
.=
|[((((s / r) * (y `1)) - ((s / r) * (u `1))) + (u `1)),((((s / r) * (y `2)) - ((s / r) * (u `2))) + (u `2))]|
by EUCLID:56
.=
|[(((s / r) * (y `1)) + ((1 - (s / r)) * (u `1))),(((s / r) * (y `2)) + ((1 - (s / r)) * (u `2)))]|
.=
|[((1 - (s / r)) * (u `1)),((1 - (s / r)) * (u `2))]| + |[((s / r) * (y `1)),((s / r) * (y `2))]|
by EUCLID:56
.=
((1 - (s / r)) * u) + |[((s / r) * (y `1)),((s / r) * (y `2))]|
by EUCLID:57
.=
((1 - (s / r)) * u) + ((s / r) * 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
( z <> p or z = p )
;
suppose A42:
z <> p
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )
(
Mid z1,
p1,
b1 &
Mid z1,
p1,
a1 )
by A38, A39, THSS3;
per cases then
( Mid p1,b1,a1 or Mid p1,a1,b1 )
by A42, DIRAF:15;
suppose
Mid p1,
b1,
a1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )per cases
( Mid z1,p1,q1 or Mid z1,q1,p1 )
by A41, DIRAF:17;
suppose
Mid z1,
p1,
q1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A43;
verum end; suppose
Mid z1,
q1,
p1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A44;
verum end; suppose
Mid p1,
a1,
b1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )per cases
( Mid z1,p1,q1 or Mid z1,q1,p1 )
by A41, DIRAF:17;
suppose
Mid z1,
p1,
q1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A45;
verum end; suppose
Mid z1,
q1,
p1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A46;
verum end; end; end; end; suppose
b1,
z1 // z1,
p1
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )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;
end; end; suppose A53:
not
z1,
p1,
b1 are_collinear
;
ex x being POINT of TarskiEuclid2Space st
( between b3,b6,b2 & between b4,b6,x )consider y being
Element of
OAS such that A54:
Mid p1,
y,
b1
and A55:
Mid q1,
y,
a1
by A3, A53, A4, A5;
MetrStruct(# the
U1 of
TarskiEuclid2Space, the
distance of
TarskiEuclid2Space #)
= MetrStruct(# the
U1 of
(Euclid 2), the
distance of
(Euclid 2) #)
by GTARSKI1:def 13;
then reconsider yt =
y as
POINT of
TarskiEuclid2Space by EUCLID:22;
A56:
between p,
yt,
b
by A54, THSS3;
between q,
yt,
a
by A55, THSS3;
hence
ex
x being
POINT of
TarskiEuclid2Space st
(
between p,
x,
b &
between q,
x,
a )
by A56;
verum end; end;
hence
TarskiEuclid2Space is satisfying_Pasch
; verum