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