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 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;
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;
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;
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;
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;
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;
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 H1, BTransitivityOrdered;
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 H1, Gupta; :: thesis: verum
end;
end;
end;
hence c on_line a,x by H2, Bsymmetry; :: thesis: verum