Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ANALMETR, DIRAF, ANALOAF, SYMSP_1, CONAFFM;
notation SUBSET_1, STRUCT_0, ANALOAF, AFF_1, ANALMETR;
constructors AFF_1, ANALMETR, XBOOLE_0;
clusters ANALMETR, ZFMISC_1, XBOOLE_0;
theorems AFF_1, ANALMETR, DIRAF;
begin
reserve X for OrtAfPl;
reserve o,a,a1,a2,b,b1,b2,c,c1,c2,d,e1,e2
for Element of X;
reserve b2',c2',d1'
for Element of Af(X);
definition let X;
attr X is satisfying_DES means
for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 &
not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 &
LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1;
synonym DES_holds_in X;
attr X is satisfying_AH means
for o,a,a1,b,b1,c,c1 st o,a _|_ o,a1 & o,b _|_ o,b1
& o,c _|_ o,c1 & a,b _|_ a1,b1 & o,a // b,c &
a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1;
synonym AH_holds_in X;
attr X is satisfying_3H means
for a,b,c st not LIN a,b,c holds (ex d st d,a _|_ b,c & d,b _|_ a,c &
d,c _|_ a,b);
synonym 3H_holds_in X;
attr X is satisfying_ODES means :Def4:
for o,a,a1,b,b1,c,c1 st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 &
a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b
holds b,c _|_ b1,c1;
synonym ODES_holds_in X;
attr X is satisfying_LIN means :Def5:
for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c &
o<>c1 & a<>b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 &
not LIN o,c,a & LIN o,a,b & LIN
o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1
holds a,a1 // b,b1;
synonym LIN_holds_in X;
attr X is satisfying_LIN1 means :Def6:
for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c &
o<>c1 & a<>b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 &
not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1
holds b,c _|_ b1,c1;
synonym LIN1_holds_in X;
attr X is satisfying_LIN2 means
for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c &
o<>c1 & a<>b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 &
not LIN o,c,a & LIN o,a,b & LIN
o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1
holds o,c _|_ o,c1;
synonym LIN2_holds_in X;
end;
theorem ODES_holds_in X implies DES_holds_in X
proof
assume A1:ODES_holds_in X;
let o,a,a1,b,b1,c,c1;
assume A2:o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & not LIN b,b1,a
& not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 &
a,b // a1,b1 & a,c // a1,c1;
consider a2 such that A3:o,a _|_ o,a2 & o<>a2 by ANALMETR:def 10;
consider e1 such that A4:o,b _|_ o,e1 & o<>e1 by ANALMETR:def 10;
consider e2 such that A5:a,b _|_ a2,e2 & a2<>e2 by ANALMETR:def 10;
reconsider o'=o,a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1,a2'=a2,e1'=e1,e2'=e2
as Element of Af(X) by ANALMETR:47;
not o',e1' // a2',e2'
proof assume o',e1' // a2',e2';
then o,e1 // a2,e2 by ANALMETR:48;
then a2,e2 _|_ o,b by A4,ANALMETR:84;
then a,b // o,b by A5,ANALMETR:85;
then A6: a',b' // o',b' by ANALMETR:48;
then b',a' // b',o' by AFF_1:13;
then A7:LIN b',a',o' by AFF_1:def 1;
o',b' // b',a' by A6,AFF_1:13;
then A8:o,b // b,a by ANALMETR:48;
A9:b'<>a'
proof assume b'=a';
then LIN b',b1',a' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
o,b // o,b1 by A2,ANALMETR:def 11;
then b,a // o,b1 by A2,A8,ANALMETR:82;
then b',a' // o',b1' by ANALMETR:48;
then LIN b',a',b1' by A7,A9,AFF_1:18;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then consider b2' such that A10:LIN o',e1',b2' & LIN a2',e2',b2'
by AFF_1:74;
reconsider b2=b2' as Element of X by ANALMETR:47;
A11:o,b _|_ o,b2
proof LIN o,e1,b2 by A10,ANALMETR:55;
then o,e1 // o,b2 by ANALMETR:def 11;
hence thesis by A4,ANALMETR:84;end;
A12:a,b _|_ a2,b2
proof LIN a2,e2,b2 by A10,ANALMETR:55;
then a2,e2 // a2,b2 by ANALMETR:def 11;
hence thesis by A5,ANALMETR:84;end;
consider e1 such that A13:o,c _|_ o,e1 & o<>e1 by ANALMETR:def 10;
consider e2 such that A14:a,c _|_ a2,e2 & a2<>e2 by ANALMETR:def 10;
reconsider e1'=e1,e2'=e2 as Element of Af(X) by ANALMETR:47;
not o',e1' // a2',e2'
proof assume o',e1' // a2',e2';
then o,e1 // a2,e2 by ANALMETR:48;
then o,c _|_ a2,e2 by A13,ANALMETR:84;
then o,c // a,c by A14,ANALMETR:85;
then c,o // c,a by ANALMETR:81;
then LIN c,o,a by ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN a',c',o' by AFF_1:15;
then LIN a,c,o by ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A15:o,a // a,c by ANALMETR:81;
LIN o',a',a1' by A2,ANALMETR:55;
then LIN a',o',a1' by AFF_1:15;
then LIN a,o,a1 by ANALMETR:55;
then a,o // a,a1 by ANALMETR:def 11;
then o,a // a,a1 by ANALMETR:81;
then a,a1 // a,c by A2,A15,ANALMETR:82;
hence contradiction by A2,ANALMETR:def 11;end;
then consider c2' such that A16:LIN o',e1',c2' & LIN
a2',e2',c2' by AFF_1:74;
reconsider c2=c2' as Element of X by ANALMETR:47;
A17:o,c _|_ o,c2
proof LIN o,e1,c2 by A16,ANALMETR:55;
then o,e1 // o,c2 by ANALMETR:def 11;
hence thesis by A13,ANALMETR:84;end;
A18:a,c _|_ a2,c2
proof LIN a2,e2,c2 by A16,ANALMETR:55;
then a2,e2 // a2,c2 by ANALMETR:def 11;
hence thesis by A14,ANALMETR:84;end;
A19:not o,c // o,a
proof assume o,c // o,a;
then LIN o,c,a by ANALMETR:def 11;
then LIN o',c',a' by ANALMETR:55;
then LIN a',o',c' by AFF_1:15;
then LIN a,o,c by ANALMETR:55;
then A20:a,o // a,c by ANALMETR:def 11;
LIN o',a',a1' by A2,ANALMETR:55;
then LIN a',o',a1' by AFF_1:15;
then LIN a,o,a1 by ANALMETR:55;
then a,o // a,a1 by ANALMETR:def 11;
then a,a1 // a,c by A2,A20,ANALMETR:82;
hence contradiction by A2,ANALMETR:def 11;end;
not o,a // o,b
proof assume o,a // o,b;
then LIN o,a,b by ANALMETR:def 11;
then LIN o',a',b' by ANALMETR:55;
then LIN b',o',a' by AFF_1:15;
then LIN b,o,a by ANALMETR:55;
then A21:b,o // b,a by ANALMETR:def 11;
LIN o',b',b1' by A2,ANALMETR:55;
then LIN b',o',b1' by AFF_1:15;
then LIN b,o,b1 by ANALMETR:55;
then b,o // b,b1 by ANALMETR:def 11;
then b,b1 // b,a by A2,A21,ANALMETR:82;
hence contradiction by A2,ANALMETR:def 11;end;
then A22:b,c _|_ b2,c2 by A1,A3,A11,A12,A17,A18,A19,Def4;
A23:o,a1 _|_ o,a2
proof
o,a // o,a1 by A2,ANALMETR:def 11;
hence thesis by A2,A3,ANALMETR:84;end;
A24:o,b1 _|_ o,b2
proof
o,b // o,b1 by A2,ANALMETR:def 11;
hence thesis by A2,A11,ANALMETR:84;end;
A25:o,c1 _|_ o,c2
proof
o,c // o,c1 by A2,ANALMETR:def 11;
hence thesis by A2,A17,ANALMETR:84;end;
A26:a1,b1 _|_ a2,b2
proof
a<>b
proof assume a=b;
then LIN b',b1',a' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
hence thesis by A2,A12,ANALMETR:84;end;
A27:a1,c1 _|_ a2,c2
proof
a<>c
proof assume a= c;
then LIN a',a1',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
hence thesis by A2,A18,ANALMETR:84;end;
A28:not o,c1 // o,a1
proof assume o,c1 // o,a1;
then LIN o,c1,a1 by ANALMETR:def 11;
then LIN o',c1',a1' by ANALMETR:55;
then LIN a1',o',c1' by AFF_1:15;
then LIN a1,o,c1 by ANALMETR:55;
then A29:a1,o // a1,c1 by ANALMETR:def 11;
A30:a1<> c1
proof assume a1 = c1;
then LIN o',c',a1' by A2,ANALMETR:55;
then LIN a1',c',o' by AFF_1:15;
then LIN a1,c,o by ANALMETR:55;
then A31:a1,c // a1,o by ANALMETR:def 11;
LIN o',a',a1' by A2,ANALMETR:55;
then LIN a1',o',a' by AFF_1:15;
then LIN a1,o,a by ANALMETR:55;
then a1,o // a1,a by ANALMETR:def 11;
then a1,c // a1,a by A2,A31,ANALMETR:82;
then LIN a1,c,a by ANALMETR:def 11;
then LIN a1',c',a' by ANALMETR:55;
then LIN a',a1',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
LIN o',a',a1' by A2,ANALMETR:55;
then LIN a1',o',a' by AFF_1:15;
then LIN a1,o,a by ANALMETR:55;
then a1,o // a1,a by ANALMETR:def 11;
then a1,c1 // a1,a by A2,A29,ANALMETR:82;
then a1,a // a,c by A2,A30,ANALMETR:82;
then a,a1 // a,c by ANALMETR:81;
hence contradiction by A2,ANALMETR:def 11;end;
not o,a1 // o,b1
proof assume o,a1 // o,b1;
then LIN o,a1,b1 by ANALMETR:def 11;
then LIN o',a1',b1' by ANALMETR:55;
then LIN b1',a1',o' by AFF_1:15;
then LIN b1,a1,o by ANALMETR:55;
then A32:b1,a1 // b1,o by ANALMETR:def 11;
A33:a1<>b1
proof assume a1=b1;
then LIN o',a',b1' by A2,ANALMETR:55;
then LIN b1',o',a' by AFF_1:15;
then LIN b1,o,a by ANALMETR:55;
then A34:b1,o // b1,a by ANALMETR:def 11;
LIN o',b',b1' by A2,ANALMETR:55;
then LIN b1',b',o' by AFF_1:15;
then LIN b1,b,o by ANALMETR:55;
then b1,b // b1,o by ANALMETR:def 11;
then b1,a // b1,b by A2,A34,ANALMETR:82;
then LIN b1,a,b by ANALMETR:def 11;
then LIN b1',a',b' by ANALMETR:55;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A35:b1,a1 // a,b by A2,ANALMETR:81;
LIN o',b',b1' by A2,ANALMETR:55;
then LIN b1',b',o' by AFF_1:15;
then LIN b1,b,o by ANALMETR:55;
then b1,b // b1,o by ANALMETR:def 11;
then b1,a1 // b1,b by A2,A32,ANALMETR:82;
then b1,b // a,b by A33,A35,ANALMETR:82;
then b,b1 // b,a by ANALMETR:81;
hence contradiction by A2,ANALMETR:def 11;end;
then A36:b1,c1 _|_ b2,c2 by A1,A23,A24,A25,A26,A27,A28,Def4;
A37:now assume A38:not LIN o,b,c;
b2<>c2
proof assume A39: b2 = c2;
o<>b2
proof assume A40: o=b2;
a2,o _|_ a,o by A3,ANALMETR:83;
then a,o // a,b by A3,A12,A40,ANALMETR:85;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN b',o',a' by AFF_1:15;
then LIN b,o,a by ANALMETR:55;
then A41:b,o // b,a by ANALMETR:def 11;
LIN o',b',b1' by A2,ANALMETR:55;
then LIN b',o',b1' by AFF_1:15;
then LIN b,o,b1 by ANALMETR:55;
then b,o // b,b1 by ANALMETR:def 11;
then b,b1 // b,a by A2,A41,ANALMETR:82;
hence contradiction by A2,ANALMETR:def 11;end;
then o,b // o,c by A11,A17,A39,ANALMETR:85;
hence contradiction by A38,ANALMETR:def 11;end;
hence thesis by A22,A36,ANALMETR:85;end;
now assume A42:LIN o,b,c;
now A43:LIN b',c',b1'
proof LIN o',b',c' by A42,ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then A44:b',o' // b',c' by AFF_1:def 1;
LIN o',b',b1' by A2,ANALMETR:55;
then LIN b',o',b1' by AFF_1:15;
then b',o' // b',b1' by AFF_1:def 1;
then b',c' // b',b1' by A2,A44,AFF_1:14;
hence thesis by AFF_1:def 1;end;
LIN b',c',c1'
proof LIN o',b',c' by A42,ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then A45:c',o' // c',b' by AFF_1:def 1;
LIN o',c',c1' by A2,ANALMETR:55;
then LIN c',o',c1' by AFF_1:15;
then c',o' // c',c1' by AFF_1:def 1;
then c',b' // c',c1' by A2,A45,AFF_1:14;
then LIN c',b',c1' by AFF_1:def 1;
hence thesis by AFF_1:15;end;
then b',c' // b1',c1' by A43,AFF_1:19;
hence thesis by ANALMETR:48;end;
hence thesis;end;
hence thesis by A37;end;
theorem ODES_holds_in X implies AH_holds_in X
proof
assume A1: ODES_holds_in X;
let o,a,a1,b,b1,c,c1;
assume o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 &
o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b;
hence b,c _|_ b1,c1 by A1,Def4;
end;
theorem Th3: LIN_holds_in X implies LIN1_holds_in X
proof
assume A1: LIN_holds_in X;
let o,a,a1,b,b1,c,c1;
assume A2: o<>a & o<>a1 & o<>b & o<>b1 & o<>c &
o<>c1 & a<>b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 &
not LIN o,c,a & LIN o,a,b & LIN
o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1;
reconsider a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1,o'=o
as Element of Af(X) by ANALMETR:47;
now ex b2 st LIN o,a1,b2 & c1,b2 _|_ b,c & c1<>b2
proof
consider y be Element of X such that
A3: o,a1 // o,y & o<>y by ANALMETR:51;
consider x be Element of X such that
A4: b,c _|_ c1,x & c1<>x by ANALMETR:51;
A5: not o,y // c1,x
proof
assume A6: o,y // c1,x;
reconsider y'=y,x'=x as Element of the carrier
of Af(X) by ANALMETR:47;
A7: o',y' // c1',x' by A6,ANALMETR:48;
o',a1' // o',y' & o'<>y' by A3,ANALMETR:48;
then o',y' // o',a1' & o'<>y' by AFF_1:13;
then c1',x' // o',a1' by A7,DIRAF:47;
then c1,x // o,a1 by ANALMETR:48;
then o,a1 _|_ b,c by A4,ANALMETR:84;
then A8: o,a // b,c by A2,ANALMETR:85;
o,a // o,b by A2,ANALMETR:def 11;
then b,c // o,b by A2,A8,ANALMETR:82;
then b',c' // o',b' by ANALMETR:48;
then b',c' // b',o' by AFF_1:13;
then LIN b',c',o' by AFF_1:def 1;
then LIN o',b',c' by AFF_1:15;
then A9: o',b' // o',c' by AFF_1:def 1;
LIN o',a',b' & o'<>b' by A2,ANALMETR:55;
then LIN o',b',a' & o'<>b' by AFF_1:15;
then o',b' // o',a' & o'<>b' by AFF_1:def 1;
then o',c' // o',a' by A9,DIRAF:47;
then LIN o',c',a' by AFF_1:def 1;
hence contradiction by A2,ANALMETR:55; end;
reconsider y'=y,x'=x as Element of the carrier
of Af(X) by ANALMETR:47;
not o',y' // c1',x' by A5,ANALMETR:48;
then consider b2' be Element of Af(X) such
that A10: LIN o',y',b2' & LIN c1',x',b2' by AFF_1:74;
reconsider b2=b2' as Element of X by ANALMETR:47;
LIN c1,x,b2 by A10,ANALMETR:55;
then c1,x // c1,b2 by ANALMETR:def 11;
then A11: c1,b2 _|_ b,c by A4,ANALMETR:84;
o',a1' // o',y' & o'<>y' by A3,ANALMETR:48;
then A12: o',y' // o',a1' & o'<>y' by AFF_1:13;
o',y' // o',b2' by A10,AFF_1:def 1;
then o',a1' // o',b2' by A12,DIRAF:47;
then LIN o',a1',b2' by AFF_1:def 1;
then A13: LIN o,a1,b2 by ANALMETR:55;
c1<>b2
proof
assume c1=b2;
then o,a1 // o,c1 by A13,ANALMETR:def 11;
then o,c1 _|_ o,a by A2,ANALMETR:84;
then o,c // o,a by A2,ANALMETR:85;
hence contradiction by A2,ANALMETR:def 11; end;
hence thesis by A11,A13;end;
then consider b2 such that A14: LIN o,a1,b2 & c1,b2 _|_ b,c & c1<>b2;
reconsider b2'=b2 as Element of Af(X) by ANALMETR:47;
A15: o,b _|_ o,b2 & o<>b2
proof
A16: o,b _|_ o,b2
proof
o,a1 // o,b2 by A14,ANALMETR:def 11;
then A17: o,a _|_ o,b2 by A2,ANALMETR:84;
o,a // o,b by A2,ANALMETR:def 11;
hence thesis by A2,A17,ANALMETR:84;end;
o<>b2
proof
assume o=b2;
then o,c1 _|_ b,c by A14,ANALMETR:83;
then o,c // b,c by A2,ANALMETR:85;
then o',c' // b',c' by ANALMETR:48;
then c',o' // c',b' by AFF_1:13;
then LIN c',o',b' by AFF_1:def 1;
then LIN o',b',c' by AFF_1:15;
then A18: o',b' // o',c' by AFF_1:def 1;
LIN o',a',b' & o'<>b' by A2,ANALMETR:55;
then LIN o',b',a' & o'<>b' by AFF_1:15;
then o',b' // o',a' & o'<>b' by AFF_1:def 1;
then o',c' // o',a' by A18,DIRAF:47;
then LIN o',c',a' by AFF_1:def 1;
hence contradiction by A2,ANALMETR:55;end;
hence thesis by A16;end;
b,c _|_ b2,c1 by A14,ANALMETR:83;
then A19: a,a1 // b,b2 by A1,A2,A14,A15,Def5;
b1=b2
proof
not LIN o,a,a1
proof
assume LIN o,a,a1;
then o,a // o,a1 by ANALMETR:def 11;
then o,a1 _|_ o,a1 by A2,ANALMETR:84;
hence contradiction by A2,ANALMETR:51;end;
then A20: not LIN o',a',a1' by ANALMETR:55;
A21: LIN o',a',b' by A2,ANALMETR:55;
A22: LIN o',a1',b1' by A2,ANALMETR:55;
A23: LIN o',a1',b2' by A14,ANALMETR:55;
A24: a',a1' // b',b1' by A2,ANALMETR:48;
a',a1' // b',b2' by A19,ANALMETR:48;
hence thesis by A20,A21,A22,A23,A24,AFF_1:70;end;
hence thesis by A14,ANALMETR:83;end;
hence thesis;end;
theorem LIN1_holds_in X implies LIN2_holds_in X
proof
assume A1: LIN1_holds_in X;
let o,a,a1,b,b1,c,c1;
assume A2: o<>a & o<>a1 & o<>b & o<>b1 & o<>c &
o<>c1 & a<>b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 &
not LIN o,c,a & LIN o,a,b & LIN
o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1;
reconsider a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1,o'=o
as Element of Af(X) by ANALMETR:47;
ex c2 st LIN a1,c1,c2 & o,c _|_ o,c2 & o<>c2
proof
consider e1 such that A3:a1,c1 // a1,e1 & a1<>e1 by ANALMETR:51;
consider e2 such that A4:o,c _|_ o,e2 & o<>e2 by ANALMETR:51;
reconsider e1'=e1,e2'=e2 as Element of Af(X)
by ANALMETR:47;
not a1',e1' // o',e2' proof assume a1',e1' // o',e2';
then a1,e1 // o,e2 by ANALMETR:48;
then a1,c1 // o,e2 by A3,ANALMETR:82;
then A5:a1,c1 _|_ o,c by A4,ANALMETR:84;
a1<>c1 proof assume A6: a1=c1;
A7:b1<>a1 proof assume b1=a1;
then a1,a // a1,b by A2,ANALMETR:81;
then LIN a1,a,b by ANALMETR:def 11;
then LIN a1',a',b' by ANALMETR:55;
then LIN a',b',a1' by AFF_1:15;
then LIN a,b,a1 by ANALMETR:55;
then A8:a,b // a,a1 by ANALMETR:def 11;
o,a // a,b
proof
LIN o',a',b' by A2,ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
hence thesis by ANALMETR:81;end;
then a,a1 // o,a by A2,A8,ANALMETR:82;
then a,a1 // a,o by ANALMETR:81;
then LIN a,a1,o by ANALMETR:def 11;
then LIN a',a1',o' by ANALMETR:55;
then LIN o',a',a1' by AFF_1:15;
then LIN o,a,a1 by ANALMETR:55;
then o,a // o,a1 by ANALMETR:def 11;
then o,a _|_ o,a by A2,ANALMETR:84;
hence contradiction by A2,ANALMETR:51;end;
b1,a1 _|_ b,a
proof
LIN o',a',b' & LIN o',a1',b1' by A2,ANALMETR:55;
then LIN b',o',a' & LIN b1',o',a1' by AFF_1:15;
then LIN b,o,a & LIN b1,o,a1 by ANALMETR:55;
then A9:b,o // b,a & b1,o // b1,a1 by ANALMETR:def 11;
b,o _|_ b1,o by A2,ANALMETR:83;
then b,a _|_ b1,o by A2,A9,ANALMETR:84;
hence thesis by A2,A9,ANALMETR:84;end;
then b,c // b,a by A2,A6,A7,ANALMETR:85;
then LIN b,c,a by ANALMETR:def 11;
then LIN b',c',a' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
then LIN a,b,c by ANALMETR:55;
then A10:a,b // a,c by ANALMETR:def 11;
LIN o',a',b' by A2,ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
then a,c // a,o by A2,A10,ANALMETR:82;
then LIN a,c,o by ANALMETR:def 11;
then LIN a',c',o' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then a,c // o,c by A2,A5,ANALMETR:85;
then c,a // c,o by ANALMETR:81;
then c',a' // c',o' by ANALMETR:48;
then LIN c',a',o' by AFF_1:def 1;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then consider c2' such that A11:LIN a1',e1',c2' & LIN
o',e2',c2' by AFF_1:74;
reconsider c2=c2' as Element of X by ANALMETR:47;take c2;
a1',e1' // a1',c2' by A11,AFF_1:def 1;
then a1,e1 // a1,c2 by ANALMETR:48;
then A12: a1,c1 // a1,c2 by A3,ANALMETR:82;
LIN o,e2,c2 by A11,ANALMETR:55;
then A13: o,e2 // o,c2 by ANALMETR:def 11;
o<>c2 proof assume o=c2;
then a1,c1 // o,a1 by A12,ANALMETR:81;
then A14:o,a _|_ a1,c1 by A2,ANALMETR:84;
a1<>c1 proof assume A15:a1=c1;
A16:a1<>b1 proof assume a1=b1;
then a1,a // a1,b by A2,ANALMETR:81;
then LIN a1,a,b by ANALMETR:def 11;
then LIN a1',a',b' by ANALMETR:55;
then LIN a',b',a1' by AFF_1:15;
then LIN a,b,a1 by ANALMETR:55;
then A17:a,b // a,a1 by ANALMETR:def 11;
o,a // a,b
proof
LIN o',a',b' by A2,ANALMETR:55;
then LIN a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55;
then a,b // a,o by ANALMETR:def 11;
hence thesis by ANALMETR:81;end;
then a,a1 // o,a by A2,A17,ANALMETR:82;
then a,a1 // a,o by ANALMETR:81;
then LIN a,a1,o by ANALMETR:def 11;
then LIN a',a1',o' by ANALMETR:55;
then LIN o',a',a1' by AFF_1:15;
then LIN o,a,a1 by ANALMETR:55;
then o,a // o,a1 by ANALMETR:def 11;
then o,a _|_ o,a by A2,ANALMETR:84;
hence contradiction by A2,ANALMETR:51;end;
b1,a1 // o,b1
proof
LIN o',a1',b1' by A2,ANALMETR:55;
then LIN b1',a1',o' by AFF_1:15;
then LIN b1,a1,o by ANALMETR:55;
then b1,a1 // b1,o by ANALMETR:def 11;
hence thesis by ANALMETR:81;end;
then b,c _|_ o,b1 by A2,A15,A16,ANALMETR:84;
then A18:b,c // o,b by A2,ANALMETR:85;
LIN o',a',b' by A2,ANALMETR:55;
then LIN b',a',o' & LIN a',b',o' by AFF_1:15;
then LIN b,a,o & LIN a,b,o by ANALMETR:55;
then A19:b,a // b,o & a,b // a,o by ANALMETR:def 11;
then o,b // b,a by ANALMETR:81;
then b,a // b,c by A2,A18,ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
then LIN a,b,c by ANALMETR:55;
then a,b // a,c by ANALMETR:def 11;
then a,o // a,c by A2,A19,ANALMETR:82;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then o,a // a,c by A2,A14,ANALMETR:85;
then a,c // a,o by ANALMETR:81;
then LIN a,c,o by ANALMETR:def 11;
then LIN a',c',o' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
hence thesis by A4,A12,A13,ANALMETR:84,def 11;end;
then consider c2 such that A20: LIN a1,c1,c2 & o,c _|_ o,c2 & o<>c2;
reconsider c2'=c2 as Element of Af(X) by ANALMETR:47;
A21: b<>c & a1<>b1 & a1<>c1
proof assume A22:b=c or a1=b1 or a1=c1;
A23:now assume b=c;
then LIN o',a',c' by A2,ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A24:now assume a1=b1;
then a1,a // a1,b by A2,ANALMETR:81;
then LIN a1,a,b by ANALMETR:def 11;
then LIN a1',a',b' by ANALMETR:55;
then LIN a',b',a1' by AFF_1:15;
then LIN a,b,a1 by ANALMETR:55;
then A25:a,b // a,a1 by ANALMETR:def 11;
o,a // a,b
proof LIN o',a',b' by A2,ANALMETR:55; then LIN
a',b',o' by AFF_1:15;
then LIN a,b,o by ANALMETR:55; then a,b // a,o by ANALMETR:def 11;
hence thesis by ANALMETR:81;end;
then a,a1 // o,a by A2,A25,ANALMETR:82; then a,a1 // a,o by ANALMETR:81
;
then LIN a,a1,o by ANALMETR:def 11; then LIN
a',a1',o' by ANALMETR:55;
then LIN o',a',a1' by AFF_1:15; then LIN o,a,a1 by ANALMETR:55;
then o,a // o,a1 by ANALMETR:def 11; then o,a _|_ o,a by A2,ANALMETR:84
;
hence contradiction by A2,ANALMETR:51;end;
now assume A26: a1=c1;
b1,a1 // o,b1
proof LIN o',a1',b1' by A2,ANALMETR:55; then LIN
b1',a1',o' by AFF_1:15;
then LIN b1,a1,o by ANALMETR:55; then b1,a1 // b1,o by ANALMETR:def 11
;
hence thesis by ANALMETR:81;end;
then b,c _|_ o,b1 by A2,A24,A26,ANALMETR:84;
then A27:b,c // o,b by A2,ANALMETR:85;
LIN o',a',b' by A2,ANALMETR:55; then LIN b',a',o' & LIN
a',b',o' by AFF_1:15;
then LIN b,a,o & LIN a,b,o by ANALMETR:55;
then A28:b,a // b,o & a,b // a,o by ANALMETR:def 11;
then o,b // b,a by ANALMETR:81;
then b,a // b,c by A2,A27,ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
then LIN a,b,c by ANALMETR:55;
then a,b // a,c by ANALMETR:def 11;
then a,o // a,c by A2,A28,ANALMETR:82;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
hence contradiction by A22,A23,A24;end;
a,c _|_ a1,c2
proof
a1,c1 // a1,c2 by A20,ANALMETR:def 11;
hence thesis by A2,A21,ANALMETR:84;end;
then b,c _|_ b1,c2 by A1,A2,A20,Def6;
then b1,c1 // b1,c2 by A2,A21,ANALMETR:85;
then A29: LIN b1,c1,c2 by ANALMETR:def 11;
c1 = c2
proof
not LIN b1,a1,c1
proof
assume LIN b1,a1,c1;
then LIN b1',a1',c1' by ANALMETR:55;
then LIN a1',b1',c1' by AFF_1:15;
then a1',b1' // a1',c1' by AFF_1:def 1;
then A30: a1,b1 // a1,c1 by ANALMETR:48;
LIN o',a1',b1' by A2,ANALMETR:55;
then LIN a1',b1',o' by AFF_1:15;
then LIN a1,b1,o by ANALMETR:55;
then a1,b1 // a1,o by ANALMETR:def 11;
then a1,c1 // a1,o by A21,A30,ANALMETR:82;
then a,c _|_ a1,o by A2,A21,ANALMETR:84;
then A31: o,a1 _|_ a,c by ANALMETR:83;
o,a1 _|_ a,o by A2,ANALMETR:83;
then a,o // a,c by A2,A31,ANALMETR:85;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then A32: not LIN b1',a1',c1' by ANALMETR:55;
A33: LIN b1',c1',c2' by A29,ANALMETR:55;
a1,c1 // a1,c2 by A20,ANALMETR:def 11;
then a1',c1' // a1',c2' by ANALMETR:48;
hence thesis by A32,A33,AFF_1:23;end;
hence thesis by A20;end;
theorem LIN_holds_in X implies ODES_holds_in X
proof
assume A1: LIN_holds_in X;
let o,a,a1,b,b1,c,c1;
assume A2: o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 &
a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b;
A3: LIN1_holds_in X by A1,Th3;
now let o,a,a1,b,b1,c,c1;
assume A4: LIN_holds_in X;
assume A5: o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 &
a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b;
assume A6: not o,b // a,c;
reconsider a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1,o'=o
as Element of Af(X) by ANALMETR:47;
A7: now assume A8: o=a1;
then A9: a1,b1 _|_ b,a1 by A5,ANALMETR:83;
A10: a1,b1 _|_ b,a by A5,ANALMETR:83;
not b,a1 // b,a
proof
assume b,a1 // b,a;
then LIN b,o,a by A8,ANALMETR:def 11;
then LIN b',o',a' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11; end;
then A11: a1=b1 by A9,A10,ANALMETR:85;
A12: a1,c1 _|_ c,a1 by A5,A8,ANALMETR:83;
a1,c1 _|_ c,a by A5,ANALMETR:83;
then A13: c,a1 // c,a or a1=c1 by A12,ANALMETR:85;
not c,a1 // c,a
proof
assume c,a1 // c,a;
then LIN c,o,a by A8,ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
hence b,c _|_ b1,c1 by A11,A13,ANALMETR:51;end;
A14: now assume A15: LIN o,b,c & o<>a1;
A16: o<>b by A5,ANALMETR:51;
A17: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:51;
then o',a' // o',c' by ANALMETR:48;
then o',c' // o',a' by AFF_1:13;
hence contradiction by A5,ANALMETR:48;end;
A18: o<>b1
proof
assume A19: o=b1;
a1,o _|_ a,o by A5,ANALMETR:83;
then a,o // a,b by A5,A15,A19,ANALMETR:85;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
o,b // o,c by A15,ANALMETR:def 11;
then o,c _|_ o,b1 by A5,A16,ANALMETR:84;
then o,b1 // o,c1 by A5,A17,ANALMETR:85;
then LIN o,b1,c1 by ANALMETR:def 11;
then LIN o',b1',c1' by ANALMETR:55;
then LIN b1',o',c1' by AFF_1:15;
then LIN b1,o,c1 by ANALMETR:55;
then A20: b1,o // b1,c1 by ANALMETR:def 11;
b1,o _|_ b,o by A5,ANALMETR:83;
then A21: b,o _|_ b1,c1 by A18,A20,ANALMETR:84;
LIN o',b',c' by A15,ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then LIN b,o,c by ANALMETR:55;
then b,o // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A16,A21,ANALMETR:84;end;
A22: now assume A23: LIN a,b,c & not LIN o,b,c & o<>a1;
A24: a<>c
proof
assume a=c;
then a,o // a,c by ANALMETR:51;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
A25: a<>b
proof
assume a=b;
then a,o // a,b by ANALMETR:51;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
A26: a1<>b1 by A5,A23,ANALMETR:85;
a,b // a,c by A23,ANALMETR:def 11;
then a,c _|_ a1,b1 by A5,A25,ANALMETR:84;
then a1,b1 // a1,c1 by A5,A24,ANALMETR:85;
then LIN a1,b1,c1 by ANALMETR:def 11;
then LIN a1',b1',c1' by ANALMETR:55;
then LIN b1',a1',c1' by AFF_1:15;
then LIN b1,a1,c1 by ANALMETR:55;
then A27: b1,a1 // b1,c1 by ANALMETR:def 11;
b1,a1 _|_ b,a by A5,ANALMETR:83;
then A28: b,a _|_ b1,c1 by A26,A27,ANALMETR:84;
LIN a',b',c' by A23,ANALMETR:55;
then LIN b',a',c' by AFF_1:15;
then LIN b,a,c by ANALMETR:55;
then b,a // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A25,A28,ANALMETR:84;end;
now assume A29: not LIN a,b,c & not LIN o,b,c & o<>a1;
A30: o<>a & o<>b & o<>b1 & o<>c & o<>c1 & a<>c & a1<>c1
proof
A31: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:51;
then o',a' // o',c' by ANALMETR:48;
then o',c' // o',a' by AFF_1:13;
hence contradiction by A5,ANALMETR:48;end;
A32: o<>b1
proof
assume A33: o=b1;
a1,o _|_ a,o by A5,ANALMETR:83;
then a,o // a,b by A5,A29,A33,ANALMETR:85;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
o<>c1
proof
assume A34: o=c1;
a1,o _|_ a,o by A5,ANALMETR:83;
then a,o // a,c by A5,A29,A34,ANALMETR:85;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
hence thesis by A5,A31,A32,ANALMETR:51,85;end;
ex e be Element of X st LIN o,e,b &
LIN a,c,e & e<>c & e<>b
proof
consider p be Element of X such that
A35: o,b // o,p & o<>p by ANALMETR:51;
reconsider p'=p as Element of
the carrier of Af(X) by ANALMETR:47;
consider p1 be Element of X such that
A36: a,c // a,p1 & a<>p1 by ANALMETR:51;
reconsider p1'=p1 as Element of
the carrier of Af(X) by ANALMETR:47;
not o,p // a,p1
proof
assume o,p // a,p1;
then a,p1 // o,b by A35,ANALMETR:82;
hence contradiction by A6,A36,ANALMETR:82;end;
then not o',p' // a',p1' by ANALMETR:48;
then consider e' be Element of
the carrier of Af(X) such
that A37: LIN o',p',e' & LIN a',p1',e' by AFF_1:74;
reconsider e=e' as Element of
the carrier of X by ANALMETR:47;
LIN o,p,e by A37,ANALMETR:55;
then o,p // o,e by ANALMETR:def 11;
then o,e // o,b by A35,ANALMETR:82;
then A38: LIN o,e,b by ANALMETR:def 11;
LIN a,p1,e by A37,ANALMETR:55;
then a,p1 // a,e by ANALMETR:def 11;
then a,c // a,e by A36,ANALMETR:82;
then A39: LIN a,c,e by ANALMETR:def 11;
A40: c <>e
proof
assume c = e;
then LIN o',c',b' by A38,ANALMETR:55;
then LIN o',b',c' by AFF_1:15;
hence contradiction by A29,ANALMETR:55;end;
b<>e
proof
assume b=e;
then LIN a',c',b' by A39,ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A29,ANALMETR:55;end;
hence thesis by A38,A39,A40;end;
then consider e be Element of X such that
A41: LIN o,e,b & LIN a,c,e & e<>c & e<>b;
reconsider e'=e as Element of
the carrier of Af(X) by ANALMETR:47;
ex e1 be Element of X st
LIN o,e1,b1 & LIN a1,c1,e1
proof
consider p be Element of X such that
A42: o,b1 // o,p & o<>p by ANALMETR:51;
reconsider p'=p as Element of
the carrier of Af(X) by ANALMETR:47;
consider p1 be Element of X such that
A43: a1,c1 // a1,p1 & a1<>p1 by ANALMETR:51;
reconsider p1'=p1 as Element of
the carrier of Af(X) by ANALMETR:47;
A44: not o,b1 // a1,c1
proof
assume o,b1 // a1,c1;
then a1,c1 _|_ o,b by A5,A30,ANALMETR:84;
hence contradiction by A5,A6,A30,ANALMETR:85;end;
not o,p // a1,p1
proof
assume o,p // a1,p1;
then a1,p1 // o,b1 by A42,ANALMETR:82;
hence contradiction by A43,A44,ANALMETR:82;end;
then not o',p' // a1',p1' by ANALMETR:48;
then consider e1' be Element of
the carrier of Af(X) such
that A45: LIN o',p',e1' & LIN a1',p1',e1' by AFF_1:74;
reconsider e1=e1' as Element of
the carrier of X by ANALMETR:47;
LIN o,p,e1 by A45,ANALMETR:55;
then o,p // o,e1 by ANALMETR:def 11;
then o,e1 // o,b1 by A42,ANALMETR:82;
then A46: LIN o,e1,b1 by ANALMETR:def 11;
LIN a1,p1,e1 by A45,ANALMETR:55;
then a1,p1 // a1,e1 by ANALMETR:def 11;
then a1,c1 // a1,e1 by A43,ANALMETR:82;
then LIN a1,c1,e1 by ANALMETR:def 11;
hence thesis by A46;end;
then consider e1 be Element of X such that
A47: LIN o,e1,b1 & LIN a1,c1,e1;
reconsider e1'=e1 as Element of
the carrier of Af(X) by ANALMETR:47;
A48: o,e _|_ o,e1 & o<>e & o<>e1
proof
A49: o,e _|_ o,e1
proof
o,e // o,b by A41,ANALMETR:def 11;
then o',e' // o',b' by ANALMETR:48;
then o',b' // o',e' by AFF_1:13;
then o,b // o,e by ANALMETR:48;
then A50: o,b1 _|_ o,e by A5,A30,ANALMETR:84;
o,e1 // o,b1 by A47,ANALMETR:def 11;
then o',e1' // o',b1' by ANALMETR:48;
then o',b1' // o',e1' by AFF_1:13;
then o,b1 // o,e1 by ANALMETR:48;
hence thesis by A30,A50,ANALMETR:84;end;
A51: o<>e
proof
assume o=e;
then LIN a',c',o' by A41,ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
o<>e1
proof
assume o=e1;
then LIN a1',c1',o' by A47,ANALMETR:55;
then LIN o',a1',c1' by AFF_1:15;
then LIN o,a1,c1 by ANALMETR:55;
then o,a1 // o,c1 by ANALMETR:def 11;
then o,c1 _|_ o,a by A5,A29,ANALMETR:84;
hence contradiction by A5,A30,ANALMETR:85;end;
hence thesis by A49,A51;end;
A52: not LIN o,a,e
proof
assume LIN o,a,e;
then o,a // o,e by ANALMETR:def 11;
then o',a' // o',e' by ANALMETR:48;
then o',e' // o',a' by AFF_1:13;
then A53: o,e // o,a by ANALMETR:48;
o,e // o,b by A41,ANALMETR:def 11;
hence contradiction by A5,A48,A53,ANALMETR:82;end;
A54: e,a _|_ e1,a1
proof
a,c // a,e by A41,ANALMETR:def 11;
then a',c' // a',e' by ANALMETR:48;
then a',c' // e',a' by AFF_1:13;
then a,c // e,a by ANALMETR:48;
then A55: a1,c1 _|_ e,a by A5,A30,ANALMETR:84;
a1,c1 // a1,e1 by A47,ANALMETR:def 11;
then e,a _|_ a1,e1 by A30,A55,ANALMETR:84;
hence thesis by ANALMETR:83;end;
b,a _|_ b1,a1 by A5,ANALMETR:83;
then A56: e,e1 // b,b1 by A4,A5,A29,A30,A41,A47,A48,A52,A54,Def5;
A57: not LIN o,c,e
proof
assume LIN o,c,e;
then LIN o',c',e' by ANALMETR:55;
then LIN c',e',o' by AFF_1:15;
then c',e' // c',o' by AFF_1:def 1;
then A58: c,e // c,o by ANALMETR:48;
LIN a',c',e' by A41,ANALMETR:55;
then LIN c',e',a' by AFF_1:15;
then c',e' // c',a' by AFF_1:def 1;
then c,e // c,a by ANALMETR:48;
then c,o // c,a by A41,A58,ANALMETR:82;
then LIN c,o,a by ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5,ANALMETR:def 11;end;
e,c _|_ e1,c1
proof
LIN a',c',e' by A41,ANALMETR:55;
then LIN c',a',e' by AFF_1:15;
then c',a' // c',e' by AFF_1:def 1;
then a',c' // e',c' by AFF_1:13;
then a,c // e,c by ANALMETR:48;
then A59: a1,c1 _|_ e,c by A5,A30,ANALMETR:84;
LIN a1',c1',e1' by A47,ANALMETR:55;
then LIN c1',a1',e1' by AFF_1:15;
then c1', a1' // c1', e1' by AFF_1:def 1;
then a1',c1' // e1',c1' by AFF_1:13;
then a1,c1 // e1,c1 by ANALMETR:48;
hence thesis by A30,A59,ANALMETR:84;end;
hence b,c _|_ b1,c1 by A3,A5,A30,A41,A47,A48,A56,A57,Def6;end;
hence b,c _|_ b1,c1 by A7,A14,A22;end;
then A60: not o,b // a,c implies b,c _|_ b1,c1 by A1,A2;
A61: now let o,a,a1,b,b1,c,c1;
assume A62: o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 &
a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b;
assume A63: not o,a // c,b;
reconsider a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1,o'=o
as Element of Af(X) by ANALMETR:47;
A64: now assume A65: o=a1;
then A66: a1,b1 _|_ b,a1 by A62,ANALMETR:83;
A67: a1,b1 _|_ b,a by A62,ANALMETR:83;
not b,a1 // b,a
proof
assume b,a1 // b,a;
then LIN b,o,a by A65,ANALMETR:def 11;
then LIN b',o',a' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11; end;
then A68: a1=b1 by A66,A67,ANALMETR:85;
A69: a1,c1 _|_ c,a1 by A62,A65,ANALMETR:83;
a1,c1 _|_ c,a by A62,ANALMETR:83;
then A70: c,a1 // c,a or a1=c1 by A69,ANALMETR:85;
not c,a1 // c,a
proof
assume c,a1 // c,a;
then LIN c,o,a by A65,ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
hence b,c _|_ b1,c1 by A68,A70,ANALMETR:51;end;
A71: now assume A72: LIN o,b,c & o<>a1;
A73: o<>b by A62,ANALMETR:51;
A74: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:51;
then o',a' // o',c' by ANALMETR:48;
then o',c' // o',a' by AFF_1:13;
hence contradiction by A62,ANALMETR:48;end;
A75: o<>b1
proof
assume A76: o=b1;
a1,o _|_ a,o by A62,ANALMETR:83;
then a,o // a,b by A62,A72,A76,ANALMETR:85;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
o,b // o,c by A72,ANALMETR:def 11;
then o,c _|_ o,b1 by A62,A73,ANALMETR:84;
then o,b1 // o,c1 by A62,A74,ANALMETR:85;
then LIN o,b1,c1 by ANALMETR:def 11;
then LIN o',b1',c1' by ANALMETR:55;
then LIN b1',o',c1' by AFF_1:15;
then LIN b1,o,c1 by ANALMETR:55;
then A77: b1,o // b1,c1 by ANALMETR:def 11;
b1,o _|_ b,o by A62,ANALMETR:83;
then A78: b,o _|_ b1,c1 by A75,A77,ANALMETR:84;
LIN o',b',c' by A72,ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then LIN b,o,c by ANALMETR:55;
then b,o // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A73,A78,ANALMETR:84;end;
A79: now assume A80: LIN a,b,c & not LIN o,b,c & o<>a1;
A81: a<>c
proof
assume a=c;
then a,o // a,c by ANALMETR:51;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
A82: a<>b
proof
assume a=b;
then a,o // a,b by ANALMETR:51;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
A83: a1<>b1 by A62,A80,ANALMETR:85;
a,b // a,c by A80,ANALMETR:def 11;
then a,c _|_ a1,b1 by A62,A82,ANALMETR:84;
then a1,b1 // a1,c1 by A62,A81,ANALMETR:85;
then LIN a1,b1,c1 by ANALMETR:def 11;
then LIN a1',b1',c1' by ANALMETR:55;
then LIN b1',a1',c1' by AFF_1:15;
then LIN b1,a1,c1 by ANALMETR:55;
then A84: b1,a1 // b1,c1 by ANALMETR:def 11;
b1,a1 _|_ b,a by A62,ANALMETR:83;
then A85: b,a _|_ b1,c1 by A83,A84,ANALMETR:84;
LIN a',b',c' by A80,ANALMETR:55;
then LIN b',a',c' by AFF_1:15;
then LIN b,a,c by ANALMETR:55;
then b,a // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A82,A85,ANALMETR:84;end;
now assume A86: not LIN a,b,c & not LIN o,b,c & o<>a1;
A87: o<>a & o<>b & o<>c & o<>b1 & o<>c1 & a<>a1 &
a<>b & a1<>b1 & a<>c & a1<>c1
proof
A88: o<>a by A62,ANALMETR:51;
A89: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:51;
then o',a' // o',c' by ANALMETR:48;
then o',c' // o',a' by AFF_1:13;
hence contradiction by A62,ANALMETR:48;end;
A90: o<>b1
proof
assume A91: o=b1;
a1,o _|_ a,o by A62,ANALMETR:83;
then a,o // a,b by A62,A86,A91,ANALMETR:85;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
o<>c1
proof
assume A92: o=c1;
a1,o _|_ a,o by A62,ANALMETR:83;
then a,o // a,c by A62,A86,A92,ANALMETR:85;
then LIN a,o,c by ANALMETR:def 11;
then LIN a',o',c' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
hence thesis by A62,A88,A89,A90,ANALMETR:51,85;end;
ex e be Element of X st
LIN b,c,e & LIN o,e,a & c <>e & e<>b & a<>e
proof
consider p be Element of X such that
A93: o,a // o,p & o<>p by ANALMETR:51;
reconsider p'=p as Element of Af(X) by ANALMETR:47;
consider p1 be Element of X such that
A94: b,c // b,p1 & b<>p1 by ANALMETR:51;
reconsider p1'=p1 as Element of Af(X) by ANALMETR:47;
not o,p // b,p1
proof
assume o,p // b,p1;
then b,p1 // o,a by A93,ANALMETR:82;
then o,a // b,c by A94,ANALMETR:82;
then o',a' // b',c' by ANALMETR:48;
then o',a' // c',b' by AFF_1:13;
hence contradiction by A63,ANALMETR:48;end;
then not o',p' // b',p1' by ANALMETR:48;
then consider e' be Element of Af(X) such
that A95: LIN o',p',e' & LIN b',p1',e' by AFF_1:74;
reconsider e=e' as Element of X by ANALMETR:47;
LIN o,p,e by A95,ANALMETR:55;
then A96: o,p // o,e by ANALMETR:def 11;
then o,e // o,a by A93,ANALMETR:82;
then A97: LIN o,e,a by ANALMETR:def 11;
LIN b,p1,e by A95,ANALMETR:55;
then b,p1 // b,e by ANALMETR:def 11;
then b,c // b,e by A94,ANALMETR:82;
then A98: LIN b,c,e by ANALMETR:def 11;
A99: c <>e by A62,A93,A96,ANALMETR:82;
A100: b<>e
proof
assume b=e;
then LIN o',b',a' by A97,ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62,ANALMETR:def 11;end;
a<>e
proof
assume a=e;
then LIN b',c',a' by A98,ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A86,ANALMETR:55;end;
hence thesis by A97,A98,A99,A100;end;
then consider e be Element of X such
that A101: LIN b,c,e & LIN o,e,a & e<>b & c <>e & a<>e;
reconsider e'=e as Element of Af(X)
by ANALMETR:47;
ex e1 be Element of X st LIN o,e1,a1 &
e,e1 // a,a1
proof
consider p be Element of X such that
A102: o,a1 // o,p & o<>p by ANALMETR:51;
reconsider p'=p as Element of Af(X) by ANALMETR:47;
consider p1 be Element of X such that
A103: a,a1 // e,p1 & e<>p1 by ANALMETR:51;
reconsider p1'=p1 as Element of Af(X) by ANALMETR:47
;
not o,p // e,p1
proof
assume o,p // e,p1;
then e,p1 // o,a1 by A102,ANALMETR:82;
then e',p1' // o',a1' by ANALMETR:48;
then o',a1' // e',p1' by AFF_1:13;
then o,a1 // e,p1 by ANALMETR:48;
then e,p1 _|_ o,a by A62,A86,ANALMETR:84;
then o,a _|_ a,a1 by A103,ANALMETR:84;
then A104: o,a _|_ a1,a by ANALMETR:83;
o,a _|_ a1,o by A62,ANALMETR:83;
then a1,o // a1,a by A87,A104,ANALMETR:85;
then LIN a1,o,a by ANALMETR:def 11;
then LIN a1',o',a' by ANALMETR:55;
then LIN a',o',a1' by AFF_1:15;
then a',o' // a',a1' by AFF_1:def 1;
then o',a' // a1',a' by AFF_1:13;
then o,a // a1,a by ANALMETR:48;
then a1,a _|_ a1,a by A87,A104,ANALMETR:84;
hence contradiction by A87,ANALMETR:51;end;
then not o',p' // e',p1' by ANALMETR:48;
then consider e1' be Element of Af(X) such
that A105: LIN o',p',e1' & LIN e',p1',e1' by AFF_1:74;
reconsider e1=e1' as Element of X by ANALMETR:47;
LIN o,p,e1 by A105,ANALMETR:55;
then o,p // o,e1 by ANALMETR:def 11;
then o,e1 // o,a1 by A102,ANALMETR:82;
then A106: LIN o,e1,a1 by ANALMETR:def 11;
LIN e,p1,e1 by A105,ANALMETR:55;
then e,p1 // e,e1 by ANALMETR:def 11;
then e,e1 // a,a1 by A103,ANALMETR:82;
hence thesis by A106;end;
then consider e1 be Element of X such
that A107: LIN o,e1,a1 & e,e1 // a,a1;
reconsider e1'=e1 as Element of Af(X) by ANALMETR:47;
A108: o,e _|_ o,e1 & o<>e & o<>e1
proof
A109: o,e _|_ o,e1
proof
o,e // o,a by A101,ANALMETR:def 11;
then o',e' // o',a' by ANALMETR:48;
then o',a' // o',e' by AFF_1:13;
then o,a // o,e by ANALMETR:48;
then A110: o,a1 _|_ o,e by A62,A87,ANALMETR:84;
o,e1 // o,a1 by A107,ANALMETR:def 11;
then o',e1' // o',a1' by ANALMETR:48;
then o',a1' // o',e1' by AFF_1:13;
then o,a1 // o,e1 by ANALMETR:48;
hence thesis by A86,A110,ANALMETR:84;end;
A111: o<>e
proof
assume o=e;
then LIN b',c',o' by A101,ANALMETR:55;
then LIN o',b',c' by AFF_1:15;
hence contradiction by A86,ANALMETR:55;end;
o<>e1
proof
assume o=e1;
then e',o' // a',a1' by A107,ANALMETR:48;
then o',e' // a',a1' by AFF_1:13;
then A112: o,e // a,a1 by ANALMETR:48;
o,e // o,a by A101,ANALMETR:def 11;
then A113: o,a // a,a1 by A111,A112,ANALMETR:82;
then A114: o,a1 _|_ a,a1 by A62,A87,ANALMETR:84;
o',a' // a',a1' by A113,ANALMETR:48;
then a',o' // a',a1' by AFF_1:13;
then LIN a',o',a1' by AFF_1:def 1;
then LIN a1',o',a' by AFF_1:15;
then a1',o' // a1',a' by AFF_1:def 1;
then o',a1' // a',a1' by AFF_1:13;
then o,a1 // a,a1 by ANALMETR:48;
then a,a1 _|_ a,a1 by A86,A114,ANALMETR:84;
hence contradiction by A87,ANALMETR:51;end;
hence thesis by A109,A111;end;
A115: not LIN o,b,a
proof
assume LIN o,b,a;
then o,b // o,a by ANALMETR:def 11;
then o',b' // o',a' by ANALMETR:48;
then o',a' // o',b' by AFF_1:13;
hence contradiction by A62,ANALMETR:48;end;
o,e // o,a by A101,ANALMETR:def 11;
then o',e' // o',a' by ANALMETR:48;
then o',a' // o',e' by AFF_1:13;
then o,a // o,e by ANALMETR:48;
then A116: LIN o,a,e by ANALMETR:def 11;
o,e1 // o,a1 by A107,ANALMETR:def 11;
then o',e1' // o',a1' by ANALMETR:48;
then o',a1' // o',e1' by AFF_1:13;
then o,a1 // o,e1 by ANALMETR:48;
then A117: LIN o,a1,e1 by ANALMETR:def 11;
e',e1' // a',a1' by A107,ANALMETR:48;
then a',a1' // e',e1' by AFF_1:13;
then A118: a,a1 // e,e1 by ANALMETR:48;
then A119: e,b _|_ e1,b1 by A3,A62,A86,A87,A101,A108,A115,A116,
A117,Def6;
not LIN o,c,a by A62,ANALMETR:def 11;
then A120: e,c _|_ e1,c1 by A3,A62,A86,A87,A101,A108,A116,A117,
A118,Def6;
A121: e1<>c1 & e1<>b1
proof
A122: e1<>c1
proof
assume e1=c1;
then o,c1 // o,a1 by A107,ANALMETR:def 11;
then o,a1 _|_ o,c by A62,A87,ANALMETR:84;
hence contradiction by A62,A86,ANALMETR:85;end;
e1<>b1
proof
assume e1=b1;
then o,b1 // o,a1 by A107,ANALMETR:def 11;
then o,a1 _|_ o,b by A62,A87,ANALMETR:84;
hence contradiction by A62,A86,ANALMETR:85;end;
hence thesis by A122;end;
A123: c,e _|_ c1,e1 by A120,ANALMETR:83;
A124: LIN b',c',e' by A101,ANALMETR:55;
then LIN c',e',b' by AFF_1:15;
then LIN c,e,b by ANALMETR:55;
then c,e // c,b by ANALMETR:def 11;
then A125: c,b _|_ c1,e1 by A101,A123,ANALMETR:84;
A126: c <>b
proof
assume c = b;
then LIN o',b',c' by AFF_1:16;
hence contradiction by A86,ANALMETR:55;end;
b',c' // b',e' by A124,AFF_1:def 1;
then c',b' // e',b' by AFF_1:13;
then c,b // e,b by ANALMETR:48;
then e,b _|_ c1,e1 by A125,A126,ANALMETR:84;
then e1,b1 // c1,e1 by A101,A119,ANALMETR:85;
then e1',b1' // c1',e1' by ANALMETR:48;
then e1',b1' // e1',c1' by AFF_1:13;
then LIN e1',b1',c1' by AFF_1:def 1;
then LIN b1',e1',c1' by AFF_1:15;
then b1',e1' // b1',c1' by AFF_1:def 1;
then e1',b1' // b1',c1' by AFF_1:13;
then A127: e1,b1 // b1,c1 by ANALMETR:48;
LIN b',e',c' by A124,AFF_1:15;
then b',e' // b',c' by AFF_1:def 1;
then e',b' // b',c' by AFF_1:13;
then e,b // b,c by ANALMETR:48;
then e1,b1 _|_ b,c by A101,A119,ANALMETR:84;
hence b,c _|_ b1,c1 by A121,A127,ANALMETR:84;end;
hence b,c _|_ b1,c1 by A64,A71,A79;end;
then A128: not o,a // c,b implies b,c _|_ b1,c1 by A2;
now let o,a,a1,b,b1,c,c1;
assume LIN_holds_in X;
assume A129: o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 &
a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b;
assume A130: o,a // c,b & o,b // a,c;
reconsider a'=a,b'=b,c'=c,o'=o
as Element of Af(X) by ANALMETR:47;
A131: now assume A132: o=a1;
then A133: a1,b1 _|_ b,a1 by A129,ANALMETR:83;
A134: a1,b1 _|_ b,a by A129,ANALMETR:83;
not b,a1 // b,a
proof
assume b,a1 // b,a;
then LIN b,o,a by A132,ANALMETR:def 11;
then LIN b',o',a' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A129,ANALMETR:def 11; end;
then A135: a1=b1 by A133,A134,ANALMETR:85;
A136: a1,c1 _|_ c,a1 by A129,A132,ANALMETR:83;
a1,c1 _|_ c,a by A129,ANALMETR:83;
then A137: c,a1 // c,a or a1=c1 by A136,ANALMETR:85;
not c,a1 // c,a
proof
assume c,a1 // c,a;
then LIN c,o,a by A132,ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A129,ANALMETR:def 11;end;
hence b,c _|_ b1,c1 by A135,A137,ANALMETR:51;end;
A138: now assume A139: o,a1 // c1,b1 & o<>a1;
o<>a
proof
assume o=a;
then LIN o',c',a' by AFF_1:16;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A129,ANALMETR:def 11;end;
then c,b _|_ o,a1 by A129,A130,ANALMETR:84;
then c,b _|_ c1,b1 by A139,ANALMETR:84;
hence b,c _|_ b1,c1 by ANALMETR:83;end;
now assume A140: not o,a1 // c1,b1 & o<>a1;
A141:o,a1 _|_ o,a & o,b1 _|_ o,b & o,c1 _|_ o,c & a1,b1 _|_
a,b &
a1,c1 _|_ a,c by A129,ANALMETR:83;
A142:not o,c1 // o,a1
proof
assume A143:o,c1 // o,a1;
o<>c1
proof assume o=c1;
then a,c _|_ o,a1 by A129,ANALMETR:83;
then a,c // o,a by A129,A140,ANALMETR:85;
then a,c // a,o by ANALMETR:81;
then LIN a,c,o by ANALMETR:def 11;
then LIN a',c',o' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A129,ANALMETR:def 11;end;
then o,c _|_ o,a1 by A129,A143,ANALMETR:84;
hence contradiction by A129,A140,ANALMETR:85;end;
not o,a1 // o,b1
proof
assume A144:o,a1 // o,b1;
A145:o<>b1
proof
assume o=b1;
then a,b _|_ o,a1 by A129,ANALMETR:83;
then a,b // o,a by A129,A140,ANALMETR:85;
then a,b // a,o by ANALMETR:81;
then LIN a,b,o by ANALMETR:def 11;
then LIN a',b',o' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A129,ANALMETR:def 11;end;
o,a _|_ o,b1 by A129,A140,A144,ANALMETR:84;
hence contradiction by A129,A145,ANALMETR:85;end;
then b1,c1 _|_ b,c by A61,A140,A141,A142;
hence b,c _|_ b1,c1 by ANALMETR:83;end;
hence b,c _|_ b1,c1 by A131,A138;end;
hence thesis by A1,A2,A60,A128;end;
theorem LIN_holds_in X implies 3H_holds_in X
proof
assume A1:LIN_holds_in X;
let a,b,c;
assume A2:not LIN a,b,c;
consider e1 such that A3:b,c _|_ a,e1 & a<>e1 by ANALMETR:def 10;
consider e2 such that A4:a,c _|_ b,e2 & b<>e2 by ANALMETR:def 10;
reconsider a'=a,b'=b,c' = c,e1'=e1,e2'=e2
as Element of Af(X) by ANALMETR:47;
not a',e1' // b',e2'
proof assume a',e1' // b',e2';
then a,e1 // b,e2 by ANALMETR:48;
then b,e2 _|_ b,c by A3,ANALMETR:84;
then a,c // b,c by A4,ANALMETR:85;
then a',c' // b',c' by ANALMETR:48;
then c',a' // c',b' by AFF_1:13;
then LIN c',a',b' by AFF_1:def 1;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then consider d' be Element of Af(X) such that
A5:LIN a',e1',d' & LIN b',e2',d' by AFF_1:74;
reconsider d=d' as Element of X by ANALMETR:47;take d;
LIN b,e2,d by A5,ANALMETR:55;
then A6: b,e2 // b,d by ANALMETR:def 11;
then A7:a,c _|_ b,d by A4,ANALMETR:84;
then A8:d,b _|_ a,c by ANALMETR:83;
LIN a,e1,d by A5,ANALMETR:55;
then A9: a,e1 // a,d by ANALMETR:def 11;
then A10:b,c _|_ a,d by A3,ANALMETR:84;
then A11:d,a _|_ b,c by ANALMETR:83;
A12:LIN1_holds_in X by A1,Th3;
A13:now assume A14:d<>c;
now assume A15:b<>d;
not b',d' // a',c'
proof assume b',d' // a',c';
then a',c' // b',d' by AFF_1:13;
then A16:a,c // b,d by ANALMETR:48;
a<>c
proof assume a= c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
then b,d _|_ b,d by A7,A16,ANALMETR:84;
hence contradiction by A15,ANALMETR:51;end;
then consider o' be Element of Af(X) such that
A17:LIN b',d',o' & LIN a',c',o' by AFF_1:74;
reconsider o=o' as Element of X by ANALMETR:47;
now assume A18:d<>a;
A19:o<>a
proof assume A20: o = a;
then LIN b,d,a by A17,ANALMETR:55;
then b,d // b,a by ANALMETR:def 11;
then b,a _|_ a,c by A7,A15,ANALMETR:84;
then A21:a,b _|_ a,c by ANALMETR:83;
LIN a',b',d' by A17,A20,AFF_1:15;
then LIN a,b,d by ANALMETR:55;
then A22:a,b // a,d by ANALMETR:def 11;
a<>b
proof assume a=b;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
then a,d _|_ a,c by A21,A22,ANALMETR:84;
then d,a _|_ a,c by ANALMETR:83;
then a,c // b,c by A11,A18,ANALMETR:85;
then c,a // c,b by ANALMETR:81;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A23:c <>o
proof assume A24:c = o;
then LIN b,d,c by A17,ANALMETR:55;
then b,d // b,c by ANALMETR:def 11;
then A25:b,c _|_ a,c by A7,A15,ANALMETR:84;
b<>c
proof assume b = c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
then a,d // a,c by A10,A25,ANALMETR:85;
then LIN a,d,c by ANALMETR:def 11;
then LIN a',d',c' by ANALMETR:55;
then LIN c',d',a' by AFF_1:15;
then LIN c,d,a by ANALMETR:55;
then A26:c,d // c,a by ANALMETR:def 11;
LIN c',d',b' by A17,A24,AFF_1:15;
then LIN c,d,b by ANALMETR:55;
then c,d // c,b by ANALMETR:def 11;
then c,a // c,b by A14,A26,ANALMETR:82;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
consider e1 such that A27:a,c // a,e1 & a<>e1 by ANALMETR:51;
consider e2 such that A28:b,c // d,e2 & d<>e2 by ANALMETR:51;
reconsider e1'=e1,e2'=e2 as Element of the carrier
of Af(X) by ANALMETR:47;
not a',e1' // d',e2'
proof assume a',e1' // d',e2';
then a,e1 // d,e2 by ANALMETR:48;
then d,e2 // a,c by A27,ANALMETR:82;
then a,c // b,c by A28,ANALMETR:82;
then c,a // c,b by ANALMETR:81;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
then consider d1' such that A29:LIN a',e1',d1' & LIN d',e2',d1'
by AFF_1:74;
reconsider d1=d1' as Element of X by ANALMETR:47;
A30:LIN a,c,d1
proof LIN a,e1,d1 by A29,ANALMETR:55;
then a,e1 // a,d1 by ANALMETR:def 11;
then a,c // a,d1 by A27,ANALMETR:82;
hence thesis by ANALMETR:def 11;end;
A31: b,c // d,d1
proof LIN d,e2,d1 by A29,ANALMETR:55;
then d,e2 // d,d1 by ANALMETR:def 11;
hence thesis by A28,ANALMETR:82;end;
A32:o<>d
proof assume A33:o = d;
then A34:a,o _|_ b,c by A3,A9,ANALMETR:84;
LIN a,c,o by A17,ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A35:a,c _|_ b,c by A19,A34,ANALMETR:84;
a<>c
proof assume a= c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
then b,o // b,c by A7,A33,A35,ANALMETR:85;
then LIN b,o,c by ANALMETR:def 11;
then LIN b',o',c' by ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then LIN c,o,b by ANALMETR:55;
then A36:c,o // c,b by ANALMETR:def 11;
LIN c',o',a' by A17,AFF_1:15;
then LIN c,o,a by ANALMETR:55;
then c,o // c,a by ANALMETR:def 11;
then c,b // c,a by A23,A36,ANALMETR:82;
then LIN c,b,a by ANALMETR:def 11;
then LIN c',b',a' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A37:o<>d1
proof assume A38: o = d1;
LIN o',d',b' by A17,AFF_1:15;
then LIN o,d,b by ANALMETR:55;
then o,d // o,b by ANALMETR:def 11;
then d,o // b,o by ANALMETR:81;
then b,c //b,o by A31,A32,A38,ANALMETR:82;
then LIN b,c,o by ANALMETR:def 11;
then LIN b',c',o' by ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then LIN c,o,b by ANALMETR:55;
then A39:c,o // c,b by ANALMETR:def 11;
LIN c',o',a' by A17,AFF_1:15;
then LIN c,o,a by ANALMETR:55;
then c,o // c,a by ANALMETR:def 11;
then c,a // c,b by A23,A39,ANALMETR:82;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A40:o<>b
proof assume o=b;
then LIN a',b',c' by A17,AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A41:d1<>c
proof assume A42:d1 = c;
A43:b<>c
proof assume b = c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
c,b // c,d by A31,A42,ANALMETR:81;
then LIN c,b,d by ANALMETR:def 11;
then A44:LIN c',b',d' by ANALMETR:55;
b,c // c,d by A31,A42,ANALMETR:81;
then d,a _|_ c,d by A11,A43,ANALMETR:84;
then A45:d,c _|_ d,a by ANALMETR:83;
LIN d',c',b' by A44,AFF_1:15;
then LIN d,c,b by ANALMETR:55;
then d,c // d,b by ANALMETR:def 11;
then d,b _|_ d,a by A14,A45,ANALMETR:84;
then a,c // d,a by A8,A15,ANALMETR:85;
then a,c // a,d by ANALMETR:81;
then LIN a,c,d by ANALMETR:def 11;
then LIN a',c',d' by ANALMETR:55;
then LIN c',a',d' by AFF_1:15;
then LIN c,a,d by ANALMETR:55;
then A46: c,a // c,d by ANALMETR:def 11;
c,d // b,c by A31,A42,ANALMETR:81;
then c,a // b,c by A14,A46,ANALMETR:82;
then c,a // c,b by ANALMETR:81;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2,ANALMETR:55;end;
A47:o,d _|_ o,a
proof LIN d',o',b' by A17,AFF_1:15;
then d',o' // d',b' by AFF_1:def 1;
then b',d' // o',d' by AFF_1:13;
then b,d // o,d by ANALMETR:48;
then A48:a,c _|_ o,d by A7,A15,ANALMETR:84;
LIN a,c,o by A17,ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A49:a,c // o,a by ANALMETR:81;
a<>c
proof assume a= c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
hence thesis by A48,A49,ANALMETR:84;end;
A50:o,d1 _|_ o,d
proof LIN a,c,o by A17,ANALMETR:55;
then A51:a,c // a,o by ANALMETR:def 11;
A52:a<>c
proof assume a= c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
a,c // a,d1 by A30,ANALMETR:def 11;
then a,o // a,d1 by A51,A52,ANALMETR:82;
then LIN a,o,d1 by ANALMETR:def 11;
then LIN a',o',d1' by ANALMETR:55;
then LIN o',a',d1' by AFF_1:15;
then LIN o,a,d1 by ANALMETR:55;
then A53:o,a // o,d1 by ANALMETR:def 11;
LIN a,c,o by A17,ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then o,a // a,c by ANALMETR:81;
then a,c // o,d1 by A19,A53,ANALMETR:82;
then A54:b,d _|_ o,d1 by A7,A52,ANALMETR:84;
LIN d',o',b' by A17,AFF_1:15;
then LIN d,o,b by ANALMETR:55;
then d,o // d,b by ANALMETR:def 11;
then b,d // o,d by ANALMETR:81;
hence thesis by A15,A54,ANALMETR:84;end;
A55:o,c _|_ o,b
proof LIN c',o',a' by A17,AFF_1:15;
then c',o' // c',a' by AFF_1:def 1;
then a',c' // o',c' by AFF_1:13;
then A56:a,c // o,c by ANALMETR:48;
a<>c
proof assume a= c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
then A57:b,d _|_ o,c by A7,A56,ANALMETR:84;
b',d' // b',o' by A17,AFF_1:def 1;
then b',d' // o',b' by AFF_1:13;
then b,d // o,b by ANALMETR:48;
hence thesis by A15,A57,ANALMETR:84;end;
A58:not LIN o,d,d1
proof assume LIN o,d,d1;
then o,d // o,d1 by ANALMETR:def 11;
then o,d _|_ o,d by A37,A50,ANALMETR:84;
hence contradiction by A32,ANALMETR:51;end;
A59:LIN o,d1,c
proof
LIN a',c',d1' by A30,ANALMETR:55;
then LIN c',d1',a' by AFF_1:15;
then c',d1' // c',a' by AFF_1:def 1;
then a',c' // c',d1' by AFF_1:13;
then A60:a,c // c,d1 by ANALMETR:48;
A61:a<>c
proof assume a= c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
LIN c',a',o' by A17,AFF_1:15;
then c',a' // c',o' by AFF_1:def 1;
then a',c' // c',o' by AFF_1:13;
then a,c // c,o by ANALMETR:48;
then c,d1 // c,o by A60,A61,ANALMETR:82;
then LIN c,d1,o by ANALMETR:def 11;
then LIN c',d1',o' by ANALMETR:55;
then LIN o',d1',c' by AFF_1:15;
hence thesis by ANALMETR:55;end;
LIN o',d',b' by A17,AFF_1:15;
then A62:LIN o,d,b by ANALMETR:55;
A63:d1,d // c,b by A31,ANALMETR:81;
d1,d _|_ d,a
proof
b<>c
proof assume b = c;
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2,ANALMETR:55;end;
then d,d1 _|_ a,d by A10,A31,ANALMETR:84;
hence thesis by ANALMETR:83;end;
then c,d _|_
b,a by A12,A19,A23,A32,A37,A40,A41,A47,A50,A55,A58,A59,A62,A63,Def6;
hence thesis by A7,A10,ANALMETR:83;end;
hence thesis by A3,A7,A9,ANALMETR:83,84;end;
hence thesis by A4,A6,A10,ANALMETR:83,84;end;
now assume d = c;
then a,b _|_ d,c by ANALMETR:51;
hence thesis by A7,A10,ANALMETR:83;end;
hence thesis by A13;end;