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

a,b,c,d are_ordered

let a, b, c, d be POINT of S; :: thesis: ( b <> c & between a,b,c & between b,c,d implies a,b,c,d are_ordered )

assume that

H1: b <> c and

H2: between a,b,c ; :: thesis: ( not between b,c,d or a,b,c,d are_ordered )

assume H3: between b,c,d ; :: thesis: a,b,c,d are_ordered

then X1: between a,c,d by H1, H2, BTransitivity;

X2: between d,c,b by H3, Bsymmetry;

between c,b,a by H2, Bsymmetry;

then between d,b,a by H1, X2, BTransitivity;

hence a,b,c,d are_ordered by H2, X1, H3, Bsymmetry; :: thesis: verum

a,b,c,d are_ordered

let a, b, c, d be POINT of S; :: thesis: ( b <> c & between a,b,c & between b,c,d implies a,b,c,d are_ordered )

assume that

H1: b <> c and

H2: between a,b,c ; :: thesis: ( not between b,c,d or a,b,c,d are_ordered )

assume H3: between b,c,d ; :: thesis: a,b,c,d are_ordered

then X1: between a,c,d by H1, H2, BTransitivity;

X2: between d,c,b by H3, Bsymmetry;

between c,b,a by H2, Bsymmetry;

then between d,b,a by H1, X2, BTransitivity;

hence a,b,c,d are_ordered by H2, X1, H3, Bsymmetry; :: thesis: verum