for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st ex p, q being POINT of S st p <> q holds
( Collinear a,b,c iff ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) )