let FCPS be up-3-dimensional CollProjectiveSpace; 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; ( 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
; not s,t,u are_collinear
A15:
d,b,c,b are_coplanar
by Th14;
A16:
not d,b,c,a are_coplanar
by A2, Th7;
then A17:
not d,b,c are_collinear
by Th6;
not b,d,o are_collinear
by A3, Th6;
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 A17, A18, Lm1;
A20:
d,b,c,d are_coplanar
by Th14;
not d,o,a are_collinear
by A3, Th6;
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 A7, A16, Th15;
b <> d
by A2, Th14;
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 A21, A22, A19, Th10;
hence
not s,t,u are_collinear
by Th1; verum