theorem
for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Element of
(ProjectiveSpace (TOP-REAL 3)) st
o <> p2 &
o <> p3 &
p2 <> p3 &
p1 <> p2 &
p1 <> p3 &
o <> q2 &
o <> q3 &
q2 <> q3 &
q1 <> q2 &
q1 <> q3 & not
o,
p1,
q1 are_collinear &
o,
p1,
p2 are_collinear &
o,
p1,
p3 are_collinear &
o,
q1,
q2 are_collinear &
o,
q1,
q3 are_collinear &
p1,
q2,
r3 are_collinear &
q1,
p2,
r3 are_collinear &
p1,
q3,
r2 are_collinear &
p3,
q1,
r2 are_collinear &
p2,
q3,
r1 are_collinear &
p3,
q2,
r1 are_collinear holds
r1,
r2,
r3 are_collinear