let FCPS be up-3-dimensional CollProjectiveSpace; for a, b, c, o, a', b', c' being Element of st not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & o <> a' & o <> b' & o <> c' holds
( not a',b',c' is_collinear & not a',b',c',o are_coplanar )
let a, b, c, o, a', b', c' be Element of ; ( not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & o <> a' & o <> b' & o <> c' implies ( not a',b',c' is_collinear & not a',b',c',o are_coplanar ) )
assume that
A1:
( not a,b,c,o are_coplanar & o,a,a' is_collinear )
and
A2:
o,b,b' is_collinear
and
A3:
o,c,c' is_collinear
and
A4:
o <> a'
and
A5:
o <> b'
and
A6:
o <> c'
; ( not a',b',c' is_collinear & not a',b',c',o are_coplanar )
( a,o,a' is_collinear & not o,b,c,a are_coplanar )
by A1, Th1, Th11;
then
not o,b,c,a' are_coplanar
by A4, Th19;
then A7:
not o,a',b,c are_coplanar
by Th11;
c,o,c' is_collinear
by A3, Th1;
then
not o,a',b,c' are_coplanar
by A6, A7, Th19;
then A8:
not o,a',c',b are_coplanar
by Th11;
b,o,b' is_collinear
by A2, Th1;
then
not o,a',c',b' are_coplanar
by A5, A8, Th19;
then
not a',b',c',o are_coplanar
by Th11;
hence
( not a',b',c' is_collinear & not a',b',c',o are_coplanar )
by Th10; verum