theorem :: GTARSKI3:81

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for p, q, r being POINT of S st p <> q & p <> r & between q,p,r holds
Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))