theorem Th26:
for
V being non
trivial RealLinearSpace for
p,
p1,
q,
q1,
r,
r1,
r2 being
Element of
(ProjectiveSpace V) 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