:: Hessenberg Theorem
:: by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received October 2, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ANPROJ_2, SUBSET_1, AFF_2, INCSP_1, PENCIL_1;
notations STRUCT_0, COLLSP, ANPROJ_2;
constructors ANPROJ_2;
registrations ANPROJ_2, PROJDES1;
theorems ANPROJ_2, COLLSP;
begin
reserve PCPP for CollProjectiveSpace,
a,a9,a1,a2,a3,b,b9,b1,b2,c,c1,c3,d,d9,e,
o,p,p1,p2,p3,r,q, q1,q2,q3,x,y for Element of PCPP;
theorem Th1:
a,b,c are_collinear implies b,c,a are_collinear & c,a,b
are_collinear & b,a,c are_collinear & a,c,b are_collinear &
c,b,a are_collinear
proof
assume
A1: a,b,c are_collinear;
then b,a,c are_collinear by COLLSP:4;
then
A2: b,c,a are_collinear by COLLSP:4;
a,c,b are_collinear by A1,COLLSP:4;
hence thesis by A2,COLLSP:4;
end;
theorem Th2:
a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear
proof
A1: a,b,a are_collinear by ANPROJ_2:def 7;
assume a<>b & a,b,c are_collinear & a,b,d are_collinear;
hence thesis by A1,ANPROJ_2:def 8;
end;
theorem
p<>q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear
implies a,b,r are_collinear
proof
assume that
A1: p<>q and
A2: a,b,p are_collinear & a,b,q are_collinear and
A3: p,q,r are_collinear;
now
assume
A4: a<>b;
b,a,p are_collinear & b,a,q are_collinear by A2,Th1;
then b,p,q are_collinear by A4,Th2;
then
A5: p,q,b are_collinear by Th1;
a,p,q are_collinear by A2,A4,Th2;
then p,q,a are_collinear by Th1;
hence thesis by A1,A3,A5,ANPROJ_2:def 8;
end;
hence thesis by ANPROJ_2:def 7;
end;
theorem Th4:
p<>q implies ex r st not p,q,r are_collinear
proof
consider a,b,c such that
A1: not a,b,c are_collinear by COLLSP:def 6;
assume p<>q;
then p,q,a are_collinear & p,q,b are_collinear & p,q,c are_collinear implies
contradiction by A1,ANPROJ_2:def 8;
hence thesis;
end;
theorem
ex q,r st not p,q,r are_collinear
proof
consider q such that
A1: p<>q and
p<>q and
p,p,q are_collinear by ANPROJ_2:def 10;
ex r st not p,q,r are_collinear by A1,Th4;
hence thesis;
end;
theorem Th6:
not a,b,c are_collinear & a,b,b9 are_collinear & a<>b9 implies not
a,b9,c are_collinear
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,b9 are_collinear and
A3: a<>b9;
assume
A4: not thesis;
a,b9,b are_collinear by A2,Th1;
hence contradiction by A1,A3,A4,Th2;
end;
theorem Th7:
not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear
implies a=d
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,d are_collinear & a,c,d are_collinear;
assume
A3: not thesis;
A4: a,d,a are_collinear by ANPROJ_2:def 7;
a,d,b are_collinear & a,d,c are_collinear by A2,Th1;
hence contradiction by A1,A3,A4,ANPROJ_2:def 8;
end;
theorem Th8:
not o,a,d are_collinear & o,d,d9 are_collinear & d<>d9 & a9,d9,x
are_collinear & o,a,a9 are_collinear & o<>a9 implies x<>d
proof
assume that
A1: not o,a,d are_collinear and
A2: o,d,d9 are_collinear and
A3: d<>d9 and
A4: a9,d9,x are_collinear and
A5: o,a,a9 are_collinear and
A6: o<>a9;
assume not thesis;
then
A7: d,d9,a9 are_collinear by A4,Th1;
d,d9,o are_collinear by A2,Th1;
then d,o,a9 are_collinear by A3,A7,Th2;
then
A8: o,a9,d are_collinear by Th1;
o,a9,a are_collinear by A5,Th1;
hence contradiction by A1,A6,A8,Th2;
end;
theorem Th9:
not a1,a2,a3 are_collinear & a1,a2,c3 are_collinear & a2,a3,c1
are_collinear & c1,c3,x are_collinear & c3<>a1 & c3<>a2 & c1<>a2 & c1<>a3
implies
a1<>x & a3<>x
proof
assume that
A1: not a1,a2,a3 are_collinear and
A2: a1,a2,c3 are_collinear and
A3: a2,a3,c1 are_collinear and
A4: c1,c3,x are_collinear and
A5: c3<>a1 and
A6: c3<>a2 and
A7: c1<>a2 and
A8: c1<>a3;
A9: a3<>x
proof
assume not thesis;
then
A10: a3,c1,c3 are_collinear by A4,Th1;
a3,c1,a2 are_collinear by A3,Th1;
then a3,a2,c3 are_collinear by A8,A10,Th2;
then
A11: a2,c3,a3 are_collinear by Th1;
a2,c3,a1 are_collinear by A2,Th1;
then a2,a1,a3 are_collinear by A6,A11,Th2;
hence contradiction by A1,Th1;
end;
a1<>x
proof
assume not thesis;
then
A12: a1,c3,c1 are_collinear by A4,Th1;
a1,c3,a2 are_collinear by A2,Th1;
then a1,c1,a2 are_collinear by A5,A12,Th2;
then
A13: a2,c1,a1 are_collinear by Th1;
a2,c1,a3 are_collinear by A3,Th1;
then a2,a1,a3 are_collinear by A7,A13,Th2;
hence contradiction by A1,Th1;
end;
hence thesis by A9;
end;
theorem Th10:
not a,b,c are_collinear & a,b,d are_collinear & c,e,d are_collinear
& e<>c & d<>a implies not e,a,c are_collinear
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b,d are_collinear and
A3: c,e,d are_collinear & e<>c and
A4: d<>a;
assume not thesis;
then c,e,a are_collinear by Th1;
then c,a,d are_collinear by A3,Th2;
then
A5: a,d,c are_collinear by Th1;
a,d,b are_collinear by A2,Th1;
hence contradiction by A1,A4,A5,Th2;
end;
theorem Th11:
not p1,p2,q1 are_collinear & p1,p2,q2 are_collinear & q1,q2,q3
are_collinear & q2<>q3 implies not p2,p1,q3 are_collinear
proof
assume that
A1: not p1,p2,q1 are_collinear and
A2: p1,p2,q2 are_collinear and
A3: q1,q2,q3 are_collinear and
A4: q2<>q3;
A5: p1<>p2 by A1,ANPROJ_2:def 7;
assume
A6: not thesis;
then p1,p2,q3 are_collinear by Th1;
then p1,q2,q3 are_collinear by A2,A5,Th2;
then
A7: q2,q3,p1 are_collinear by Th1;
p2,p1,q2 are_collinear by A2,Th1;
then p2,q2,q3 are_collinear by A6,A5,Th2;
then
A8: q2,q3,p2 are_collinear by Th1;
q2,q3,q1 are_collinear by A3,Th1;
hence contradiction by A1,A4,A7,A8,ANPROJ_2:def 8;
end;
theorem
not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,p3
are_collinear & p3<>q2 & p2<>p3 implies not p3,p2,q2 are_collinear
proof
assume that
A1: not p1,p2,q1 are_collinear and
A2: p1,p2,p3 are_collinear and
A3: q1,q2,p3 are_collinear and
A4: p3<>q2 and
A5: p2<>p3;
assume
A6: not thesis;
p3,p2,p1 are_collinear by A2,Th1;
then
A7: p3,q2,p1 are_collinear by A5,A6,Th2;
A8: p3,q2,q1 are_collinear by A3,Th1;
p3,q2,p2 are_collinear by A6,Th1;
hence contradiction by A1,A4,A7,A8,ANPROJ_2:def 8;
end;
theorem Th13:
not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,p1
are_collinear & p1<>p3 & p1<>q2 implies not p3,p1,q2 are_collinear
proof
assume that
A1: not p1,p2,q1 are_collinear and
A2: p1,p2,p3 are_collinear and
A3: q1,q2,p1 are_collinear and
A4: p1<>p3 and
A5: p1<>q2;
A6: p1,q2,q1 are_collinear by A3,Th1;
assume not thesis;
then
A7: p1,p3,q2 are_collinear by Th1;
p1,p3,p2 are_collinear by A2,Th1;
then p1,q2,p2 are_collinear by A4,A7,Th2;
hence contradiction by A1,A5,A6,Th2;
end;
theorem Th14:
a1<>a2 & b1<>b2 & b1,b2,x are_collinear & b1,b2,y are_collinear &
a1,a2,x are_collinear & a1,a2,y are_collinear & not a1,a2,b1 are_collinear
implies
x=y
proof
assume that
A1: a1<>a2 and
A2: b1<>b2 & b1,b2,x are_collinear & b1,b2,y are_collinear and
A3: a1,a2,x are_collinear & a1,a2,y are_collinear and
A4: not a1,a2,b1 are_collinear;
a1,a2,a2 are_collinear by ANPROJ_2:def 7;
then
A5: x,y,a2 are_collinear by A1,A3,ANPROJ_2:def 8;
b1,b2,b1 are_collinear by ANPROJ_2:def 7;
then
A6: x,y,b1 are_collinear by A2,ANPROJ_2:def 8;
assume
A7: not thesis;
a1,a2,a1 are_collinear by ANPROJ_2:def 7;
then x,y,a1 are_collinear by A1,A3,ANPROJ_2:def 8;
hence contradiction by A4,A7,A6,A5,ANPROJ_2:def 8;
end;
theorem Th15:
not o,a1,a2 are_collinear & o,a1,b1 are_collinear & o,a2,b2
are_collinear & o<>b1 & o<>b2 implies not o,b1,b2 are_collinear
proof
assume that
A1: ( not o,a1,a2 are_collinear)& o,a1,b1 are_collinear and
A2: o,a2,b2 are_collinear and
A3: o<>b1 and
A4: o<>b2;
not o,b1,a2 are_collinear by A1,A3,Th6;
then not o,a2,b1 are_collinear by Th1;
then not o,b2,b1 are_collinear by A2,A4,Th6;
hence thesis by Th1;
end;
reserve PCPP for Pappian CollProjectivePlane,
a,a1,a2,a3,b1,b2,b3,c1,c2,c3,o,p
,p1,p2,p3,q,q9, q1,q2,q3,r,r1,r2,r3,x,y,z for Element of PCPP;
theorem Th16:
p2<>p3 & p1<>p3 & q2<>q3 & q1<>q2 & q1<>q3 & not p1,p2,q1
are_collinear & p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & p1,q2,r3
are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2
are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear
implies r1,r2,r3
are_collinear
proof
assume that
A1: p2<>p3 and
A2: p1<>p3 and
A3: q2<>q3 and
A4: q1<>q2 and
A5: q1<>q3 and
A6: not p1,p2,q1 are_collinear and
A7: p1,p2,p3 are_collinear and
A8: q1,q2,q3 are_collinear and
A9: p1,q2,r3 are_collinear and
A10: q1,p2,r3 are_collinear and
A11: p1,q3,r2 are_collinear and
A12: p3,q1,r2 are_collinear and
A13: p2,q3,r1 are_collinear and
A14: p3,q2,r1 are_collinear;
A15: p1<>p2 by A6,ANPROJ_2:def 7;
A16: now
assume
A17: not p1,p2,q2 are_collinear;
A18: now
assume
A19: not p1,p2,q3 are_collinear;
A20: now
A21: now
( not p2,p1,q2 are_collinear)& p2,p1,p3 are_collinear by A7,A17,Th1;
then not p2,p3,q2 are_collinear by A1,Th6;
then
A22: not q2,p2,p3 are_collinear by Th1;
assume
A23: q1,q2,p2 are_collinear;
then
A24: p2,q1,q2 are_collinear by Th1;
p2<>q1 & p2,q1,r3 are_collinear by A6,A10,Th1,ANPROJ_2:def 7;
then p2,r3,q2 are_collinear by A24,Th2;
then
A25: q2,p2,r3 are_collinear by Th1;
q2,p1,r3 are_collinear & not q2,p1,p2 are_collinear by A9,A17,Th1;
then
A26: q2=r3 by A25,Th7;
A27: q2,q1,q3 are_collinear by A8,Th1;
q2,q1,p2 are_collinear by A23,Th1;
then q2,p2,q3 are_collinear by A4,A27,Th2;
then
A28: p2,q3,q2 are_collinear by Th1;
p2<>q3 by A19,ANPROJ_2:def 7;
then p2,r1,q2 are_collinear by A13,A28,Th2;
then
A29: q2,p2,r1 are_collinear by Th1;
q2,p3,r1 are_collinear by A14,Th1;
then q2=r1 by A29,A22,Th7;
hence thesis by A26,ANPROJ_2:def 7;
end;
A30: now
( not p2,p1,q3 are_collinear)& p2,p1,p3 are_collinear by A7,A19,Th1;
then not p2,p3,q3 are_collinear by A1,Th6;
then
A31: not q3,p2,p3 are_collinear by Th1;
assume
A32: q1,q2,p3 are_collinear;
then
A33: q2,q1,p3 are_collinear by Th1;
q2,q1,q3 are_collinear by A8,Th1;
then q2,q3, p3 are_collinear by A4,A33,Th2;
then p3,q2,q3 are_collinear by Th1;
then p3,r1,q3 are_collinear by A7,A14,A17,Th2;
then
A34: q3,p3,r1 are_collinear by Th1;
not p1,p3,q3 are_collinear by A2,A7,A19,Th6;
then
A35: not q3,p1,p3 are_collinear by Th1;
q1,q3,p3 are_collinear by A4,A8,A32,Th2;
then p3,q1,q3 are_collinear by Th1;
then p3,r2,q3 are_collinear by A6,A7,A12,Th2;
then
A36: q3,p3,r2 are_collinear by Th1;
q3,p2,r1 are_collinear by A13,Th1;
then
A37: q3=r1 by A34,A31,Th7;
q3,p1,r2 are_collinear by A11,Th1;
then q3=r2 by A36,A35,Th7;
hence thesis by A37,ANPROJ_2:def 7;
end;
A38: now
not p1,p3,q1 are_collinear by A2,A6,A7,Th6;
then
A39: not q1,p1,p3 are_collinear by Th1;
assume
A40: q1,q2,p1 are_collinear;
then q1,p1,q3 are_collinear by A4,A8,Th2;
then
A41: p1,q3,q1 are_collinear by Th1;
p1<>q3 by A19,ANPROJ_2:def 7;
then p1,r2,q1 are_collinear by A11,A41,Th2;
then
A42: q1,p1,r2 are_collinear by Th1;
A43: p1<>q2 by A17,ANPROJ_2:def 7;
p1,q2,q1 are_collinear by A40,Th1;
then p1,r3,q1 are_collinear by A9,A43,Th2;
then
A44: q1,p1,r3 are_collinear by Th1;
not q1,p2,p1 are_collinear by A6,Th1;
then
A45: q1=r3 by A10,A44,Th7;
q1,p3,r2 are_collinear by A12,Th1;
then q1=r2 by A42,A39,Th7;
hence thesis by A45,ANPROJ_2:def 7;
end;
assume q1,q2,p1 are_collinear or q1,q2,p2 are_collinear or q1,q2,p3
are_collinear;
hence thesis by A38,A21,A30;
end;
now
assume that
A46: not q1,q2,p1 are_collinear and
A47: ( not q1,q2,p2 are_collinear)& not q1,q2,p3 are_collinear;
consider o such that
A48: p1,p2,o are_collinear and
A49: q1,q2,o are_collinear by ANPROJ_2:def 14;
not p1,o,q1 are_collinear by A6,A46,A48,A49,Th6;
then
A50: not o,p1,q1 are_collinear by Th1;
q1,q3,o are_collinear by A4,A8,A49,Th2;
then
A51: o,q1,q3 are_collinear by Th1;
p1,p3,o are_collinear by A7,A15,A48,Th2;
then
A52: o,p1,p3 are_collinear by Th1;
o,p1,p2 are_collinear & o,q1,q2 are_collinear by A48,A49,Th1;
hence
thesis by A1,A2,A3,A4,A5,A9,A10,A11,A12,A13,A14,A15,A17,A19,A47,A48,A49
,A52,A51,A50,ANPROJ_2:def 13;
end;
hence thesis by A20;
end;
now
assume
A53: p1,p2,q3 are_collinear;
A54: now
assume that
A55: p2<>q3 and
A56: p1<>q3;
p1,q3,p2 are_collinear by A53,Th1;
then p1,p2,r2 are_collinear by A11,A56,Th2;
then p1,r2,p3 are_collinear by A7,A15,Th2;
then
A57: p3,p1,r2 are_collinear by Th1;
not p1,p3,q1 are_collinear by A2,A6,A7,Th6;
then not p3,q1,p1 are_collinear by Th1;
then
A58: p3=r2 by A12,A57,Th7;
A59: p2,p1,p3 are_collinear by A7,Th1;
p2,q3,p1 are_collinear by A53,Th1;
then p2,p1,r1 are_collinear by A13,A55,Th2;
then p2,r1,p3 are_collinear by A15,A59,Th2;
then
A60: p3,p2,r1 are_collinear by Th1;
( not p2,p1,q2 are_collinear)& p2,p1,p3 are_collinear by A7,A17,Th1;
then not p2,p3,q2 are_collinear by A1,Th6;
then not p3,q2,p2 are_collinear by Th1;
then p3=r1 by A14,A60,Th7;
hence thesis by A58,ANPROJ_2:def 7;
end;
A61: now
not p1,p3,q1 are_collinear by A2,A6,A7,Th6;
then
A62: not p3,p1,q1 are_collinear by Th1;
A63: not p2,q1,p1 are_collinear by A6,Th1;
A64: p2,q1,r3 are_collinear by A10,Th1;
assume
A65: p2=q3;
then p2,q1,q2 are_collinear by A8,Th1;
then p2,q2,r3 are_collinear by A5,A65,A64,Th2;
then
A66: q2,p2,r3 are_collinear by Th1;
p2,q1,q2 are_collinear by A8,A65,Th1;
then not p2,q2,p1 are_collinear by A3,A65,A63,Th6;
then
A67: not q2,p1,p2 are_collinear by Th1;
p1,p3,r2 are_collinear by A7,A11,A15,A65,Th2;
then p3,p1,r2 are_collinear by Th1;
then
A68: p3=r2 by A12,A62,Th7;
q2,p1,r3 are_collinear by A9,Th1;
then q2=r3 by A66,A67,Th7;
hence thesis by A14,A68,Th1;
end;
now
assume
A69: p1=q3;
then p1,p2,r1 are_collinear by A13,Th1;
then p1,p3,r1 are_collinear by A7,A15,Th2;
then
A70: p3,p1,r1 are_collinear by Th1;
p1,q2,q1 are_collinear by A8,A69,Th1;
then p1,q1,r3 are_collinear by A3,A9,A69,Th2;
then
A71: q1,p1,r3 are_collinear by Th1;
not p3,p1,q2 are_collinear by A2,A3,A6,A7,A8,A69,Th13;
then
A72: p3=r1 by A14,A70,Th7;
not q1,p1,p2 are_collinear by A6,Th1;
then q1=r3 by A10,A71,Th7;
hence thesis by A12,A72,Th1;
end;
hence thesis by A61,A54;
end;
hence thesis by A18;
end;
now
A73: now
not p1,p3,q1 are_collinear by A2,A6,A7,Th6;
then
A74: not q1,p1,p3 are_collinear by Th1;
A75: not p1,q1,p2 are_collinear by A6,Th1;
assume
A76: p1=q2;
then p1,q3,q1 are_collinear by A8,Th1;
then p1,q1,r2 are_collinear by A3,A11,A76,Th2;
then
A77: q1,p1,r2 are_collinear by Th1;
A78: p1,p3,p2 are_collinear by A7,Th1;
p1,p3,r1 are_collinear by A14,A76,Th1;
then p1,p2,r1 are_collinear by A2,A78,Th2;
then
A79: p2,p1,r1 are_collinear by Th1;
q1,p3,r2 are_collinear by A12,Th1;
then
A80: q1=r2 by A77,A74,Th7;
p1,q1,q3 are_collinear by A8,A76,Th1;
then not p1,q3,p2 are_collinear by A3,A76,A75,Th6;
then not p2,p1,q3 are_collinear by Th1;
then r1=p2 by A13,A79,Th7;
hence thesis by A10,A80,Th1;
end;
assume
A81: p1,p2,q2 are_collinear;
A82: now
assume that
A83: p1<>q2 and
A84: p3<>q2;
p1,q2,p2 are_collinear by A81,Th1;
then p1,p2,r3 are_collinear by A9,A83,Th2;
then
A85: p2,p1,r3 are_collinear by Th1;
p1,q2,p3 are_collinear by A7,A15,A81,Th2;
then p3,q2,p1 are_collinear by Th1;
then p3,p1,r1 are_collinear by A14,A84,Th2;
then
A86: p1,p3,r1 are_collinear by Th1;
p1,p3,p2 are_collinear by A7,Th1;
then p1,p2,r1 are_collinear by A2,A86,Th2;
then
A87: p2,p1,r1 are_collinear by Th1;
not p2,p1,q3 are_collinear by A3,A6,A8,A81,Th11;
then
A88: p2=r1 by A13,A87,Th7;
( not p2,p1,q1 are_collinear)& p2,q1,r3 are_collinear by A6,A10,Th1;
then p2=r3 by A85,Th7;
hence thesis by A88,ANPROJ_2:def 7;
end;
now
assume
A89: p3=q2;
then q1,q3,p3 are_collinear by A8,Th1;
then
A90: not q3,p1,q1 are_collinear by A2,A5,A6,A7,Th10;
p1,p3,p2 are_collinear by A7,Th1;
then p1,p2,r3 are_collinear by A2,A9,A89,Th2;
then
A91: p2,p1,r3 are_collinear by Th1;
( not p2,p1,q1 are_collinear)& p2,q1,r3 are_collinear by A6,A10,Th1;
then
A92: p2=r3 by A91,Th7;
q1,q2,r2 are_collinear by A12,A89,Th1;
then q1,q3,r2 are_collinear by A4,A8,Th2;
then
A93: q3,q1,r2 are_collinear by Th1;
q3,p1,r2 are_collinear by A11,Th1;
then r3,r2,r1 are_collinear by A13,A92,A90,A93,Th7;
hence thesis by Th1;
end;
hence thesis by A73,A82;
end;
hence thesis by A16;
end;
Lm1: 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
proof
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;
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 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 thesis by A6,A18,A21,ANPROJ_2:def 8;
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
assume
A25: b1,b2,b3 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 thesis by A7,A24,A26,ANPROJ_2:def 8;
end;
hence thesis by A15,A19;
end;
Lm2: 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
proof
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;
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 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;
A50: b1<>b3 by A49,ANPROJ_2:def 7;
consider z such that
A51: a1,a3,z are_collinear and
A52: c1,c3,z are_collinear by ANPROJ_2:def 14;
consider p 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 thesis;
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;
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 such that
A66: o,a1,q are_collinear and
A67: p,c3,q are_collinear by ANPROJ_2:def 14;
consider r 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 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 thesis;
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;
end;
assume
A85: not thesis;
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 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 thesis;
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;
end;
consider z99 be 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 thesis;
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;
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 be 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
o,b1,q are_collinear by A17,A23,A66,Th2;
then
A120: b1,o,q are_collinear by Th1;
assume b1<>q;
then 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;
end;
A135: not p,o,a are_collinear by A111,Th1;
now
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;
then
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 be 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;
end;
hence contradiction by A119;
end;
A146: b2<>b3 by A3,A9,A18,A19,Th7;
A147: b1<>b2 by A1,A7,A17,A18,Th7;
now
A148: now
assume
A149: b1,b2,b3 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 thesis by A12,A147,A150,ANPROJ_2:def 8;
end;
A151: now
assume
A152: a1,a2,a3 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 thesis by A11,A25,A153,ANPROJ_2:def 8;
end;
assume a1,a2,a3 are_collinear or b1,b2,b3 are_collinear;
hence thesis by A151,A148;
end;
hence thesis by A31;
end;
Lm3: 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
proof
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;
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
assume that
not a1,a2,a3 are_collinear and
not b1,b2,b3 are_collinear;
consider x such that
A21: a1,a3,x are_collinear and
A22: o,a2,x are_collinear by ANPROJ_2:def 14;
consider y such that
A23: b1,b3,y are_collinear and
A24: o,a2,y are_collinear by ANPROJ_2:def 14;
assume
A25: not thesis;
A26: now
( 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;
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;
end;
now
A33: now
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;
( 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;
end;
assume not c1,c3,x are_collinear or not c1,c3,y are_collinear;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16
,A17,A21,A22,A33,Lm2;
end;
hence thesis by A26;
end;
hence thesis by A1,A3,A7,A8,A9,A11,A12,A13,A14,A15,A16,A17,Lm1;
end;
theorem Th17:
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 &
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
proof
assume that
A1: o<>b1 & a1<>b1 & o<>b2 & a2<>b2 & o<>b3 & a3<>b3 & ( not o,a1,a2
are_collinear)& not o,a1,a3 are_collinear and
A2: not o,a2,a3 are_collinear and
A3: a1,a2,c3 are_collinear & b1,b2,c3 are_collinear and
A4: a2,a3,c1 are_collinear and
A5: b2,b3,c1 are_collinear and
A6: 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;
A7: o<>c1 by A2,A4,Th1;
A8: b3,b2,c1 are_collinear by A5,Th1;
A9: ( not o,a3,a2 are_collinear)& a3,a2,c1 are_collinear by A2,A4,Th1;
now
assume o,c1,c3 are_collinear;
then
A10: c1,c3,o are_collinear by Th1;
assume not thesis;
then
A11: not c1,c3,c2 are_collinear by Th1;
then not c1,o,c2 are_collinear by A7,A10,Th6;
then not o,c1,c2 are_collinear by Th1;
hence contradiction by A1,A3,A6,A9,A8,A11,Lm3;
end;
hence thesis by A1,A2,A3,A4,A5,A6,Lm3;
end;
registration
cluster Pappian -> Desarguesian for CollProjectiveSpace;
coherence
proof
let PCPP be CollProjectiveSpace such that
A1: PCPP is Pappian;
A2: now
assume not ex p,p1,q,q1 being Element of PCPP st not ex r being Element
of PCPP st p,p1,r are_collinear & q,q1,r are_collinear;
then PCPP is Pappian CollProjectivePlane by A1,ANPROJ_2:def 14;
then
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of PCPP st o<>q1 & p1<>
q1 & o<>q2 & p2<>q2 & o<>q3 & p3<>q3 & not o,p1,p2 are_collinear & not o,p1,p3
are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3
are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear &
p1,p3,r2
are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2
are_collinear & o,p3,q3 are_collinear holds r1,r2,r3 are_collinear
by Th17;
hence thesis by ANPROJ_2:def 12;
end;
now
assume ex p,p1,q,q1 being Element of PCPP st not ex r being Element of
PCPP st p,p1,r are_collinear & q,q1,r are_collinear;
then PCPP is up-3-dimensional CollProjectiveSpace by ANPROJ_2:def 14;
hence thesis;
end;
hence thesis by A2;
end;
end;