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