let CPS be proper CollSp; :: thesis: for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
let p, q be POINT of (IncProjSp_of CPS); :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
reconsider p9 = p, q9 = q as Point of CPS ;

A1: now :: thesis: ( p9 = q9 implies ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) )

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: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
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: verum

end;

now :: thesis: ( p9 <> q9 implies ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) )

assume p9 <> q9 ; :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
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: verum

end;

hence ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) by A1; :: thesis: verum