let CPS be CollProjectiveSpace; ( ( for p, p1, q, q1, r2 being Point of ex r, r1 being Point of st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) ) implies for a being POINT of
for M, N being LINE of ex b, c being POINT of ex S being LINE of st
( a on S & b on S & c on S & b on M & c on N ) )
assume A1:
for p, p1, q, q1, r2 being Point of ex r, r1 being Point of st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear )
; for a being POINT of
for M, N being LINE of ex b, c being POINT of ex S being LINE of st
( a on S & b on S & c on S & b on M & c on N )
let a be POINT of ; for M, N being LINE of ex b, c being POINT of ex S being LINE of st
( a on S & b on S & c on S & b on M & c on N )
let M, N be LINE of ; ex b, c being POINT of ex S being LINE of st
( a on S & b on S & c on S & b on M & c on N )
reconsider M' = M, N' = N as LINE of CPS by Th2;
reconsider a' = a as Point of ;
consider p, q being Point of such that
p <> q
and
A2:
M' = Line p,q
by COLLSP:def 7;
consider p1, q1 being Point of such that
p1 <> q1
and
A3:
N' = Line p1,q1
by COLLSP:def 7;
consider b', c' being Point of such that
A4:
p,q,b' is_collinear
and
A5:
p1,q1,c' is_collinear
and
A6:
a',b',c' is_collinear
by A1;
reconsider b = b', c = c' as POINT of ;
b' in M'
by A2, A4, COLLSP:17;
then A7:
b on M
by Th9;
c' in N'
by A3, A5, COLLSP:17;
then A8:
c on N
by Th9;
ex S being LINE of st
( a on S & b on S & c on S )
by A6, Th14;
hence
ex b, c being POINT of ex S being LINE of st
( a on S & b on S & c on S & b on M & c on N )
by A7, A8; verum