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 b,c,d holds
between b,d,c
let a, b, c, d be POINT of S; ( a <> b & between a,b,c & between a,b,d & not between b,c,d implies between b,d,c )
assume A1:
( a <> b & between a,b,c & between a,b,d )
; ( between b,c,d or between b,d,c )
then
( between a,c,d or between a,d,c )
by Satz5p1;
hence
( between b,c,d or between b,d,c )
by A1, Satz3p6p1; verum