theorem Th7:
for
FCPS being
up-3-dimensional CollProjectiveSpace for
a,
b,
c,
d being
Element of
FCPS st
a,
b,
c,
d are_coplanar holds
(
b,
c,
d,
a are_coplanar &
c,
d,
a,
b are_coplanar &
d,
a,
b,
c are_coplanar &
b,
a,
c,
d are_coplanar &
c,
b,
d,
a are_coplanar &
d,
c,
a,
b are_coplanar &
a,
d,
b,
c are_coplanar &
a,
c,
d,
b are_coplanar &
b,
d,
a,
c are_coplanar &
c,
a,
b,
d are_coplanar &
d,
b,
c,
a are_coplanar &
c,
a,
d,
b are_coplanar &
d,
b,
a,
c are_coplanar &
a,
c,
b,
d are_coplanar &
b,
d,
c,
a are_coplanar &
a,
b,
d,
c are_coplanar &
a,
d,
c,
b are_coplanar &
b,
c,
a,
d are_coplanar &
b,
a,
d,
c are_coplanar &
c,
b,
a,
d are_coplanar &
c,
d,
b,
a are_coplanar &
d,
a,
c,
b are_coplanar &
d,
c,
b,
a are_coplanar )