let PCPP be Pappian CollProjectivePlane; for o, b1, a1, b2, a2, b3, a3, c1, c3, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 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 holds
c1,c2,c3 is_collinear
let o, b1, a1, b2, a2, b3, a3, c1, c3, c2 be Element of PCPP; ( o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 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 implies c1,c2,c3 is_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 is_collinear
and
A8:
not o,a1,a3 is_collinear
and
A9:
not o,a2,a3 is_collinear
and
A10:
not o,c1,c3 is_collinear
and
A11:
( a1,a2,c3 is_collinear & b1,b2,c3 is_collinear )
and
A12:
a2,a3,c1 is_collinear
and
A13:
b2,b3,c1 is_collinear
and
A14:
( a1,a3,c2 is_collinear & b1,b3,c2 is_collinear )
and
A15:
o,a1,b1 is_collinear
and
A16:
o,a2,b2 is_collinear
and
A17:
o,a3,b3 is_collinear
; c1,c2,c3 is_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 consider a being
Element of
PCPP;
assume that
not
a1,
a2,
a3 is_collinear
and
not
b1,
b2,
b3 is_collinear
;
( not c1,c2,c3 is_collinear implies c1,c2,c3 is_collinear )consider x being
Element of
PCPP such that A21:
a1,
a3,
x is_collinear
and A22:
o,
a2,
x is_collinear
by ANPROJ_2:def 14;
consider z being
Element of
PCPP;
consider y being
Element of
PCPP such that A23:
b1,
b3,
y is_collinear
and A24:
o,
a2,
y is_collinear
by ANPROJ_2:def 14;
assume A25:
not
c1,
c2,
c3 is_collinear
;
c1,c2,c3 is_collinear A26:
now
( not
o,
a3,
a2 is_collinear &
b3,
b2,
c1 is_collinear )
by A9, A13, Th3;
then A27:
a2 <> c1
by A4, A5, A16, A17, Th10;
not
a2,
a3,
o is_collinear
by A9, Th3;
then
not
a2,
c1,
o is_collinear
by A12, A27, Th8;
then A28:
not
o,
a2,
c1 is_collinear
by Th3;
A29:
b1 <> b3
by A1, A8, A15, A17, Th9;
( not
a1,
o,
a3 is_collinear &
a1,
o,
b1 is_collinear )
by A8, A15, Th3;
then
not
a1,
b1,
a3 is_collinear
by A2, Th8;
then A30:
not
a1,
a3,
b1 is_collinear
by Th3;
assume that A31:
c1,
c3,
x is_collinear
and A32:
c1,
c3,
y is_collinear
;
contradiction
(
c1 <> c3 &
o <> a2 )
by A7, A10, ANPROJ_2:def 7;
then
b1,
b3,
x is_collinear
by A22, A23, A24, A31, A32, A28, Th17;
then
c1,
c3,
c2 is_collinear
by A14, A19, A21, A31, A29, A30, Th17;
hence
contradiction
by A25, Th3;
verum now A33:
now A34:
not
o,
b1,
b3 is_collinear
by A1, A5, A8, A15, A17, Th19;
A35:
(
o,
b2,
a2 is_collinear &
o,
b3,
a3 is_collinear )
by A16, A17, Th3;
A36:
(
o,
b2,
y is_collinear &
o,
b1,
a1 is_collinear )
by A15, A16, A18, A24, Th3, Th4;
assume A37:
not
c1,
c3,
y is_collinear
;
contradiction
( not
o,
b1,
b2 is_collinear & not
o,
b2,
b3 is_collinear )
by A1, A3, A5, A7, A9, A15, A16, A17, Th19;
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 is_collinear or not
c1,
c3,
y is_collinear )
;
c1,c2,c3 is_collinear hence
c1,
c2,
c3 is_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 is_collinear
by A26;
verum end;
hence
c1,c2,c3 is_collinear
by A1, A3, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, Lm1; verum