:: deftheorem defines half-plane GTARSKI5:def 8 :
for S being non empty TarskiGeometryStruct
for p, q, a being POINT of S st not Collinear p,q,a holds
half-plane (p,q,a) = half-plane ((Line (p,q)),a);