let PCPP be 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
let a1, a2, a3, b1, b2, b3, c1, c2, c3, o be Element of PCPP; ( 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 implies c1,c2,c3 are_collinear )
assume that
A1:
( o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 are_collinear & not o,a1,a3 are_collinear )
and
A2:
not o,a2,a3 are_collinear
and
A3:
( a1,a2,c3 are_collinear & b1,b2,c3 are_collinear )
and
A4:
a2,a3,c1 are_collinear
and
A5:
b2,b3,c1 are_collinear
and
A6:
( 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 )
; c1,c2,c3 are_collinear
A7:
o <> c1
by A2, A4, Th1;
A8:
b3,b2,c1 are_collinear
by A5, Th1;
A9:
( not o,a3,a2 are_collinear & a3,a2,c1 are_collinear )
by A2, A4, Th1;
now ( o,c1,c3 are_collinear implies c1,c2,c3 are_collinear )assume
o,
c1,
c3 are_collinear
;
c1,c2,c3 are_collinear then A10:
c1,
c3,
o are_collinear
by Th1;
assume
not
c1,
c2,
c3 are_collinear
;
contradictionthen A11:
not
c1,
c3,
c2 are_collinear
by Th1;
then
not
c1,
o,
c2 are_collinear
by A7, A10, Th6;
then
not
o,
c1,
c2 are_collinear
by Th1;
hence
contradiction
by A1, A3, A6, A9, A8, A11, Lm3;
verum end;
hence
c1,c2,c3 are_collinear
by A1, A2, A3, A4, A5, A6, Lm3; verum