let FCPS be up-3-dimensional CollProjectiveSpace; for a, a', o, b, c, b', c', p, q, r being Element of st a <> a' & o,a,a' is_collinear & not a,b,c,o are_coplanar & not a',b',c' is_collinear & a,b,p is_collinear & a',b',p is_collinear & b,c,q is_collinear & b',c',q is_collinear & a,c,r is_collinear & a',c',r is_collinear holds
p,q,r is_collinear
let a, a', o, b, c, b', c', p, q, r be Element of ; ( a <> a' & o,a,a' is_collinear & not a,b,c,o are_coplanar & not a',b',c' is_collinear & a,b,p is_collinear & a',b',p is_collinear & b,c,q is_collinear & b',c',q is_collinear & a,c,r is_collinear & a',c',r is_collinear implies p,q,r is_collinear )
assume that
A1:
( a <> a' & o,a,a' is_collinear & not a,b,c,o are_coplanar )
and
A2:
not a',b',c' is_collinear
and
A3:
a,b,p is_collinear
and
A4:
a',b',p is_collinear
and
A5:
( b,c,q is_collinear & b',c',q is_collinear )
and
A6:
a,c,r is_collinear
and
A7:
a',c',r is_collinear
; p,q,r is_collinear
A8:
( a,b,c,q are_coplanar & a',b',c',q are_coplanar )
by A5, Th10;
c',r,a' is_collinear
by A7, Th1;
then A9:
a',b',c',r are_coplanar
by Th10;
p,a',b' is_collinear
by A4, Th1;
then A10:
a',b',c',p are_coplanar
by Th10;
c,r,a is_collinear
by A6, Th1;
then A11:
a,b,c,r are_coplanar
by Th10;
p,a,b is_collinear
by A3, Th1;
then A12:
a,b,c,p are_coplanar
by Th10;
( not a,b,c,a' are_coplanar & not a,b,c is_collinear )
by A1, Th10, Th19;
hence
p,q,r is_collinear
by A2, A12, A11, A10, A8, A9, Th20; verum