theorem Th17:
for
FCPS being
up-3-dimensional CollProjectiveSpace for
a,
a9,
b,
b9,
c,
c9,
o,
p,
q,
r being
Element of
FCPS st
a <> a9 &
o,
a,
a9 are_collinear & not
a,
b,
c,
o are_coplanar & not
a9,
b9,
c9 are_collinear &
a,
b,
p are_collinear &
a9,
b9,
p are_collinear &
b,
c,
q are_collinear &
b9,
c9,
q are_collinear &
a,
c,
r are_collinear &
a9,
c9,
r are_collinear holds
p,
q,
r are_collinear