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

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