let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a', o, b, c, b', c', p, q, r being Element of FCPS 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 FCPS; :: thesis: ( 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 A1: ( 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 ) ; :: thesis: p,q,r is_collinear
then A2: not a,b,c,a' are_coplanar by Th19;
A3: not a,b,c is_collinear by A1, Th10;
p,a,b is_collinear by A1, Th1;
then A4: a,b,c,p are_coplanar by Th10;
A5: a,b,c,q are_coplanar by A1, Th10;
c,r,a is_collinear by A1, Th1;
then A6: a,b,c,r are_coplanar by Th10;
p,a',b' is_collinear by A1, Th1;
then A7: a',b',c',p are_coplanar by Th10;
A8: a',b',c',q are_coplanar by A1, Th10;
c',r,a' is_collinear by A1, Th1;
then a',b',c',r are_coplanar by Th10;
hence p,q,r is_collinear by A1, A2, A3, A4, A5, A6, A7, A8, Th20; :: thesis: verum