let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, a', b', c', p, q, r being Element of FCPS 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 FCPS; :: 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 A1: ( 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 ) ; :: thesis: p,q,r is_collinear
assume A2: not p,q,r is_collinear ; :: thesis: contradiction
( a,b,c,a are_coplanar & a,b,c,b are_coplanar & a,b,c,c are_coplanar ) by Th18;
then A3: ( p,q,r,a are_coplanar & p,q,r,b are_coplanar & p,q,r,c are_coplanar ) by A1, Th12;
a',b',c',a' are_coplanar by Th18;
then p,q,r,a' are_coplanar by A1, Th12;
hence contradiction by A1, A2, A3, Th12; :: thesis: verum