let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a9, b, b9, c, c9, p, q, r being Element of FCPS st not a,b,c are_collinear & not a9,b9,c9 are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9 are_coplanar holds
p,q,r are_collinear
let a, a9, b, b9, c, c9, p, q, r be Element of FCPS; :: thesis: ( not a,b,c are_collinear & not a9,b9,c9 are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar & not a,b,c,a9 are_coplanar implies p,q,r are_collinear )
assume that
A1: not a,b,c are_collinear and
A2: not a9,b9,c9 are_collinear and
A3: ( a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar ) and
A4: ( a9,b9,c9,p are_coplanar & a9,b9,c9,q are_coplanar & a9,b9,c9,r are_coplanar ) and
A5: not a,b,c,a9 are_coplanar ; :: thesis: p,q,r are_collinear
a,b,c,a are_coplanar by Th14;
then A6: p,q,r,a are_coplanar by A1, A3, Th8;
a9,b9,c9,a9 are_coplanar by Th14;
then A7: p,q,r,a9 are_coplanar by A2, A4, Th8;
a,b,c,c are_coplanar by Th14;
then A8: p,q,r,c are_coplanar by A1, A3, Th8;
a,b,c,b are_coplanar by Th14;
then A9: p,q,r,b are_coplanar by A1, A3, Th8;
assume not p,q,r are_collinear ; :: thesis: contradiction
hence contradiction by A5, A6, A9, A8, A7, Th8; :: thesis: verum