:: deftheorem defines is_line GTARSKI3:def 11 :
for S being non empty TarskiGeometryStruct
for A being Subset of S holds
( A is_line iff ex p, q being POINT of S st
( p <> q & A = Line (p,q) ) );