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 p' = p, q' = q as Point of CPS ;

A1: now

assume p' <> q' ; :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
then consider P' being LINE of CPS such that
A2: ( p' in P' & q' in P' ) by COLLSP:24;
reconsider P = P' as LINE of (IncProjSp_of CPS) by Th2;
( p on P & q on P ) by A2, Th9;
hence ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) ; :: thesis: verum

end;

now

assume A3: p' = q' ; :: thesis: ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
consider r' being Point of CPS such that
A4: p' <> r' by Th11;
consider P' being LINE of CPS such that
A5: ( p' in P' & r' in P' ) by A4, COLLSP:24;
reconsider P = P' as LINE of (IncProjSp_of CPS) by Th2;
( p on P & q on P ) by A3, A5, Th9;
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