let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a9, b, b9, c, c9, o, p, q, r being Element of FCPS st not o,a,b are_collinear & not o,b,c are_collinear & not o,a,c are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & a <> a9 & b,c,r are_collinear & b9,c9,r are_collinear & a,c,q are_collinear & b <> b9 & a9,c9,q are_collinear & o <> a9 & o <> b9 & o <> c9 holds
r,q,p are_collinear
let a, a9, b, b9, c, c9, o, p, q, r be Element of FCPS; :: thesis: ( not o,a,b are_collinear & not o,b,c are_collinear & not o,a,c are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & a <> a9 & b,c,r are_collinear & b9,c9,r are_collinear & a,c,q are_collinear & b <> b9 & a9,c9,q are_collinear & o <> a9 & o <> b9 & o <> c9 implies r,q,p are_collinear )
assume that
A1: not o,a,b are_collinear and
A2: not o,b,c are_collinear and
A3: not o,a,c are_collinear and
A4: ( o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear ) and
A5: a,b,p are_collinear and
A6: ( a9,b9,p are_collinear & a <> a9 ) and
A7: b,c,r are_collinear and
A8: b9,c9,r are_collinear and
A9: a,c,q are_collinear and
A10: ( b <> b9 & a9,c9,q are_collinear & o <> a9 & o <> b9 & o <> c9 ) ; :: thesis: r,q,p are_collinear

A11: now :: thesis: ( a,b,c are_collinear implies r,q,p are_collinear )

A12: ( b <> c & b,c,b are_collinear ) by A2, ANPROJ_2:def 7;
assume A13: a,b,c are_collinear ; :: thesis: r,q,p are_collinear
then b,c,a are_collinear by Th1;
then A14: a,b,r are_collinear by A7, A12, ANPROJ_2:def 8;
A15: ( c <> a & a,c,a are_collinear ) by A3, ANPROJ_2:def 7;
a,c,b are_collinear by A13, Th1;
then A16: a,b,q are_collinear by A9, A15, ANPROJ_2:def 8;
a <> b by A1, ANPROJ_2:def 7;
hence r,q,p are_collinear by A5, A14, A16, ANPROJ_2:def 8; :: thesis: verum

end;

A17: not o,c,a are_collinear by A3, Th1;

now :: thesis: ( not a,b,c are_collinear implies r,q,p are_collinear )

assume not a,b,c are_collinear ; :: thesis: r,q,p are_collinear
then o,a,b,c constitute_a_quadrangle by A1, A2, A17;
then p,r,q are_collinear by A4, A5, A6, A7, A8, A9, A10, Lm7;
hence r,q,p are_collinear by Th1; :: thesis: verum

end;

hence r,q,p are_collinear by A11; :: thesis: verum