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