theorem :: GTARSKI3:32

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,d,p holds
( between5 a,b,c,d,p & ( a <> d implies between5 a,b,c,d,p ) )