let CPS be proper CollSp; :: thesis: not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P
consider p9, q9, r9 being Point of CPS such that
A1: not p9,q9,r9 are_collinear by COLLSP:def 6;
set X = Line (p9,q9);
p9 <> q9 by A1, COLLSP:2;
then reconsider P9 = Line (p9,q9) as LINE of CPS by COLLSP:def 7;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
reconsider r = r9 as POINT of (IncProjSp_of CPS) ;
not r on P

proof

assume r on P ; :: thesis: contradiction
then r9 in Line (p9,q9) by Th5;
hence contradiction by A1, COLLSP:11; :: thesis: verum

end;

hence not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P ; :: thesis: verum