for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for p, q, s being POINT of S st p <> q & s <> p & s in Line (p,q) holds
Line (p,q) = Line (p,s)