theorem Th24:
for
V being non
trivial RealLinearSpace for
p,
q,
r being
Element of
(ProjectiveSpace V) st
p,
q,
r are_collinear holds
(
p,
r,
q are_collinear &
q,
p,
r are_collinear &
r,
q,
p are_collinear &
r,
p,
q are_collinear &
q,
r,
p are_collinear )