theorem Th7: :: PROJRED1:7

for IPP being IncProjSp
for A being LINE of IPP ex a being POINT of IPP st a on A