theorem Th17:
for
CPS being
CollProjectiveSpace st ( for
p1,
r2,
q,
r1,
q1,
p,
r being
Point of
CPS st
p1,
r2,
q are_collinear &
r1,
q1,
q are_collinear &
p1,
r1,
p are_collinear &
r2,
q1,
p are_collinear &
p1,
q1,
r are_collinear &
r2,
r1,
r are_collinear &
p,
q,
r are_collinear & not
p1,
r2,
q1 are_collinear & not
p1,
r2,
r1 are_collinear & not
p1,
r1,
q1 are_collinear holds
r2,
r1,
q1 are_collinear ) holds
for
p,
q,
r,
s,
a,
b,
c being
POINT of
(IncProjSp_of CPS) for
L,
Q,
R,
S,
A,
B,
C being
LINE of
(IncProjSp_of CPS) st not
q on L & not
r on L & not
p on Q & not
s on Q & not
p on R & not
r on R &
{a,p,s} on L &
{a,q,r} on Q &
{b,q,s} on R &
{b,p,r} on S &
{c,p,q} on A &
{c,r,s} on B &
{a,b} on C holds
not
c on C