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

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