:: deftheorem defines halfline GTARSKI3:def 9 :
for S being TarskiGeometryStruct
for a, p being POINT of S holds halfline (p,a) = { x where x is POINT of S : p out x,a } ;