set A = the LINE of IPP;
consider a being POINT of IPP such that
A1: ( not a on the LINE of IPP & not a on the LINE of IPP ) by PROJRED1:6;
take IncProj ( the LINE of IPP,a, the LINE of IPP) ; :: thesis: ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & IncProj ( the LINE of IPP,a, the LINE of IPP) = 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 ( the LINE of IPP,a, the LINE of IPP) = IncProj (A,a,B) ) by A1; :: thesis: verum