for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & Collinear a,b,c & Collinear a,b,d holds
Collinear a,c,d