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 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds
r1,r2,r3 are_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 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_distinct 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 o9 = o, b19 = b1, a19 = a1, b29 = b2, a29 = a2, b39 = b3, a39 = a3, r9 = r, s9 = s, t9 = t as Element of CPS ;
A17: ( o on C2 & b2 on C2 ) by A3, INCSP_1:2;
A18: s on B3 by A10, INCSP_1:2;
( b2 on B3 & b1 on B3 ) by A10, INCSP_1:2;
then A19: b19,b29,s9 are_collinear by A18, Th10;
A20: r on B2 by A9, INCSP_1:2;
( b3 on B2 & b1 on B2 ) by A9, INCSP_1:2;
then A21: b19,b39,r9 are_collinear by A20, Th10;
A22: t on B1 by A8, INCSP_1:2;
( b3 on B1 & b2 on B1 ) by A8, INCSP_1:2;
then A23: b29,b39,t9 are_collinear by A22, Th10;
A24: s on A3 by A7, INCSP_1:2;
( a2 on A3 & a1 on A3 ) by A7, INCSP_1:2;
then A25: a19,a29,s9 are_collinear by A24, Th10;
A26: ( o on C3 & b3 on C3 ) by A4, INCSP_1:2;
a3 on C3 by A4, INCSP_1:2;
then A27: o9,b39,a39 are_collinear by A26, Th10;
a2 on C2 by A3, INCSP_1:2;
then A28: o9,b29,a29 are_collinear by A17, Th10;
A29: r on A2 by A6, INCSP_1:2;
( a3 on A2 & a1 on A2 ) by A6, INCSP_1:2;
then A30: a19,a39,r9 are_collinear by A29, Th10;
A31: t on A1 by A5, INCSP_1:2;
( a3 on A1 & a2 on A1 ) by A5, INCSP_1:2;
then A32: a29,a39,t9 are_collinear by A31, Th10;
A33: ( o on C1 & b1 on C1 ) by A2, INCSP_1:2;
A34: ( not o9,b19,b29 are_collinear & not o9,b19,b39 are_collinear & not o9,b29,b39 are_collinear )

proof

A35: now :: thesis:

assume o9,b19,b39 are_collinear ; :: thesis:
then consider K being LINE of (IncProjSp_of CPS) such that
A36: ( o on K & b1 on K & b3 on K ) by Th10;
( K = C1 & K = C3 ) by A13, A15, A33, A26, A36, Th8;
hence contradiction by A11, ZFMISC_1:def 5; :: thesis:

end;

A37: now :: thesis:

assume o9,b19,b29 are_collinear ; :: thesis:
then consider K being LINE of (IncProjSp_of CPS) such that
A38: ( o on K & b1 on K & b2 on K ) by Th10;
( K = C1 & K = C2 ) by A13, A14, A33, A17, A38, Th8;
hence contradiction by A11, ZFMISC_1:def 5; :: thesis:

end;

A39: now :: thesis:

assume o9,b29,b39 are_collinear ; :: thesis:
then consider K being LINE of (IncProjSp_of CPS) such that
A40: ( o on K & b2 on K & b3 on K ) by Th10;
( K = C2 & K = C3 ) by A14, A15, A17, A26, A40, Th8;
hence contradiction by A11, ZFMISC_1:def 5; :: thesis:

end;

assume ( o9,b19,b29 are_collinear or o9,b19,b39 are_collinear or o9,b29,b39 are_collinear ) ; :: thesis:
hence contradiction by A37, A35, A39; :: thesis:

end;

a1 on C1 by A2, INCSP_1:2;
then o9,b19,a19 are_collinear by A33, Th10;
then t9,r9,s9 are_collinear by A1, A12, A16, A19, A25, A21, A30, A23, A32, A28, A27, A34;
then consider O being LINE of (IncProjSp_of CPS) such that
A41: ( t on O & r on O & s on O ) by Th10;
{r,s,t} on O by A41, INCSP_1:2;
hence ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O ; :: thesis: