theorem :: AFPROJ:21

for AS being AffinSpace
for x being set holds
( x is Element of the Points of (ProjHorizon AS) iff ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by Th14;