:: Metric-Affine Configurations in Metric Affine Planes - Part I
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received October 31, 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 ANALMETR, SUBSET_1, DIRAF, ANALOAF, SYMSP_1, CONAFFM;
notations STRUCT_0, ANALOAF, AFF_1, ANALMETR;
constructors AFF_1, ANALMETR;
registrations ANALMETR;
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 b29,c29,d19 for Element of the AffinStruct of 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;
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;
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;
attr X is satisfying_ODES 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 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b
holds b,c _|_ b1,c1;
attr X is satisfying_LIN means
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;
attr X is satisfying_LIN1 means
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;
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;
end;
theorem
X is satisfying_ODES implies X is satisfying_DES
proof
assume
A1: X is satisfying_ODES;
let o,a,a1,b,b1,c,c1;
assume that
A2: o<>a and
A3: o<>a1 and
A4: o<>b and
A5: o<>b1 and
A6: o<>c and o<>c1 and
A7: not LIN b,b1,a and
A8: not LIN a,a1,c and
A9: LIN o,a,a1 and
A10: LIN o,b,b1 and
A11: LIN o,c,c1 and
A12: a,b // a1,b1 and
A13: a,c // a1,c1;
consider a2 such that
A14: o,a _|_ o,a2 and
A15: o<>a2 by ANALMETR:def 9;
consider e1 such that
A16: o,b _|_ o,e1 and
A17: o<>e1 by ANALMETR:def 9;
consider e2 such that
A18: a,b _|_ a2,e2 and
A19: a2<>e2 by ANALMETR:def 9;
reconsider o9=o,a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1,a29=a2,e19=e1,e29=e2
as Element of the AffinStruct of X;
not o9,e19 // a29,e29
proof
assume o9,e19 // a29,e29;
then o,e1 // a2,e2 by ANALMETR:36;
then a2,e2 _|_ o,b by A16,A17,ANALMETR:62;
then a,b // o,b by A18,A19,ANALMETR:63;
then
A20: a9,b9 // o9,b9 by ANALMETR:36;
then b9,a9 // b9,o9 by AFF_1:4;
then
A21: LIN b9,a9,o9 by AFF_1:def 1;
o9,b9 // b9,a9 by A20,AFF_1:4;
then
A22: o,b // b,a by ANALMETR:36;
A23: b9<>a9
proof
assume b9=a9;
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A7,ANALMETR:40;
end;
o,b // o,b1 by A10,ANALMETR:def 10;
then b,a // o,b1 by A4,A22,ANALMETR:60;
then b9,a9 // o9,b19 by ANALMETR:36;
then LIN b9,a9,b19 by A21,A23,AFF_1:9;
then LIN b9,b19,a9 by AFF_1:6;
hence contradiction by A7,ANALMETR:40;
end;
then consider b29 such that
A24: LIN o9,e19,b29 and
A25: LIN a29,e29,b29 by AFF_1:60;
reconsider b2=b29 as Element of X;
LIN o,e1,b2 by A24,ANALMETR:40;
then o,e1 // o,b2 by ANALMETR:def 10;
then
A26: o,b _|_ o,b2 by A16,A17,ANALMETR:62;
LIN a2,e2,b2 by A25,ANALMETR:40;
then a2,e2 // a2,b2 by ANALMETR:def 10;
then
A27: a,b _|_ a2,b2 by A18,A19,ANALMETR:62;
consider e1 such that
A28: o,c _|_ o,e1 and
A29: o<>e1 by ANALMETR:def 9;
consider e2 such that
A30: a,c _|_ a2,e2 and
A31: a2<>e2 by ANALMETR:def 9;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not o9,e19 // a29,e29
proof
assume o9,e19 // a29,e29;
then o,e1 // a2,e2 by ANALMETR:36;
then o,c _|_ a2,e2 by A28,A29,ANALMETR:62;
then o,c // a,c by A30,A31,ANALMETR:63;
then c,o // c,a by ANALMETR:59;
then LIN c,o,a by ANALMETR:def 10;
then LIN c9,o9,a9 by ANALMETR:40;
then LIN a9,c9,o9 by AFF_1:6;
then LIN a,c,o by ANALMETR:40;
then a,c // a,o by ANALMETR:def 10;
then
A32: o,a // a,c by ANALMETR:59;
LIN o9,a9,a19 by A9,ANALMETR:40;
then LIN a9,o9,a19 by AFF_1:6;
then LIN a,o,a1 by ANALMETR:40;
then a,o // a,a1 by ANALMETR:def 10;
then o,a // a,a1 by ANALMETR:59;
then a,a1 // a,c by A2,A32,ANALMETR:60;
hence contradiction by A8,ANALMETR:def 10;
end;
then consider c29 such that
A33: LIN o9,e19,c29 and
A34: LIN a29,e29,c29 by AFF_1:60;
reconsider c2=c29 as Element of X;
LIN o,e1,c2 by A33,ANALMETR:40;
then o,e1 // o,c2 by ANALMETR:def 10;
then
A35: o,c _|_ o,c2 by A28,A29,ANALMETR:62;
LIN a2,e2,c2 by A34,ANALMETR:40;
then a2,e2 // a2,c2 by ANALMETR:def 10;
then
A36: a,c _|_ a2,c2 by A30,A31,ANALMETR:62;
A37: not o,c // o,a
proof
assume o,c // o,a;
then LIN o,c,a by ANALMETR:def 10;
then LIN o9,c9,a9 by ANALMETR:40;
then LIN a9,o9,c9 by AFF_1:6;
then LIN a,o,c by ANALMETR:40;
then
A38: a,o // a,c by ANALMETR:def 10;
LIN o9,a9,a19 by A9,ANALMETR:40;
then LIN a9,o9,a19 by AFF_1:6;
then LIN a,o,a1 by ANALMETR:40;
then a,o // a,a1 by ANALMETR:def 10;
then a,a1 // a,c by A2,A38,ANALMETR:60;
hence contradiction by A8,ANALMETR:def 10;
end;
not o,a // o,b
proof
assume o,a // o,b;
then LIN o,a,b by ANALMETR:def 10;
then LIN o9,a9,b9 by ANALMETR:40;
then LIN b9,o9,a9 by AFF_1:6;
then LIN b,o,a by ANALMETR:40;
then
A39: b,o // b,a by ANALMETR:def 10;
LIN o9,b9,b19 by A10,ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then LIN b,o,b1 by ANALMETR:40;
then b,o // b,b1 by ANALMETR:def 10;
then b,b1 // b,a by A4,A39,ANALMETR:60;
hence contradiction by A7,ANALMETR:def 10;
end;
then
A40: b,c _|_ b2,c2 by A1,A14,A26,A27,A35,A36,A37;
o,a // o,a1 by A9,ANALMETR:def 10;
then
A41: o,a1 _|_ o,a2 by A2,A14,ANALMETR:62;
o,b // o,b1 by A10,ANALMETR:def 10;
then
A42: o,b1 _|_ o,b2 by A4,A26,ANALMETR:62;
o,c // o,c1 by A11,ANALMETR:def 10;
then
A43: o,c1 _|_ o,c2 by A6,A35,ANALMETR:62;
a<>b
proof
assume a=b;
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A7,ANALMETR:40;
end;
then
A44: a1,b1 _|_ a2,b2 by A12,A27,ANALMETR:62;
a<>c
proof
assume a= c;
then LIN a9,a19,c9 by AFF_1:7;
hence contradiction by A8,ANALMETR:40;
end;
then
A45: a1,c1 _|_ a2,c2 by A13,A36,ANALMETR:62;
A46: not o,c1 // o,a1
proof
assume o,c1 // o,a1;
then LIN o,c1,a1 by ANALMETR:def 10;
then LIN o9,c19,a19 by ANALMETR:40;
then LIN a19,o9,c19 by AFF_1:6;
then LIN a1,o,c1 by ANALMETR:40;
then
A47: a1,o // a1,c1 by ANALMETR:def 10;
A48: a1<> c1
proof
assume a1 = c1;
then LIN o9,c9,a19 by A11,ANALMETR:40;
then LIN a19,c9,o9 by AFF_1:6;
then LIN a1,c,o by ANALMETR:40;
then
A49: a1,c // a1,o by ANALMETR:def 10;
LIN o9,a9,a19 by A9,ANALMETR:40;
then LIN a19,o9,a9 by AFF_1:6;
then LIN a1,o,a by ANALMETR:40;
then a1,o // a1,a by ANALMETR:def 10;
then a1,c // a1,a by A3,A49,ANALMETR:60;
then LIN a1,c,a by ANALMETR:def 10;
then LIN a19,c9,a9 by ANALMETR:40;
then LIN a9,a19,c9 by AFF_1:6;
hence contradiction by A8,ANALMETR:40;
end;
LIN o9,a9,a19 by A9,ANALMETR:40;
then LIN a19,o9,a9 by AFF_1:6;
then LIN a1,o,a by ANALMETR:40;
then a1,o // a1,a by ANALMETR:def 10;
then a1,c1 // a1,a by A3,A47,ANALMETR:60;
then a1,a // a,c by A13,A48,ANALMETR:60;
then a,a1 // a,c by ANALMETR:59;
hence contradiction by A8,ANALMETR:def 10;
end;
not o,a1 // o,b1
proof
assume o,a1 // o,b1;
then LIN o,a1,b1 by ANALMETR:def 10;
then LIN o9,a19,b19 by ANALMETR:40;
then LIN b19,a19,o9 by AFF_1:6;
then LIN b1,a1,o by ANALMETR:40;
then
A50: b1,a1 // b1,o by ANALMETR:def 10;
A51: a1<>b1
proof
assume a1=b1;
then LIN o9,a9,b19 by A9,ANALMETR:40;
then LIN b19,o9,a9 by AFF_1:6;
then LIN b1,o,a by ANALMETR:40;
then
A52: b1,o // b1,a by ANALMETR:def 10;
LIN o9,b9,b19 by A10,ANALMETR:40;
then LIN b19,b9,o9 by AFF_1:6;
then LIN b1,b,o by ANALMETR:40;
then b1,b // b1,o by ANALMETR:def 10;
then b1,a // b1,b by A5,A52,ANALMETR:60;
then LIN b1,a,b by ANALMETR:def 10;
then LIN b19,a9,b9 by ANALMETR:40;
then LIN b9,b19,a9 by AFF_1:6;
hence contradiction by A7,ANALMETR:40;
end;
A53: b1,a1 // a,b by A12,ANALMETR:59;
LIN o9,b9,b19 by A10,ANALMETR:40;
then LIN b19,b9,o9 by AFF_1:6;
then LIN b1,b,o by ANALMETR:40;
then b1,b // b1,o by ANALMETR:def 10;
then b1,a1 // b1,b by A5,A50,ANALMETR:60;
then b1,b // a,b by A51,A53,ANALMETR:60;
then b,b1 // b,a by ANALMETR:59;
hence contradiction by A7,ANALMETR:def 10;
end;
then
A54: b1,c1 _|_ b2,c2 by A1,A41,A42,A43,A44,A45,A46;
A55: now
assume
A56: not LIN o,b,c;
b2<>c2
proof
assume
A57: b2 = c2;
o<>b2
proof
assume
A58: o=b2;
a2,o _|_ a,o by A14,ANALMETR:61;
then a,o // a,b by A15,A27,A58,ANALMETR:63;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN b9,o9,a9 by AFF_1:6;
then LIN b,o,a by ANALMETR:40;
then
A59: b,o // b,a by ANALMETR:def 10;
LIN o9,b9,b19 by A10,ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then LIN b,o,b1 by ANALMETR:40;
then b,o // b,b1 by ANALMETR:def 10;
then b,b1 // b,a by A4,A59,ANALMETR:60;
hence contradiction by A7,ANALMETR:def 10;
end;
then o,b // o,c by A26,A35,A57,ANALMETR:63;
hence contradiction by A56,ANALMETR:def 10;
end;
hence thesis by A40,A54,ANALMETR:63;
end;
now
assume
A60: LIN o,b,c;
then LIN o9,b9,c9 by ANALMETR:40;
then LIN b9,o9,c9 by AFF_1:6;
then
A61: b9,o9 // b9,c9 by AFF_1:def 1;
LIN o9,b9,b19 by A10,ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then b9,o9 // b9,b19 by AFF_1:def 1;
then b9,c9 // b9,b19 by A4,A61,AFF_1:5;
then
A62: LIN b9,c9,b19 by AFF_1:def 1;
LIN o9,b9,c9 by A60,ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then
A63: c9,o9 // c9,b9 by AFF_1:def 1;
LIN o9,c9,c19 by A11,ANALMETR:40;
then LIN c9,o9,c19 by AFF_1:6;
then c9,o9 // c9,c19 by AFF_1:def 1;
then c9,b9 // c9,c19 by A6,A63,AFF_1:5;
then LIN c9,b9,c19 by AFF_1:def 1;
then LIN b9,c9,c19 by AFF_1:6;
then b9,c9 // b19,c19 by A62,AFF_1:10;
hence thesis by ANALMETR:36;
end;
hence thesis by A55;
end;
theorem
X is satisfying_ODES implies X is satisfying_AH;
theorem Th3:
X is satisfying_LIN implies X is satisfying_LIN1
proof
assume
A1: X is satisfying_LIN;
let o,a,a1,b,b1,c,c1;
assume that
A2: o<>a and
A3: o<>a1 and
A4: o<>b and o<>b1 and
A5: o<>c and
A6: o<>c1 and
A7: a<>b and
A8: o,c _|_ o,c1 and
A9: o,a _|_ o,a1 and o,b _|_ o,b1 and
A10: not LIN o,c,a and
A11: LIN o,a,b and
A12: LIN o,a1,b1 and
A13: a,c _|_ a1,c1 and
A14: a,a1 // b,b1;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1,o9=o
as Element of the AffinStruct of X;
now ex b2 st LIN o,a1,b2 & c1,b2 _|_ b,c & c1<>b2
proof
consider y be Element of X such that
A15: o,a1 // o,y and
A16: o<>y by ANALMETR:39;
consider x be Element of X such that
A17: b,c _|_ c1,x and
A18: c1<>x by ANALMETR:39;
A19: not o,y // c1,x
proof
assume
A20: o,y // c1,x;
reconsider y9=y,x9=x as Element of the AffinStruct of X;
A21: o9,y9 // c19,x9 by A20,ANALMETR:36;
o9,a19 // o9,y9 by A15,ANALMETR:36;
then o9,y9 // o9,a19 by AFF_1:4;
then c19,x9 // o9,a19 by A16,A21,DIRAF:40;
then c1,x // o,a1 by ANALMETR:36;
then o,a1 _|_ b,c by A17,A18,ANALMETR:62;
then
A22: o,a // b,c by A3,A9,ANALMETR:63;
o,a // o,b by A11,ANALMETR:def 10;
then b,c // o,b by A2,A22,ANALMETR:60;
then b9,c9 // o9,b9 by ANALMETR:36;
then b9,c9 // b9,o9 by AFF_1:4;
then LIN b9,c9,o9 by AFF_1:def 1;
then LIN o9,b9,c9 by AFF_1:6;
then
A23: o9,b9 // o9,c9 by AFF_1:def 1;
LIN o9,a9,b9 by A11,ANALMETR:40;
then LIN o9,b9,a9 by AFF_1:6;
then o9,b9 // o9,a9 by AFF_1:def 1;
then o9,c9 // o9,a9 by A4,A23,DIRAF:40;
then LIN o9,c9,a9 by AFF_1:def 1;
hence contradiction by A10,ANALMETR:40;
end;
reconsider y9=y,x9=x as Element of the AffinStruct of X;
not o9,y9 // c19,x9 by A19,ANALMETR:36;
then consider b29 be Element of the AffinStruct of X such that
A24: LIN o9,y9,b29 and
A25: LIN c19,x9,b29 by AFF_1:60;
reconsider b2=b29 as Element of X;
LIN c1,x,b2 by A25,ANALMETR:40;
then c1,x // c1,b2 by ANALMETR:def 10;
then
A26: c1,b2 _|_ b,c by A17,A18,ANALMETR:62;
o9,a19 // o9,y9 by A15,ANALMETR:36;
then
A27: o9,y9 // o9,a19 by AFF_1:4;
o9,y9 // o9,b29 by A24,AFF_1:def 1;
then o9,a19 // o9,b29 by A16,A27,DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then
A28: LIN o,a1,b2 by ANALMETR:40;
c1<>b2
proof
assume c1=b2;
then o,a1 // o,c1 by A28,ANALMETR:def 10;
then o,c1 _|_ o,a by A3,A9,ANALMETR:62;
then o,c // o,a by A6,A8,ANALMETR:63;
hence contradiction by A10,ANALMETR:def 10;
end;
hence thesis by A26,A28;
end;
then consider b2 such that
A29: LIN o,a1,b2 and
A30: c1,b2 _|_ b,c and c1<>b2;
reconsider b29=b2 as Element of the AffinStruct of X;
o,a1 // o,b2 by A29,ANALMETR:def 10;
then
A31: o,a _|_ o,b2 by A3,A9,ANALMETR:62;
A32: o,a // o,b by A11,ANALMETR:def 10;
A33: o<>b2
proof
assume o=b2;
then o,c1 _|_ b,c by A30,ANALMETR:61;
then o,c // b,c by A6,A8,ANALMETR:63;
then o9,c9 // b9,c9 by ANALMETR:36;
then c9,o9 // c9,b9 by AFF_1:4;
then LIN c9,o9,b9 by AFF_1:def 1;
then LIN o9,b9,c9 by AFF_1:6;
then
A34: o9,b9 // o9,c9 by AFF_1:def 1;
LIN o9,a9,b9 by A11,ANALMETR:40;
then LIN o9,b9,a9 by AFF_1:6;
then o9,b9 // o9,a9 by AFF_1:def 1;
then o9,c9 // o9,a9 by A4,A34,DIRAF:40;
then LIN o9,c9,a9 by AFF_1:def 1;
hence contradiction by A10,ANALMETR:40;
end;
A35: o,b _|_ o,b2 by A2,A31,A32,ANALMETR:62;
b,c _|_ b2,c1 by A30,ANALMETR:61;
then
A36: a,a1 // b,b2 by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A13,A29,A33,A35;
not LIN o,a,a1
proof
assume LIN o,a,a1;
then o,a // o,a1 by ANALMETR:def 10;
then o,a1 _|_ o,a1 by A2,A9,ANALMETR:62;
hence contradiction by A3,ANALMETR:39;
end;
then
A37: not LIN o9,a9,a19 by ANALMETR:40;
A38: LIN o9,a9,b9 by A11,ANALMETR:40;
A39: LIN o9,a19,b19 by A12,ANALMETR:40;
A40: LIN o9,a19,b29 by A29,ANALMETR:40;
A41: a9,a19 // b9,b19 by A14,ANALMETR:36;
a9,a19 // b9,b29 by A36,ANALMETR:36;
then b1=b2 by A37,A38,A39,A40,A41,AFF_1:56;
hence thesis by A30,ANALMETR:61;
end;
hence thesis;
end;
theorem
X is satisfying_LIN1 implies X is satisfying_LIN2
proof
assume
A1: X is satisfying_LIN1;
let o,a,a1,b,b1,c,c1;
assume that
A2: o<>a and
A3: o<>a1 and
A4: o<>b and
A5: o<>b1 and
A6: o<>c and o<>c1 and
A7: a<>b and
A8: a,a1 // b,b1 and
A9: o,a _|_ o,a1 and
A10: o,b _|_ o,b1 and
A11: not LIN o,c,a and
A12: LIN o,a,b and
A13: LIN o,a1,b1 and
A14: a,c _|_ a1,c1 and
A15: b,c _|_ b1,c1;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1,o9=o
as Element of the AffinStruct of X;
ex c2 st LIN a1,c1,c2 & o,c _|_ o,c2 & o<>c2
proof
consider e1 such that
A16: a1,c1 // a1,e1 and
A17: a1<>e1 by ANALMETR:39;
consider e2 such that
A18: o,c _|_ o,e2 and
A19: o<>e2 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not a19,e19 // o9,e29
proof
assume a19,e19 // o9,e29;
then a1,e1 // o,e2 by ANALMETR:36;
then a1,c1 // o,e2 by A16,A17,ANALMETR:60;
then
A20: a1,c1 _|_ o,c by A18,A19,ANALMETR:62;
a1<>c1
proof
assume
A21: a1=c1;
A22: b1<>a1
proof
assume b1=a1;
then a1,a // a1,b by A8,ANALMETR:59;
then LIN a1,a,b by ANALMETR:def 10;
then LIN a19,a9,b9 by ANALMETR:40;
then LIN a9,b9,a19 by AFF_1:6;
then LIN a,b,a1 by ANALMETR:40;
then
A23: a,b // a,a1 by ANALMETR:def 10;
LIN o9,a9,b9 by A12,ANALMETR:40;
then LIN a9,b9,o9 by AFF_1:6;
then LIN a,b,o by ANALMETR:40;
then a,b // a,o by ANALMETR:def 10;
then o,a // a,b by ANALMETR:59;
then a,a1 // o,a by A7,A23,ANALMETR:60;
then a,a1 // a,o by ANALMETR:59;
then LIN a,a1,o by ANALMETR:def 10;
then LIN a9,a19,o9 by ANALMETR:40;
then LIN o9,a9,a19 by AFF_1:6;
then LIN o,a,a1 by ANALMETR:40;
then o,a // o,a1 by ANALMETR:def 10;
then o,a _|_ o,a by A3,A9,ANALMETR:62;
hence contradiction by A2,ANALMETR:39;
end;
A24: LIN o9,a9,b9 by A12,ANALMETR:40;
A25: LIN o9,a19,b19 by A13,ANALMETR:40;
A26: LIN b9,o9,a9 by A24,AFF_1:6;
A27: LIN b19,o9,a19 by A25,AFF_1:6;
A28: LIN b,o,a by A26,ANALMETR:40;
A29: LIN b1,o,a1 by A27,ANALMETR:40;
A30: b,o // b,a by A28,ANALMETR:def 10;
A31: b1,o // b1,a1 by A29,ANALMETR:def 10;
b,o _|_ b1,o by A10,ANALMETR:61;
then b,a _|_ b1,o by A4,A30,ANALMETR:62;
then b1,a1 _|_ b,a by A5,A31,ANALMETR:62;
then b,c // b,a by A15,A21,A22,ANALMETR:63;
then LIN b,c,a by ANALMETR:def 10;
then LIN b9,c9,a9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
then LIN a,b,c by ANALMETR:40;
then
A32: a,b // a,c by ANALMETR:def 10;
LIN o9,a9,b9 by A12,ANALMETR:40;
then LIN a9,b9,o9 by AFF_1:6;
then LIN a,b,o by ANALMETR:40;
then a,b // a,o by ANALMETR:def 10;
then a,c // a,o by A7,A32,ANALMETR:60;
then LIN a,c,o by ANALMETR:def 10;
then LIN a9,c9,o9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
then a,c // o,c by A14,A20,ANALMETR:63;
then c,a // c,o by ANALMETR:59;
then c9,a9 // c9,o9 by ANALMETR:36;
then LIN c9,a9,o9 by AFF_1:def 1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
then consider c29 such that
A33: LIN a19,e19,c29 and
A34: LIN o9,e29,c29 by AFF_1:60;
reconsider c2=c29 as Element of X;
take c2;
a19,e19 // a19,c29 by A33,AFF_1:def 1;
then a1,e1 // a1,c2 by ANALMETR:36;
then
A35: a1,c1 // a1,c2 by A16,A17,ANALMETR:60;
LIN o,e2,c2 by A34,ANALMETR:40;
then
A36: o,e2 // o,c2 by ANALMETR:def 10;
o<>c2
proof
assume o=c2;
then a1,c1 // o,a1 by A35,ANALMETR:59;
then
A37: o,a _|_ a1,c1 by A3,A9,ANALMETR:62;
a1<>c1
proof
assume
A38: a1=c1;
A39: a1<>b1
proof
assume a1=b1;
then a1,a // a1,b by A8,ANALMETR:59;
then LIN a1,a,b by ANALMETR:def 10;
then LIN a19,a9,b9 by ANALMETR:40;
then LIN a9,b9,a19 by AFF_1:6;
then LIN a,b,a1 by ANALMETR:40;
then
A40: a,b // a,a1 by ANALMETR:def 10;
LIN o9,a9,b9 by A12,ANALMETR:40;
then LIN a9,b9,o9 by AFF_1:6;
then LIN a,b,o by ANALMETR:40;
then a,b // a,o by ANALMETR:def 10;
then o,a // a,b by ANALMETR:59;
then a,a1 // o,a by A7,A40,ANALMETR:60;
then a,a1 // a,o by ANALMETR:59;
then LIN a,a1,o by ANALMETR:def 10;
then LIN a9,a19,o9 by ANALMETR:40;
then LIN o9,a9,a19 by AFF_1:6;
then LIN o,a,a1 by ANALMETR:40;
then o,a // o,a1 by ANALMETR:def 10;
then o,a _|_ o,a by A3,A9,ANALMETR:62;
hence contradiction by A2,ANALMETR:39;
end;
LIN o9,a19,b19 by A13,ANALMETR:40;
then LIN b19,a19,o9 by AFF_1:6;
then LIN b1,a1,o by ANALMETR:40;
then b1,a1 // b1,o by ANALMETR:def 10;
then b1,a1 // o,b1 by ANALMETR:59;
then b,c _|_ o,b1 by A15,A38,A39,ANALMETR:62;
then
A41: b,c // o,b by A5,A10,ANALMETR:63;
A42: LIN o9,a9,b9 by A12,ANALMETR:40;
then
A43: LIN b9,a9,o9 by AFF_1:6;
A44: LIN a9,b9,o9 by A42,AFF_1:6;
A45: LIN b,a,o by A43,ANALMETR:40;
A46: LIN a,b,o by A44,ANALMETR:40;
A47: b,a // b,o by A45,ANALMETR:def 10;
A48: a,b // a,o by A46,ANALMETR:def 10;
o,b // b,a by A47,ANALMETR:59;
then b,a // b,c by A4,A41,ANALMETR:60;
then LIN b,a,c by ANALMETR:def 10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
then LIN a,b,c by ANALMETR:40;
then a,b // a,c by ANALMETR:def 10;
then a,o // a,c by A7,A48,ANALMETR:60;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
then o,a // a,c by A14,A37,ANALMETR:63;
then a,c // a,o by ANALMETR:59;
then LIN a,c,o by ANALMETR:def 10;
then LIN a9,c9,o9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
hence thesis by A18,A19,A35,A36,ANALMETR:62,def 10;
end;
then consider c2 such that
A49: LIN a1,c1,c2 and
A50: o,c _|_ o,c2 and
A51: o<>c2;
reconsider c29=c2 as Element of the AffinStruct of X;
A52: b<>c & a1<>b1 & a1<>c1
proof
assume
A53: b=c or a1=b1 or a1=c1;
A54: now
assume b=c;
then LIN o9,a9,c9 by A12,ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
A55: now
assume a1=b1;
then a1,a // a1,b by A8,ANALMETR:59;
then LIN a1,a,b by ANALMETR:def 10;
then LIN a19,a9,b9 by ANALMETR:40;
then LIN a9,b9,a19 by AFF_1:6;
then LIN a,b,a1 by ANALMETR:40;
then
A56: a,b // a,a1 by ANALMETR:def 10;
LIN o9,a9,b9 by A12,ANALMETR:40;
then LIN a9,b9,o9 by AFF_1:6;
then LIN a,b,o by ANALMETR:40;
then a,b // a,o by ANALMETR:def 10;
then o,a // a,b by ANALMETR:59;
then a,a1 // o,a by A7,A56,ANALMETR:60;
then a,a1 // a,o by ANALMETR:59;
then LIN a,a1,o by ANALMETR:def 10;
then LIN a9,a19,o9 by ANALMETR:40;
then LIN o9,a9,a19 by AFF_1:6;
then LIN o,a,a1 by ANALMETR:40;
then o,a // o,a1 by ANALMETR:def 10;
then o,a _|_ o,a by A3,A9,ANALMETR:62;
hence contradiction by A2,ANALMETR:39;
end;
now
assume
A57: a1=c1;
LIN o9,a19,b19 by A13,ANALMETR:40;
then LIN b19,a19,o9 by AFF_1:6;
then LIN b1,a1,o by ANALMETR:40;
then b1,a1 // b1,o by ANALMETR:def 10;
then b1,a1 // o,b1 by ANALMETR:59;
then b,c _|_ o,b1 by A15,A55,A57,ANALMETR:62;
then
A58: b,c // o,b by A5,A10,ANALMETR:63;
A59: LIN o9,a9,b9 by A12,ANALMETR:40;
then
A60: LIN b9,a9,o9 by AFF_1:6;
A61: LIN a9,b9,o9 by A59,AFF_1:6;
A62: LIN b,a,o by A60,ANALMETR:40;
A63: LIN a,b,o by A61,ANALMETR:40;
A64: b,a // b,o by A62,ANALMETR:def 10;
A65: a,b // a,o by A63,ANALMETR:def 10;
o,b // b,a by A64,ANALMETR:59;
then b,a // b,c by A4,A58,ANALMETR:60;
then LIN b,a,c by ANALMETR:def 10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
then LIN a,b,c by ANALMETR:40;
then a,b // a,c by ANALMETR:def 10;
then a,o // a,c by A7,A65,ANALMETR:60;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
hence contradiction by A53,A54,A55;
end;
a1,c1 // a1,c2 by A49,ANALMETR:def 10;
then a,c _|_ a1,c2 by A14,A52,ANALMETR:62;
then b,c _|_ b1,c2 by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A50,A51;
then b1,c1 // b1,c2 by A15,A52,ANALMETR:63;
then
A66: LIN b1,c1,c2 by ANALMETR:def 10;
not LIN b1,a1,c1
proof
assume LIN b1,a1,c1;
then LIN b19,a19,c19 by ANALMETR:40;
then LIN a19,b19,c19 by AFF_1:6;
then a19,b19 // a19,c19 by AFF_1:def 1;
then
A67: a1,b1 // a1,c1 by ANALMETR:36;
LIN o9,a19,b19 by A13,ANALMETR:40;
then LIN a19,b19,o9 by AFF_1:6;
then LIN a1,b1,o by ANALMETR:40;
then a1,b1 // a1,o by ANALMETR:def 10;
then a1,c1 // a1,o by A52,A67,ANALMETR:60;
then a,c _|_ a1,o by A14,A52,ANALMETR:62;
then
A68: o,a1 _|_ a,c by ANALMETR:61;
o,a1 _|_ a,o by A9,ANALMETR:61;
then a,o // a,c by A3,A68,ANALMETR:63;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A11,ANALMETR:40;
end;
then
A69: not LIN b19,a19,c19 by ANALMETR:40;
A70: LIN b19,c19,c29 by A66,ANALMETR:40;
a1,c1 // a1,c2 by A49,ANALMETR:def 10;
then a19,c19 // a19,c29 by ANALMETR:36;
hence thesis by A50,A69,A70,AFF_1:14;
end;
theorem
X is satisfying_LIN implies X is satisfying_ODES
proof
assume
A1: X is satisfying_LIN;
let o,a,a1,b,b1,c,c1;
assume that
A2: o,a _|_ o,a1 and
A3: o,b _|_ o,b1 and
A4: o,c _|_ o,c1 and
A5: a,b _|_ a1,b1 and
A6: a,c _|_ a1,c1 and
A7: not o,c // o,a and
A8: not o,a // o,b;
A9: X is satisfying_LIN1 by A1,Th3;
now
let o,a,a1,b,b1,c,c1;
assume
A10: X is satisfying_LIN;
assume that
A11: o,a _|_ o,a1 and
A12: o,b _|_ o,b1 and
A13: o,c _|_ o,c1 and
A14: a,b _|_ a1,b1 and
A15: a,c _|_ a1,c1 and
A16: not o,c // o,a and
A17: not o,a // o,b;
assume
A18: not o,b // a,c;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1,o9=o
as Element of the AffinStruct of X;
A19: now
assume
A20: o=a1;
then
A21: a1,b1 _|_ b,a1 by A12,ANALMETR:61;
A22: a1,b1 _|_ b,a by A14,ANALMETR:61;
not b,a1 // b,a
proof
assume b,a1 // b,a;
then LIN b,o,a by A20,ANALMETR:def 10;
then LIN b9,o9,a9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A17,ANALMETR:def 10;
end;
then
A23: a1=b1 by A21,A22,ANALMETR:63;
A24: a1,c1 _|_ c,a1 by A13,A20,ANALMETR:61;
a1,c1 _|_ c,a by A15,ANALMETR:61;
then
A25: c,a1 // c,a or a1=c1 by A24,ANALMETR:63;
not c,a1 // c,a
proof
assume c,a1 // c,a;
then LIN c,o,a by A20,ANALMETR:def 10;
then LIN c9,o9,a9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A16,ANALMETR:def 10;
end;
hence b,c _|_ b1,c1 by A23,A25,ANALMETR:39;
end;
A26: now
assume that
A27: LIN o,b,c and
A28: o<>a1;
A29: o<>b by A17,ANALMETR:39;
A30: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:39;
then o9,a9 // o9,c9 by ANALMETR:36;
then o9,c9 // o9,a9 by AFF_1:4;
hence contradiction by A16,ANALMETR:36;
end;
A31: o<>b1
proof
assume
A32: o=b1;
a1,o _|_ a,o by A11,ANALMETR:61;
then a,o // a,b by A14,A28,A32,ANALMETR:63;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A17,ANALMETR:def 10;
end;
o,b // o,c by A27,ANALMETR:def 10;
then o,c _|_ o,b1 by A12,A29,ANALMETR:62;
then o,b1 // o,c1 by A13,A30,ANALMETR:63;
then LIN o,b1,c1 by ANALMETR:def 10;
then LIN o9,b19,c19 by ANALMETR:40;
then LIN b19,o9,c19 by AFF_1:6;
then LIN b1,o,c1 by ANALMETR:40;
then
A33: b1,o // b1,c1 by ANALMETR:def 10;
b1,o _|_ b,o by A12,ANALMETR:61;
then
A34: b,o _|_ b1,c1 by A31,A33,ANALMETR:62;
LIN o9,b9,c9 by A27,ANALMETR:40;
then LIN b9,o9,c9 by AFF_1:6;
then LIN b,o,c by ANALMETR:40;
then b,o // b,c by ANALMETR:def 10;
hence b,c _|_ b1,c1 by A29,A34,ANALMETR:62;
end;
A35: now
assume that
A36: LIN a,b,c and not LIN o,b,c and
A37: o<>a1;
A38: a<>c
proof
assume a=c;
then a,o // a,c by ANALMETR:39;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A16,ANALMETR:def 10;
end;
A39: a<>b
proof
assume a=b;
then a,o // a,b by ANALMETR:39;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A17,ANALMETR:def 10;
end;
A40: a1<>b1 by A11,A12,A17,A37,ANALMETR:63;
a,b // a,c by A36,ANALMETR:def 10;
then a,c _|_ a1,b1 by A14,A39,ANALMETR:62;
then a1,b1 // a1,c1 by A15,A38,ANALMETR:63;
then LIN a1,b1,c1 by ANALMETR:def 10;
then LIN a19,b19,c19 by ANALMETR:40;
then LIN b19,a19,c19 by AFF_1:6;
then LIN b1,a1,c1 by ANALMETR:40;
then
A41: b1,a1 // b1,c1 by ANALMETR:def 10;
b1,a1 _|_ b,a by A14,ANALMETR:61;
then
A42: b,a _|_ b1,c1 by A40,A41,ANALMETR:62;
LIN a9,b9,c9 by A36,ANALMETR:40;
then LIN b9,a9,c9 by AFF_1:6;
then LIN b,a,c by ANALMETR:40;
then b,a // b,c by ANALMETR:def 10;
hence b,c _|_ b1,c1 by A39,A42,ANALMETR:62;
end;
now
assume that
A43: not LIN a,b,c and
A44: not LIN o,b,c and
A45: o<>a1;
A46: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:39;
then o9,a9 // o9,c9 by ANALMETR:36;
then o9,c9 // o9,a9 by AFF_1:4;
hence contradiction by A16,ANALMETR:36;
end;
A47: o<>b1
proof
assume
A48: o=b1;
a1,o _|_ a,o by A11,ANALMETR:61;
then a,o // a,b by A14,A45,A48,ANALMETR:63;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A17,ANALMETR:def 10;
end;
A49: o<>c1
proof
assume
A50: o=c1;
a1,o _|_ a,o by A11,ANALMETR:61;
then a,o // a,c by A15,A45,A50,ANALMETR:63;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A16,ANALMETR:def 10;
end;
A51: o<>a by A16,ANALMETR:39;
A52: o<>b by A17,ANALMETR:39;
A53: a<>c by A13,A16,A49,ANALMETR:63;
A54: a1<>c1 by A11,A13,A16,A49,ANALMETR:63;
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
A55: o,b // o,p and
A56: o<>p by ANALMETR:39;
reconsider p9=p as Element of the AffinStruct of X;
consider p1 be Element of X such that
A57: a,c // a,p1 and
A58: a<>p1 by ANALMETR:39;
reconsider p19=p1 as Element of the AffinStruct of X;
not o,p // a,p1
proof
assume o,p // a,p1;
then a,p1 // o,b by A55,A56,ANALMETR:60;
hence contradiction by A18,A57,A58,ANALMETR:60;
end;
then not o9,p9 // a9,p19 by ANALMETR:36;
then consider e9 be Element of the AffinStruct of X such that
A59: LIN o9,p9,e9 and
A60: LIN a9,p19,e9 by AFF_1:60;
reconsider e=e9 as Element of X;
LIN o,p,e by A59,ANALMETR:40;
then o,p // o,e by ANALMETR:def 10;
then o,e // o,b by A55,A56,ANALMETR:60;
then
A61: LIN o,e,b by ANALMETR:def 10;
LIN a,p1,e by A60,ANALMETR:40;
then a,p1 // a,e by ANALMETR:def 10;
then a,c // a,e by A57,A58,ANALMETR:60;
then
A62: LIN a,c,e by ANALMETR:def 10;
A63: c <>e
proof
assume c = e;
then LIN o9,c9,b9 by A61,ANALMETR:40;
then LIN o9,b9,c9 by AFF_1:6;
hence contradiction by A44,ANALMETR:40;
end;
b<>e
proof
assume b=e;
then LIN a9,c9,b9 by A62,ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A43,ANALMETR:40;
end;
hence thesis by A61,A62,A63;
end;
then consider e be Element of X such that
A64: LIN o,e,b and
A65: LIN a,c,e and
A66: e<>c and
A67: e<>b;
reconsider e9=e as Element of the AffinStruct of X;
ex e1 be Element of X st LIN o,e1,b1 & LIN a1,c1,e1
proof
consider p be Element of X such that
A68: o,b1 // o,p and
A69: o<>p by ANALMETR:39;
reconsider p9=p as Element of the AffinStruct of X;
consider p1 be Element of X such that
A70: a1,c1 // a1,p1 and
A71: a1<>p1 by ANALMETR:39;
reconsider p19=p1 as Element of the AffinStruct of X;
A72: not o,b1 // a1,c1
proof
assume o,b1 // a1,c1;
then a1,c1 _|_ o,b by A12,A47,ANALMETR:62;
hence contradiction by A15,A18,A54,ANALMETR:63;
end;
not o,p // a1,p1
proof
assume o,p // a1,p1;
then a1,p1 // o,b1 by A68,A69,ANALMETR:60;
hence contradiction by A70,A71,A72,ANALMETR:60;
end;
then not o9,p9 // a19,p19 by ANALMETR:36;
then consider e19 be Element of the AffinStruct of X such that
A73: LIN o9,p9,e19 and
A74: LIN a19,p19,e19 by AFF_1:60;
reconsider e1=e19 as Element of X;
LIN o,p,e1 by A73,ANALMETR:40;
then o,p // o,e1 by ANALMETR:def 10;
then o,e1 // o,b1 by A68,A69,ANALMETR:60;
then
A75: LIN o,e1,b1 by ANALMETR:def 10;
LIN a1,p1,e1 by A74,ANALMETR:40;
then a1,p1 // a1,e1 by ANALMETR:def 10;
then a1,c1 // a1,e1 by A70,A71,ANALMETR:60;
then LIN a1,c1,e1 by ANALMETR:def 10;
hence thesis by A75;
end;
then consider e1 be Element of X such that
A76: LIN o,e1,b1 and
A77: LIN a1,c1,e1;
reconsider e19=e1 as Element of the AffinStruct of X;
o,e // o,b by A64,ANALMETR:def 10;
then o9,e9 // o9,b9 by ANALMETR:36;
then o9,b9 // o9,e9 by AFF_1:4;
then o,b // o,e by ANALMETR:36;
then
A78: o,b1 _|_ o,e by A12,A52,ANALMETR:62;
o,e1 // o,b1 by A76,ANALMETR:def 10;
then o9,e19 // o9,b19 by ANALMETR:36;
then o9,b19 // o9,e19 by AFF_1:4;
then
A79: o,b1 // o,e1 by ANALMETR:36;
A80: o<>e
proof
assume o=e;
then LIN a9,c9,o9 by A65,ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A16,ANALMETR:def 10;
end;
A81: o<>e1
proof
assume o=e1;
then LIN a19,c19,o9 by A77,ANALMETR:40;
then LIN o9,a19,c19 by AFF_1:6;
then LIN o,a1,c1 by ANALMETR:40;
then o,a1 // o,c1 by ANALMETR:def 10;
then o,c1 _|_ o,a by A11,A45,ANALMETR:62;
hence contradiction by A13,A16,A49,ANALMETR:63;
end;
A82: o,e _|_ o,e1 by A47,A78,A79,ANALMETR:62;
A83: not LIN o,a,e
proof
assume LIN o,a,e;
then o,a // o,e by ANALMETR:def 10;
then o9,a9 // o9,e9 by ANALMETR:36;
then o9,e9 // o9,a9 by AFF_1:4;
then
A84: o,e // o,a by ANALMETR:36;
o,e // o,b by A64,ANALMETR:def 10;
hence contradiction by A17,A80,A84,ANALMETR:60;
end;
a,c // a,e by A65,ANALMETR:def 10;
then a9,c9 // a9,e9 by ANALMETR:36;
then a9,c9 // e9,a9 by AFF_1:4;
then a,c // e,a by ANALMETR:36;
then
A85: a1,c1 _|_ e,a by A15,A53,ANALMETR:62;
a1,c1 // a1,e1 by A77,ANALMETR:def 10;
then e,a _|_ a1,e1 by A54,A85,ANALMETR:62;
then
A86: e,a _|_ e1,a1 by ANALMETR:61;
b,a _|_ b1,a1 by A14,ANALMETR:61;
then
A87: e,e1 // b,b1 by A10,A11,A12,A45,A47,A51,A52,A64,A67,A76,A80,A81,A82,A83
,A86;
A88: not LIN o,c,e
proof
assume LIN o,c,e;
then LIN o9,c9,e9 by ANALMETR:40;
then LIN c9,e9,o9 by AFF_1:6;
then c9,e9 // c9,o9 by AFF_1:def 1;
then
A89: c,e // c,o by ANALMETR:36;
LIN a9,c9,e9 by A65,ANALMETR:40;
then LIN c9,e9,a9 by AFF_1:6;
then c9,e9 // c9,a9 by AFF_1:def 1;
then c,e // c,a by ANALMETR:36;
then c,o // c,a by A66,A89,ANALMETR:60;
then LIN c,o,a by ANALMETR:def 10;
then LIN c9,o9,a9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A16,ANALMETR:def 10;
end;
LIN a9,c9,e9 by A65,ANALMETR:40;
then LIN c9,a9,e9 by AFF_1:6;
then c9,a9 // c9,e9 by AFF_1:def 1;
then a9,c9 // e9,c9 by AFF_1:4;
then a,c // e,c by ANALMETR:36;
then
A90: a1,c1 _|_ e,c by A15,A53,ANALMETR:62;
LIN a19,c19,e19 by A77,ANALMETR:40;
then LIN c19,a19,e19 by AFF_1:6;
then c19, a19 // c19, e19 by AFF_1:def 1;
then a19,c19 // e19,c19 by AFF_1:4;
then a1,c1 // e1,c1 by ANALMETR:36;
then e,c _|_ e1,c1 by A54,A90,ANALMETR:62;
hence b,c _|_ b1,c1 by A9,A12,A13,A46,A47,A49,A52,A64,A67,A76,A80,A81,A82
,A87,A88;
end;
hence b,c _|_ b1,c1 by A19,A26,A35;
end;
then
A91: not o,b // a,c implies b,c _|_ b1,c1 by A1,A2,A3,A4,A5,A6,A7,A8;
A92: now
let o,a,a1,b,b1,c,c1;
assume that
A93: o,a _|_ o,a1 and
A94: o,b _|_ o,b1 and
A95: o,c _|_ o,c1 and
A96: a,b _|_ a1,b1 and
A97: a,c _|_ a1,c1 and
A98: not o,c // o,a and
A99: not o,a // o,b;
assume
A100: not o,a // c,b;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1,o9=o
as Element of the AffinStruct of X;
A101: now
assume
A102: o=a1;
then
A103: a1,b1 _|_ b,a1 by A94,ANALMETR:61;
A104: a1,b1 _|_ b,a by A96,ANALMETR:61;
not b,a1 // b,a
proof
assume b,a1 // b,a;
then LIN b,o,a by A102,ANALMETR:def 10;
then LIN b9,o9,a9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A99,ANALMETR:def 10;
end;
then
A105: a1=b1 by A103,A104,ANALMETR:63;
A106: a1,c1 _|_ c,a1 by A95,A102,ANALMETR:61;
a1,c1 _|_ c,a by A97,ANALMETR:61;
then
A107: c,a1 // c,a or a1=c1 by A106,ANALMETR:63;
not c,a1 // c,a
proof
assume c,a1 // c,a;
then LIN c,o,a by A102,ANALMETR:def 10;
then LIN c9,o9,a9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A98,ANALMETR:def 10;
end;
hence b,c _|_ b1,c1 by A105,A107,ANALMETR:39;
end;
A108: now
assume that
A109: LIN o,b,c and
A110: o<>a1;
A111: o<>b by A99,ANALMETR:39;
A112: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:39;
then o9,a9 // o9,c9 by ANALMETR:36;
then o9,c9 // o9,a9 by AFF_1:4;
hence contradiction by A98,ANALMETR:36;
end;
A113: o<>b1
proof
assume
A114: o=b1;
a1,o _|_ a,o by A93,ANALMETR:61;
then a,o // a,b by A96,A110,A114,ANALMETR:63;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A99,ANALMETR:def 10;
end;
o,b // o,c by A109,ANALMETR:def 10;
then o,c _|_ o,b1 by A94,A111,ANALMETR:62;
then o,b1 // o,c1 by A95,A112,ANALMETR:63;
then LIN o,b1,c1 by ANALMETR:def 10;
then LIN o9,b19,c19 by ANALMETR:40;
then LIN b19,o9,c19 by AFF_1:6;
then LIN b1,o,c1 by ANALMETR:40;
then
A115: b1,o // b1,c1 by ANALMETR:def 10;
b1,o _|_ b,o by A94,ANALMETR:61;
then
A116: b,o _|_ b1,c1 by A113,A115,ANALMETR:62;
LIN o9,b9,c9 by A109,ANALMETR:40;
then LIN b9,o9,c9 by AFF_1:6;
then LIN b,o,c by ANALMETR:40;
then b,o // b,c by ANALMETR:def 10;
hence b,c _|_ b1,c1 by A111,A116,ANALMETR:62;
end;
A117: now
assume that
A118: LIN a,b,c and not LIN o,b,c and
A119: o<>a1;
A120: a<>c
proof
assume a=c;
then a,o // a,c by ANALMETR:39;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A98,ANALMETR:def 10;
end;
A121: a<>b
proof
assume a=b;
then a,o // a,b by ANALMETR:39;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A99,ANALMETR:def 10;
end;
A122: a1<>b1 by A93,A94,A99,A119,ANALMETR:63;
a,b // a,c by A118,ANALMETR:def 10;
then a,c _|_ a1,b1 by A96,A121,ANALMETR:62;
then a1,b1 // a1,c1 by A97,A120,ANALMETR:63;
then LIN a1,b1,c1 by ANALMETR:def 10;
then LIN a19,b19,c19 by ANALMETR:40;
then LIN b19,a19,c19 by AFF_1:6;
then LIN b1,a1,c1 by ANALMETR:40;
then
A123: b1,a1 // b1,c1 by ANALMETR:def 10;
b1,a1 _|_ b,a by A96,ANALMETR:61;
then
A124: b,a _|_ b1,c1 by A122,A123,ANALMETR:62;
LIN a9,b9,c9 by A118,ANALMETR:40;
then LIN b9,a9,c9 by AFF_1:6;
then LIN b,a,c by ANALMETR:40;
then b,a // b,c by ANALMETR:def 10;
hence b,c _|_ b1,c1 by A121,A124,ANALMETR:62;
end;
now
assume that
A125: not LIN a,b,c and
A126: not LIN o,b,c and
A127: o<>a1;
A128: o<>a by A98,ANALMETR:39;
A129: o<>c
proof
assume o=c;
then o,a // o,c by ANALMETR:39;
then o9,a9 // o9,c9 by ANALMETR:36;
then o9,c9 // o9,a9 by AFF_1:4;
hence contradiction by A98,ANALMETR:36;
end;
A130: o<>b1
proof
assume
A131: o=b1;
a1,o _|_ a,o by A93,ANALMETR:61;
then a,o // a,b by A96,A127,A131,ANALMETR:63;
then LIN a,o,b by ANALMETR:def 10;
then LIN a9,o9,b9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A99,ANALMETR:def 10;
end;
A132: o<>c1
proof
assume
A133: o=c1;
a1,o _|_ a,o by A93,ANALMETR:61;
then a,o // a,c by A97,A127,A133,ANALMETR:63;
then LIN a,o,c by ANALMETR:def 10;
then LIN a9,o9,c9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A98,ANALMETR:def 10;
end;
A134: o<>a by A98,ANALMETR:39;
A135: o<>b by A99,ANALMETR:39;
A136: a<>a1 by A93,A128,ANALMETR:39;
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
A137: o,a // o,p and
A138: o<>p by ANALMETR:39;
reconsider p9=p as Element of the AffinStruct of X;
consider p1 be Element of X such that
A139: b,c // b,p1 and
A140: b<>p1 by ANALMETR:39;
reconsider p19=p1 as Element of the AffinStruct of X;
not o,p // b,p1
proof
assume o,p // b,p1;
then b,p1 // o,a by A137,A138,ANALMETR:60;
then o,a // b,c by A139,A140,ANALMETR:60;
then o9,a9 // b9,c9 by ANALMETR:36;
then o9,a9 // c9,b9 by AFF_1:4;
hence contradiction by A100,ANALMETR:36;
end;
then not o9,p9 // b9,p19 by ANALMETR:36;
then consider e9 be Element of the AffinStruct of X such that
A141: LIN o9,p9,e9 and
A142: LIN b9,p19,e9 by AFF_1:60;
reconsider e=e9 as Element of X;
LIN o,p,e by A141,ANALMETR:40;
then
A143: o,p // o,e by ANALMETR:def 10;
then o,e // o,a by A137,A138,ANALMETR:60;
then
A144: LIN o,e,a by ANALMETR:def 10;
LIN b,p1,e by A142,ANALMETR:40;
then b,p1 // b,e by ANALMETR:def 10;
then b,c // b,e by A139,A140,ANALMETR:60;
then
A145: LIN b,c,e by ANALMETR:def 10;
A146: c <>e by A98,A137,A138,A143,ANALMETR:60;
A147: b<>e
proof
assume b=e;
then LIN o9,b9,a9 by A144,ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A99,ANALMETR:def 10;
end;
a<>e
proof
assume a=e;
then LIN b9,c9,a9 by A145,ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A125,ANALMETR:40;
end;
hence thesis by A144,A145,A146,A147;
end;
then consider e be Element of X such that
A148: LIN b,c,e and
A149: LIN o,e,a and
A150: e<>b and
A151: c <>e and
A152: a<>e;
reconsider e9=e as Element of the AffinStruct of X;
ex e1 be Element of X st LIN o,e1,a1 & e,e1 // a,a1
proof
consider p be Element of X such that
A153: o,a1 // o,p and
A154: o<>p by ANALMETR:39;
reconsider p9=p as Element of the AffinStruct of X;
consider p1 be Element of X such that
A155: a,a1 // e,p1 and
A156: e<>p1 by ANALMETR:39;
reconsider p19=p1 as Element of the AffinStruct of X;
not o,p // e,p1
proof
assume o,p // e,p1;
then e,p1 // o,a1 by A153,A154,ANALMETR:60;
then e9,p19 // o9,a19 by ANALMETR:36;
then o9,a19 // e9,p19 by AFF_1:4;
then o,a1 // e,p1 by ANALMETR:36;
then e,p1 _|_ o,a by A93,A127,ANALMETR:62;
then o,a _|_ a,a1 by A155,A156,ANALMETR:62;
then
A157: o,a _|_ a1,a by ANALMETR:61;
o,a _|_ a1,o by A93,ANALMETR:61;
then a1,o // a1,a by A134,A157,ANALMETR:63;
then LIN a1,o,a by ANALMETR:def 10;
then LIN a19,o9,a9 by ANALMETR:40;
then LIN a9,o9,a19 by AFF_1:6;
then a9,o9 // a9,a19 by AFF_1:def 1;
then o9,a9 // a19,a9 by AFF_1:4;
then o,a // a1,a by ANALMETR:36;
then a1,a _|_ a1,a by A134,A157,ANALMETR:62;
hence contradiction by A136,ANALMETR:39;
end;
then not o9,p9 // e9,p19 by ANALMETR:36;
then consider e19 be Element of the AffinStruct of X such that
A158: LIN o9,p9,e19 and
A159: LIN e9,p19,e19 by AFF_1:60;
reconsider e1=e19 as Element of X;
LIN o,p,e1 by A158,ANALMETR:40;
then o,p // o,e1 by ANALMETR:def 10;
then o,e1 // o,a1 by A153,A154,ANALMETR:60;
then
A160: LIN o,e1,a1 by ANALMETR:def 10;
LIN e,p1,e1 by A159,ANALMETR:40;
then e,p1 // e,e1 by ANALMETR:def 10;
then e,e1 // a,a1 by A155,A156,ANALMETR:60;
hence thesis by A160;
end;
then consider e1 be Element of X such that
A161: LIN o,e1,a1 and
A162: e,e1 // a,a1;
reconsider e19=e1 as Element of the AffinStruct of X;
o,e // o,a by A149,ANALMETR:def 10;
then o9,e9 // o9,a9 by ANALMETR:36;
then o9,a9 // o9,e9 by AFF_1:4;
then o,a // o,e by ANALMETR:36;
then
A163: o,a1 _|_ o,e by A93,A134,ANALMETR:62;
o,e1 // o,a1 by A161,ANALMETR:def 10;
then o9,e19 // o9,a19 by ANALMETR:36;
then o9,a19 // o9,e19 by AFF_1:4;
then
A164: o,a1 // o,e1 by ANALMETR:36;
A165: o<>e
proof
assume o=e;
then LIN b9,c9,o9 by A148,ANALMETR:40;
then LIN o9,b9,c9 by AFF_1:6;
hence contradiction by A126,ANALMETR:40;
end;
A166: o<>e1
proof
assume o=e1;
then e9,o9 // a9,a19 by A162,ANALMETR:36;
then o9,e9 // a9,a19 by AFF_1:4;
then
A167: o,e // a,a1 by ANALMETR:36;
o,e // o,a by A149,ANALMETR:def 10;
then
A168: o,a // a,a1 by A165,A167,ANALMETR:60;
then
A169: o,a1 _|_ a,a1 by A93,A134,ANALMETR:62;
o9,a9 // a9,a19 by A168,ANALMETR:36;
then a9,o9 // a9,a19 by AFF_1:4;
then LIN a9,o9,a19 by AFF_1:def 1;
then LIN a19,o9,a9 by AFF_1:6;
then a19,o9 // a19,a9 by AFF_1:def 1;
then o9,a19 // a9,a19 by AFF_1:4;
then o,a1 // a,a1 by ANALMETR:36;
then a,a1 _|_ a,a1 by A127,A169,ANALMETR:62;
hence contradiction by A136,ANALMETR:39;
end;
A170: o,e _|_ o,e1 by A127,A163,A164,ANALMETR:62;
A171: not LIN o,b,a
proof
assume LIN o,b,a;
then o,b // o,a by ANALMETR:def 10;
then o9,b9 // o9,a9 by ANALMETR:36;
then o9,a9 // o9,b9 by AFF_1:4;
hence contradiction by A99,ANALMETR:36;
end;
o,e // o,a by A149,ANALMETR:def 10;
then o9,e9 // o9,a9 by ANALMETR:36;
then o9,a9 // o9,e9 by AFF_1:4;
then o,a // o,e by ANALMETR:36;
then
A172: LIN o,a,e by ANALMETR:def 10;
o,e1 // o,a1 by A161,ANALMETR:def 10;
then o9,e19 // o9,a19 by ANALMETR:36;
then o9,a19 // o9,e19 by AFF_1:4;
then o,a1 // o,e1 by ANALMETR:36;
then
A173: LIN o,a1,e1 by ANALMETR:def 10;
e9,e19 // a9,a19 by A162,ANALMETR:36;
then a9,a19 // e9,e19 by AFF_1:4;
then
A174: a,a1 // e,e1 by ANALMETR:36;
then
A175: e,b _|_ e1,b1 by A9,A93,A94,A96,A127,A130,A134,A135,A152,A165,A166,A170
,A171,A172,A173;
not LIN o,c,a by A98,ANALMETR:def 10;
then
A176: e,c _|_ e1,c1 by A9,A93,A95,A97,A127,A129,A132,A134,A152,A165,A166,A170
,A172,A173,A174;
A177: e1<>b1
proof
assume e1=b1;
then o,b1 // o,a1 by A161,ANALMETR:def 10;
then o,a1 _|_ o,b by A94,A130,ANALMETR:62;
hence contradiction by A93,A99,A127,ANALMETR:63;
end;
A178: c,e _|_ c1,e1 by A176,ANALMETR:61;
A179: LIN b9,c9,e9 by A148,ANALMETR:40;
then LIN c9,e9,b9 by AFF_1:6;
then LIN c,e,b by ANALMETR:40;
then c,e // c,b by ANALMETR:def 10;
then
A180: c,b _|_ c1,e1 by A151,A178,ANALMETR:62;
A181: c <>b
proof
assume c = b;
then LIN o9,b9,c9 by AFF_1:7;
hence contradiction by A126,ANALMETR:40;
end;
b9,c9 // b9,e9 by A179,AFF_1:def 1;
then c9,b9 // e9,b9 by AFF_1:4;
then c,b // e,b by ANALMETR:36;
then e,b _|_ c1,e1 by A180,A181,ANALMETR:62;
then e1,b1 // c1,e1 by A150,A175,ANALMETR:63;
then e19,b19 // c19,e19 by ANALMETR:36;
then e19,b19 // e19,c19 by AFF_1:4;
then LIN e19,b19,c19 by AFF_1:def 1;
then LIN b19,e19,c19 by AFF_1:6;
then b19,e19 // b19,c19 by AFF_1:def 1;
then e19,b19 // b19,c19 by AFF_1:4;
then
A182: e1,b1 // b1,c1 by ANALMETR:36;
LIN b9,e9,c9 by A179,AFF_1:6;
then b9,e9 // b9,c9 by AFF_1:def 1;
then e9,b9 // b9,c9 by AFF_1:4;
then e,b // b,c by ANALMETR:36;
then e1,b1 _|_ b,c by A150,A175,ANALMETR:62;
hence b,c _|_ b1,c1 by A177,A182,ANALMETR:62;
end;
hence b,c _|_ b1,c1 by A101,A108,A117;
end;
then
A183: not o,a // c,b implies b,c _|_ b1,c1 by A2,A3,A4,A5,A6,A7,A8;
now
let o,a,a1,b,b1,c,c1;
assume X is satisfying_LIN;
assume that
A184: o,a _|_ o,a1 and
A185: o,b _|_ o,b1 and
A186: o,c _|_ o,c1 and
A187: a,b _|_ a1,b1 and
A188: a,c _|_ a1,c1 and
A189: not o,c // o,a and
A190: not o,a // o,b;
assume that
A191: o,a // c,b and o,b // a,c;
reconsider a9=a,b9=b,c9=c,o9=o as Element of the AffinStruct of X;
A192: now
assume
A193: o=a1;
then
A194: a1,b1 _|_ b,a1 by A185,ANALMETR:61;
A195: a1,b1 _|_ b,a by A187,ANALMETR:61;
not b,a1 // b,a
proof
assume b,a1 // b,a;
then LIN b,o,a by A193,ANALMETR:def 10;
then LIN b9,o9,a9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A190,ANALMETR:def 10;
end;
then
A196: a1=b1 by A194,A195,ANALMETR:63;
A197: a1,c1 _|_ c,a1 by A186,A193,ANALMETR:61;
a1,c1 _|_ c,a by A188,ANALMETR:61;
then
A198: c,a1 // c,a or a1=c1 by A197,ANALMETR:63;
not c,a1 // c,a
proof
assume c,a1 // c,a;
then LIN c,o,a by A193,ANALMETR:def 10;
then LIN c9,o9,a9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A189,ANALMETR:def 10;
end;
hence b,c _|_ b1,c1 by A196,A198,ANALMETR:39;
end;
A199: now
assume that
A200: o,a1 // c1,b1 and
A201: o<>a1;
o<>a
proof
assume o=a;
then LIN o9,c9,a9 by AFF_1:7;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A189,ANALMETR:def 10;
end;
then c,b _|_ o,a1 by A184,A191,ANALMETR:62;
then c,b _|_ c1,b1 by A200,A201,ANALMETR:62;
hence b,c _|_ b1,c1 by ANALMETR:61;
end;
now
assume that
A202: not o,a1 // c1,b1 and
A203: o<>a1;
A204: o,a1 _|_ o,a by A184,ANALMETR:61;
A205: o,b1 _|_ o,b by A185,ANALMETR:61;
A206: o,c1 _|_ o,c by A186,ANALMETR:61;
A207: a1,b1 _|_ a,b by A187,ANALMETR:61;
A208: a1,c1 _|_ a,c by A188,ANALMETR:61;
A209: not o,c1 // o,a1
proof
assume
A210: o,c1 // o,a1;
o<>c1
proof
assume o=c1;
then a,c _|_ o,a1 by A188,ANALMETR:61;
then a,c // o,a by A184,A203,ANALMETR:63;
then a,c // a,o by ANALMETR:59;
then LIN a,c,o by ANALMETR:def 10;
then LIN a9,c9,o9 by ANALMETR:40;
then LIN o9,c9,a9 by AFF_1:6;
then LIN o,c,a by ANALMETR:40;
hence contradiction by A189,ANALMETR:def 10;
end;
then o,c _|_ o,a1 by A186,A210,ANALMETR:62;
hence contradiction by A184,A189,A203,ANALMETR:63;
end;
not o,a1 // o,b1
proof
assume
A211: o,a1 // o,b1;
A212: o<>b1
proof
assume o=b1;
then a,b _|_ o,a1 by A187,ANALMETR:61;
then a,b // o,a by A184,A203,ANALMETR:63;
then a,b // a,o by ANALMETR:59;
then LIN a,b,o by ANALMETR:def 10;
then LIN a9,b9,o9 by ANALMETR:40;
then LIN o9,a9,b9 by AFF_1:6;
then LIN o,a,b by ANALMETR:40;
hence contradiction by A190,ANALMETR:def 10;
end;
o,a _|_ o,b1 by A184,A203,A211,ANALMETR:62;
hence contradiction by A185,A190,A212,ANALMETR:63;
end;
then b1,c1 _|_ b,c by A92,A202,A204,A205,A206,A207,A208,A209;
hence b,c _|_ b1,c1 by ANALMETR:61;
end;
hence b,c _|_ b1,c1 by A192,A199;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A91,A183;
end;
theorem
X is satisfying_LIN implies X is satisfying_3H
proof
assume
A1: X is satisfying_LIN;
let a,b,c;
assume
A2: not LIN a,b,c;
consider e1 such that
A3: b,c _|_ a,e1 and
A4: a<>e1 by ANALMETR:def 9;
consider e2 such that
A5: a,c _|_ b,e2 and
A6: b<>e2 by ANALMETR:def 9;
reconsider a9=a,b9=b,c9 = c,e19=e1,e29=e2
as Element of the AffinStruct of X;
not a9,e19 // b9,e29
proof
assume a9,e19 // b9,e29;
then a,e1 // b,e2 by ANALMETR:36;
then b,e2 _|_ b,c by A3,A4,ANALMETR:62;
then a,c // b,c by A5,A6,ANALMETR:63;
then a9,c9 // b9,c9 by ANALMETR:36;
then c9,a9 // c9,b9 by AFF_1:4;
then LIN c9,a9,b9 by AFF_1:def 1;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
then consider d9 be Element of the AffinStruct of X such that
A7: LIN a9,e19,d9 and
A8: LIN b9,e29,d9 by AFF_1:60;
reconsider d=d9 as Element of X;
take d;
LIN b,e2,d by A8,ANALMETR:40;
then
A9: b,e2 // b,d by ANALMETR:def 10;
then
A10: a,c _|_ b,d by A5,A6,ANALMETR:62;
then
A11: d,b _|_ a,c by ANALMETR:61;
LIN a,e1,d by A7,ANALMETR:40;
then
A12: a,e1 // a,d by ANALMETR:def 10;
then
A13: b,c _|_ a,d by A3,A4,ANALMETR:62;
then
A14: d,a _|_ b,c by ANALMETR:61;
A15: X is satisfying_LIN1 by A1,Th3;
A16: now
assume
A17: d<>c;
now
assume
A18: b<>d;
not b9,d9 // a9,c9
proof
assume b9,d9 // a9,c9;
then a9,c9 // b9,d9 by AFF_1:4;
then
A19: a,c // b,d by ANALMETR:36;
a<>c
proof
assume a= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then b,d _|_ b,d by A10,A19,ANALMETR:62;
hence contradiction by A18,ANALMETR:39;
end;
then consider o9 be Element of the AffinStruct of X such that
A20: LIN b9,d9,o9 and
A21: LIN a9,c9,o9 by AFF_1:60;
reconsider o=o9 as Element of X;
now
assume
A22: d<>a;
A23: o<>a
proof
assume
A24: o = a;
then LIN b,d,a by A20,ANALMETR:40;
then b,d // b,a by ANALMETR:def 10;
then b,a _|_ a,c by A10,A18,ANALMETR:62;
then
A25: a,b _|_ a,c by ANALMETR:61;
LIN a9,b9,d9 by A20,A24,AFF_1:6;
then LIN a,b,d by ANALMETR:40;
then
A26: a,b // a,d by ANALMETR:def 10;
a<>b
proof
assume a=b;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then a,d _|_ a,c by A25,A26,ANALMETR:62;
then d,a _|_ a,c by ANALMETR:61;
then a,c // b,c by A14,A22,ANALMETR:63;
then c,a // c,b by ANALMETR:59;
then LIN c,a,b by ANALMETR:def 10;
then LIN c9,a9,b9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
A27: c <>o
proof
assume
A28: c = o;
then LIN b,d,c by A20,ANALMETR:40;
then b,d // b,c by ANALMETR:def 10;
then
A29: b,c _|_ a,c by A10,A18,ANALMETR:62;
b<>c
proof
assume b = c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then a,d // a,c by A13,A29,ANALMETR:63;
then LIN a,d,c by ANALMETR:def 10;
then LIN a9,d9,c9 by ANALMETR:40;
then LIN c9,d9,a9 by AFF_1:6;
then LIN c,d,a by ANALMETR:40;
then
A30: c,d // c,a by ANALMETR:def 10;
LIN c9,d9,b9 by A20,A28,AFF_1:6;
then LIN c,d,b by ANALMETR:40;
then c,d // c,b by ANALMETR:def 10;
then c,a // c,b by A17,A30,ANALMETR:60;
then LIN c,a,b by ANALMETR:def 10;
then LIN c9,a9,b9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
consider e1 such that
A31: a,c // a,e1 and
A32: a<>e1 by ANALMETR:39;
consider e2 such that
A33: b,c // d,e2 and
A34: d<>e2 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not a9,e19 // d9,e29
proof
assume a9,e19 // d9,e29;
then a,e1 // d,e2 by ANALMETR:36;
then d,e2 // a,c by A31,A32,ANALMETR:60;
then a,c // b,c by A33,A34,ANALMETR:60;
then c,a // c,b by ANALMETR:59;
then LIN c,a,b by ANALMETR:def 10;
then LIN c9,a9,b9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
then consider d19 such that
A35: LIN a9,e19,d19 and
A36: LIN d9,e29,d19 by AFF_1:60;
reconsider d1=d19 as Element of X;
LIN a,e1,d1 by A35,ANALMETR:40;
then a,e1 // a,d1 by ANALMETR:def 10;
then
A37: a,c // a,d1 by A31,A32,ANALMETR:60;
then
A38: LIN a,c,d1 by ANALMETR:def 10;
LIN d,e2,d1 by A36,ANALMETR:40;
then d,e2 // d,d1 by ANALMETR:def 10;
then
A39: b,c // d,d1 by A33,A34,ANALMETR:60;
A40: o<>d
proof
assume
A41: o = d;
then
A42: a,o _|_ b,c by A3,A4,A12,ANALMETR:62;
LIN a,c,o by A21,ANALMETR:40;
then a,c // a,o by ANALMETR:def 10;
then
A43: a,c _|_ b,c by A23,A42,ANALMETR:62;
a<>c
proof
assume a= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then b,o // b,c by A10,A41,A43,ANALMETR:63;
then LIN b,o,c by ANALMETR:def 10;
then LIN b9,o9,c9 by ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then LIN c,o,b by ANALMETR:40;
then
A44: c,o // c,b by ANALMETR:def 10;
LIN c9,o9,a9 by A21,AFF_1:6;
then LIN c,o,a by ANALMETR:40;
then c,o // c,a by ANALMETR:def 10;
then c,b // c,a by A27,A44,ANALMETR:60;
then LIN c,b,a by ANALMETR:def 10;
then LIN c9,b9,a9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
A45: o<>d1
proof
assume
A46: o = d1;
LIN o9,d9,b9 by A20,AFF_1:6;
then LIN o,d,b by ANALMETR:40;
then o,d // o,b by ANALMETR:def 10;
then d,o // b,o by ANALMETR:59;
then b,c //b,o by A39,A40,A46,ANALMETR:60;
then LIN b,c,o by ANALMETR:def 10;
then LIN b9,c9,o9 by ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then LIN c,o,b by ANALMETR:40;
then
A47: c,o // c,b by ANALMETR:def 10;
LIN c9,o9,a9 by A21,AFF_1:6;
then LIN c,o,a by ANALMETR:40;
then c,o // c,a by ANALMETR:def 10;
then c,a // c,b by A27,A47,ANALMETR:60;
then LIN c,a,b by ANALMETR:def 10;
then LIN c9,a9,b9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
A48: o<>b
proof
assume o=b;
then LIN a9,b9,c9 by A21,AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
A49: d1<>c
proof
assume
A50: d1 = c;
A51: b<>c
proof
assume b = c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
c,b // c,d by A39,A50,ANALMETR:59;
then LIN c,b,d by ANALMETR:def 10;
then
A52: LIN c9,b9,d9 by ANALMETR:40;
b,c // c,d by A39,A50,ANALMETR:59;
then d,a _|_ c,d by A14,A51,ANALMETR:62;
then
A53: d,c _|_ d,a by ANALMETR:61;
LIN d9,c9,b9 by A52,AFF_1:6;
then LIN d,c,b by ANALMETR:40;
then d,c // d,b by ANALMETR:def 10;
then d,b _|_ d,a by A17,A53,ANALMETR:62;
then a,c // d,a by A11,A18,ANALMETR:63;
then a,c // a,d by ANALMETR:59;
then LIN a,c,d by ANALMETR:def 10;
then LIN a9,c9,d9 by ANALMETR:40;
then LIN c9,a9,d9 by AFF_1:6;
then LIN c,a,d by ANALMETR:40;
then
A54: c,a // c,d by ANALMETR:def 10;
c,d // b,c by A39,A50,ANALMETR:59;
then c,a // b,c by A17,A54,ANALMETR:60;
then c,a // c,b by ANALMETR:59;
then LIN c,a,b by ANALMETR:def 10;
then LIN c9,a9,b9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
LIN d9,o9,b9 by A20,AFF_1:6;
then d9,o9 // d9,b9 by AFF_1:def 1;
then b9,d9 // o9,d9 by AFF_1:4;
then b,d // o,d by ANALMETR:36;
then
A55: a,c _|_ o,d by A10,A18,ANALMETR:62;
LIN a,c,o by A21,ANALMETR:40;
then a,c // a,o by ANALMETR:def 10;
then
A56: a,c // o,a by ANALMETR:59;
a<>c
proof
assume a= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then
A57: o,d _|_ o,a by A55,A56,ANALMETR:62;
LIN a,c,o by A21,ANALMETR:40;
then
A58: a,c // a,o by ANALMETR:def 10;
A59: a<>c
proof
assume a= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then a,o // a,d1 by A37,A58,ANALMETR:60;
then LIN a,o,d1 by ANALMETR:def 10;
then LIN a9,o9,d19 by ANALMETR:40;
then LIN o9,a9,d19 by AFF_1:6;
then LIN o,a,d1 by ANALMETR:40;
then
A60: o,a // o,d1 by ANALMETR:def 10;
LIN a,c,o by A21,ANALMETR:40;
then a,c // a,o by ANALMETR:def 10;
then o,a // a,c by ANALMETR:59;
then a,c // o,d1 by A23,A60,ANALMETR:60;
then
A61: b,d _|_ o,d1 by A10,A59,ANALMETR:62;
LIN d9,o9,b9 by A20,AFF_1:6;
then LIN d,o,b by ANALMETR:40;
then d,o // d,b by ANALMETR:def 10;
then b,d // o,d by ANALMETR:59;
then
A62: o,d1 _|_ o,d by A18,A61,ANALMETR:62;
LIN c9,o9,a9 by A21,AFF_1:6;
then c9,o9 // c9,a9 by AFF_1:def 1;
then a9,c9 // o9,c9 by AFF_1:4;
then
A63: a,c // o,c by ANALMETR:36;
a<>c
proof
assume a= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then
A64: b,d _|_ o,c by A10,A63,ANALMETR:62;
b9,d9 // b9,o9 by A20,AFF_1:def 1;
then b9,d9 // o9,b9 by AFF_1:4;
then b,d // o,b by ANALMETR:36;
then
A65: o,c _|_ o,b by A18,A64,ANALMETR:62;
A66: not LIN o,d,d1
proof
assume LIN o,d,d1;
then o,d // o,d1 by ANALMETR:def 10;
then o,d _|_ o,d by A45,A62,ANALMETR:62;
hence contradiction by A40,ANALMETR:39;
end;
LIN a9,c9,d19 by A38,ANALMETR:40;
then LIN c9,d19,a9 by AFF_1:6;
then c9,d19 // c9,a9 by AFF_1:def 1;
then a9,c9 // c9,d19 by AFF_1:4;
then
A67: a,c // c,d1 by ANALMETR:36;
A68: a<>c
proof
assume a= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
LIN c9,a9,o9 by A21,AFF_1:6;
then c9,a9 // c9,o9 by AFF_1:def 1;
then a9,c9 // c9,o9 by AFF_1:4;
then a,c // c,o by ANALMETR:36;
then c,d1 // c,o by A67,A68,ANALMETR:60;
then LIN c,d1,o by ANALMETR:def 10;
then LIN c9,d19,o9 by ANALMETR:40;
then LIN o9,d19,c9 by AFF_1:6;
then
A69: LIN o,d1,c by ANALMETR:40;
LIN o9,d9,b9 by A20,AFF_1:6;
then
A70: LIN o,d,b by ANALMETR:40;
A71: d1,d // c,b by A39,ANALMETR:59;
b<>c
proof
assume b = c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then d,d1 _|_ a,d by A13,A39,ANALMETR:62;
then d1,d _|_ d,a by ANALMETR:61;
then c,d _|_ b,a by A15,A23,A27,A40,A45,A48,A49,A57,A62,A65,A66,A69,A70
,A71;
hence thesis by A10,A13,ANALMETR:61;
end;
hence thesis by A3,A4,A10,A12,ANALMETR:61,62;
end;
hence thesis by A5,A6,A9,A13,ANALMETR:61,62;
end;
now
assume d = c;
then a,b _|_ d,c by ANALMETR:39;
hence thesis by A10,A13,ANALMETR:61;
end;
hence thesis by A16;
end;