theorem Th25: :: AFPROJ:25

for AS being AffinSpace
for x being set st x is Element of the Lines of (ProjHorizon AS) holds
[x,2] is LINE of (IncProjSp_of AS)