let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( between a,b,c & between a,c,d implies a,b,c,d are_ordered )
assume
( between a,b,c & between a,c,d )
; 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; verum