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 6;
now :: thesis: ( A <> L implies ex a being POINT of IPP st not a on A )
assume A2: A <> L ; :: thesis: not for a being POINT of IPP holds a on A
now :: thesis: not for a being POINT of IPP holds a on A
consider q, r, s being POINT of IPP such that
A3: q <> r and
r <> s and
s <> q and
A4: ( q on L & r on L ) and
s on L by INCPROJ:def 7;
( not q on A or not r on A ) by A2, A3, A4, INCPROJ:def 4;
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