theorem Th42: :: AFPROJ:42

for AS being AffinSpace
for x being POINT of (IncProjSp_of AS)
for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)