:: Metric-Affine Configurations in Metric Affine Planes -  Part I
::  by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received October 31, 1990
:: Copyright (c) 1990-2012 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 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;
  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
  :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;
  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;
  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;
  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 Af(X) by ANALMETR:35;
  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 by ANALMETR:35;
  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 Af(X) by ANALMETR:35;
  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 by ANALMETR:35;
  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,Def4;
  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,Def4;
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
proof
  assume
A1: X is satisfying_ODES;
  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 o,a // b,c and
A6: a,c _|_ a1,c1 and
A7: not o,c // o,a and
A8: not o,a // o,b;
  thus thesis by A1,A2,A3,A4,A5,A6,A7,A8,Def4;
end;

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 Af(X) by ANALMETR:35;
  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 Af(X) by ANALMETR:35;
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 Af(X) by ANALMETR:35;
      not o9,y9 // c19,x9 by A19,ANALMETR:36;
      then consider b29 be Element of Af(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 by ANALMETR:35;
      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 Af(X) by ANALMETR:35;
    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,Def5;
    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 Af(X) by ANALMETR:35;
  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 Af(X) by ANALMETR:35;
    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 by ANALMETR:35;
    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 Af(X) by ANALMETR:35;
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,Def6
;
  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 Af(X) by ANALMETR:35;
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 Af(X) by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
        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 Af(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 by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
      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 Af(X) by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
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 Af(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 by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
      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,Def5;
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,Def6;
    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 Af(X) by ANALMETR:35;
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 Af(X) by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
        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 Af(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 by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
      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 Af(X) by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
        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 Af(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 by ANALMETR:35;
        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 Af(X) by ANALMETR:35;
      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,Def6;
      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,Def6;
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 Af(X) by ANALMETR:35;
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 Af(X) by ANALMETR:35;
  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 Af(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 by ANALMETR:35;
  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 Af(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 by ANALMETR:35;
      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 Af X by ANALMETR:35;
        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 by ANALMETR:35;
        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,Def6;
        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;