let CPS be CollProjectiveSpace; :: thesis: ( ex p, p1, r, r1 being Point of st
for s being Point of holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) implies ex M, N being LINE of st
for q being POINT of holds
( not q on M or not q on N ) )
given p, p1, r, r1 being Point of such that A1: for s being Point of holds
( not p,p1,s is_collinear or not r,r1,s is_collinear ) ; :: thesis: ex M, N being LINE of st
for q being POINT of 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

A2: now

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

end;

A4: 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;

assume ( not p <> p1 or not r <> r1 ) ; :: thesis: contradiction
hence contradiction by A2, A4; :: 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 by Th2;
take M ; :: thesis: ex N being LINE of st
for q being POINT of holds
( not q on M or not q on N )
take N ; :: thesis: for q being POINT of holds
( not q on M or not q on N )
thus for q being POINT of holds
( not q on M or not q on N ) :: thesis: verum

proof

assume ex q being POINT of st
( q on M & q on N ) ; :: thesis: contradiction
then consider q being POINT of such that
A5: q on M and
A6: q on N ;
reconsider q' = q as Point of ;
q' in Line r,r1 by A6, Th9;
then A7: r,r1,q' is_collinear by COLLSP:17;
q' in Line p,p1 by A5, Th9;
then p,p1,q' is_collinear by COLLSP:17;
hence contradiction by A1, A7; :: thesis: verum

end;