let CPS be CollProjectiveSpace; :: thesis:
assume A1: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of CPS st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear ; :: thesis:
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of (IncProjSp_of CPS); :: thesis:
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (IncProjSp_of CPS); :: thesis:
assume that
A2: ( {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 ) and
A3: C1,C2,C3 are_mutually_different and
A4: ( o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 ) ; :: thesis:
reconsider o' = o, b1' = b1, a1' = a1, b2' = b2, a2' = a2, b3' = b3, a3' = a3, r' = r, s' = s, t' = t as Element of CPS ;
A5: ( o on C1 & b1 on C1 & a1 on C1 & o on C2 & b2 on C2 & a2 on C2 & o on C3 & b3 on C3 & a3 on C3 & a3 on A1 & a2 on A1 & t on A1 & a3 on A2 & a1 on A2 & r on A2 & a2 on A3 & a1 on A3 & s on A3 & b3 on B1 & b2 on B1 & t on B1 & b3 on B2 & b1 on B2 & r on B2 & b2 on B3 & b1 on B3 & s on B3 ) by A2, INCSP_1:12;
then A6: ( b1',b2',s' is_collinear & a1',a2',s' is_collinear & b1',b3',r' is_collinear & a1',a3',r' is_collinear & b2',b3',t' is_collinear & a2',a3',t' is_collinear ) by Th14;
A7: ( o',b1',a1' is_collinear & o',b2',a2' is_collinear & o',b3',a3' is_collinear ) by A5, Th14;
( not o',b1',b2' is_collinear & not o',b1',b3' is_collinear & not o',b2',b3' is_collinear )

proof

assume A8: ( o',b1',b2' is_collinear or o',b1',b3' is_collinear or o',b2',b3' is_collinear ) ; :: thesis:

A9: now

assume o',b1',b2' is_collinear ; :: thesis:
then consider K being LINE of (IncProjSp_of CPS) such that
A10: ( o on K & b1 on K & b2 on K ) by Th14;
( K = C1 & K = C2 ) by A4, A5, A10, Th12;
hence contradiction by A3, ZFMISC_1:def 5; :: thesis:

end;

A11: now

assume o',b1',b3' is_collinear ; :: thesis:
then consider K being LINE of (IncProjSp_of CPS) such that
A12: ( o on K & b1 on K & b3 on K ) by Th14;
( K = C1 & K = C3 ) by A4, A5, A12, Th12;
hence contradiction by A3, ZFMISC_1:def 5; :: thesis:

end;

now

assume o',b2',b3' is_collinear ; :: thesis:
then consider K being LINE of (IncProjSp_of CPS) such that
A13: ( o on K & b2 on K & b3 on K ) by Th14;
( K = C2 & K = C3 ) by A4, A5, A13, Th12;
hence contradiction by A3, ZFMISC_1:def 5; :: thesis:

end;

hence contradiction by A8, A9, A11; :: thesis:

end;

then t',r',s' is_collinear by A1, A4, A6, A7;
then consider O being LINE of (IncProjSp_of CPS) such that
A14: ( t on O & r on O & s on O ) by Th14;
{r,s,t} on O by A14, INCSP_1:12;
hence ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O ; :: thesis: