let IPP be IncProjSp; :: thesis: for A being LINE of IPP ex a being POINT of IPP st a on A
let A be LINE of IPP; :: thesis: ex a being POINT of IPP st a on A
consider a, b, c being POINT of IPP such that
A1: ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) by INCPROJ:def 12;
take a ; :: thesis: a on A
thus a on A by A1; :: thesis: verum