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

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