theorem Th20:
for
FCPS being
up-3-dimensional CollProjectiveSpace for
a,
a9,
b,
b9,
c,
d,
d9,
o,
s,
t,
u being
Element of
FCPS st
a,
b,
c,
o are_coplanar & not
a,
b,
c,
d are_coplanar & not
a,
b,
d,
o are_coplanar &
o,
d,
d9 are_collinear &
o,
a,
a9 are_collinear &
o,
b,
b9 are_collinear &
a,
d,
s are_collinear &
a9,
d9,
s are_collinear &
b,
d,
t are_collinear &
b9,
d9,
t are_collinear &
c,
d,
u are_collinear &
o <> a9 &
d <> d9 &
o <> b9 holds
not
s,
t,
u are_collinear