let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis:
let a, b, p be POINT of S; :: thesis:
let A be Subset of S; :: thesis:
assume that
A1: A is_line and
A2: p in A and
A3: Collinear a,b,p ; :: thesis:

hereby :: thesis:

assume A4: between a,A,b ; :: thesis:
then consider t being POINT of S such that
A5: t in A and
A6: between a,t,b ;
a <> b by A4, GTARSKI1:def 10;
then A7: Line (a,b) is_line ;

per cases ;

suppose p = t ; :: thesis:

hence ( between a,p,b & not a in A & not b in A ) by A4, A6; :: thesis:

end;

suppose A8: p <> t ; :: thesis:

then A9: Line (p,t) = A by A1, A2, A5, GTARSKI3:87;
between a,p,b

proof

per cases by A3;

suppose between a,b,p ; :: thesis:

then ( between p,b,a & between b,t,a ) by A6, GTARSKI3:14;
then Collinear p,b,t by GTARSKI3:17;
then Collinear p,t,b by GTARSKI3:45;
hence between a,p,b by A9, A4; :: thesis:

end;

suppose between b,p,a ; :: thesis:

hence between a,p,b by GTARSKI3:14; :: thesis:

end;

suppose between p,a,b ; :: thesis:

then ( Collinear a,b,p & Collinear a,b,t ) by A6, GTARSKI3:14;
then ( p in { x where x is POINT of S : Collinear a,b,x } & t in { x where x is POINT of S : Collinear a,b,x } ) ;
then Line (a,b) = Line (p,t) by A7, A8, GTARSKI3:87
.= A by A8, A1, A2, A5, GTARSKI3:87 ;
hence between a,p,b by A4, GTARSKI3:83; :: thesis:

end;

end;

end;

hence ( between a,p,b & not a in A & not b in A ) by A4; :: thesis:

end;

end;

end;

assume ( between a,p,b & not a in A & not b in A ) ; :: thesis:
hence between a,A,b by A1, A2; :: thesis: