let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for f being Projection of IPP holds f " is Projection of IPP
let f be Projection of IPP; :: thesis: f " is Projection of IPP
consider a being POINT of IPP, A, B being LINE of IPP such that
A1: ( not a on A & not a on B ) and
A2: f = IncProj (A,a,B) by Def3;
f " = IncProj (B,a,A) by A1, A2, Th8;
hence f " is Projection of IPP by A1, Def3; :: thesis: verum