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