theorem Th28:
for
V being non
trivial RealLinearSpace st ex
x1,
x2 being
Element of
(ProjectiveSpace V) st
(
x1 <> x2 & ( for
r1,
r2 being
Element of
(ProjectiveSpace V) ex
q being
Element of
(ProjectiveSpace V) st
(
x1,
x2,
q are_collinear &
r1,
r2,
q are_collinear ) ) ) holds
for
p,
p1,
q,
q1 being
Element of
(ProjectiveSpace V) ex
r being
Element of
(ProjectiveSpace V) st
(
p,
p1,
r are_collinear &
q,
q1,
r are_collinear )