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