theorem :: GTARSKI3:29

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