let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for o, a, b, c, a', b', c', 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,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 FCPS; :: 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 A1: ( 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' ) ; :: thesis: r,q,p is_collinear
then A2: not o,c,a is_collinear by Th1;

A3: 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, Def2;
then p,r,q is_collinear by A1, Lm7;
hence r,q,p is_collinear by Th1; :: thesis: verum

end;

now

assume A4: a,b,c is_collinear ; :: thesis: r,q,p is_collinear
A5: ( a <> b & b <> c & c <> a ) by A1, ANPROJ_2:def 7;
( b,c,a is_collinear & b,c,b is_collinear ) by A4, Th1, ANPROJ_2:def 7;
then A6: a,b,r is_collinear by A1, A5, ANPROJ_2:def 8;
( a,c,a is_collinear & a,c,b is_collinear ) by A4, Th1, ANPROJ_2:def 7;
then a,b,q is_collinear by A1, A5, ANPROJ_2:def 8;
hence r,q,p is_collinear by A1, A5, A6, ANPROJ_2:def 8; :: thesis: verum

end;

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