let FCPS be up-3-dimensional CollProjectiveSpace; for a, a9, b, b9, c, c9, o being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & o <> a9 & o <> b9 & o <> c9 holds
( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar )
let a, a9, b, b9, c, c9, o be Element of FCPS; ( not a,b,c,o are_coplanar & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & o <> a9 & o <> b9 & o <> c9 implies ( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar ) )
assume that
A1:
( not a,b,c,o are_coplanar & o,a,a9 are_collinear )
and
A2:
o,b,b9 are_collinear
and
A3:
o,c,c9 are_collinear
and
A4:
o <> a9
and
A5:
o <> b9
and
A6:
o <> c9
; ( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar )
( a,o,a9 are_collinear & not o,b,c,a are_coplanar )
by A1, Th1, Th7;
then
not o,b,c,a9 are_coplanar
by A4, Th15;
then A7:
not o,a9,b,c are_coplanar
by Th7;
c,o,c9 are_collinear
by A3, Th1;
then
not o,a9,b,c9 are_coplanar
by A6, A7, Th15;
then A8:
not o,a9,c9,b are_coplanar
by Th7;
b,o,b9 are_collinear
by A2, Th1;
then
not o,a9,c9,b9 are_coplanar
by A5, A8, Th15;
then
not a9,b9,c9,o are_coplanar
by Th7;
hence
( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar )
by Th6; verum