let PCPP be Pappian CollProjectivePlane; for a1, a2, a3, b1, b2, b3, c1, c2, c3, o, x 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 & o,a2,x are_collinear & a1,a3,x are_collinear & not c1,c3,x are_collinear holds
c1,c2,c3 are_collinear
let a1, a2, a3, b1, b2, b3, c1, c2, c3, o, x 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 & o,a2,x are_collinear & a1,a3,x are_collinear & not c1,c3,x 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
and
A12:
b1,b2,c3 are_collinear
and
A13:
a2,a3,c1 are_collinear
and
A14:
b2,b3,c1 are_collinear
and
A15:
a1,a3,c2 are_collinear
and
A16:
b1,b3,c2 are_collinear
and
A17:
o,a1,b1 are_collinear
and
A18:
o,a2,b2 are_collinear
and
A19:
o,a3,b3 are_collinear
and
A20:
o,a2,x are_collinear
and
A21:
a1,a3,x are_collinear
and
A22:
not c1,c3,x are_collinear
; c1,c2,c3 are_collinear
A23:
o <> a1
by A7, ANPROJ_2:def 7;
A24:
b1 <> b3
by A1, A8, A17, A19, Th7;
A25:
a1 <> a2
by A7, ANPROJ_2:def 7;
A26:
o <> a2
by A7, ANPROJ_2:def 7;
A27:
o <> a3
by A8, ANPROJ_2:def 7;
A28:
a1 <> a3
by A8, ANPROJ_2:def 7;
A29:
a2 <> a3
by A9, ANPROJ_2:def 7;
( not a1,o,a3 are_collinear & a1,o,b1 are_collinear )
by A8, A17, Th1;
then
not a1,b1,a3 are_collinear
by A2, Th6;
then A30:
not a1,a3,b1 are_collinear
by Th1;
A31:
now ( not a1,a2,a3 are_collinear & not b1,b2,b3 are_collinear implies c1,c2,c3 are_collinear )
( not
o,
a2,
a1 are_collinear &
b2,
b1,
c3 are_collinear )
by A7, A12, Th1;
then A32:
a1 <> c3
by A2, A3, A17, A18, Th8;
not
a1,
a2,
o are_collinear
by A7, Th1;
then
not
a1,
c3,
o are_collinear
by A11, A32, Th6;
then A33:
not
o,
a1,
c3 are_collinear
by Th1;
A34:
c1 <> c3
by A10, ANPROJ_2:def 7;
o <> x
by A8, A21, Th1;
then
not
o,
x,
a3 are_collinear
by A9, A20, Th6;
then A35:
not
x,
a3,
o are_collinear
by Th1;
A36:
a1 <> a3
by A8, ANPROJ_2:def 7;
( not
o,
a2,
a1 are_collinear &
b2,
b1,
c3 are_collinear )
by A7, A12, Th1;
then A37:
a1 <> c3
by A2, A3, A17, A18, Th8;
A38:
a2,
a1,
c3 are_collinear
by A11, Th1;
A39:
a2,
a1,
c3 are_collinear
by A11, Th1;
A40:
a2 <> c3
by A1, A4, A7, A12, A17, A18, Th8;
not
o,
b2,
a3 are_collinear
by A3, A9, A18, Th6;
then A41:
not
a3,
o,
b2 are_collinear
by Th1;
A42:
c1 <> c3
by A10, ANPROJ_2:def 7;
A43:
o,
b1,
a1 are_collinear
by A17, Th1;
A44:
not
a1,
a3,
o are_collinear
by A8, Th1;
( not
o,
a3,
a2 are_collinear &
b3,
b2,
c1 are_collinear )
by A9, A14, Th1;
then A45:
a2 <> c1
by A4, A5, A18, A19, Th8;
a3,
b3,
o are_collinear
by A19, Th1;
then
not
b2,
o,
b3 are_collinear
by A3, A5, A9, A18, Th13;
then A46:
not
o,
b3,
b2 are_collinear
by Th1;
A47:
o <> a2
by A7, ANPROJ_2:def 7;
assume that A48:
not
a1,
a2,
a3 are_collinear
and A49:
not
b1,
b2,
b3 are_collinear
;
c1,c2,c3 are_collinear A50:
b1 <> b3
by A49, ANPROJ_2:def 7;
consider z being
Element of
PCPP such that A51:
a1,
a3,
z are_collinear
and A52:
c1,
c3,
z are_collinear
by ANPROJ_2:def 14;
consider p being
Element of
PCPP such that A53:
o,
z,
p are_collinear
and A54:
a2,
a3,
p are_collinear
by ANPROJ_2:def 14;
A55:
o <> p
by A9, A54, Th1;
A56:
a3 <> c1
by A3, A6, A9, A14, A18, A19, Th8;
then A57:
a1 <> z
by A11, A13, A48, A52, A40, A45, A37, Th9;
A58:
a3 <> z
by A11, A13, A48, A52, A40, A45, A37, A56, Th9;
A59:
a3 <> p
proof
assume
not
a3 <> p
;
contradiction
then A60:
a3,
o,
z are_collinear
by A53, Th1;
(
a3,
a1,
z are_collinear & not
a3,
o,
a1 are_collinear )
by A8, A51, Th1;
hence
contradiction
by A58, A60, Th7;
verum
end; A61:
a3,
a1,
x are_collinear
by A21, Th1;
A62:
o,
b2,
a2 are_collinear
by A18, Th1;
a1 <> z
by A11, A13, A48, A52, A40, A45, A37, A56, Th9;
then
not
a1,
z,
o are_collinear
by A51, A44, Th6;
then
not
o,
z,
a1 are_collinear
by Th1;
then
not
o,
p,
a1 are_collinear
by A53, A55, Th6;
then A63:
not
o,
a1,
p are_collinear
by Th1;
A64:
a3,
z,
a1 are_collinear
by A51, Th1;
A65:
p,
a2,
a3 are_collinear
by A54, Th1;
consider q being
Element of
PCPP such that A66:
o,
a1,
q are_collinear
and A67:
p,
c3,
q are_collinear
by ANPROJ_2:def 14;
consider r being
Element of
PCPP such that A68:
p,
b2,
r are_collinear
and A69:
q,
a3,
r are_collinear
by ANPROJ_2:def 14;
A70:
a3,
q,
r are_collinear
by A69, Th1;
(
o,
b3,
a3 are_collinear &
a3,
a2,
c1 are_collinear )
by A13, A19, Th1;
then A71:
b2 <> c1
by A4, A27, A62, A46, Th8;
A72:
a2 <> c3
by A1, A4, A7, A12, A17, A18, Th8;
not
a1,
a3,
o are_collinear
by A8, Th1;
then
not
a1,
z,
o are_collinear
by A51, A57, Th6;
then
not
o,
z,
a1 are_collinear
by Th1;
then
not
o,
p,
a1 are_collinear
by A53, A55, Th6;
then A73:
b1 <> p
by A17, Th1;
consider a being
Element of
PCPP such that A74:
c1,
c3,
a are_collinear
and A75:
o,
a2,
a are_collinear
by ANPROJ_2:def 14;
A76:
c3,
c1,
a are_collinear
by A74, Th1;
A77:
a,
o,
a2 are_collinear
by A75, Th1;
A78:
o <> a
by A10, A74, Th1;
A79:
c1 <> c3
by A10, ANPROJ_2:def 7;
A80:
a2 <> a
proof
A81:
c3,
a2,
a1 are_collinear
by A11, Th1;
assume A82:
not
a2 <> a
;
contradiction
then
c3,
a2,
c1 are_collinear
by A74, Th1;
then
c3,
c1,
a1 are_collinear
by A40, A81, Th2;
then A83:
c1,
c3,
a1 are_collinear
by Th1;
A84:
c1,
a2,
a3 are_collinear
by A13, Th1;
c1,
a2,
c3 are_collinear
by A74, A82, Th1;
then
c1,
c3,
a3 are_collinear
by A45, A84, Th2;
hence
contradiction
by A48, A74, A79, A82, A83, ANPROJ_2:def 8;
verum
end; assume A85:
not
c1,
c2,
c3 are_collinear
;
contradiction
c3,
c1,
z are_collinear
by A52, Th1;
then
c3,
a,
z are_collinear
by A76, A42, Th2;
then A86:
a,
z,
c3 are_collinear
by Th1;
A87:
o,
x,
a are_collinear
by A20, A26, A75, Th2;
consider q9 being
Element of
PCPP such that A88:
(
o,
a1,
q9 are_collinear &
a,
a3,
q9 are_collinear )
by ANPROJ_2:def 14;
a3,
a2,
p are_collinear
by A54, Th1;
then
c3,
q9,
p are_collinear
by A9, A53, A75, A88, A80, A78, A36, A57, A58, A64, A39, A86, Th16;
then A89:
p,
c3,
q9 are_collinear
by Th1;
not
a2,
a1,
a3 are_collinear
by A48, Th1;
then
not
a2,
c3,
a3 are_collinear
by A72, A38, Th6;
then
p <> c3
by A54, Th1;
then A90:
a,
a3,
q are_collinear
by A23, A66, A67, A88, A89, A63, Th14;
then
a3,
q,
a are_collinear
by Th1;
then A91:
a3,
r,
a are_collinear
by A8, A66, A70, Th2;
( not
o,
a3,
a2 are_collinear &
b3,
b2,
c1 are_collinear )
by A9, A14, Th1;
then A92:
a2 <> c1
by A4, A5, A18, A19, Th8;
A93:
a <> a2
proof
A94:
c3,
a2,
a1 are_collinear
by A11, Th1;
assume A95:
not
a <> a2
;
contradiction
then
c3,
a2,
c1 are_collinear
by A74, Th1;
then
c3,
c1,
a1 are_collinear
by A72, A94, Th2;
then A96:
c1,
c3,
a1 are_collinear
by Th1;
A97:
c1,
a2,
a3 are_collinear
by A13, Th1;
c1,
a2,
c3 are_collinear
by A74, A95, Th1;
then
c1,
c3,
a3 are_collinear
by A92, A97, Th2;
hence
contradiction
by A48, A74, A34, A95, A96, ANPROJ_2:def 8;
verum
end; consider z99 being
Element of
PCPP such that A98:
(
b3,
r,
z99 are_collinear &
o,
p,
z99 are_collinear )
by ANPROJ_2:def 14;
a2,
b2,
o are_collinear
by A18, Th1;
then A99:
not
b1,
o,
b2 are_collinear
by A1, A3, A7, A17, Th13;
then
not
o,
b1,
b2 are_collinear
by Th1;
then A100:
b2 <> c3
by A4, A11, A23, A43, A62, Th8;
A101:
a <> b2
proof
A102:
c3,
b2,
b1 are_collinear
by A12, Th1;
assume A103:
not
a <> b2
;
contradiction
then
c3,
b2,
c1 are_collinear
by A74, Th1;
then
c3,
c1,
b1 are_collinear
by A100, A102, Th2;
then A104:
c1,
c3,
b1 are_collinear
by Th1;
A105:
c1,
b2,
b3 are_collinear
by A14, Th1;
c1,
b2,
c3 are_collinear
by A74, A103, Th1;
then
c1,
c3,
b3 are_collinear
by A71, A105, Th2;
hence
contradiction
by A49, A74, A34, A103, A104, ANPROJ_2:def 8;
verum
end;
not
a2,
a3,
o are_collinear
by A9, Th1;
then
not
a2,
c1,
o are_collinear
by A13, A92, Th6;
then A106:
a <> c1
by A75, Th1;
( not
a2,
a1,
o are_collinear &
a2,
a1,
c3 are_collinear )
by A7, A11, Th1;
then
not
a2,
c3,
o are_collinear
by A72, Th6;
then A107:
a <> c3
by A75, Th1;
o,
a,
b2 are_collinear
by A18, A26, A75, Th2;
then A108:
a,
o,
b2 are_collinear
by Th1;
(
a2,
o,
b2 are_collinear & not
a2,
o,
a3 are_collinear )
by A9, A18, Th1;
then A109:
not
a2,
b2,
a3 are_collinear
by A4, Th6;
then A110:
b2 <> p
by A54, Th1;
a3,
a1,
z are_collinear
by A51, Th1;
then
a3,
x,
z are_collinear
by A36, A61, Th2;
then
x,
a3,
z are_collinear
by Th1;
then
not
x,
z,
o are_collinear
by A22, A52, A35, Th6;
then
not
o,
z,
x are_collinear
by Th1;
then
not
o,
p,
x are_collinear
by A53, A55, Th6;
then
not
o,
x,
p are_collinear
by Th1;
then A111:
not
o,
a,
p are_collinear
by A78, A87, Th6;
then
not
a,
o,
p are_collinear
by Th1;
then
not
a,
a2,
p are_collinear
by A93, A77, Th6;
then
not
p,
a2,
a are_collinear
by Th1;
then A112:
not
p,
a3,
a are_collinear
by A59, A65, Th6;
then A113:
p <> r
by A91, Th1;
o,
a,
b2 are_collinear
by A18, A26, A75, Th2;
then
not
o,
b2,
p are_collinear
by A3, A111, Th6;
then
not
p,
b2,
o are_collinear
by Th1;
then
not
p,
r,
o are_collinear
by A68, A113, Th6;
then A114:
z <> r
by A53, Th1;
consider z9 being
Element of
PCPP such that A115:
(
b1,
r,
z9 are_collinear &
o,
p,
z9 are_collinear )
by ANPROJ_2:def 14;
A116:
not
o,
a,
a3 are_collinear
by A9, A75, A78, Th6;
then
not
a,
o,
a3 are_collinear
by Th1;
then A117:
not
a,
b2,
a3 are_collinear
by A101, A108, Th6;
then A118:
b2 <> r
by A91, Th1;
A119:
now not b1 <> q
o,
b1,
q are_collinear
by A17, A23, A66, Th2;
then A120:
b1,
o,
q are_collinear
by Th1;
assume
b1 <> q
;
contradictionthen
not
b1,
q,
b2 are_collinear
by A99, A120, Th6;
then A121:
not
q,
b1,
b2 are_collinear
by Th1;
A122:
(
b2,
p,
r are_collinear &
q,
p,
c3 are_collinear )
by A67, A68, Th1;
o,
b1,
q are_collinear
by A17, A23, A66, Th2;
then A123:
q,
b1,
o are_collinear
by Th1;
A124:
(
q <> o &
b2 <> p )
by A54, A116, A109, A90, Th1;
(
c3,
c1,
z are_collinear &
c3,
c1,
a are_collinear )
by A52, A74, Th1;
then
c3,
z,
a are_collinear
by A34, Th2;
then A125:
a,
c3,
z are_collinear
by Th1;
A126:
( not
c1,
c3,
o are_collinear &
o,
p,
z are_collinear )
by A10, A53, Th1;
(
a3,
a2,
c1 are_collinear &
a3,
a2,
p are_collinear )
by A13, A54, Th1;
then A127:
a3,
p,
c1 are_collinear
by A29, Th2;
o,
a,
b2 are_collinear
by A18, A26, A75, Th2;
then A128:
b2,
o,
a are_collinear
by Th1;
q,
a3,
a are_collinear
by A90, Th1;
then A129:
q,
r,
a are_collinear
by A8, A66, A69, Th2;
A130:
(
b2 <> r &
p <> r )
by A117, A91, A112, Th1;
(
b2,
b1,
c3 are_collinear &
o,
b2,
a are_collinear )
by A12, A18, A26, A75, Th1, Th2;
then
z9,
a,
c3 are_collinear
by A1, A115, A124, A130, A121, A123, A122, A129, Th16;
then A131:
a,
c3,
z9 are_collinear
by Th1;
A132:
b3,
b2,
c1 are_collinear
by A14, Th1;
(
a3,
o,
b3 are_collinear &
b2,
r,
p are_collinear )
by A19, A68, Th1;
then
z99,
c1,
a are_collinear
by A5, A6, A98, A110, A91, A118, A41, A113, A128, A127, A132, Th16;
then A133:
c1,
a,
z99 are_collinear
by Th1;
c1,
a,
c3 are_collinear
by A74, Th1;
then
c1,
c3,
z99 are_collinear
by A106, A133, Th2;
then
b3,
r,
z are_collinear
by A52, A98, A34, A55, A126, Th14;
then A134:
z,
r,
b3 are_collinear
by Th1;
(
o,
p,
z are_collinear & not
o,
p,
a are_collinear )
by A53, A111, Th1;
then
b1,
r,
z are_collinear
by A115, A55, A107, A125, A131, Th14;
then
z,
r,
b1 are_collinear
by Th1;
then
z,
b1,
b3 are_collinear
by A114, A134, Th2;
then
b1,
b3,
z are_collinear
by Th1;
then
c1,
c3,
c2 are_collinear
by A15, A16, A28, A30, A50, A51, A52, Th14;
hence
contradiction
by A85, Th1;
verum end; A135:
not
p,
o,
a are_collinear
by A111, Th1;
now not b1 = q
(
a3,
a2,
c1 are_collinear &
a3,
a2,
p are_collinear )
by A13, A54, Th1;
then
a3,
c1,
p are_collinear
by A29, Th2;
then A136:
p,
a3,
c1 are_collinear
by Th1;
A137:
b1,
c3,
b2 are_collinear
by A12, Th1;
( not
a1,
o,
a3 are_collinear &
a1,
o,
b1 are_collinear )
by A8, A17, Th1;
then
not
a1,
b1,
a3 are_collinear
by A2, Th6;
then A138:
not
a1,
a3,
b1 are_collinear
by Th1;
assume A139:
b1 = q
;
contradictionthen A140:
b1,
a3,
a are_collinear
by A90, Th1;
c1,
a,
z are_collinear
by A52, A74, A34, Th2;
then A141:
a,
c1,
z are_collinear
by Th1;
a2,
b2,
o are_collinear
by A18, Th1;
then
not
b1,
o,
b2 are_collinear
by A1, A3, A7, A17, Th13;
then A142:
not
b1,
b2,
o are_collinear
by Th1;
consider z9 being
Element of
PCPP such that A143:
(
b1,
b3,
z9 are_collinear &
p,
o,
z9 are_collinear )
by ANPROJ_2:def 14;
b1,
c3,
p are_collinear
by A67, A139, Th1;
then A144:
b1,
b2,
p are_collinear
by A17, A33, A137, Th2;
o,
b2,
a are_collinear
by A18, A75, A47, Th2;
then
c1,
z9,
a are_collinear
by A5, A6, A14, A19, A27, A73, A110, A143, A144, A142, A140, A136, Th16;
then A145:
a,
c1,
z9 are_collinear
by Th1;
p,
o,
z are_collinear
by A53, Th1;
then
b1,
b3,
z are_collinear
by A55, A106, A135, A143, A145, A141, Th14;
then
c1,
c3,
c2 are_collinear
by A15, A16, A28, A50, A51, A52, A138, Th14;
hence
contradiction
by A85, Th1;
verum hence
contradiction
by A119;
verum
A146:
b2 <> b3
by A3, A9, A18, A19, Th7;
A147:
b1 <> b2
by A1, A7, A17, A18, Th7;
now ( ( a1,a2,a3 are_collinear or b1,b2,b3 are_collinear ) implies c1,c2,c3 are_collinear )A148:
now ( b1,b2,b3 are_collinear implies c1,c2,c3 are_collinear )assume A149:
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 A14, A146, Th2;
then A150:
b1,
b2,
c1 are_collinear
by Th1;
b1,
b3,
b2 are_collinear
by A149, Th1;
then
b1,
b2,
c2 are_collinear
by A16, A24, Th2;
hence
c1,
c2,
c3 are_collinear
by A12, A147, A150, ANPROJ_2:def 8;
verum end; A151:
now ( a1,a2,a3 are_collinear implies c1,c2,c3 are_collinear )assume A152:
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 A13, A29, Th2;
then A153:
a1,
a2,
c1 are_collinear
by Th1;
a1,
a3,
a2 are_collinear
by A152, Th1;
then
a1,
a2,
c2 are_collinear
by A15, A28, Th2;
hence
c1,
c2,
c3 are_collinear
by A11, A25, A153, ANPROJ_2:def 8;
verum end; assume
(
a1,
a2,
a3 are_collinear or
b1,
b2,
b3 are_collinear )
;
c1,c2,c3 are_collinear hence
c1,
c2,
c3 are_collinear
by A151, A148;
verum
hence
c1,c2,c3 are_collinear
by A31; verum