let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between a,c,d holds
between a,d,c
let a, b, c, d be POINT of S; ( a <> b & between a,b,c & between a,b,d & not between a,c,d implies between a,d,c )
assume A1:
( a <> b & between a,b,c & between a,b,d )
; ( between a,c,d or between a,d,c )
then
( between b,d,c or between b,c,d )
by GTARSKI1:37;
hence
( between a,c,d or between a,d,c )
by A1, Satz3p5p2; verum