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
between a,b,d
let a, b, c, d be POINT of S; ( between a,b,c & between a,c,d implies between a,b,d )
assume
( between a,b,c & between a,c,d )
; between a,b,d
then
( between c,b,a & between d,c,a )
by Satz3p2;
then
between d,b,a
by Satz3p5p2;
hence
between a,b,d
by Satz3p2; verum