for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A being Subset of S
for a, b being POINT of S st A is_line & a <> b & a in A & b in A holds
A = Line (a,b)