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,d & between b,c,d holds
between a,b,c
let a, b, c, d be POINT of S; ( between a,b,d & between b,c,d implies between a,b,c )
assume
( between a,b,d & between b,c,d )
; between a,b,c
then consider x being POINT of S such that
A1:
( between b,x,b & between c,x,a )
by GTARSKI1:def 11;
b = x
by A1, GTARSKI1:def 10;
hence
between a,b,c
by A1, Satz3p2; verum