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