theorem Th16:
for
PCPP being
Pappian CollProjectivePlane for
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Element of
PCPP st
p2 <> p3 &
p1 <> p3 &
q2 <> q3 &
q1 <> q2 &
q1 <> q3 & not
p1,
p2,
q1 are_collinear &
p1,
p2,
p3 are_collinear &
q1,
q2,
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