let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, p, q being POINT of S st between a,c,p & between b,q,c holds
ex x being POINT of S st
( between a,x,b & between p,q,x )
let a, b, c, p, q be POINT of S; :: thesis: ( between a,c,p & between b,q,c implies ex x being POINT of S st
( between a,x,b & between p,q,x ) )
assume that
A1: between a,c,p and
A2: between b,q,c ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

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

suppose A3: p = q ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

take b ; :: thesis: ( between a,b,b & between p,q,b )
thus ( between a,b,b & between p,q,b ) by A3, GTARSKI3:13, GTARSKI3:14; :: thesis: verum

end;

suppose A4: p <> q ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

per cases ( c = q or c <> q ) ;

suppose A5: c = q ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

take a ; :: thesis: ( between a,a,b & between p,q,a )
thus ( between a,a,b & between p,q,a ) by A1, A5, GTARSKI3:13, GTARSKI3:14; :: thesis: verum

end;

suppose A6: c <> q ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

A7: between p,c,a by A1, GTARSKI3:14;

per cases ( Collinear p,q,c or not Collinear p,q,c ) ;

suppose A8: Collinear p,q,c ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

per cases ( between p,q,c or not between p,q,c ) ;

suppose A9: between p,q,c ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

take a ; :: thesis: ( between a,a,b & between p,q,a )
thus ( between a,a,b & between p,q,a ) by A7, A9, GTARSKI3:15, GTARSKI3:18; :: thesis: verum

end;

suppose not between p,q,c ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

then A10: q out p,c by A8, GTARSKI3:73;

per cases then ( between q,p,c or between q,c,p ) ;

suppose between q,p,c ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

then A11: ( between c,q,b & between c,p,q ) by A2, GTARSKI3:14;
take b ; :: thesis: ( between a,b,b & between p,q,b )
thus ( between a,b,b & between p,q,b ) by A11, GTARSKI3:13, GTARSKI3:18; :: thesis: verum

end;

suppose between q,c,p ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

then A12: ( between c,q,b & between p,c,q ) by A2, GTARSKI3:14;
take b ; :: thesis: ( between a,b,b & between p,q,b )
thus ( between a,b,b & between p,q,b ) by A10, A12, GTARSKI3:13, GTARSKI3:19; :: thesis: verum

end;

end;

end;

end;

end;

suppose A13: not Collinear p,q,c ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

set A = Line (p,q);
A14: Line (p,q) <> Line (c,q)

proof

assume Line (p,q) = Line (c,q) ; :: thesis: contradiction
then c in Line (p,q) by GTARSKI3:83;
then ex x being POINT of S st
( c = x & Collinear p,q,x ) ;
hence contradiction by A13; :: thesis: verum

end;

per cases ( b in Line (p,q) or not b in Line (p,q) ) ;

suppose A15: b in Line (p,q) ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

Collinear b,q,c by A2;
then Collinear c,q,b by GTARSKI3:45;
then A16: b in Line (c,q) ;
A17: ( q in Line (p,q) & q in Line (c,q) ) by GTARSKI3:83;
take b ; :: thesis: ( between a,b,b & between p,q,b )
b = q

proof

assume A18: b <> q ; :: thesis: contradiction
Line (p,q) is_line by A4;
then G1: Line (b,q) = Line (p,q) by A15, A17, A18, GTARSKI3:87;
Line (c,q) is_line by A6;
hence contradiction by G1, A14, A16, A17, A18, GTARSKI3:87; :: thesis: verum

end;

hence ( between a,b,b & between p,q,b ) by GTARSKI3:13; :: thesis: verum

end;

suppose A19: not b in Line (p,q) ; :: thesis: ex x being POINT of S st
( between a,x,b & between p,q,x )

R1: Line (p,q) is_line by A4;
R2: not c in Line (p,q)

proof

assume A20: c in Line (p,q) ; :: thesis: contradiction
( q in Line (p,q) & Line (p,q) is_line ) by A4, GTARSKI3:83;
then A21: Line (c,q) = Line (p,q) by A20, A6, GTARSKI3:87;
Collinear c,q,b by A2, GTARSKI3:14;
hence contradiction by A19, A21; :: thesis: verum

end;

( between b,q,c & q in Line (p,q) ) by A2, GTARSKI3:83;
then T2: between c, Line (p,q),b by R1, R2, A19, GTARSKI3:14;
O1: p <> c

proof

assume p = c ; :: thesis: contradiction
then Collinear p,c,q by GTARSKI3:46;
hence contradiction by A13, GTARSKI3:45; :: thesis: verum

end;

p <> a

proof

assume p = a ; :: thesis: contradiction
then Collinear b,q,p by A2, A1, GTARSKI1:def 10;
then Collinear p,q,b by GTARSKI3:45;
hence contradiction by A19; :: thesis: verum

end;

then p out c,a by O1, A1, GTARSKI3:14;
then between a, Line (p,q),b by GTARSKI3:83, T2, Th12;
then consider x being POINT of S such that
A22: x in Line (p,q) and
A23: between a,x,b ;
P1: p <> x

proof

assume p = x ; :: thesis: contradiction
then ( between c,p,b & between c,q,b ) by A23, A1, A2, GTARSKI3:14, GTARSKI3:18;
then ( Collinear c,p,q or Collinear c,q,p ) by GTARSKI3:58;
hence contradiction by A13, GTARSKI3:45; :: thesis: verum

end;

( Line (p,q) is_line & p in Line (p,q) ) by A4, GTARSKI3:83;
then A24: Line (p,x) = Line (p,q) by P1, A22, GTARSKI3:87;
take x ; :: thesis: ( between a,x,b & between p,q,x )
( between b,x,a & between p,c,a ) by A1, A23, GTARSKI3:14;
then consider t being POINT of S such that
A25: between x,t,p and
A26: between c,t,b by GTARSKI1:def 11;
A27: Collinear p,x,t by A25;
Collinear c,t,b by A26;
then Collinear c,b,t by GTARSKI3:45;
then A28: t in Line (c,b) ;
R1: c <> b by A6, A2, GTARSKI1:def 10;
Collinear c,b,q by A2;
then q in Line (c,b) ;
then ( t in Line (c,q) & t in Line (p,q) & q in Line (c,q) & q in Line (p,q) & Line (c,q) is_line & Line (p,q) is_line ) by A4, A27, A28, A24, GTARSKI3:82, GTARSKI3:83, R1, A6;
then t = q by A14, GTARSKI3:89;
hence ( between a,x,b & between p,q,x ) by A23, A25, GTARSKI3:14; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;