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

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