theorem :: GTARSKI3:25

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,b,c & between a,p,b holds
between4 a,p,b,c by Satz3p6p1, Satz3p6p2;