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 P9 = P as LINE of CPS by Th1;
consider a99, b99 being Point of CPS such that
A1: a99 <> b99 and
A2: P9 = Line (a99,b99) by COLLSP:def 7;
consider c9 being Point of CPS such that
A3: ( a99 <> c9 & b99 <> c9 ) and
A4: a99,b99,c9 are_collinear by ANPROJ_2:def 10;
reconsider a = a99, b = b99, c = c9 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, A3; :: thesis: ( a on P & b on P & c on P )
a99 in P9 by A2, COLLSP:10;
then A5: a on P by Th5;
b99 in P9 by A2, COLLSP:10;
then A6: b on P by Th5;
ex Q being LINE of (IncProjSp_of CPS) st
( a on Q & b on Q & c on Q ) by A4, Th10;
hence ( a on P & b on P & c on P ) by A1, A5, A6, Th8; :: thesis: verum