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