let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for o, a, b, c, a', b', c', p, r, q being Element of st not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,b,p is_collinear & a',b',p is_collinear & a <> a' & b,c,r is_collinear & b',c',r is_collinear & a,c,q is_collinear & b <> b' & a',c',q is_collinear & o <> a' & o <> b' & o <> c' holds
r,q,p is_collinear
let o, a, b, c, a', b', c', p, r, q be Element of ; :: thesis: ( not o,a,b is_collinear & not o,b,c is_collinear & not o,a,c is_collinear & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,b,p is_collinear & a',b',p is_collinear & a <> a' & b,c,r is_collinear & b',c',r is_collinear & a,c,q is_collinear & b <> b' & a',c',q is_collinear & o <> a' & o <> b' & o <> c' 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,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear ) and
A5: a,b,p is_collinear and
A6: ( a',b',p is_collinear & a <> a' ) and
A7: b,c,r is_collinear and
A8: b',c',r is_collinear and
A9: a,c,q is_collinear and
A10: ( b <> b' & a',c',q is_collinear & o <> a' & o <> b' & o <> c' ) ; :: 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