let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds
a,b,c,d are_ordered
let a, b, c, d be POINT of S; ( between a,b,d & between b,c,d implies a,b,c,d are_ordered )
assume that
H1:
between a,b,d
and
H2:
between b,c,d
; a,b,c,d are_ordered