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

now :: thesis: ( a on L implies ex A being LINE of IPP st not a on A )

consider q, r, s being POINT of IPP such that
q <> r and
r <> s and
A2: s <> q and
A3: q on L and
r on L and
A4: s on L by INCPROJ:def 7;
assume A5: a on L ; :: thesis: not for A being LINE of IPP holds a on A

A6: now :: thesis: ( a <> s implies ex A being LINE of IPP st not a on A )

consider S being LINE of IPP such that
A7: ( s on S & p on S ) by INCPROJ:def 5;
assume a <> s ; :: thesis: not for A being LINE of IPP holds a on A
then not a on S by A1, A5, A4, A7, INCPROJ:def 4;
hence not for A being LINE of IPP holds a on A ; :: thesis: verum

end;

now :: thesis: ( a <> q implies ex A being LINE of IPP st not a on A )

consider S being LINE of IPP such that
A8: ( q on S & p on S ) by INCPROJ:def 5;
assume a <> q ; :: thesis: not for A being LINE of IPP holds a on A
then not a on S by A1, A5, A3, A8, INCPROJ:def 4;
hence not for A being LINE of IPP holds a on A ; :: thesis: verum

end;

hence not for A being LINE of IPP holds a on A by A2, A6; :: thesis: verum

end;

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

end;

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