let IPP be IncProjSp; for A being LINE of IPP holds
not for a being POINT of IPP holds a on A
let A be LINE of IPP; not for a being POINT of IPP holds a on A
consider p being POINT of IPP, L being LINE of IPP such that
A1:
not p on L
by INCPROJ:def 6;
now ( A <> L implies ex a being POINT of IPP st not a on A )assume A2:
A <> L
;
not for a being POINT of IPP holds a on Ahence
not for
a being
POINT of
IPP holds
a on A
;
verum end;
hence
not for a being POINT of IPP holds a on A
by A1; verum