let CPS be CollProjectiveSpace; :: thesis:
given p, p1, r, r1 being Point of CPS such that A1: for s being Point of CPS holds
( not p,p1,s are_collinear or not r,r1,s are_collinear ) ; :: thesis:
set M99 = Line (p,p1);
set N99 = Line (r,r1);
( p <> p1 & r <> r1 )

proof

A2: now :: thesis:

assume p = p1 ; :: thesis:
then A3: p,p1,r1 are_collinear by COLLSP:2;
r,r1,r1 are_collinear by COLLSP:2;
hence contradiction by A1, A3; :: thesis:

end;

A4: now :: thesis:

assume r = r1 ; :: thesis:
then ( p,p1,p1 are_collinear & r,r1,p1 are_collinear ) by COLLSP:2;
hence contradiction by A1; :: thesis:

end;

assume ( not p <> p1 or not r <> r1 ) ; :: thesis:
hence contradiction by A2, A4; :: thesis:

end;

then reconsider M9 = Line (p,p1), N9 = Line (r,r1) as LINE of CPS by COLLSP:def 7;
reconsider M = M9, N = N9 as LINE of (IncProjSp_of CPS) by Th1;
take M ; :: thesis:
take N ; :: thesis:
thus for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N ) :: thesis:

proof

assume ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) ; :: thesis:
then consider q being POINT of (IncProjSp_of CPS) such that
A5: q on M and
A6: q on N ;
reconsider q9 = q as Point of CPS ;
q9 in Line (r,r1) by A6, Th5;
then A7: r,r1,q9 are_collinear by COLLSP:11;
q9 in Line (p,p1) by A5, Th5;
then p,p1,q9 are_collinear by COLLSP:11;
hence contradiction by A1, A7; :: thesis:

end;