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)
; 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; verum