let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, o, d, d', a', b', c', 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 & not b,c,d,o are_coplanar & not a,c,d,o are_coplanar & o,d,d' is_collinear & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,d,s is_collinear & a',d',s is_collinear & b,d,t is_collinear & b',d',t is_collinear & c,d,u is_collinear & o <> a' & o <> d' & d <> d' & o <> b' holds
not s,t,u is_collinear
let a, b, c, o, d, d', a', b', c', 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 & not b,c,d,o are_coplanar & not a,c,d,o are_coplanar & o,d,d' is_collinear & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,d,s is_collinear & a',d',s is_collinear & b,d,t is_collinear & b',d',t is_collinear & c,d,u is_collinear & o <> a' & o <> d' & d <> d' & o <> b' implies not s,t,u is_collinear )
assume A1: ( a,b,c,o are_coplanar & not a,b,c,d are_coplanar & not a,b,d,o are_coplanar & not b,c,d,o are_coplanar & not a,c,d,o are_coplanar & o,d,d' is_collinear & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & a,d,s is_collinear & a',d',s is_collinear & b,d,t is_collinear & b',d',t is_collinear & c,d,u is_collinear & o <> a' & o <> d' & d <> d' & o <> b' ) ; :: thesis: not s,t,u is_collinear
then not d,o,a is_collinear by Th10;
then not o,a,d is_collinear by Th1;
then A2: s <> d by A1, Th8;
A3: not d,b,c,a are_coplanar by A1, Th11;
then A4: not d,b,c,s are_coplanar by A1, A2, Th19;
A5: ( d,b,c,b are_coplanar & d,b,c,d are_coplanar & d,b,c,c are_coplanar ) by Th18;
b <> d by A1, Th18;
then A6: d,b,c,t are_coplanar by A1, A5, Th14;
A7: d,b,c,u are_coplanar by A1, A5, Th14;
A8: not d,b,c is_collinear by A3, Th10;
not b,d,o is_collinear by A1, Th10;
then not o,b,d is_collinear by Th1;
then A9: t <> d by A1, Th8;
A10: d,b,t is_collinear by A1, Th1;
d,c,u is_collinear by A1, Th1;
then t <> u by A8, A9, A10, Lm1;
then not t,u,s is_collinear by A4, A6, A7, Th14;
hence not s,t,u is_collinear by Th1; :: thesis: verum