theorem Th40: :: AFPROJ:40

for AS being AffinSpace
for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )