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