theorem Th37: :: AFPROJ:37

for AS being AffinSpace
for a being Element of the Points of (ProjHorizon AS)
for a9 being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )