let IPP be IncProjSp; :: thesis: for A being LINE of IPP holds
not for a being POINT of IPP holds a on A
let A be LINE of IPP; :: thesis: 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 11;

now

assume A2: A <> L ; :: thesis: not for a being POINT of IPP holds a on A

now

consider q, r, s being POINT of IPP such that
A3: ( q <> r & r <> s & s <> q & q on L & r on L & s on L ) by INCPROJ:def 12;
( not q on A or not r on A ) by A2, A3, INCPROJ:def 9;
hence not for a being POINT of IPP holds a on A ; :: thesis: verum

end;

hence not for a being POINT of IPP holds a on A ; :: thesis: verum

end;

hence not for a being POINT of IPP holds a on A by A1; :: thesis: verum