theorem :: GTARSKI3:31

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