let CPS be proper CollSp; :: thesis:
let p, q be POINT of (IncProjSp_of CPS); :: thesis:
reconsider p9 = p, q9 = q as Point of CPS ;

consider r9 being Point of CPS such that
A2: p9 <> r9 by Th7;
consider P9 being LINE of CPS such that
A3: p9 in P9 and
r9 in P9 by A2, COLLSP:15;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
assume A4: p9 = q9 ; :: thesis:
p on P by A3, Th5;
hence ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) by A4; :: thesis:

end;

assume p9 <> q9 ; :: thesis:
then consider P9 being LINE of CPS such that
A5: ( p9 in P9 & q9 in P9 ) by COLLSP:15;
reconsider P = P9 as LINE of (IncProjSp_of CPS) by Th1;
( p on P & q on P ) by A5, Th5;
hence ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) ; :: thesis:

end;