set S = TarskiEuclid2Space ;

now :: thesis: 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; :: thesis: ( between a,p,z & between b,q,z implies ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,x ) )
assume that
A1: between a,p,z and
A2: between b,q,z ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

suppose u = y ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

suppose ex a, b being Real st
( 0 < a & 0 < b & a * (v - u) = b * (y - u) ) ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

suppose A20: r < s ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

suppose A33: s < r ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,x )

per cases ( Mid z1,p1,q1 or Mid z1,q1,p1 ) by A41, DIRAF:17;

suppose Mid z1,p1,q1 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

suppose Mid z1,q1,p1 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

end;

end;

suppose Mid p1,a1,b1 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,x )

per cases ( Mid z1,p1,q1 or Mid z1,q1,p1 ) by A41, DIRAF:17;

suppose Mid z1,p1,q1 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

suppose Mid z1,q1,p1 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

end;

end;

end;

end;

suppose A47: z = p ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,x )

between q,q,a by ThConv7;
hence ex x being POINT of TarskiEuclid2Space st
( between p,x,b & between q,x,a ) by A47, A40; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose b1,z1 // z1,p1 ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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;

per cases ( z = p or z <> p ) ;

suppose z = p ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,x )

then A52: between p,q,b by 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 A52; :: thesis: verum

end;

suppose z <> p ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,x )

then between q,z,a by A50, A51, THNOIX3;
hence ex x being POINT of TarskiEuclid2Space st
( between p,x,b & between q,x,a ) by A48; :: thesis: verum

end;

end;

end;

end;

end;

suppose A53: not z1,p1,b1 are_collinear ; :: thesis: ex x being POINT of TarskiEuclid2Space st
( between b₃,b₆,b₂ & between b₄,b₆,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; :: thesis: verum

end;

end;

end;

hence TarskiEuclid2Space is satisfying_Pasch ; :: thesis: verum