theorem :: GTARSKI3:33

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