let PCPP be Pappian CollProjectivePlane; for o, b1, b2, a1, a2, a3, c3, c1, b3, c2 being Element of PCPP st o <> b1 & o <> b2 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) holds
c1,c2,c3 is_collinear
let o, b1, b2, a1, a2, a3, c3, c1, b3, c2 be Element of PCPP; ( o <> b1 & o <> b2 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) implies c1,c2,c3 is_collinear )
assume that
A1:
o <> b1
and
A2:
o <> b2
and
A3:
not o,a1,a2 is_collinear
and
A4:
not o,a1,a3 is_collinear
and
A5:
not o,a2,a3 is_collinear
and
A6:
a1,a2,c3 is_collinear
and
A7:
b1,b2,c3 is_collinear
and
A8:
a2,a3,c1 is_collinear
and
A9:
b2,b3,c1 is_collinear
and
A10:
a1,a3,c2 is_collinear
and
A11:
b1,b3,c2 is_collinear
and
A12:
o,a1,b1 is_collinear
and
A13:
o,a2,b2 is_collinear
and
A14:
o,a3,b3 is_collinear
and
A15:
( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear )
; c1,c2,c3 is_collinear
A16:
a1 <> a3
by A4, ANPROJ_2:def 7;
A17:
a2 <> a3
by A5, ANPROJ_2:def 7;
A18:
a1 <> a2
by A3, ANPROJ_2:def 7;
A19:
now assume A20:
a1,
a2,
a3 is_collinear
;
c1,c2,c3 is_collinear then
a2,
a3,
a1 is_collinear
by Th3;
then
a2,
a1,
c1 is_collinear
by A8, A17, Th4;
then A21:
a1,
a2,
c1 is_collinear
by Th3;
a1,
a3,
a2 is_collinear
by A20, Th3;
then
a1,
a2,
c2 is_collinear
by A10, A16, Th4;
hence
c1,
c2,
c3 is_collinear
by A6, A18, A21, ANPROJ_2:def 8;
verum end;
A22:
b2 <> b3
by A2, A5, A13, A14, Th9;
A23:
b1 <> b3
by A1, A4, A12, A14, Th9;
A24:
b1 <> b2
by A1, A3, A12, A13, Th9;
now assume A25:
b1,
b2,
b3 is_collinear
;
c1,c2,c3 is_collinear then
b2,
b3,
b1 is_collinear
by Th3;
then
b2,
b1,
c1 is_collinear
by A9, A22, Th4;
then A26:
b1,
b2,
c1 is_collinear
by Th3;
b1,
b3,
b2 is_collinear
by A25, Th3;
then
b1,
b2,
c2 is_collinear
by A11, A23, Th4;
hence
c1,
c2,
c3 is_collinear
by A7, A24, A26, ANPROJ_2:def 8;
verum end;
hence
c1,c2,c3 is_collinear
by A15, A19; verum