theorem Th17:
for
PCPP being
Pappian CollProjectivePlane for
a1,
a2,
a3,
b1,
b2,
b3,
c1,
c2,
c3,
o being
Element of
PCPP st
o <> b1 &
a1 <> b1 &
o <> b2 &
a2 <> b2 &
o <> b3 &
a3 <> b3 & not
o,
a1,
a2 are_collinear & not
o,
a1,
a3 are_collinear & not
o,
a2,
a3 are_collinear &
a1,
a2,
c3 are_collinear &
b1,
b2,
c3 are_collinear &
a2,
a3,
c1 are_collinear &
b2,
b3,
c1 are_collinear &
a1,
a3,
c2 are_collinear &
b1,
b3,
c2 are_collinear &
o,
a1,
b1 are_collinear &
o,
a2,
b2 are_collinear &
o,
a3,
b3 are_collinear holds
c1,
c2,
c3 are_collinear