let CPS be CollProjectiveSpace; :: thesis: for P being LINE of ex a, b, c being POINT of st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
let P be LINE of ; :: thesis: ex a, b, c being POINT of st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
reconsider P' = P as LINE of CPS by Th2;
consider a'', b'' being Point of such that
A1: a'' <> b'' and
A2: P' = Line a'',b'' by COLLSP:def 7;
consider c' being Point of such that
A3: ( a'' <> c' & b'' <> c' ) and
A4: a'',b'',c' is_collinear by ANPROJ_2:def 10;
reconsider a = a'', b = b'', c = c' as POINT of ;
take a ; :: thesis: ex b, c being POINT of st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
take b ; :: thesis: ex c being POINT of st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
take c ; :: thesis: ( a <> b & b <> c & c <> a & a on P & b on P & c on P )
thus ( a <> b & b <> c & c <> a ) by A1, A3; :: thesis: ( a on P & b on P & c on P )
a'' in P' by A2, COLLSP:16;
then A5: a on P by Th9;
b'' in P' by A2, COLLSP:16;
then A6: b on P by Th9;
ex Q being LINE of st
( a on Q & b on Q & c on Q ) by A4, Th14;
hence ( a on P & b on P & c on P ) by A1, A5, A6, Th12; :: thesis: verum