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