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 & not o,c1,c3 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 & not o,c1,c3 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
and
A2:
a1 <> b1
and
A3:
o <> b2
and
A4:
a2 <> b2
and
A5:
o <> b3
and
A6:
a3 <> b3
and
A7:
not o,a1,a2 are_collinear
and
A8:
not o,a1,a3 are_collinear
and
A9:
not o,a2,a3 are_collinear
and
A10:
not o,c1,c3 are_collinear
and
A11:
( a1,a2,c3 are_collinear & b1,b2,c3 are_collinear )
and
A12:
a2,a3,c1 are_collinear
and
A13:
b2,b3,c1 are_collinear
and
A14:
( a1,a3,c2 are_collinear & b1,b3,c2 are_collinear )
and
A15:
o,a1,b1 are_collinear
and
A16:
o,a2,b2 are_collinear
and
A17:
o,a3,b3 are_collinear
; c1,c2,c3 are_collinear
A18:
o <> a2
by A7, ANPROJ_2:def 7;
A19:
a1 <> a3
by A8, ANPROJ_2:def 7;
A20:
( o <> a1 & o <> a3 )
by A8, ANPROJ_2:def 7;
now ( not a1,a2,a3 are_collinear & not b1,b2,b3 are_collinear & not c1,c2,c3 are_collinear implies c1,c2,c3 are_collinear )assume that
not
a1,
a2,
a3 are_collinear
and
not
b1,
b2,
b3 are_collinear
;
( not c1,c2,c3 are_collinear implies c1,c2,c3 are_collinear )consider x being
Element of
PCPP such that A21:
a1,
a3,
x are_collinear
and A22:
o,
a2,
x are_collinear
by ANPROJ_2:def 14;
consider y being
Element of
PCPP such that A23:
b1,
b3,
y are_collinear
and A24:
o,
a2,
y are_collinear
by ANPROJ_2:def 14;
assume A25:
not
c1,
c2,
c3 are_collinear
;
c1,c2,c3 are_collinear A26:
now ( c1,c3,x are_collinear implies not c1,c3,y are_collinear )
( not
o,
a3,
a2 are_collinear &
b3,
b2,
c1 are_collinear )
by A9, A13, Th1;
then A27:
a2 <> c1
by A4, A5, A16, A17, Th8;
not
a2,
a3,
o are_collinear
by A9, Th1;
then
not
a2,
c1,
o are_collinear
by A12, A27, Th6;
then A28:
not
o,
a2,
c1 are_collinear
by Th1;
A29:
b1 <> b3
by A1, A8, A15, A17, Th7;
( not
a1,
o,
a3 are_collinear &
a1,
o,
b1 are_collinear )
by A8, A15, Th1;
then
not
a1,
b1,
a3 are_collinear
by A2, Th6;
then A30:
not
a1,
a3,
b1 are_collinear
by Th1;
assume that A31:
c1,
c3,
x are_collinear
and A32:
c1,
c3,
y are_collinear
;
contradiction
(
c1 <> c3 &
o <> a2 )
by A7, A10, ANPROJ_2:def 7;
then
b1,
b3,
x are_collinear
by A22, A23, A24, A31, A32, A28, Th14;
then
c1,
c3,
c2 are_collinear
by A14, A19, A21, A31, A29, A30, Th14;
hence
contradiction
by A25, Th1;
verum now ( ( not c1,c3,x are_collinear or not c1,c3,y are_collinear ) implies c1,c2,c3 are_collinear )A33:
now c1,c3,y are_collinear A34:
not
o,
b1,
b3 are_collinear
by A1, A5, A8, A15, A17, Th15;
A35:
(
o,
b2,
a2 are_collinear &
o,
b3,
a3 are_collinear )
by A16, A17, Th1;
A36:
(
o,
b2,
y are_collinear &
o,
b1,
a1 are_collinear )
by A15, A16, A18, A24, Th1, Th2;
assume A37:
not
c1,
c3,
y are_collinear
;
contradiction
( not
o,
b1,
b2 are_collinear & not
o,
b2,
b3 are_collinear )
by A1, A3, A5, A7, A9, A15, A16, A17, Th15;
hence
contradiction
by A2, A4, A6, A10, A11, A12, A13, A14, A18, A20, A23, A25, A37, A36, A35, A34, Lm2;
verum end; assume
( not
c1,
c3,
x are_collinear or not
c1,
c3,
y are_collinear )
;
c1,c2,c3 are_collinear hence
c1,
c2,
c3 are_collinear
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A21, A22, A33, Lm2;
verum hence
c1,
c2,
c3 are_collinear
by A26;
verum end;
hence
c1,c2,c3 are_collinear
by A1, A3, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, Lm1; verum