Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ANPROJ_2, INCSP_1, AFF_2;
notation STRUCT_0, COLLSP, ANPROJ_2;
constructors ANPROJ_2, XBOOLE_0;
clusters ANPROJ_2, PROJDES1, ZFMISC_1, XBOOLE_0;
theorems ANPROJ_2, COLLSP;
begin
reserve PCPP for CollProjectiveSpace,
a,a',a1,a2,a3,b,b',b1,b2,c,c1,c3,d,d',e,o,p,p1,p2,p3,r,q,
q1,q2,q3,x,y for Element of PCPP;
canceled 2;
theorem Th3:
a,b,c is_collinear implies b,c,a is_collinear & c,a,b is_collinear &
b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear
proof
assume A1: a,b,c is_collinear;
then A2:b,a,c is_collinear by COLLSP:9;
A3:a,c,b is_collinear by A1,COLLSP:9;
b,c,a is_collinear by A2,COLLSP:9;
hence thesis by A3,COLLSP:9;
end;
theorem Th4:
a<>b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear
proof
assume A1: a<>b & a,b,c is_collinear & a,b,d is_collinear;
a,b,a is_collinear by ANPROJ_2:def 7;
hence thesis by A1,ANPROJ_2:def 8;
end;
theorem
p<>q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear
implies a,b,r is_collinear
proof
assume A1:p<>q & a,b,p is_collinear & a,b,q is_collinear &
p,q,r is_collinear;
now assume A2: a<>b;
A3: b,a,p is_collinear by A1,Th3;
b,a,q is_collinear by A1,Th3;
then b,p,q is_collinear by A2,A3,Th4;
then A4: p,q,b is_collinear by Th3;
a,p,q is_collinear by A1,A2,Th4;
then p,q,a is_collinear by Th3;
hence thesis by A1,A4,ANPROJ_2:def 8;
end;
hence thesis by ANPROJ_2:def 7;
end;
theorem Th6:
p<>q implies ex r st not p,q,r is_collinear
proof
assume A1: p<>q;
consider a,b,c such that A2: not a,b,c is_collinear by COLLSP:def 6;
p,q,a is_collinear & p,q,b is_collinear & p,q,c is_collinear implies
contradiction by A1,A2,ANPROJ_2:def 8;
hence thesis;
end;
theorem
ex q,r st not p,q,r is_collinear
proof
consider q such that
A1:p<>q & p<>q & p,p,q is_collinear by ANPROJ_2:def 10;
ex r st not p,q,r is_collinear by A1,Th6;
hence thesis;
end;
theorem Th8:
not a,b,c is_collinear & a,b,b' is_collinear & a<>b' implies
not a,b',c is_collinear
proof
assume A1: not a,b,c is_collinear & a,b,b' is_collinear & a<>b';
assume not thesis;
then a,b',b is_collinear & a,b',c is_collinear by A1,Th3;
hence contradiction by A1,Th4;
end;
theorem
Th9: not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear
implies a=d
proof assume A1: not a,b,c is_collinear & a,b,d is_collinear &
a,c,d is_collinear; assume A2: not thesis; a,d,a is_collinear &
a,d,b is_collinear & a,d,c is_collinear by A1,Th3,ANPROJ_2:def 7;
hence contradiction by A1,A2,ANPROJ_2:def 8; end;
theorem
Th10: not o,a,d is_collinear & o,d,d' is_collinear & a,d,x is_collinear &
d<>d' & a',d',x is_collinear & o,a,a' is_collinear & o<>a' implies x<>d
proof assume A1: not o,a,d is_collinear & o,d,d' is_collinear &
a,d,x is_collinear & d<>d' & a',d',x is_collinear & o,a,a' is_collinear &
o<>a'; assume not thesis;
then A2: d,d',a' is_collinear by A1,Th3; d,d',o is_collinear by A1,Th3;
then d,o,a' is_collinear by A1,A2,Th4; then A3: o,a',d is_collinear by Th3;
o,a',a is_collinear by A1,Th3;
hence contradiction by A1,A3,Th4; end;
canceled;
theorem
Th12: not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear &
a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear &
c3<>a1 & c3<>a2 & c1<>a2 & c1<>a3 implies a1<>x & a3<>x
proof assume A1: not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear &
a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear &
c3<>a1 & c3<>a2 & c1<>a2 & c1<>a3;
A2: a1<>x proof assume not thesis;
then a1,c3,c1 is_collinear & a1,c3,a2 is_collinear by A1,Th3;
then a1,c1,a2 is_collinear by A1,Th4; then a2,c1,a1 is_collinear &
a2,c1,a3 is_collinear by A1,Th3; then a2,a1,a3 is_collinear by A1,Th4;
hence contradiction by A1,Th3; end;
a3<>x proof assume not thesis;
then a3,c1,c3 is_collinear & a3,c1,a2 is_collinear by A1,Th3;
then a3,a2,c3 is_collinear by A1,Th4; then a2,c3,a3 is_collinear &
a2,c3,a1 is_collinear by A1,Th3; then a2,a1,a3 is_collinear by A1,Th4;
hence contradiction by A1,Th3; end; hence thesis by A2;
end;
theorem
Th13: not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear &
e<>c & d<>a implies not e,a,c is_collinear
proof assume A1: not a,b,c is_collinear & a,b,d is_collinear &
c,e,d is_collinear & e<>c & d<>a; assume not thesis;
then c,e,a is_collinear by Th3; then c,a,d is_collinear by A1,Th4;
then a,d,c is_collinear & a,d,b is_collinear by A1,Th3;
hence contradiction by A1,Th4; end;
theorem
Th14: not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear &
q1,q2,q3 is_collinear & p1<>q2 & q2<>q3 implies not p2,p1,q3 is_collinear
proof assume A1: not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear &
q1,q2,q3 is_collinear & p1<>q2 & q2<>q3;
assume A2: not thesis; A3: p1<>p2 by A1,ANPROJ_2:def 7;
p1,p2,q3 is_collinear by A2,Th3; then p1,q2,q3 is_collinear by A1,A3,Th4;
then A4: q2,q3,p1 is_collinear by Th3; p2,p1,q2 is_collinear by A1,Th3;
then p2,q2,q3 is_collinear by A2,A3,Th4;
then A5: q2,q3,p2 is_collinear by Th3; q2,q3,q1 is_collinear by A1,Th3;
hence contradiction by A1,A4,A5,ANPROJ_2:def 8; end;
theorem
not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p3 is_collinear &
p3<>q2 & p2<>p3 implies not p3,p2,q2 is_collinear
proof assume A1: not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear &
q1,q2,p3 is_collinear & p3<>q2 & p2<>p3; assume A2: not thesis;
p3,p2,p1 is_collinear by A1,Th3;
then A3: p3,q2,p1 is_collinear by A1,A2,Th4;
p3,q2,p2 is_collinear & p3,q2,q1 is_collinear by A1,A2,Th3;
hence contradiction by A1,A3,ANPROJ_2:def 8; end;
theorem
Th16: not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear &
q1,q2,p1 is_collinear & p1<>p3 & p1<>q2 implies not p3,p1,q2 is_collinear
proof assume A1: not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear &
q1,q2,p1 is_collinear & p1<>p3 & p1<>q2; assume not thesis;
then p1,p3,q2 is_collinear & p1,p3,p2 is_collinear by A1,Th3;
then A2: p1,q2,p2 is_collinear by A1,Th4; p1,q2,q1 is_collinear by A1,Th3;
hence contradiction by A1,A2,Th4; end;
theorem
Th17: a1<>a2 & b1<>b2 & b1,b2,x is_collinear & b1,b2,y is_collinear &
a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear
implies x=y
proof assume A1: a1<>a2 & b1<>b2 & b1,b2,x is_collinear & b1,b2,y is_collinear
& a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear;
assume A2: not thesis; A3: a1,a2,a1 is_collinear & a1,a2,a2 is_collinear &
b1,b2,b1 is_collinear by ANPROJ_2:def 7; then A4: x,y,b1 is_collinear by A1,
ANPROJ_2:def 8;
A5: x,y,a1 is_collinear by A1,A3,ANPROJ_2:def 8; x,y,a2 is_collinear by A1,A3,
ANPROJ_2:def 8;
hence contradiction by A1,A2,A4,A5,ANPROJ_2:def 8; end;
canceled;
theorem
Th19: not o,a1,a2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear
& o<>b1 & o<>b2 implies not o,b1,b2 is_collinear
proof assume that A1: not o,a1,a2 is_collinear and A2: o,a1,b1 is_collinear
& o,a2,b2 is_collinear and A3: o<>b1 & o<>b2;
not o,b1,a2 is_collinear by A1,A2,A3,Th8; then not o,a2,b1 is_collinear
by Th3; then not o,b2,b1 is_collinear by A2,A3,Th8;
hence thesis by Th3; end;
reserve PCPP for Pappian CollProjectivePlane,
a,a1,a2,a3,b1,b2,b3,c1,c2,c3,o,p,p1,p2,p3,q,q',
q1,q2,q3,r,r1,r2,r3,x,y,z for Element of PCPP;
theorem
Th20: p2<>p3 & p1<>p3 & q2<>q3 & q1<>q2 & q1<>q3 &
not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear &
p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear &
p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear
implies r1,r2,r3 is_collinear
proof assume A1: p2<>p3 & p1<>p3 & q2<>q3 & q1<>q2 & q1<>q3 &
not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear &
p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear &
p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear;
then A2: p1<>p2 by ANPROJ_2:def 7; A3: now assume A4: p1,p2,q2 is_collinear;
A5: now assume A6: p3=q2; p1,p3,p2 is_collinear by A1,Th3;
then p1,p2,r3 is_collinear by A1,A6,Th4;
then A7: p2,p1,r3 is_collinear by Th3;
A8: not p2,p1,q1 is_collinear by A1,Th3; p2,q1,r3 is_collinear by A1,Th3;
then A9: p2=r3 by A7,A8,Th9; q1,q3,p3 is_collinear by A1,A6,Th3;
then A10: not q3,p1,q1 is_collinear by A1,Th13;
q1,q2,r2 is_collinear by A1,A6,Th3;
then q1,q3,r2 is_collinear by A1,Th4;
then A11: q3,q1,r2 is_collinear by Th3;
q3,p1,r2 is_collinear by A1,Th3;
then r3,r2,r1 is_collinear by A1,A9,A10,A11,Th9; hence thesis by Th3; end;
A12: now assume A13: p1=q2; A14: r1=p2 proof
A15: not p1,q1,p2 is_collinear by A1,Th3; p1,q1,q3 is_collinear by A1,A13,Th3
;
then not p1,q3,p2 is_collinear by A1,A13,A15,Th8;
then A16: not p2,p1,q3 is_collinear by Th3; p1,p3,r1 is_collinear &
p1,p3,p2 is_collinear by A1,A13,Th3; then p1,p2,r1 is_collinear by A1,Th4;
then p2,p1,r1 is_collinear by Th3; hence thesis by A1,A16,Th9; end;
q1=r2 proof p1,q3,q1 is_collinear &
p1,q3,r2 is_collinear by A1,A13,Th3; then p1,q1,r2 is_collinear by A1,A13,
Th4;
then A17: q1,p1,r2 is_collinear by Th3;
not p1,p3,q1 is_collinear by A1,Th8;
then A18: not q1,p1,p3 is_collinear by Th3; q1,p3,r2 is_collinear by A1,Th3
;
hence thesis by A17,A18,Th9; end;
hence thesis by A1,A14,Th3; end;
now assume A19: p1<>q2 & p3<>q2; p2=r1 & p2=r3 proof
thus p2=r1 proof p1,q2,p3 is_collinear by A1,A2,A4,Th4;
then p3,q2,p1 is_collinear by Th3; then p3,p1,r1 is_collinear by A1,A19,Th4;
then p1,p3,r1 is_collinear & p1,p3,p2 is_collinear by A1,Th3;
then p1,p2,r1 is_collinear by A1,Th4; then A20: p2,p1,r1 is_collinear by Th3
;
not p2,p1,q3 is_collinear by A1,A4,A19,Th14; hence thesis by A1,A20,Th9
; end;
thus p2=r3 proof p1,q2,p2 is_collinear by A4,Th3;
then p1,p2,r3 is_collinear by A1,A19,Th4;
then A21: p2,p1,r3 is_collinear by Th3;
not p2,p1,q1 is_collinear & p2,q1,r3 is_collinear by A1,Th3;
hence thesis by A21,Th9; end; end; hence thesis by ANPROJ_2:def 7; end;
hence thesis by A5,A12; end; now assume A22: not p1,p2,q2 is_collinear;
A23: now assume A24: p1,p2,q3 is_collinear;
A25: now assume A26: p1=q3; q1=r3 & p3=r1 proof
thus q1=r3 proof
p1,q2,q1 is_collinear by A1,A26,Th3;
then p1,q1,r3 is_collinear by A1,A26,Th4;
then A27: q1,p1,r3 is_collinear by Th3;
not q1,p1,p2 is_collinear by A1,Th3; hence thesis by A1,A27,Th9; end;
thus p3=r1 proof p1,p2,r1 is_collinear by A1,A26,Th3;
then p1,p3,r1 is_collinear by A1,A2,Th4;
then A28: p3,p1,r1 is_collinear by Th3;
not p3,p1,q2 is_collinear by A1,A26,Th16; hence thesis by A1,A28,Th9; end;
end; hence thesis by A1,Th3; end;
A29: now assume A30: p2=q3; q2=r3 & p3=r2 proof
thus q2=r3 proof A31: q2,p1,r3 is_collinear by A1,Th3;
p2,q1,r3 is_collinear & p2,q1,q2 is_collinear by A1,A30,Th3;
then p2,q2,r3 is_collinear by A1,A30,Th4; then A32: q2,p2,r3 is_collinear by
Th3;
not q2,p1,p2 is_collinear proof A33: not p2,q1,p1 is_collinear by A1,Th3;
p2,q1,q2 is_collinear by A1,A30,Th3;
then not p2,q2,p1 is_collinear by A1,A30,A33,Th8; hence thesis by Th3; end;
hence thesis by A31,A32,Th9; end;
thus p3=r2 proof p1,p3,r2 is_collinear
by A1,A2,A30,Th4; then A34: p3,p1,r2 is_collinear by Th3;
not p3,p1,q1 is_collinear proof not p1,p3,q1 is_collinear by A1,Th8;
hence thesis by Th3; end; hence thesis by A1,A34,Th9; end; end;
hence thesis by A1,Th3; end;
now assume A35: p2<>q3 & p1<>q3;
A36: p3=r1 proof p2,q3,p1 is_collinear by A24,Th3;
then p2,p1,r1 is_collinear & p2,p1,p3 is_collinear by A1,A35,Th3,Th4;
then p2,r1,p3 is_collinear by A2,Th4; then A37: p3,p2,r1 is_collinear by Th3;
not p3,q2,p2 is_collinear proof A38: not p2,p1,q2 is_collinear by A22,Th3;
p2,p1,p3 is_collinear by A1,Th3; then not p2,p3,q2 is_collinear by A1,A38,Th8
;
hence thesis by Th3; end; hence thesis by A1,A37,Th9; end;
p3=r2 proof p1,q3,p2 is_collinear by A24,Th3;
then p1,p2,r2 is_collinear by A1,A35,Th4; then p1,r2,p3 is_collinear
by A1,A2,Th4; then A39: p3,p1,r2 is_collinear by Th3;
not p1,p3,q1 is_collinear by A1,Th8; then not p3,q1,p1 is_collinear by Th3;
hence thesis by A1,A39,Th9; end; hence thesis by A36,ANPROJ_2:def 7; end;
hence thesis by A25,A29; end; now assume
A40: not p1,p2,q3 is_collinear; A41: now assume A42: q1,q2,p1 is_collinear or
q1,q2,p2 is_collinear or q1,q2,p3 is_collinear;
A43: now assume A44: q1,q2,p1 is_collinear; q1=r2 & q1=r3 proof
thus q1=r2 proof q1,p1,q3 is_collinear by A1,A44,Th4;
then A45: p1,q3,q1 is_collinear by Th3; p1<>q3 by A40,ANPROJ_2:def 7;
then p1,r2,q1 is_collinear by A1,A45,Th4; then A46: q1,p1,r2 is_collinear by
Th3;
not p1,p3,q1 is_collinear by A1,Th8; then not q1,p1,p3 is_collinear &
q1,p3,r2 is_collinear by A1,Th3; hence thesis by A46,Th9; end;
thus q1=r3 proof A47: p1<>q2 by A22,ANPROJ_2:def 7
; p1,q2,q1 is_collinear by A44,Th3;
then p1,r3,q1 is_collinear by A1,A47,Th4; then A48: q1,p1,r3 is_collinear by
Th3; not q1,p2,p1 is_collinear by A1,Th3; hence thesis by A1,A48,Th9; end;
end;
hence thesis by ANPROJ_2:def 7
; end; A49: now assume A50: q1,q2,p2 is_collinear;
q2=r3 & q2=r1 proof thus q2=r3 proof A51: p2<>q1 by A1,ANPROJ_2:def 7
; p2,q1,r3 is_collinear
& p2,q1,q2 is_collinear by A1,A50,Th3; then p2,r3,q2 is_collinear by A51,Th4;
then A52: q2,p2,r3 is_collinear & q2,p1,r3 is_collinear by A1,Th3;
not q2,p1,p2 is_collinear by A22,Th3; hence thesis by A52,Th9; end;
thus q2=r1 proof A53: p2<>q3 by A40,ANPROJ_2:def 7; q2,q1,p2 is_collinear &
q2,q1,q3 is_collinear by A1,A50,Th3; then q2,p2,q3 is_collinear by A1,Th4;
then p2,q3,q2 is_collinear by Th3; then p2,r1,q2 is_collinear by A1,A53,Th4;
then A54: q2,p2,r1 is_collinear & q2,p3,r1 is_collinear by A1,Th3;
not p2,p1,q2 is_collinear & p2,p1,p3 is_collinear by A1,A22,Th3;
then not p2,p3,q2 is_collinear by A1,Th8; then not q2,p2,p3 is_collinear by Th3
;
hence thesis by A54,Th9; end; end; hence thesis by ANPROJ_2:def 7; end;
now assume A55: q1,q2,p3 is_collinear; q3=r2 & q3=r1 proof
thus q3=r2 proof
q1,q3,p3 is_collinear by A1,A55,Th4;
then p3,q1,q3 is_collinear by Th3; then p3,r2,q3 is_collinear by A1,Th4;
then A56: q3,p3,r2 is_collinear & q3,p1,r2 is_collinear by A1,Th3; not
p1,p3,q3 is_collinear by A1,A40,Th8; then not q3,p1,p3 is_collinear by Th3;
hence thesis by A56,Th9; end;
thus q3=r1 proof
q2,q1,q3 is_collinear & q2,q1,p3 is_collinear by A1,A55,Th3; then q2,q3,p3
is_collinear by A1,Th4; then p3,q2,q3 is_collinear by Th3;
then p3,r1,q3 is_collinear by A1,A22,Th4; then A57: q3,p3,r1 is_collinear &
q3,p2,r1 is_collinear by A1,Th3; not p2,p1,q3 is_collinear &
p2,p1,p3 is_collinear by A1,A40,Th3; then not p2,p3,q3 is_collinear by A1,Th8;
then not q3,p2,p3 is_collinear by Th3; hence thesis by A57,Th9; end; end;
hence thesis by ANPROJ_2:def 7; end; hence thesis by A42,A43,A49; end;
now assume A58: not q1,q2,p1 is_collinear & not q1,q2,p2 is_collinear &
not q1,q2,p3 is_collinear; consider o such that A59: p1,p2,o is_collinear &
q1,q2,o is_collinear by ANPROJ_2:def 14;
A60: o,p1,p3 is_collinear & o,q1,q3 is_collinear & o,p1,p2 is_collinear &
o,q1,q2 is_collinear proof p1,p3,o is_collinear by A1,A2,A59,Th4; hence
o,p1,p3 is_collinear by Th3; q1,q3,o is_collinear by A1,A59,Th4; hence
o,q1,q3 is_collinear by Th3; thus thesis by A59,Th3; end;
not o,p1,q1 is_collinear proof
not p1,o,q1 is_collinear by A1,A58,A59,Th8; hence thesis by Th3;end;
hence thesis by A1,A2,A22,A40,A58,A59,A60,ANPROJ_2:def 13; end; hence thesis
by A41; end;
hence thesis by A23; end; hence thesis by A3; end;
Lm1:
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 &
(a1,a2,a3 is_collinear or b1,b2,b3 is_collinear) implies c1,c2,c3 is_collinear
proof assume that A1: o<>b1 & a1<>b1 & o<>b2 & a2<>b2 & o<>b3 & a3<>b3 and
A2: not o,a1,a2 is_collinear & not o,a1,a3 is_collinear &
not o,a2,a3 is_collinear and
not o,c1,c3 is_collinear and
A3: 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 and
A4: o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear and
A5: a1,a2,a3 is_collinear or b1,b2,b3 is_collinear;
A6: o<>a1 & o<>a2 & a1<>a2 & o<>a3 & a1<>a3 & a2<>a3 by A2,ANPROJ_2:def 7;
A7: b1<>b2 & b1<>b3 & b2<>b3 by A1,A2,A4,Th9;
A8: now assume A9: a1,a2,a3 is_collinear;
A10: a1,a2,c1 is_collinear proof a2,a3,a1 is_collinear by A9,Th3;
then a2,a1,c1 is_collinear by A3,A6,Th4; hence thesis by Th3; end;
a1,a2,c2 is_collinear proof a1,a3,a2 is_collinear by A9,Th3;
hence thesis by A3,A6,Th4; end;
hence c1,c2,c3 is_collinear by A3,A6,A10,ANPROJ_2:def 8; end;
now assume A11: b1,b2,b3 is_collinear;
A12: b1,b2,c1 is_collinear proof b2,b3,b1 is_collinear by A11,Th3;
then b2,b1,c1 is_collinear by A3,A7,Th4; hence thesis by Th3; end;
b1,b2,c2 is_collinear proof b1,b3,b2 is_collinear by A11,Th3;
hence thesis by A3,A7,Th4;end; hence thesis by A3,A7,A12,ANPROJ_2:def 8;
end; hence thesis by A5,A8; end;
Lm2:
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 & o,a2,x is_collinear &
a1,a3,x is_collinear & not c1,c3,x is_collinear
implies c1,c2,c3 is_collinear
proof assume that A1: o<>b1 & a1<>b1 & o<>b2 & a2<>b2 & o<>b3 & a3<>b3 and
A2: not o,a1,a2 is_collinear & not o,a1,a3 is_collinear &
not o,a2,a3 is_collinear and
A3: not o,c1,c3 is_collinear and
A4: 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 and
A5: o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear and
A6: o,a2,x is_collinear &
a1,a3,x is_collinear and A7: not c1,c3,x is_collinear;
A8: o<>a1 & o<>a2 & a1<>a2 & o<>a3 & a1<>a3 & a2<>a3 by A2,ANPROJ_2:def 7;
A9: not a1,a3,b1 is_collinear proof not a1,o,a3 is_collinear &
a1,o,b1 is_collinear by A2,A5,Th3; then not a1,b1,a3 is_collinear
by A1,Th8; hence thesis by Th3; end;
A10: b1<>b2 & b1<>b3 & b2<>b3 by A1,A2,A5,Th9;
A11: now assume A12: a1,a2,a3 is_collinear or b1,b2,b3 is_collinear;
A13: now assume A14: a1,a2,a3 is_collinear; thus thesis proof
A15: a1,a2,c1 is_collinear proof a2,a3,a1 is_collinear by A14,Th3;
then a2,a1,c1 is_collinear by A4,A8,Th4; hence thesis by Th3; end;
a1,a2,c2 is_collinear proof a1,a3,a2 is_collinear by A14,Th3;
hence thesis by A4,A8,Th4; end;
hence c1,c2,c3 is_collinear by A4,A8,A15,ANPROJ_2:def 8; end; end;
now assume A16: b1,b2,b3 is_collinear; thus thesis proof
A17: b1,b2,c1 is_collinear proof b2,b3,b1 is_collinear by A16,Th3;
then b2,b1,c1 is_collinear by A4,A10,Th4; hence thesis by Th3; end;
b1,b2,c2 is_collinear proof b1,b3,b2 is_collinear by A16,Th3;
hence thesis by A4,A10,Th4;end; hence thesis by A4,A10,A17,ANPROJ_2:def 8;
end; end; hence thesis by A12,A13; end;
now assume A18: not a1,a2,a3 is_collinear & not b1,b2,b3 is_collinear;
assume A19: not thesis;
A20: b1<>b2 & b1<>b3 & b2<>b3 by A18,ANPROJ_2:def 7;
consider z such that A21: a1,a3,z is_collinear & c1,c3,z is_collinear by
ANPROJ_2:def 14;
consider p such that A22: o,z,p is_collinear & a2,a3,p is_collinear by ANPROJ_2
:def 14;
consider q such that A23: o,a1,q is_collinear & p,c3,q is_collinear by ANPROJ_2
:def 14;
consider r such that A24: p,b2,r is_collinear & q,a3,r is_collinear by ANPROJ_2
:def 14;
consider a such that A25: c1,c3,a is_collinear & o,a2,a is_collinear by
ANPROJ_2:def 14;
consider q' such that A26: o,a1,q' is_collinear & a,a3,q' is_collinear by
ANPROJ_2:def 14;
consider z' be Element of PCPP such that
A27: b1,r,z' is_collinear & o,p,z' is_collinear by ANPROJ_2:def 14;
consider z'' be Element of PCPP such that
A28: b3,r,z'' is_collinear & o,p,z'' is_collinear by ANPROJ_2:def 14;
A29: a1<>c3 & a2<>c3 & a2<>c1 & a3<>c1 & c1<>c3 proof
A30: a1<>c3 proof not o,a2,a1 is_collinear & a2,a1,c3 is_collinear &
b2,b1,c3 is_collinear by A2,A4,Th3; hence thesis by A1,A5,Th10; end;
not o,a3,a2 is_collinear & b3,b2,c1 is_collinear & a3,a2,c1 is_collinear
by A2,A4,Th3; hence thesis by A1,A2,A3,A4,A5,A30,Th10,ANPROJ_2:def 7; end;
A31: o<>p by A2,A22,Th3;
A32: a<>c1
proof
not a2,a3,o is_collinear by A2,Th3;
then not a2,c1,o is_collinear by A4,A29,Th8;hence thesis by A25,Th3; end;
A33: o<>a & a2<>a & o<>a2 & a1<>a3 & a1<>z & a3<>z proof
A34: a2<>c3 by A1,A2,A4,A5,Th10;
A35: c1<>c3 by A3,ANPROJ_2:def 7;
not o,a3,a2 is_collinear & b3,b2,c1 is_collinear & a3,a2,c1 is_collinear
by A2,A4,Th3; then A36:a2<>c1 by A1,A5,Th10;
A37: a2<>a
proof
assume A38:not thesis;
then c3,a2,c1 is_collinear & c3,a2,a1 is_collinear & c1,a2,c3 is_collinear
& c1,a2,a3 is_collinear by A4,A25,Th3;
then c3,c1,a1 is_collinear & c1,c3,a3 is_collinear by A34,A36,Th4;
then c1,c3,a1 is_collinear & c1,c3,a3 is_collinear by Th3;
hence contradiction by A18,A25,A35,A38,ANPROJ_2:def 8;
end;
not o,a2,a1 is_collinear & a2,a1,c3 is_collinear &
b2,b1,c3 is_collinear by A2,A4,Th3;
then A39: a1<>c3 by A1,A5,Th10;
a3<>c1 by A1,A2,A4,A5,Th10;
hence thesis by A2,A3,A4,A18,A21,A25,A34,A36,A37,A39,Th3,Th12,ANPROJ_2:def 7
;
end;
not a1,a2,o is_collinear by A2,Th3;
then not a1,c3,o is_collinear by A4,A29,Th8;
then A40: not o,a1,c3 is_collinear by Th3;
a2,b2,o is_collinear by A5,Th3;
then A41: not b1,o,b2 is_collinear by A1,A2,A5,Th16;
then A42: not o,b1,b2 is_collinear by Th3;
A43: not o,a,a3 is_collinear by A2,A25,A33,Th8;
A44: b1<>b2 & b1<>p & b2<>p proof A45: b1<>p proof not a1,a3,o is_collinear
by A2,Th3; then not a1,z,o is_collinear by A21,A33,Th8;
then not o,z,a1 is_collinear by Th3; then not o,p,a1 is_collinear by A22,A31,
Th8;
hence thesis by A5,Th3; end;
a2,o,b2 is_collinear & not a2,o,a3 is_collinear by A2,A5,Th3;
then not a2,b2,a3 is_collinear by A1,Th8;
hence thesis by A18,A22,A45,Th3,ANPROJ_2:def 7;end;
not a2,a1,o is_collinear & a2,a1,c3 is_collinear by A2,A4,Th3;
then not a2,c3,o is_collinear by A29,Th8;
then A46: a<>c3 by A25,Th3;
A47: a3,a,q is_collinear proof A48: a3,z,a1 is_collinear & a3,a2,p is_collinear
by A21,A22,Th3; A49: a2,a1,c3 is_collinear by A4,Th3; a,z,c3 is_collinear
proof A50:c3,c1,z is_collinear & c3,c1,a is_collinear by A21,A25,Th3; c1<>c3
by A3,ANPROJ_2:def 7; then c3,a,z is_collinear by A50,Th4; hence thesis by Th3
;end;
then c3,q',p is_collinear by A2,A22,A25,A26,A33,A48,A49,Th20;
then A51: p,c3,q' is_collinear by Th3;
not a2,a1,a3 is_collinear & a2,a1,c3 is_collinear &
a2<>c3 by A4,A18,A29,Th3; then not a2,c3,a3 is_collinear by Th8;
then A52: p<>c3 by A22,Th3;
not a1,a3,o is_collinear & a1,a3,z is_collinear & a1<>z
by A2,A21,A33,Th3;
then not a1,z,o is_collinear by Th8;
then not o,z,a1 is_collinear by Th3;
then not o,p,a1 is_collinear by A22,A31,Th8;
then not o,a1,p is_collinear by Th3;
then a,a3,q is_collinear by A8,A23,A26,A51,A52,Th17;
hence thesis by Th3; end;
A53: not a3,q,o is_collinear proof not a3,a,o is_collinear by A43,Th3;
hence thesis by A2,A23,A47,Th8;end;
A54: not o,b2,b3 is_collinear proof a3,b3,o is_collinear by A5,Th3;
then not b2,o,b3 is_collinear by A1,A2,A5,Th16; hence thesis by Th3; end;
A55: b2<>c1 & b2<>c3 proof A56: o,b1,a1 is_collinear & o,b2,a2 is_collinear
by A5,Th3;
A57: o,b2,a2 is_collinear & o,b3,a3 is_collinear by A5,Th3;
A58: not o,b3,b2 is_collinear by A54,Th3; b3,b2,c1 is_collinear &
a3,a2,c1 is_collinear by A4,Th3;
hence thesis by A1,A4,A8,A42,A56,A57,A58,Th10; end;
A59: a<>b2 proof assume A60:not thesis;
then A61: c1,b2,c3 is_collinear by A25,Th3;
c1,b2,b3 is_collinear by A4,Th3;
then A62: c1,c3,b3 is_collinear by A55,A61,Th4; A63: c3,b2,b1 is_collinear
by A4,Th3; c3,b2,c1 is_collinear by A25,A60,Th3; then c3,c1,b1
is_collinear
by A55,A63,Th4; then c1,c3,b1 is_collinear by Th3;hence contradiction by A18,
A25,A29,A60,A62,ANPROJ_2:def 8; end;
A64: not a,b2,a3 is_collinear proof A65: not a,o,a3 is_collinear by A43,Th3;
o,a,b2 is_collinear by A5,A8,A25,Th4; then a,o,b2 is_collinear by Th3;
hence thesis by A59,A65,Th8; end;
A66: a3,r,a is_collinear proof a3,q,a is_collinear & a3,q,r is_collinear
by A24,A47,Th3; hence thesis by A2,A23,Th4;end;
then A67: b2<>r by A64,Th3;
A68: a<>a2 proof assume A69:not thesis;
then c1,a2,c3 is_collinear & c1,a2,a3 is_collinear by A4,A25,Th3;
then A70: c1,c3,a3 is_collinear by A29,Th4; c3,a2,a1 is_collinear &
c3,a2,c1 is_collinear by A4,A25,A69,Th3; then c3,c1,a1 is_collinear
by A29,Th4; then c1,c3,a1 is_collinear by Th3;hence contradiction by A18,A25,
A29,A69,A70,ANPROJ_2:def 8; end;
A71: not a3,o,b2 is_collinear proof not o,b2,a3 is_collinear
by A1,A2,A5,Th8; hence thesis by Th3;end;
thus contradiction proof
A72: not p,o,a is_collinear proof
o<>x by A2,A6,Th3; then not o,x,a3 is_collinear by A2,A6,Th8;
then A73: not x,a3,o is_collinear by Th3; a3,a1,z is_collinear &
a3,a1,x is_collinear by A6,A21,Th3; then a3,x,z is_collinear by A33,Th4;
then x,a3,z is_collinear by Th3;
then not x,z,o is_collinear by A7,A21,A73,Th8;
then not o,z,x is_collinear by Th3; then not o,p,x is_collinear by A22,A31,Th8;
then A74: not o,x,p is_collinear by Th3; o,x,a is_collinear by A6,A8,A25,Th4;
then not o,a,p is_collinear by A33,A74,Th8; hence thesis by Th3; end;
A75: a3<>p proof assume not thesis;
then A76: a3,o,z is_collinear by A22,Th3; a3,a1,z is_collinear &
not a3,o,a1 is_collinear by A2,A21,Th3; hence
contradiction by A33,A76,Th9; end;
A77: not a,a3,p is_collinear proof not a,o,p is_collinear &
a,o,a2 is_collinear by A25,A72,Th3; then not a,a2,p is_collinear by A68,Th8;
then A78: not p,a2,a is_collinear by Th3; p,a2,a3 is_collinear by A22,Th3;
then not p,a3,a is_collinear by A75,A78,Th8; hence thesis by Th3;end;
then A79: p<>r by A66,Th3;
A80: z<>r proof A81: o,a,b2 is_collinear by A5,A8,A25,Th4;
not o,a,p is_collinear by A72,Th3;
then not o,b2,p is_collinear by A1,A81,Th8;
then not p,b2,o is_collinear by Th3;
then not p,r,o is_collinear by A24,A79,Th8;
hence thesis by A22,Th3; end; A82: now assume A83: b1=q;
consider z' be Element of PCPP such that
A84: b1,b3,z' is_collinear & p,o,z' is_collinear by ANPROJ_2:def 14;
b1,c3,p is_collinear & b1,c3,b2 is_collinear by A4,A23,A83,Th3;
then A85: b1,b2,p is_collinear by A5,A40,Th4;
A86: not b1,b2,o is_collinear proof not o,a1,a2 is_collinear &
o,a1,b1 is_collinear & a2,b2,o is_collinear & o<>b1 & o<>b2 by A1,A2,A5,Th3;
then not b1,o,b2 is_collinear by Th16;
hence thesis by Th3; end;
b1,a3,a is_collinear & o,b2,a is_collinear & b1,b3,z' is_collinear &
p,o,z' is_collinear & b2,b3,c1 is_collinear & p,a3,c1 is_collinear
proof
a3,a2,c1 is_collinear & a3,a2,p is_collinear by A4,A22,Th3;
then a3,c1,p is_collinear by A8,Th4;
hence thesis by A4,A5,A25,A33,A47,A83,A84,Th3,Th4;
end;
then c1,z',a is_collinear by A1,A5,A8,A44,A85,A86,Th20;
then A87: a,c1,z' is_collinear by Th3;
c1,a,z is_collinear by A21,A25,A29,Th4;
then A88: a,c1,z is_collinear by Th3;
p,o,z is_collinear by A22,Th3;
then A89: b1,b3,z is_collinear by A31,A32,A72,A84,A87,A88,Th17;
A90: not a1,o,a3 is_collinear by A2,Th3;
a1,o,b1 is_collinear by A5,Th3;
then not a1,b1,a3 is_collinear by A1,A90,Th8;
then not a1,a3,b1 is_collinear by Th3;
then c1,c3,c2 is_collinear by A4,A8,A20,A21,A89,Th17;
hence contradiction by A19,Th3; end;
now assume A91: b1<>q;
A92: q<>o & b1<>o & b2<>p & b2<>r & p<>r by A1,A44,A53,A64,A66,A77,Th3,ANPROJ_2
:def 7;
A93: not q,b1,b2 is_collinear proof o,b1,q is_collinear by A5,A8,A23,Th4;
then b1,o,q is_collinear by Th3;
then not b1,q,b2 is_collinear by A41,A91,Th8; hence thesis by Th3; end;
A94: q,b1,o is_collinear & b2,p,r is_collinear proof o,b1,q is_collinear
by A5,A8,A23,Th4; hence thesis by A24,Th3; end;
q,p,c3 is_collinear & b2,b1,c3 is_collinear & q,r,a is_collinear &
o,b2,a is_collinear & b1,r,z' is_collinear & o,p,z' is_collinear proof
q,r,a is_collinear proof q,a3,a is_collinear & q,a3,r is_collinear
by A24,A47,Th3; hence thesis by A2,A23,Th4; end;
hence thesis by A4,A5,A8,A23,A25,A27,Th3,Th4; end;
then A95: z',a,c3 is_collinear by A92,A93,A94,Th20;
c3,c1,z is_collinear & c3,c1,a is_collinear by A21,A25,Th3;
then c3,z,a is_collinear by A29,Th4;
then A96: a,c3,z is_collinear by Th3;
A97: a,c3,z' is_collinear by A95,Th3;
A98: o,p,z is_collinear by A22,Th3;
not o,p,a is_collinear by A72,Th3;
then A99: b1,r,z is_collinear by A27,A31,A46,A96,A97,A98,Th17;
A100: a3,o,b3 is_collinear by A5,Th3; A101: b2,r,p is_collinear by A24,Th3;
o,a,b2 is_collinear by A5,A8,A25,Th4;
then A102: b2,o,a is_collinear by Th3;
a3,a2,c1 is_collinear & a3,a2,p is_collinear by A4,A22,Th3;
then A103: a3,p,c1 is_collinear by A8,Th4;
b3,b2,c1 is_collinear by A4,Th3;
then z'',c1,a is_collinear
by A1,A28,A44,A66,A67,A71,A79,A100,A101,A102,A103,Th20;
then c1,a,z'' is_collinear & c1,a,c3 is_collinear by A25,Th3;
then A104: c1,c3,z'' is_collinear by A32,Th4;
A105: not c1,c3,o is_collinear by A3,Th3;
o,p,z is_collinear by A22,Th3;
then b3,r,z is_collinear by A21,A28,A29,A31,A104,A105,Th17;
then z,r,b1 is_collinear & z,r,b3 is_collinear by A99,Th3;
then z,b1,b3 is_collinear by A80,Th4;
then b1,b3,z is_collinear by Th3;
then c1,c3,c2 is_collinear by A4,A8,A9,A20,A21,Th17;
hence contradiction by A19,Th3; end; hence contradiction by A82; end;
end; hence thesis by A11; end;
Lm3:
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
proof assume that A1: o<>b1 & a1<>b1 & o<>b2 & a2<>b2 & o<>b3 & a3<>b3 and
A2: not o,a1,a2 is_collinear & not o,a1,a3 is_collinear &
not o,a2,a3 is_collinear and
A3: not o,c1,c3 is_collinear and
A4: 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 and
A5: o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear;
A6: o<>a1 & o<>a2 & a1<>a2 & o<>a3 & a1<>a3 & a2<>a3 by A2,ANPROJ_2:def 7;
now assume A7: not a1,a2,a3 is_collinear & not b1,b2,b3 is_collinear;
consider x such that A8: a1,a3,x is_collinear & o,a2,x is_collinear by ANPROJ_2
:def 14;
consider y such that A9: b1,b3,y is_collinear & o,a2,y is_collinear by ANPROJ_2
:def 14;
consider a such that A10: o,a2,a is_collinear & c1,c3,a is_collinear by
ANPROJ_2:def 14;
consider z such that A11: a1,a3,z is_collinear & c1,c3,z is_collinear by
ANPROJ_2:def 14;
assume A12: not thesis;
A13: now assume A14: c1,c3,x is_collinear & c1,c3,y is_collinear;
thus contradiction proof
A15: a1<>c3 & a2<>c3 & a2<>c1 & a3<>c1 & c1<>c3 proof
A16: a1<>c3 proof not o,a2,a1 is_collinear & a2,a1,c3 is_collinear &
b2,b1,c3 is_collinear by A2,A4,Th3; hence thesis by A1,A5,Th10; end;
not o,a3,a2 is_collinear & b3,b2,c1 is_collinear & a3,a2,c1 is_collinear
by A2,A4,Th3;hence thesis by A1,A2,A3,A4,A5,A16,Th10,ANPROJ_2:def 7; end;
A17: o<>a & a2<>a & o<>a2 & a1<>a3 & a1<>z & a3<>z proof
A18: a2<>c3 by A1,A2,A4,A5,Th10; A19: c1<>c3 by A3,ANPROJ_2:def 7;
not o,a3,a2 is_collinear & b3,b2,c1 is_collinear & a3,a2,c1 is_collinear
by A2,A4,Th3; then A20:a2<>c1 by A1,A5,Th10;
A21: a2<>a proof assume A22:not thesis; then c3,a2,c1 is_collinear &
c3,a2,a1 is_collinear & c1,a2,c3 is_collinear & c1,a2,a3 is_collinear by A4,
A10,Th3
; then c3,c1,a1 is_collinear & c1,c3,a3 is_collinear by A18,A20,Th4;
then c1,c3,a1 is_collinear & c1,c3,a3 is_collinear by Th3;
hence contradiction by A7,A10,A19,A22,ANPROJ_2:def 8; end;
A23: a1<>c3 proof not o,a2,a1 is_collinear & a2,a1,c3 is_collinear &
b2,b1,c3 is_collinear by A2,A4,Th3; hence thesis by A1,A5,Th10; end;
a3<>c1 by A1,A2,A4,A5,Th10;
hence thesis by A2,A3,A4,A7,A10,A11,A18,A20,A21,A23,Th3,Th12,ANPROJ_2:def 7;
end;
A24: not o,a2,c1 is_collinear proof not a2,a3,o is_collinear &
a2,a3,c1 is_collinear & a2<>c1 by A2,A4,A15,Th3;
then not a2,c1,o is_collinear by Th8; hence thesis by Th3;end;
A25: b1<>b2 & b1<>b3 & b2<>b3 by A1,A2,A5,Th9;
A26: b1,b3,x is_collinear by A8,A9,A14,A15,A17,A24,Th17
; not a1,o,a3 is_collinear
& a1,o,b1 is_collinear & a1<>b1 by A1,A2,A5,Th3;
then not a1,b1,a3 is_collinear by Th8; then not a1,a3,b1 is_collinear by Th3;
then c1,c3,c2 is_collinear by A4,A6,A8,A14,A25,A26,Th17; hence
contradiction by A12,Th3; end; end;
now assume A27: not c1,c3,x is_collinear or not c1,c3,y is_collinear;
now assume A28: not c1,c3,y is_collinear;
A29: o,b2,y is_collinear by A5,A6,A9,Th4;
A30: o,b1,a1 is_collinear & o,b2,a2 is_collinear & o,b3,a3 is_collinear
by A5,Th3;
not o,b1,b2 is_collinear & not o,b2,b3 is_collinear
& not o,b1,b3 is_collinear by A1,A2,A5,Th19;
hence contradiction by A1,A3,A4,A6,A9,A12,A28,A29,A30,Lm2; end;
hence thesis by A1,A2,A3,A4,A5,A8,A27,Lm2; end;
hence thesis by A13; end;
hence thesis by A1,A2,A3,A4,A5,Lm1; end;
theorem Th21:
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 & 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
proof
assume A1: 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
& 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;
then A2: not o,a3,a2 is_collinear by Th3;
A3: a3,a2,c1 is_collinear & b3,b2,c1 is_collinear by A1,Th3;
A4: o<>c1 by A1,Th3;
now assume A5: o,c1,c3 is_collinear;
assume A6:not thesis;
then A7:not c1,c3,c2 is_collinear by Th3; c1,c3,o is_collinear & c1<>c3
by A5,A6,Th3,ANPROJ_2:def 7;
then not c1,o,c2 is_collinear by A4,A7,Th8;
then not o,c1,c2 is_collinear by Th3;
hence contradiction by A1,A2,A3,A7,Lm3;
end;
hence thesis by A1,Lm3;
end;
definition
cluster Pappian -> Desarguesian CollProjectiveSpace;
coherence
proof let PCPP be CollProjectiveSpace such that
A1: PCPP is Pappian;
A2: now assume ex p,p1,q,q1 being Element of PCPP st
not ex r being Element of PCPP st
p,p1,r is_collinear & q,q1,r is_collinear;
then PCPP is up-3-dimensional CollProjectiveSpace by ANPROJ_2:def 14;
hence thesis;
end;
now assume not ex p,p1,q,q1 being Element of PCPP st
not ex r being Element of PCPP st
p,p1,r is_collinear & q,q1,r is_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 is_collinear & not o,p1,p3 is_collinear &
not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear &
p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear &
q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear &
o,p3,q3 is_collinear holds r1,r2,r3 is_collinear by Th21;
hence PCPP is Desarguesian by ANPROJ_2:def 12;
end;
hence thesis by A2;
end;
end;