let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & b <> c & b <> d holds
not between c,b,d
let a, b, c, d be POINT of S; :: thesis: ( a <> b & between a,b,c & between a,b,d & b <> c & b <> d implies not between c,b,d )
assume that
H1: a <> b and
H2: between a,b,c and
H3: between a,b,d and
H4: b <> c and
H5: b <> d and
H6: between c,b,d ; :: thesis: contradiction
consider x being POINT of S such that
X2: ( a,b,c,x are_ordered & a,b,d,x are_ordered ) by H1, H2, H3, BextendToLine;
c,b,d,x are_ordered by H5, H6, BTransitivityOrdered, X2;
hence contradiction by H4, BEquality, X2; :: thesis: verum