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

A11: now

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

end;

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

now

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

end;

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