theorem :: GTARSKI3:27

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,p,b holds
between5 a,p,b,c,d