let CPS be CollProjectiveSpace; :: thesis:
assume A1: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of 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 ; :: thesis:
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of ; :: thesis:
assume that
A2: {o,b1,a1} on C1 and
A3: {o,a2,b2} on C2 and
A4: {o,a3,b3} on C3 and
A5: {a3,a2,t} on A1 and
A6: {a3,r,a1} on A2 and
A7: {a2,s,a1} on A3 and
A8: {t,b2,b3} on B1 and
A9: {b1,r,b3} on B2 and
A10: {b1,s,b2} on B3 and
A11: C1,C2,C3 are_mutually_different and
A12: ( o <> a1 & o <> a2 & o <> a3 ) and
A13: o <> b1 and
A14: o <> b2 and
A15: o <> b3 and
A16: ( 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 ;
A17: ( o on C2 & b2 on C2 ) by A3, INCSP_1:12;
A18: s on B3 by A10, INCSP_1:12;
( b2 on B3 & b1 on B3 ) by A10, INCSP_1:12;
then A19: b1',b2',s' is_collinear by A18, Th14;
A20: r on B2 by A9, INCSP_1:12;
( b3 on B2 & b1 on B2 ) by A9, INCSP_1:12;
then A21: b1',b3',r' is_collinear by A20, Th14;
A22: t on B1 by A8, INCSP_1:12;
( b3 on B1 & b2 on B1 ) by A8, INCSP_1:12;
then A23: b2',b3',t' is_collinear by A22, Th14;
A24: s on A3 by A7, INCSP_1:12;
( a2 on A3 & a1 on A3 ) by A7, INCSP_1:12;
then A25: a1',a2',s' is_collinear by A24, Th14;
A26: ( o on C3 & b3 on C3 ) by A4, INCSP_1:12;
a3 on C3 by A4, INCSP_1:12;
then A27: o',b3',a3' is_collinear by A26, Th14;
a2 on C2 by A3, INCSP_1:12;
then A28: o',b2',a2' is_collinear by A17, Th14;
A29: r on A2 by A6, INCSP_1:12;
( a3 on A2 & a1 on A2 ) by A6, INCSP_1:12;
then A30: a1',a3',r' is_collinear by A29, Th14;
A31: t on A1 by A5, INCSP_1:12;
( a3 on A1 & a2 on A1 ) by A5, INCSP_1:12;
then A32: a2',a3',t' is_collinear by A31, Th14;
A33: ( o on C1 & b1 on C1 ) by A2, INCSP_1:12;
A34: ( not o',b1',b2' is_collinear & not o',b1',b3' is_collinear & not o',b2',b3' is_collinear )

proof

A35: now

assume o',b1',b3' is_collinear ; :: thesis:
then consider K being LINE of such that
A36: ( o on K & b1 on K & b3 on K ) by Th14;
( K = C1 & K = C3 ) by A13, A15, A33, A26, A36, Th12;
hence contradiction by A11, ZFMISC_1:def 5; :: thesis:

end;

A37: now

assume o',b1',b2' is_collinear ; :: thesis:
then consider K being LINE of such that
A38: ( o on K & b1 on K & b2 on K ) by Th14;
( K = C1 & K = C2 ) by A13, A14, A33, A17, A38, Th12;
hence contradiction by A11, ZFMISC_1:def 5; :: thesis:

end;

A39: now

assume o',b2',b3' is_collinear ; :: thesis:
then consider K being LINE of such that
A40: ( o on K & b2 on K & b3 on K ) by Th14;
( K = C2 & K = C3 ) by A14, A15, A17, A26, A40, Th12;
hence contradiction by A11, ZFMISC_1:def 5; :: thesis:

end;

assume ( o',b1',b2' is_collinear or o',b1',b3' is_collinear or o',b2',b3' is_collinear ) ; :: thesis:
hence contradiction by A37, A35, A39; :: thesis:

end;

a1 on C1 by A2, INCSP_1:12;
then o',b1',a1' is_collinear by A33, Th14;
then t',r',s' is_collinear by A1, A12, A16, A19, A25, A21, A30, A23, A32, A28, A27, A34;
then consider O being LINE of such that
A41: ( t on O & r on O & s on O ) by Th14;
{r,s,t} on O by A41, INCSP_1:12;
hence ex O being LINE of st {r,s,t} on O ; :: thesis: