let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds
between b,c,d
let a, b, c, d be POINT of S; ( between a,b,c & between a,c,d implies between b,c,d )
assume
( between a,b,c & between a,c,d )
; between b,c,d
then
( between c,b,a & between d,c,a )
by Satz3p2;
then
between d,c,b
by Satz3p5p1;
hence
between b,c,d
by Satz3p2; verum