let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for A being LINE of IPP holds id (CHAIN A) is Projection of IPP
let A be LINE of IPP; :: thesis: id (CHAIN A) is Projection of IPP
consider o being POINT of IPP such that
A1: not o on A by PROJRED1:1;
id (CHAIN A) = IncProj (A,o,A) by A1, Th10;
hence id (CHAIN A) is Projection of IPP by A1, Def3; :: thesis: verum