let CPS be CollProjectiveSpace; :: thesis:
assume A1: for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Point of st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear ; :: thesis:
let o, a1, a2, a3, b1, b2, b3, c1, c2, c3 be POINT of ; :: thesis:
let A1, A2, A3, B1, B2, B3, C1, C2, C3 be LINE of ; :: thesis:
assume that
A2: o,a1,a2,a3 are_mutually_different and
A3: o,b1,b2,b3 are_mutually_different and
A4: A3 <> B3 and
A5: o on A3 and
A6: o on B3 and
A7: {a2,b3,c1} on A1 and
A8: {a3,b1,c2} on B1 and
A9: {a1,b2,c3} on C1 and
A10: {a1,b3,c2} on A2 and
A11: {a3,b2,c1} on B2 and
A12: {a2,b1,c3} on C2 and
A13: {b1,b2,b3} on A3 and
A14: {a1,a2,a3} on B3 and
A15: {c1,c2} on C3 ; :: thesis:
reconsider o' = o, a1' = a1, a2' = a2, a3' = a3, b1' = b1, b2' = b2, b3' = b3, c1' = c1, c2' = c2, c3' = c3 as Point of ;
A16: b1 on A3 by A13, INCSP_1:12;
A17: c3 on C1 by A9, INCSP_1:12;
( a1 on C1 & b2 on C1 ) by A9, INCSP_1:12;
then A18: a1',b2',c3' is_collinear by A17, Th14;
A19: c1 on A1 by A7, INCSP_1:12;
A20: ( o' <> b3' & b2' <> b3' ) by A3, ZFMISC_1:def 6;
A21: ( a2' <> a3' & a1' <> a2' ) by A2, ZFMISC_1:def 6;
A22: ( b3 on A2 & c2 on A2 ) by A10, INCSP_1:12;
A23: a1 on A2 by A10, INCSP_1:12;
then A24: a1',b3',c2' is_collinear by A22, Th14;
A25: ( b1' <> b2' & b1' <> b3' ) by A3, ZFMISC_1:def 6;
A26: b3 on A1 by A7, INCSP_1:12;
A27: a1 on B3 by A14, INCSP_1:12;
A28: not o',a1',b1' is_collinear

proof

A29: o <> a1 by A2, ZFMISC_1:def 6;
assume o',a1',b1' is_collinear ; :: thesis:
then consider K being LINE of such that
A30: o on K and
A31: a1 on K and
A32: b1 on K by Th14;
o <> b1 by A3, ZFMISC_1:def 6;
then K = A3 by A5, A16, A30, A32, Th12;
hence contradiction by A4, A6, A27, A30, A31, A29, Th12; :: thesis:

end;

A33: c3 on C2 by A12, INCSP_1:12;
( a2 on C2 & b1 on C2 ) by A12, INCSP_1:12;
then A34: b1',a2',c3' is_collinear by A33, Th14;
A35: a3 on B1 by A8, INCSP_1:12;
A36: b2 on A3 by A13, INCSP_1:12;
then A37: o',b1',b2' is_collinear by A5, A16, Th14;
A38: ( a3 on B2 & c1 on B2 ) by A11, INCSP_1:12;
A39: b2 on B2 by A11, INCSP_1:12;
then A40: a3',b2',c1' is_collinear by A38, Th14;
A41: b3 on A3 by A13, INCSP_1:12;
then A42: o',b1',b3' is_collinear by A5, A16, Th14;
A43: ( a1' <> a3' & o' <> b2' ) by A2, A3, ZFMISC_1:def 6;
A44: ( o' <> a2' & o' <> a3' ) by A2, ZFMISC_1:def 6;
A45: c2 on B1 by A8, INCSP_1:12;
A46: a2 on A1 by A7, INCSP_1:12;
then A47: a2',b3',c1' is_collinear by A26, A19, Th14;
A48: b1 <> b2 by A3, ZFMISC_1:def 6;
A49: a1 <> a2 by A2, ZFMISC_1:def 6;
A50: o <> b3 by A3, ZFMISC_1:def 6;
A51: b1 on B1 by A8, INCSP_1:12;
then A52: a3',b1',c2' is_collinear by A35, A45, Th14;
A53: a3 on B3 by A14, INCSP_1:12;
then A54: o',a1',a3' is_collinear by A6, A27, Th14;
A55: a2 on B3 by A14, INCSP_1:12;
then o',a1',a2' is_collinear by A6, A27, Th14;
then c1',c2',c3' is_collinear by A1, A44, A21, A43, A20, A25, A28, A54, A37, A42, A18, A34, A24, A52, A47, A40;
then A56: ex K being LINE of st
( c1 on K & c2 on K & c3 on K ) by Th14;
A57: o <> a3 by A2, ZFMISC_1:def 6;
A58: c1 <> c2

proof

assume A59: not c1 <> c2 ; :: thesis:
not a3 on A3 by A4, A5, A6, A57, A53, Th12;
then B1 <> B2 by A48, A35, A51, A39, A16, A36, Th12;
then A60: c1 = a3 by A35, A45, A38, A59, Th12;
not b3 on B3 by A4, A5, A6, A50, A41, Th12;
then A1 <> A2 by A49, A46, A26, A23, A27, A55, Th12;
then c1 = b3 by A26, A19, A22, A59, Th12;
hence contradiction by A4, A5, A6, A50, A41, A53, A60, Th12; :: thesis:

end;

( c1 on C3 & c2 on C3 ) by A15, INCSP_1:11;
hence c3 on C3 by A58, A56, Th12; :: thesis: