:: deftheorem defines is_half_line GTARSKI5:def 4 :
for S being non empty TarskiGeometryStruct
for K being Subset of S holds
( K is_half_line iff ex p, a being POINT of S st
( p <> a & K = halfline (p,a) ) );