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