let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a9, b, b9, c, d, d9, o, s, t, u being Element of FCPS st a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & a,d,s are_collinear & a9,d9,s are_collinear & b,d,t are_collinear & b9,d9,t are_collinear & c,d,u are_collinear & o <> a9 & d <> d9 & o <> b9 holds
not s,t,u are_collinear

let a, a9, b, b9, c, d, d9, o, s, t, u be Element of FCPS; :: thesis: ( a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & o,d,d9 are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & a,d,s are_collinear & a9,d9,s are_collinear & b,d,t are_collinear & b9,d9,t are_collinear & c,d,u are_collinear & o <> a9 & d <> d9 & o <> b9 implies not s,t,u are_collinear )
assume that
A1: a,b,c,o are_coplanar and
A2: not a,b,c,d are_coplanar and
A3: not a,b,d,o are_coplanar and
A4: o,d,d9 are_collinear and
A5: o,a,a9 are_collinear and
A6: o,b,b9 are_collinear and
A7: a,d,s are_collinear and
A8: a9,d9,s are_collinear and
A9: b,d,t are_collinear and
A10: b9,d9,t are_collinear and
A11: c,d,u are_collinear and
A12: o <> a9 and
A13: d <> d9 and
A14: o <> b9 ; :: thesis: not s,t,u are_collinear
A15: d,b,c,b are_coplanar by Th14;
A16: not d,b,c,a are_coplanar by ;
then A17: not d,b,c are_collinear by Th6;
not b,d,o are_collinear by ;
then not o,b,d are_collinear by Th1;
then A18: t <> d by A4, A6, A10, A13, A14, Th5;
( d,b,t are_collinear & d,c,u are_collinear ) by A9, A11, Th1;
then A19: t <> u by ;
A20: d,b,c,d are_coplanar by Th14;
not d,o,a are_collinear by ;
then not o,a,d are_collinear by Th1;
then s <> d by A4, A5, A8, A12, A13, Th5;
then A21: not d,b,c,s are_coplanar by ;
b <> d by ;
then A22: d,b,c,t are_coplanar by A9, A15, A20, Th10;
d,b,c,c are_coplanar by Th14;
then d,b,c,u are_coplanar by A1, A3, A11, A20, Th10;
then not t,u,s are_collinear by ;
hence not s,t,u are_collinear by Th1; :: thesis: verum