let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, x being POINT of S st a <> b & a <> x & x on_line a,b & c on_line a,b holds
c on_line a,x

let a, b, c, x be POINT of S; :: thesis: ( a <> b & a <> x & x on_line a,b & c on_line a,b implies c on_line a,x )
assume that
H1: a <> b and
H2: a <> x ; :: thesis: ( not x on_line a,b or not c on_line a,b or c on_line a,x )
assume x on_line a,b ; :: thesis: ( not c on_line a,b or c on_line a,x )
then X1: ( between a,b,x or between a,x,b or between x,a,b ) by Bsymmetry;
assume H4: c on_line a,b ; :: thesis: c on_line a,x
( between a,x,c or between a,c,x or between x,a,c )
proof
consider m being POINT of S such that
X5: ( between b,a,m & a,m equiv a,b ) by A4;
X6: a <> m by ;
per cases ( ( between a,b,x & between a,b,c ) or ( between a,b,x & between a,c,b ) or ( between a,b,x & between c,a,b ) or ( between a,x,b & between a,b,c ) or ( between a,x,b & between a,c,b ) or ( between a,x,b & between c,a,b ) or ( between x,a,b & between a,b,c ) or ( between x,a,b & between a,c,b ) or ( between x,a,b & between c,a,b ) ) by ;
suppose X3: ( between a,b,x & between a,b,c ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
then ( between b,x,c or between b,c,x ) by ;
then ( a,b,x,c are_ordered or a,b,c,x are_ordered ) by ;
hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum
end;
suppose ( between a,b,x & between a,c,b ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
end;
suppose ( between a,b,x & between c,a,b ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
then c,a,b,x are_ordered by ;
hence ( between a,x,c or between a,c,x or between x,a,c ) by Bsymmetry; :: thesis: verum
end;
suppose ( between a,x,b & between a,b,c ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
end;
suppose X4: ( between a,x,b & between a,c,b ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
between m,a,b by ;
then ( between m,a,c & between m,a,x ) by ;
hence ( between a,x,c or between a,c,x or between x,a,c ) by ; :: thesis: verum
end;
suppose ( between a,x,b & between c,a,b ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
then between c,a,x by B124and234then123;
hence ( between a,x,c or between a,c,x or between x,a,c ) by Bsymmetry; :: thesis: verum
end;
suppose ( between x,a,b & between a,b,c ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
then x,a,b,c are_ordered by ;
hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum
end;
suppose ( between x,a,b & between a,c,b ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
hence ( between a,x,c or between a,c,x or between x,a,c ) by B124and234then123; :: thesis: verum
end;
suppose ( between x,a,b & between c,a,b ) ; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )
then ( between b,a,x & between b,a,c ) by Bsymmetry;
hence ( between a,x,c or between a,c,x or between x,a,c ) by ; :: thesis: verum
end;
end;
end;
hence c on_line a,x by ; :: thesis: verum