let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, a', b', c', p, q, r being Element of st not a,b,c is_collinear & not a',b',c' is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a',b',c',p are_coplanar & a',b',c',q are_coplanar & a',b',c',r are_coplanar & not a,b,c,a' are_coplanar holds
p,q,r is_collinear
let a, b, c, a', b', c', p, q, r be Element of ; :: thesis: ( not a,b,c is_collinear & not a',b',c' is_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a',b',c',p are_coplanar & a',b',c',q are_coplanar & a',b',c',r are_coplanar & not a,b,c,a' are_coplanar implies p,q,r is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: not a',b',c' is_collinear and
A3: ( a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar ) and
A4: ( a',b',c',p are_coplanar & a',b',c',q are_coplanar & a',b',c',r are_coplanar ) and
A5: not a,b,c,a' 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;
a',b',c',a' are_coplanar by Th18;
then A7: p,q,r,a' 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