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 is_collinear or not r,r1,s is_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 is_collinear or not r,r1,s is_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 M'' = Line p,p1;
set N'' = Line r,r1;
( p <> p1 & r <> r1 )

proof

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

A3: now

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

end;

now

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

end;

hence contradiction by A2, A3; :: thesis: verum

end;

then reconsider M' = Line p,p1, N' = Line r,r1 as LINE of CPS by COLLSP:def 7;
reconsider M = M', N = N' as LINE of (IncProjSp_of CPS) by Th2;
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
A4: ( q on M & q on N ) ;
reconsider q' = q as Point of CPS ;
( q' in Line p,p1 & q' in Line r,r1 ) by A4, Th9;
then ( p,p1,q' is_collinear & r,r1,q' is_collinear ) by COLLSP:17;
hence contradiction by A1; :: thesis: verum

end;