consider A, B being LINE of IPP;
consider a being POINT of IPP such that
A1: ( not a on A & not a on B ) by PROJRED1:6;
take IncProj A,a,B ; :: thesis: ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & IncProj A,a,B = IncProj A,a,B )
thus ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & IncProj A,a,B = IncProj A,a,B ) by A1; :: thesis: verum