let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S
for A being Subset of S st A out a,b & between a,c,b holds
A out c,a
let a, b, c be POINT of S; :: thesis: for A being Subset of S st A out a,b & between a,c,b holds
A out c,a
let A be Subset of S; :: thesis: ( A out a,b & between a,c,b implies A out c,a )
assume that
A1: A out a,b and
A2: between a,c,b ; :: thesis: A out c,a
consider d being POINT of S such that
A3: between a,A,d and
A4: between b,A,d by A1;
consider x being POINT of S such that
A5: x in A and
A6: between a,x,d by A3;
consider y being POINT of S such that
A7: y in A and
A8: between b,y,d by A4;
consider t being POINT of S such that
A9: between c,t,d and
A10: between x,t,y by A2, A6, A8, GTARSKI3:40;
A11: not c in A

proof

assume c in A ; :: thesis: contradiction
then between a,A,b by A2, A3, A4;
hence contradiction by A1, Th15; :: thesis: verum

end;

between c,A,d

proof

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: between c,A,d

then t = x by A10, GTARSKI1:def 10;
hence between c,A,d by A5, A11, A3, A9; :: thesis: verum

end;

suppose A12: x <> y ; :: thesis: between c,A,d

G1: Line (x,y) = A by A12, A5, A7, A1, Th24, GTARSKI3:87;
Collinear x,y,t by A10, GTARSKI3:14;
then t in A by G1;
hence between c,A,d by A11, A3, A9; :: thesis: verum

end;

end;

end;

hence A out c,a by A3; :: thesis: verum