theorem :: GTARSKI3:19

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds
( between a,c,d & between a,b,d ) by Satz3p7p1, Satz3p7p2;