theorem Th19:
for
FCPS being
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 )