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