let CPS be CollProjectiveSpace; :: thesis: ( ex p, p1, r, r1 being Point of CPS st
for s being Point of CPS holds
( not p,p1,s are_collinear or not r,r1,s are_collinear ) implies ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N ) )
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: ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
set M99 = Line (p,p1);
set N99 = Line (r,r1);
( p <> p1 & r <> r1 )

proof

A2: now :: thesis: not p = p1

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

end;

A4: now :: thesis: not r = r1

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

end;

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

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: ex N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
take N ; :: thesis: for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
thus for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N ) :: thesis: verum

proof

assume ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N ) ; :: thesis: contradiction
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: verum

end;