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 p', q', r' being Point of CPS such that
A1: not p',q',r' is_collinear by COLLSP:def 6;
set X = Line p',q';
p' <> q' by A1, COLLSP:7;
then reconsider P' = Line p',q' as LINE of CPS by COLLSP:def 7;
reconsider P = P' as LINE of (IncProjSp_of CPS) by Th2;
reconsider r = r' as POINT of (IncProjSp_of CPS) ;
not r on P

proof

assume r on P ; :: thesis: contradiction
then r' in Line p',q' by Th9;
hence contradiction by A1, COLLSP:17; :: 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