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