:: deftheorem defines Line GTARSKI3:def 10 :
for S being non empty TarskiGeometryStruct
for p, q being POINT of S holds Line (p,q) = { x where x is POINT of S : Collinear p,q,x } ;