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

a,b,c,d are_ordered

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

assume ( between a,b,c & between a,c,d ) ; :: thesis: a,b,c,d are_ordered

then ( between d,c,a & between c,b,a ) by Bsymmetry;

then d,c,b,a are_ordered by B124and234Ordered;

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

a,b,c,d are_ordered

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

assume ( between a,b,c & between a,c,d ) ; :: thesis: a,b,c,d are_ordered

then ( between d,c,a & between c,b,a ) by Bsymmetry;

then d,c,b,a are_ordered by B124and234Ordered;

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