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 )

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

hence
c on_line a,x
by H2, Bsymmetry; :: thesis: verum
consider m being POINT of S such that

X5: ( between b,a,m & a,m equiv a,b ) by A4;

X6: a <> m by H1, X5, EquivSymmetric, A3;

end;X5: ( between b,a,m & a,m equiv a,b ) by A4;

X6: a <> m by H1, X5, EquivSymmetric, A3;

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 X1, Bsymmetry, H4;

end;

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 H1, Gupta;

then ( a,b,x,c are_ordered or a,b,c,x are_ordered ) by X3, BTransitivityOrdered;

hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

end;then ( a,b,x,c are_ordered or a,b,c,x are_ordered ) by X3, BTransitivityOrdered;

hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

suppose
( between a,b,x & between a,c,b )
; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )

then
a,c,b,x are_ordered
by B123and134Ordered;

hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

end;hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

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 H1, BTransitivityOrdered;

hence ( between a,x,c or between a,c,x or between x,a,c ) by Bsymmetry; :: thesis: verum

end;hence ( between a,x,c or between a,c,x or between x,a,c ) by Bsymmetry; :: thesis: verum

suppose
( between a,x,b & between a,b,c )
; :: thesis: ( between a,x,c or between a,c,x or between x,a,c )

then
a,x,b,c are_ordered
by B123and134Ordered;

hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

end;hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

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 X5, Bsymmetry;

then ( between m,a,c & between m,a,x ) by X4, B124and234then123;

hence ( between a,x,c or between a,c,x or between x,a,c ) by X6, Gupta; :: thesis: verum

end;then ( between m,a,c & between m,a,x ) by X4, B124and234then123;

hence ( between a,x,c or between a,c,x or between x,a,c ) by X6, Gupta; :: thesis: verum

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;hence ( between a,x,c or between a,c,x or between x,a,c ) by Bsymmetry; :: thesis: verum

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 H1, BTransitivityOrdered;

hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum

end;hence ( between a,x,c or between a,c,x or between x,a,c ) ; :: thesis: verum