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