theorem :: AFPROJ:24

for AS being AffinSpace
for x being set holds
( x is Element of the Lines of (ProjHorizon AS) iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) ) by Th15;