:: Arrow's Impossibility Theorem
::  by Freek Wiedijk
::
:: Received August 13, 2007
:: Copyright (c) 2007-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 NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, FINSET_1, CARD_1, XXREAL_0,
      TARSKI, ARYTM_1, RELAT_1, ZFMISC_1, RELAT_2, ORDERS_1, WELLORD1, FUNCT_2,
      NAT_1, FINSEQ_1, ARYTM_3, ARROW;
 notations ORDERS_1, RELAT_1, RELAT_2, RELSET_1, XBOOLE_0, SUBSET_1, TARSKI,
      FINSET_1, FUNCT_1, FUNCT_2, CARD_1, XXREAL_0, ZFMISC_1, ORDINAL1, NAT_1,
      NUMBERS, FINSEQ_1, XCMPLX_0, WELLORD1;
 constructors XXREAL_0, FUNCT_2, REAL_1, FINSEQ_1, INT_1, RELAT_2, PARTFUN1,
      WELLORD1, RELSET_1;
 registrations RELSET_1, FINSET_1, NAT_1, INT_1, XREAL_0, XBOOLE_0, ORDINAL1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions RELAT_1, FUNCT_2, WELLORD1;
 theorems RELSET_1, ZFMISC_1, TARSKI, FUNCT_2, FINSEQ_4, FINSEQ_1, FINSEQ_3,
      NAT_1, ORDINAL1, XREAL_1, FUNCT_1, XXREAL_0, PARTFUN1, INT_1, CARD_2,
      CARD_1, XBOOLE_0, SUBSET_1, RELAT_2, RELAT_1, ORDERS_1, XBOOLE_1,
      WELLORD2, WELLORD1, XTUPLE_0;
 schemes XBOOLE_0, FUNCT_2, NAT_1, RELSET_1;

begin :: Preliminaries

definition
  let A,B9 be non empty set;
  let B be non empty Subset of B9;
  let f be Function of A,B;
  let x be Element of A;
  redefine func f.x -> Element of B;
  coherence
  proof
    thus f.x is Element of B;
  end;
end;

theorem Th1:
  for A being finite set st card A >= 2 holds for a being Element of A holds
  ex b being Element of A st b <> a
proof
  let A9 be finite set;
  assume
A1: card A9 >= 2;
  then reconsider A = A9 as finite non empty set by CARD_1:27;
  let a be Element of A9;
 {a} c= A by ZFMISC_1:31;
then  card (A \ {a}) = card A - card {a} by CARD_2:44
    .= card A - 1 by CARD_1:30;
then  card (A \ {a}) <> 0 by A1;
  then consider b being set such that
A2: b in A \ {a} by CARD_1:27,XBOOLE_0:def 1;
  reconsider b as Element of A9 by A2;
  take b;
 not b in {a} by A2,XBOOLE_0:def 5;
  hence thesis by TARSKI:def 1;
end;

theorem Th2:
  for A being finite set st card A >= 3 holds for a,b being Element of A holds
  ex c being Element of A st c <> a & c <> b
proof
  let A9 be finite set;
  assume
A1: card A9 >= 3;
  then reconsider A = A9 as finite non empty set by CARD_1:27;
  let a,b be Element of A9;
 {a,b} c= A by ZFMISC_1:32;
then A2: card (A \ {a,b}) = card A - card {a,b} by CARD_2:44;
 card {a,b} <= 2 by CARD_2:50;
then  card (A \ {a,b}) >= 3 - 2 by A1,A2,XREAL_1:13;
then  card (A \ {a,b}) <> 0;
  then consider c being set such that
A3: c in A \ {a,b} by CARD_1:27,XBOOLE_0:def 1;
  reconsider c as Element of A9 by A3;
  take c;
 not c in {a,b} by A3,XBOOLE_0:def 5;
  hence thesis by TARSKI:def 2;
end;

begin :: Linear preorders and linear orders

reserve A for non empty set;
reserve a,b,c,x,y,z for Element of A;

definition
  let A;
  defpred P[set] means $1 is Relation of A &
  (for a,b holds [a,b] in $1 or [b,a] in $1) &
  (for a,b,c st [a,b] in $1 & [b,c] in $1 holds [a,c] in $1);
  defpred Q[set] means for R being set holds R in $1 iff P[R];
  func LinPreorders A means
  :Def1:
  for R being set holds R in it iff
  R is Relation of A & (for a,b holds [a,b] in R or [b,a] in R) &
  for a,b,c st [a,b] in R & [b,c] in R holds [a,c] in R;
  existence
  proof
    consider it0 being set such that
A1: for R being set holds R in it0 iff R in bool [:A,A:] & P[R]
    from XBOOLE_0:sch 1;
    take it0;
    let R be set;
    thus R in it0 implies P[R] by A1;
    assume
A2: P[R];
 [:A,A:] in bool [:A,A:] by ZFMISC_1:def 1;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    let it1,it2 be set;
    assume that
A3: Q[it1] and
A4: Q[it2];
 now
      let R be set;
   R in it1 iff P[R] by A3;
      hence R in it1 iff R in it2 by A4;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let A;
  cluster LinPreorders A -> non empty;
  coherence
  proof
 [:A,A:] c= [:A,A:];
    then reconsider R = [:A,A:] as Relation of A;
     (
 for a,b holds [a,b] in R or [b,a] in R)& for a,b,c st [a,b] in R & [b,c] in
    R holds [a,c] in R by ZFMISC_1:87;
    hence thesis by Def1;
  end;
end;

definition
  let A;
  defpred P[set] means for a,b st [a,b] in $1 & [b,a] in $1 holds a = b;
  defpred Q[set] means
  for R being Element of LinPreorders A holds R in $1 iff P[R];
  func LinOrders A -> Subset of LinPreorders A means
  :Def2:
  for R being Element of LinPreorders A holds R in it iff
  for a,b st [a,b] in R & [b,a] in R holds a = b;
  existence
  proof
    consider it0 being set such that
A1: for R being set holds R in it0 iff R in LinPreorders A & P[R]
    from XBOOLE_0:sch 1;
 for R being set st R in it0 holds R in LinPreorders A by A1;
    then reconsider it0 as Subset of LinPreorders A by TARSKI:def 3;
    take it0;
    let R be Element of LinPreorders A;
    thus R in it0 implies P[R] by A1;
    assume P[R];
    hence thesis by A1;
  end;
  uniqueness
  proof
    let it1,it2 be Subset of LinPreorders A;
    assume that
A2: Q[it1] and
A3: Q[it2];
 now
      let R be Element of LinPreorders A;
   R in it1 iff P[R] by A2;
      hence R in it1 iff R in it2 by A3;
    end;
    hence thesis by SUBSET_1:3;
  end;
end;

registration
  let A be set;
  cluster connected for Order of A;
  existence
  proof
    consider R9 being Relation such that
A1: R9 well_orders A by WELLORD2:17;
    set R = R9 |_2 A;
A2: R is well-ordering by A1,WELLORD2:16;
    reconsider R as Relation of A by XBOOLE_1:17;
 now
      let a be set;
      assume
A3:   a in A;
   R9 is_reflexive_in A by A1,WELLORD1:def 5;
then A4:   [a,a] in R9 by A3,RELAT_2:def 1;
   [a,a] in [:A,A:] by A3,ZFMISC_1:def 2;
then    [a,a] in R by A4,XBOOLE_0:def 4;
      hence a in dom R by XTUPLE_0:def 12;
    end;
then  A c= dom R by TARSKI:def 3;
then  dom R = A by XBOOLE_0:def 10;
    then reconsider R as Order of A by A2,PARTFUN1:def 2,WELLORD1:def 4;
    take R;
    thus thesis by A2,WELLORD1:def 4;
  end;
end;

definition
  let A;
  redefine func LinOrders A means
  :Def3:
  for R being set holds R in it iff R is connected Order of A;
  compatibility
  proof
A1: now
      let R be set;
      assume
A2:   R in LinOrders A;
      then reconsider R9 = R as Relation of A by Def1;
   now
        let a be set;
        assume a in A;
then      [a,a] in R by A2,Def1;
        hence a in dom R9 by XTUPLE_0:def 12;
      end;
then    A c= dom R9 by TARSKI:def 3;
then A3:   dom R9 = A by XBOOLE_0:def 10;
   now
        let a be set;
        assume a in A;
then     [a,a] in R by A2,Def1;
        hence a in rng R9 by XTUPLE_0:def 13;
      end;
then   A c= rng R9 by TARSKI:def 3;
then A4:  field R9 = A \/ A by A3,XBOOLE_0:def 10;
  for a,b being set st a in A & b in A & a <> b
      holds [a,b] in R or [b,a] in R by A2,Def1;
then A5:  R9 is_connected_in A by RELAT_2:def 6;
  for a being set st a in A holds [a,a] in R by A2,Def1;
then A6:  R9 is_reflexive_in A by RELAT_2:def 1;
  for
 a,b being set st a in A & b in A & [a,b] in R & [b,a] in R holds a = b
      by A2,Def2;
then A7:  R9 is_antisymmetric_in A by RELAT_2:def 4;
        for
 a,b,c being set st a in A & b in A & c in A & [a,b] in R & [b,c] in
      R holds [a,c] in R by A2,Def1;
then   R9 is_transitive_in A by RELAT_2:def 8;
      hence R is connected Order of A
      by A3,A4,A5,A6,A7,PARTFUN1:def 2,RELAT_2:def 9,def 12,def 14,def 16;
    end;
A8: now
      let R be set;
      assume
A9:  R is connected Order of A;
      then reconsider R9 = R as connected Order of A;
A10:  now
        let a,b;
    dom R9 = A by PARTFUN1:def 2;
then     A c= dom R9 \/ rng R9 by XBOOLE_1:7;
then A11:    field R9 = A by XBOOLE_0:def 10;
        A12:    R9
 is_connected_in field R9 & R9 is_reflexive_in field R9 by RELAT_2:def 9,def 14
;
    a = b or a <> b;
        hence [a,b] in R or [b,a] in R by A11,A12,RELAT_2:def 1,def 6;
      end;
  for a,b,c st [a,b] in R & [b,c] in R holds [a,c] in R by A9,ORDERS_1:5;
then A13:  R in LinPreorders A by A9,A10,Def1;
  for a,b st [a,b] in R & [b,a] in R holds a = b by A9,ORDERS_1:4;
      hence R in LinOrders A by A13,Def2;
    end;
    let it0 be Subset of LinPreorders A;
    thus it0 = LinOrders A implies
    for R being set holds R in it0 iff R is connected Order of A by A1,A8;
    assume
A14: for R being set holds R in it0 iff R is connected Order of A;
 now
      let R be set;
  R in it0 iff R is connected Order of A by A14;
      hence R in it0 iff R in LinOrders A by A1,A8;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let A;
  cluster LinOrders A -> non empty;
  coherence
  proof
    set R = the connected Order of A;
 R in LinOrders A by Def3;
    hence thesis;
  end;
end;

registration let A;
 cluster -> Relation-like for Element of LinPreorders A;
 coherence by Def1;
 cluster -> Relation-like for Element of LinOrders A;
 coherence;
end;

reserve o,o9 for Element of LinPreorders A;
reserve o99 for Element of LinOrders A;

definition
  let o be Relation, a,b be set;
  pred a <=_o, b means
  :Def4:
  [a,b] in o;
end;

notation
  let o be Relation, a,b be set;
  synonym b >=_o, a for a <=_o, b;
  antonym b <_o, a for a <=_o, b;
  antonym a >_o, b for a <=_o, b;
end;

theorem Th3:
  a <=_o, a
proof
  thus [a,a] in o by Def1;
end;

theorem Th4:
  a <=_o, b or b <=_o, a
proof
 [a,b] in o or [b,a] in o by Def1;
  hence thesis by Def4;
end;

theorem Th5:
  (a <=_o, b or a <_o, b) & (b <=_ o, c or b <_o, c) implies a <=_o, c
proof
  assume a <=_o, b or a <_o, b;
then  a <=_o, b by Th4;
then A1: [a,b] in o by Def4;
  assume b <=_o, c or b <_o, c;
then  b <=_o, c by Th4;
then  [b,c] in o by Def4;
  hence [a,c] in o by A1,Def1;
end;

theorem Th6:
  a <=_o99, b & b <=_o99, a implies a = b
proof
 [a,b] in o99 & [b,a] in o99 implies a = b by Def2;
  hence thesis by Def4;
end;

theorem Th7:
  a <> b & b <> c & a <> c implies ex o st a <_o, b & b <_o, c
proof
  assume that
A1: a <> b & b <> c and
A2: a <> c;
  defpred P[set,set] means ($1 = a or $2 <> a) & ($1 <> c or $2 = c);
  consider R being Relation of A such that
A3: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A4: now
    let x,y;
 P[x,y] or P[y,x] by A2;
    hence [x,y] in R or [y,x] in R by A3;
  end;
 now
    let x,y,z;
    assume [x,y] in R & [y,z] in R;
then  ( P[x,y])& P[y,z] by A3;
    hence [x,z] in R by A3;
  end;
  then reconsider o = R as Element of LinPreorders A by A4,Def1;
  take o;
 ( not [b,a] in R)& not [c,b] in R by A1,A3;
  hence thesis by Def4;
end;

theorem Th8:
  ex o st for a st a <> b holds b <_o, a
proof
  defpred P[set,set] means $1 = b or $2 <> b;
  consider R being Relation of A such that
A1: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A2: now
    let x,y;
 P[x,y] or P[y,x];
    hence [x,y] in R or [y,x] in R by A1;
  end;
 now
    let x,y,z;
    assume that
A3: [x,y] in R and
A4: [y,z] in R;
 P[y,z] by A1,A4;
    hence [x,z] in R by A1,A3;
  end;
  then reconsider o = R as Element of LinPreorders A by A2,Def1;
  take o;
  let a;
  assume a <> b;
then  not [a,b] in R by A1;
  hence thesis by Def4;
end;

theorem Th9:
  ex o st for a st a <> b holds a <_o, b
proof
  defpred P[set,set] means $1 <> b or $2 = b;
  consider R being Relation of A such that
A1: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A2: now
    let x,y;
 P[x,y] or P[y,x];
    hence [x,y] in R or [y,x] in R by A1;
  end;
 now
    let x,y,z;
    assume that
A3: [x,y] in R and
A4: [y,z] in R;
 P[x,y] by A1,A3;
    hence [x,z] in R by A1,A4;
  end;
  then reconsider o = R as Element of LinPreorders A by A2,Def1;
  take o;
  let a;
  assume a <> b;
then  not [b,a] in R by A1;
  hence thesis by Def4;
end;

theorem Th10:
  a <> b & a <> c implies ex o st a <_o, b & a <_o, c &
  (b <_o, c iff b <_o9, c) & (c <_o, b iff c <_o9, b)
proof
  assume
A1: a <> b & a <> c;
  defpred P[Element of A,Element of A] means
  $1 = a or ($1 <=_o9, $2 & $2 <> a);
  consider R being Relation of A such that
A2: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A3: now
    let x,y;
 P[x,y] or P[y,x] by Th4;
    hence [x,y] in R or [y,x] in R by A2;
  end;
 now
    let x,y,z;
    assume [x,y] in R & [y,z] in R;
then  ( P[x,y])& P[y,z] by A2;
then  P[x,z] by Th5;
    hence [x,z] in R by A2;
  end;
  then reconsider o = R as Element of LinPreorders A by A3,Def1;
  take o;
A4: ( not [b,a] in R)& not [c,a] in R by A1,A2;
A5: not [c,b] in R iff b <_o9, c by A1,A2;
 not [b,c] in R iff c <_o9, b by A1,A2;
  hence thesis by A4,A5,Def4;
end;

theorem Th11:
  a <> b & a <> c implies ex o st b <_o, a & c <_o, a &
  (b <_o, c iff b <_o9, c) & (c <_o, b iff c <_o9, b)
proof
  assume
A1: a <> b & a <> c;
  defpred P[Element of A,Element of A] means
  ($1 <> a & $1 <=_o9, $2) or $2 = a;
  consider R being Relation of A such that
A2: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A3: now
    let x,y;
 P[x,y] or P[y,x] by Th4;
    hence [x,y] in R or [y,x] in R by A2;
  end;
 now
    let x,y,z;
    assume [x,y] in R & [y,z] in R;
then  ( P[x,y])& P[y,z] by A2;
then  P[x,z] by Th5;
    hence [x,z] in R by A2;
  end;
  then reconsider o = R as Element of LinPreorders A by A3,Def1;
  take o;
A4: ( not [a,b] in R)& not [a,c] in R by A1,A2;
A5: not [c,b] in R iff b <_o9, c by A1,A2;
 not [b,c] in R iff c <_o9, b by A1,A2;
  hence thesis by A4,A5,Def4;
end;

theorem
  for o,o9 being Element of LinOrders A holds
  (a <_o, b iff a <_o9, b) & (b <_o, a iff b <_o9, a) iff
  (a <_o, b iff a <_o9, b)
proof
  let o,o9 be Element of LinOrders A;
  thus (a <_o, b iff a <_o9, b) & (b <_o, a iff b <_o9, a) implies
  (a <_o, b iff a <_o9, b);
  assume
A1: a <_o, b iff a <_o9, b;
  hence a <_o, b iff a <_o9, b;
  hereby
    assume
A2: b <_o, a;
then  a <> b by Th4;
    hence b <_o9, a by A1,A2,Th4,Th6;
  end;
  assume
A3: b <_o9, a;
then  a <> b by Th4;
  hence thesis by A1,A3,Th4,Th6;
end;

theorem Th13:
  for o being Element of LinOrders A, o9 being Element of LinPreorders A holds
  (for a,b st a <_o, b holds a <_o9, b) iff
  for a,b holds a <_o, b iff a <_o9, b
proof
  let o be Element of LinOrders A, o9 be Element of LinPreorders A;
  hereby
    assume
A1: for a,b st a <_o, b holds a <_o9, b;
    let a,b;
    per cases by Th6;
    suppose
   a <_o, b;
      hence a <_o, b iff a <_o9, b by A1;
    end;
    suppose
   a = b;
      hence a <_o, b iff a <_o9, b by Th3;
    end;
    suppose
A2:   b <_o, a;
then    b <_o9, a by A1;
      hence a <_o, b iff a <_o9, b by A2,Th4;
    end;
  end;
  thus thesis;
end;

begin :: Arrow's theorem
:: version with weak orders, the one from the paper

reserve A,N for finite non empty set;
reserve a,b,c,d,a9,c9 for Element of A;
reserve i,n,nb,nc for Element of N;
reserve o,oI,oII for Element of LinPreorders A;
reserve p,p9,pI,pII,pI9,pII9 for Element of Funcs(N,LinPreorders A);
reserve f for Function of Funcs(N,LinPreorders A),LinPreorders A;
reserve k,k0 for Nat;

theorem Th14:
  (for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) & (for p,p9,a,b st
  for i holds (a <_p.i, b iff a <_p9.i, b) & (b <_p.i, a iff b <_p9.i, a)
  holds a <_f.p, b iff a <_f.p9, b) & card A >= 3 implies
  ex n st for p,a,b st a <_p.n, b holds a <_f.p, b
proof
  assume that
A1: for p,a,b st for i holds a <_p.i, b holds a <_f.p, b and
A2: for p,p9,a,b st
  for i holds (a <_p.i, b iff a <_p9.i, b) & (b <_p.i, a iff b <_p9.i, a)
  holds a <_f.p, b iff a <_f.p9, b and
A3: card A >= 3;
  defpred extreme[Element of LinPreorders A,Element of A] means
  (for a st a <> $2 holds $2 <_$1, a) or (for a st a <> $2 holds a <_$1, $2);
A4: for p,b st for i holds extreme[p.i,b] holds extreme[f.p,b]
  proof
    assume not thesis;
    then consider p,b such that
A5: ex a st a <> b & a <=_f.p, b and
A6: ex c st c <> b & b <=_f.p, c and
A7: for i holds extreme[p.i,b];
    consider a9 such that
A8: a9 <> b & a9 <=_f.p, b by A5;
    consider c9 such that
A9: b <> c9 & b <=_f.p, c9 by A6;
 ex a,c st a <> b & b <> c & a <> c & a <=_f.p, b & b <=_f.p, c
    proof
      per cases;
      suppose
A10:    a9 <> c9;
        take a9,c9;
        thus thesis by A8,A9,A10;
      end;
      suppose
A11:    a9 = c9;
        consider d such that
A12:    d <> b & d <> a9 by A3,Th2;
        per cases by Th4;
        suppose
A13:      d <=_f.p, b;
          take d,c9;
          thus thesis by A9,A11,A12,A13;
        end;
        suppose
A14:      b <=_f.p, d;
          take a9,d;
          thus thesis by A8,A12,A14;
        end;
      end;
    end;
    then consider a,c such that
A15: a <> b & b <> c and
A16: a <> c and
A17: a <=_f.p, b & b <=_f.p, c;
    defpred P[Element of N,Element of LinPreorders A] means
    (a <_p.$1, b iff a <_$2, b) & (b <_p.$1, a iff b <_$2, a) &
    (b <_p.$1, c iff b <_$2, c) & (c <_p.$1, b iff c <_$2, b) & c <_$2, a;
A18: for i holds ex o st P[i,o]
    proof
      let i;
      per cases by A7;
      suppose
    for c st c <> b holds b <_p.i, c;
then A19:    b <_p.i, a & b <_p.i, c by A15;
        consider o such that
A20:    b <_o, c & c <_o, a by A15,A16,Th7;
        take o;
        thus thesis by A19,A20,Th4,Th5;
      end;
      suppose
    for a st a <> b holds a <_p.i, b;
then A21:    a <_p.i, b & c <_p.i, b by A15;
        consider o such that
A22:    c <_o, a & a <_o, b by A15,A16,Th7;
        take o;
        thus thesis by A21,A22,Th4,Th5;
      end;
    end;
    consider p9 being Function of N,LinPreorders A such that
A23: for i holds P[i,p9.i] from FUNCT_2:sch 3(A18);
    reconsider p9 as Element of Funcs(N,LinPreorders A) by FUNCT_2:8;
 a <=_f.p9, b & b <=_f.p9, c by A2,A17,A23;
then  a <=_f.p9, c by Th5;
    hence contradiction by A1,A23;
  end;
A24: for b holds ex nb,pI,pII st (for i st i <> nb holds pI.i = pII.i) &
  (for i holds extreme[pI.i,b]) & (for i holds extreme[pII.i,b]) &
  (for a st a <> b holds b <_pI.nb, a) &
  (for a st a <> b holds a <_pII.nb, b) &
  (for a st a <> b holds b <_f.pI, a) & for a st a <> b holds a <_f.pII, b
  proof
    consider t being FinSequence such that
A25: rng t = N and
A26: t is one-to-one by FINSEQ_4:58;
    reconsider t as FinSequence of N by A25,FINSEQ_1:def 4;
    let b;
    consider oI such that
A27: for a st a <> b holds b <_oI, a by Th8;
    consider oII such that
A28: for a st a <> b holds a <_oII, b by Th9;
A29: for k0 holds ex p st (for k st k in dom t & k < k0 holds p.(t.k) = oII) &
    for k st k in dom t & k >= k0 holds p.(t.k) = oI
    proof
      let k0;
      defpred P[Element of N,Element of LinPreorders A] means
      ex k st k in dom t & $1 = t.k &
      (k < k0 implies $2 = oII) & (k >= k0 implies $2 = oI);
A30:  for i holds ex o st P[i,o]
      proof
        let i;
        consider k being set such that
A31:    k in dom t and
A32:    i = t.k by A25,FUNCT_1:def 3;
        reconsider k as Nat by A31;
        per cases;
        suppose
A33:      k < k0;
          take oII;
          thus thesis by A31,A32,A33;
        end;
        suppose
A34:      k >= k0;
          take oI;
          thus thesis by A31,A32,A34;
        end;
      end;
      consider p being Function of N,LinPreorders A such that
A35:  for i holds P[i,p.i] from FUNCT_2:sch 3(A30);
      reconsider p as Element of Funcs(N,LinPreorders A) by FUNCT_2:8;
      take p;
      thus for k st k in dom t & k < k0 holds p.(t.k) = oII
      proof
        let k;
        assume that
A36:    k in dom t and
A37:    k < k0;
        reconsider i = t.k as Element of N by A36,PARTFUN1:4;
    P[i,p.i] by A35;
        hence thesis by A26,A36,A37,FUNCT_1:def 4;
      end;
      let k;
      assume that
A38:  k in dom t and
A39:  k >= k0;
      reconsider i = t.k as Element of N by A38,PARTFUN1:4;
  P[i,p.i] by A35;
      hence thesis by A26,A38,A39,FUNCT_1:def 4;
    end;
    defpred Q[Nat] means for p st
    (for k st k in dom t & k < $1 holds p.(t.k) = oII) &
    (for k st k in dom t & k >= $1 holds p.(t.k) = oI)
    holds for a st a <> b holds a <_f.p, b;
    reconsider kII9 = len t + 1 as Element of NAT by ORDINAL1:def 12;
A40: Q[kII9]
    proof
      let p;
      assume that
A41:  for k st k in dom t & k < kII9 holds p.(t.k) = oII
      and for k st k in dom t & k >= kII9 holds p.(t.k) = oI;
      let a;
      assume
A42:  a <> b;
  for i holds a <_p.i, b
      proof
        let i;
        consider k being set such that
A43:    k in dom t and
A44:    i = t.k by A25,FUNCT_1:def 3;
        reconsider k as Nat by A43;
    k <= len t by A43,FINSEQ_3:25;
then     k + 0 < kII9 by XREAL_1:8;
then     p.i = oII by A41,A43,A44;
        hence thesis by A28,A42;
      end;
      hence thesis by A1;
    end;
then A45: ex kII9 being Nat st Q[kII9];
    consider kII being Nat such that
A46: Q[kII] & for k0 being Nat st Q[k0] holds k0 >= kII from NAT_1:sch 5(A45
    );
    consider pII such that
A47: for k st k in dom t & k < kII holds pII.(t.k) = oII and
A48: for k st k in dom t & k >= kII holds pII.(t.k) = oI by A29;
A49: kII > 1
    proof
      assume
A50:  kII <= 1;
      consider a such that
A51:  a <> b by A3,Th1,XXREAL_0:2;
A52:  for i holds b <_pII.i, a
      proof
        let i;
        consider k being set such that
A53:    k in dom t and
A54:    i = t.k by A25,FUNCT_1:def 3;
        reconsider k as Nat by A53;
    k >= 1 by A53,FINSEQ_3:25;
then     pII.i = oI by A48,A50,A53,A54,XXREAL_0:2;
        hence thesis by A27,A51;
      end;
A55:  a <_f.pII, b by A46,A47,A48,A51;
  b <_f.pII, a by A1,A52;
      hence contradiction by A55,Th4;
    end;
    then reconsider kI = kII - 1 as Nat by NAT_1:20;
    reconsider kI as Element of NAT by ORDINAL1:def 12;
A56: kII = kI + 1;
 kI > 1 - 1 by A49,XREAL_1:9;
then A57: kI >= 0 + 1 by INT_1:7;
 kII <= kII9 by A40,A46;
then  kI <= kII9 - 1 by XREAL_1:9;
then A58: kI in dom t by A57,FINSEQ_3:25;
    then reconsider nb = t.kI as Element of N by PARTFUN1:4;
A59: kI + 0 < kII by A56,XREAL_1:8;
    then consider pI such that
A60: for k st k in dom t & k < kI holds pI.(t.k) = oII and
A61: for k st k in dom t & k >= kI holds pI.(t.k) = oI and
A62: not(for a st a <> b holds a <_f.pI, b) by A46;
    take nb,pI,pII;
    thus for i st i <> nb holds pI.i = pII.i
    proof
      let i;
      assume
A63:  i <> nb;
      consider k being set such that
A64:  k in dom t and
A65:  i = t.k by A25,FUNCT_1:def 3;
      reconsider k as Nat by A64;
      per cases by A63,A65,XXREAL_0:1;
      suppose
    k < kI;
then     k + 0 < kII & pI.i = oII by A56,A60,A64,A65,XREAL_1:8;
        hence thesis by A47,A64,A65;
      end;
      suppose
    k > kI;
then     k >= kII & pI.i = oI by A56,A61,A64,A65,INT_1:7;
        hence thesis by A48,A64,A65;
      end;
    end;
    thus
A66: for i holds extreme[pI.i,b]
    proof
      let i;
  ex k being set st k in dom t & i = t.k by A25,FUNCT_1:def 3;
then   pI.i = oII or pI.i = oI by A60,A61;
      hence thesis by A27,A28;
    end;
    thus for i holds extreme[pII.i,b]
    proof
      let i;
  ex k being set st k in dom t & i = t.k by A25,FUNCT_1:def 3;
then   pII.i = oII or pII.i = oI by A47,A48;
      hence thesis by A27,A28;
    end;
 pI.nb = oI by A58,A61;
    hence for a st a <> b holds b <_pI.nb, a by A27;
 pII.nb = oII by A47,A58,A59;
    hence for a st a <> b holds a <_pII.nb, b by A28;
    thus for a st a <> b holds b <_f.pI, a by A4,A62,A66;
    thus thesis by A46,A47,A48;
  end;
A67: for b holds ex nb,pI,pII st (for i st i <> nb holds pI.i = pII.i) &
  (for i holds extreme[pI.i,b]) &
  (for a st a <> b holds b <_f.pI, a) & (for a st a <> b holds a <_f.pII, b) &
  for p,a,c st a <> b & c <> b & a <_p.nb, c holds a <_f.p, c
  proof
    let b;
    consider nb,pI,pII such that
A68: for i st i <> nb holds pI.i = pII.i and
A69: for i holds extreme[pI.i,b] and
A70: for i holds extreme[pII.i,b] and
A71: for a st a <> b holds b <_pI.nb, a and
A72: for a st a <> b holds a <_pII.nb, b and
    A73: (
 for a st a <> b holds b <_f.pI, a)& for a st a <> b holds a <_f.pII, b
    by A24;
    take nb,pI,pII;
    thus (for i st i <> nb holds pI.i = pII.i) &
    (for i holds extreme[pI.i,b]) &
    (for a st a <> b holds b <_f.pI, a) & for a st a <> b holds a <_f.pII, b
    by A68,A69,A73;
    let p,a,c;
    assume that
A74: a <> b and
A75: c <> b and
A76: a <_p.nb, c;
A77: a <> c by A76,Th3;
    defpred P[Element of N,Element of LinPreorders A] means
    (a <_p.$1, c iff a <_$2, c) & (c <_p.$1, a iff c <_$2, a) &
    ($1 = nb implies a <_$2, b & b <_$2, c) & ($1 <> nb implies
    ((for d st d <> b holds b <_pII.$1, d) implies b <_$2, a & b <_$2, c) &
    ((for d st d <> b holds d <_pII.$1, b) implies a <_$2, b & c <_$2, b));
A78: for i holds ex o st P[i,o]
    proof
      let i;
      per cases;
      suppose
A79:   i = nb;
        consider o such that
A80:   a <_o, b & b <_o, c by A74,A75,A77,Th7;
        take o;
        thus thesis by A76,A79,A80,Th4,Th5;
      end;
      suppose
A81:   i <> nb;
        per cases by A70;
        suppose
     for d st d <> b holds b <_pII.i, d;
then      b <_pII.i, a by A74;
then A82:     not a <_pII.i, b by Th4;
          consider o such that
          A83:     b
 <_o, a & b <_o, c & ( a <_o, c iff a <_p.i, c)&( c <_o, a iff c <_p.i,
          a)
          by A74,A75,Th10;
          take o;
          thus thesis by A74,A81,A82,A83;
        end;
        suppose
     for d st d <> b holds d <_pII.i, b;
then      a <_pII.i, b by A74;
then A84:     not b <_pII.i, a by Th4;
          consider o such that
          A85:     a
 <_o, b & c <_o, b & ( a <_o, c iff a <_p.i, c)&( c <_o, a iff c <_p.i,
          a)
          by A74,A75,Th11;
          take o;
          thus thesis by A74,A81,A84,A85;
        end;
      end;
    end;
    consider pIII being Function of N,LinPreorders A such that
A86: for i holds P[i,pIII.i] from FUNCT_2:sch 3(A78);
    reconsider pIII as Element of Funcs(N,LinPreorders A) by FUNCT_2:8;
 for i holds (a <_pII.i, b iff a <_pIII.i, b) &
    (b <_pII.i, a iff b <_pIII.i, a)
    proof
      let i;
      per cases;
      suppose
   i = nb;
then    a <_pII.i, b & a <_pIII.i, b by A72,A74,A86;
        hence thesis by Th4;
      end;
      suppose
A87:   i <> nb;
        per cases by A70;
        suppose
     for d st d <> b holds b <_pII.i, d;
then      b <_pII.i, a & b <_pIII.i, a by A74,A86,A87;
          hence thesis by Th4;
        end;
        suppose
     for d st d <> b holds d <_pII.i, b;
then      a <_pII.i, b & a <_pIII.i, b by A74,A86,A87;
          hence thesis by Th4;
        end;
      end;
    end;
then A88: a <_f.pII, b iff a <_f.pIII, b by A2;
     for
 i holds (b <_pI.i, c iff b <_pIII.i, c) & (c <_pI.i, b iff c <_pIII.i, b )
    proof
      let i;
      per cases;
      suppose
   i = nb;
then    b <_pI.i, c & b <_pIII.i, c by A71,A75,A86;
        hence thesis by Th4;
      end;
      suppose
A89:   i <> nb;
        per cases by A70;
        suppose
A90:     for d st d <> b holds b <_pII.i, d;
then      b <_pII.i, c by A75;
then A91:     b <_pI.i, c by A68,A89;
     b <_pIII.i, c by A86,A89,A90;
          hence thesis by A91,Th4;
        end;
        suppose
A92:     for d st d <> b holds d <_pII.i, b;
then      c <_pII.i, b by A75;
then A93:     c <_pI.i, b by A68,A89;
     c <_pIII.i, b by A86,A89,A92;
          hence thesis by A93,Th4;
        end;
      end;
    end;
then  b <_f.pI, c iff b <_f.pIII, c by A2;
then  a <_f.pIII, c by A73,A74,A88,Th5;
    hence thesis by A2,A86;
  end;
  set b = the Element of A;
  consider nb,pI,pII such that
A94: for i st i <> nb holds pI.i = pII.i and
A95: for i holds extreme[pI.i,b] and
  A96: (
 for a st a <> b holds b <_f.pI, a)& for a st a <> b holds a <_f.pII, b and
A97: for p,a,c st a <> b & c <> b & a <_p.nb, c holds a <_f.p, c by A67;
  take nb;
  let p,a,a9;
  assume
A98: a <_p.nb, a9;
then A99: a <> a9 by Th4;
  per cases;
  suppose
 a <> b & a9 <> b;
    hence thesis by A97,A98;
  end;
  suppose
A100: a = b or a9 = b;
    consider c such that
A101: c <> a & c <> a9 by A3,Th2;
    consider nc,pI9,pII9 such that
    for i st i <> nc holds pI9.i = pII9.i and
    for i holds extreme[pI9.i,c] and
    for a st a <> c holds c <_f.pI9, a and
    for a st a <> c holds a <_f.pII9, c and
A102: for p,a,a9 st a <> c & a9 <> c & a <_p.nc, a9 holds a <_f.p, a9 by A67;
 nc = nb
    proof
      per cases by A100;
      suppose
A103:   a = b;
        assume
A104:   nc <> nb;
   b <_pI.nc, a9 or a9 <_pI.nc, b by A95,A99,A103;
then    b <_pII.nc, a9 & a9 <_f.pII, b or
        a9 <_pI.nc, b & b <_f.pI, a9 by A94,A96,A99,A103,A104;
then    b <_pII.nc, a9 & a9 <=_f.pII, b or
        a9 <_pI.nc, b & b <=_f.pI, a9 by Th4;
        hence contradiction by A101,A102,A103;
      end;
      suppose
A105:   a9 = b;
        assume
A106:   nc <> nb;
   b <_pI.nc, a or a <_pI.nc, b by A95,A99,A105;
then    b <_pII.nc, a & a <_f.pII, b or
        a <_pI.nc, b & b <_f.pI, a by A94,A96,A99,A105,A106;
then    b <_pII.nc, a & a <=_f.pII, b or
        a <_pI.nc, b & b <=_f.pI, a by Th4;
        hence contradiction by A101,A102,A105;
      end;
    end;
    hence thesis by A98,A101,A102;
  end;
end;

:: and then a stronger version

reserve o,o1 for Element of LinOrders A;
reserve o9 for Element of LinPreorders A;
reserve p,p9 for Element of Funcs(N,LinOrders A);
reserve q,q9 for Element of Funcs(N,LinPreorders A);
reserve f for Function of Funcs(N,LinOrders A),LinPreorders A;

theorem
  (for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) & (for p,p9,a,b st
  for i holds a <_p.i, b iff a <_p9.i, b holds a <_f.p, b iff a <_f.p9, b) &
  card A >= 3 implies ex n st for p,a,b holds a <_p.n, b iff a <_f.p, b
proof
  assume that
A1: for p,a,b st for i holds a <_p.i, b holds a <_f.p, b and
A2: for p,p9,a,b st for i holds a <_p.i, b iff a <_p9.i, b
  holds a <_f.p, b iff a <_f.p9, b and
A3: card A >= 3;
  set o = the Element of LinOrders A;
  defpred O[Element of LinPreorders A,Element of A,Element of A] means
  $2 <=_$1, $3 & ($2 <_$1, $3 or $2 <=_o, $3);
  defpred P[Element of LinPreorders A,Element of LinOrders A] means
  for a,b holds O[$1,a,b] iff a <=_$2, b;
A4: for o9 ex o1 st P[o9,o1]
  proof
    let o9;
    defpred Q[Element of A,Element of A] means O[o9,$1,$2];
    consider o1 being Relation of A such that
A5: for a,b holds [a,b] in o1 iff Q[a,b] from RELSET_1:sch 2;
A6: now
      let a,b;
   Q[a,b] or Q[b,a] by Th4;
      hence [a,b] in o1 or [b,a] in o1 by A5;
    end;
 now
      let a,b,c;
   Q[a,b] & Q[b,c] implies Q[a,c] by Th5;
      hence [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 by A5;
    end;
    then reconsider o1 as Element of LinPreorders A by A6,Def1;
 now
      let a,b;
  Q[a,b] & Q[b,a] implies a = b by Th6;
      hence [a,b] in o1 & [b,a] in o1 implies a = b by A5;
    end;
    then reconsider o1 as Element of LinOrders A by Def2;
    take o1;
    let a,b;
 [a,b] in o1 iff Q[a,b] by A5;
    hence thesis by Def4;
  end;
  defpred R[Element of Funcs(N,LinPreorders A),Element of Funcs(N,LinOrders A)]
  means for i holds P[$1.i,$2.i];
A7: for q,p,p9 st R[q,p] & R[q,p9] holds p = p9
  proof
    let q,p,p9;
    assume that
A8: R[q,p] and
A9: R[q,p9];
    let i;
    reconsider pi = p.i as Relation of A by Def1;
    reconsider pi9 = p9.i as Relation of A by Def1;
 now
      let a,b;
A10:  O[q.i,a,b] iff a <=_p.i, b by A8;
  O[q.i,a,b] iff a <=_p9.i, b by A9;
      hence [a,b] in p.i iff [a,b] in p9.i by A10,Def4;
    end;
then  pi = pi9 by RELSET_1:def 2;
    hence p.i = p9.i;
  end;
A11: for q ex p st R[q,p]
  proof
    let q;
    defpred S[Element of N,Element of LinOrders A] means P[q.$1,$2];
A12: for i ex o1 st S[i,o1] by A4;
    consider p being Function of N,LinOrders A such that
A13: for i holds S[i,p.i qua Element of LinOrders A] from FUNCT_2:sch 3(A12);
    reconsider p as Element of Funcs(N,LinOrders A) by FUNCT_2:8;
    take p;
    thus thesis by A13;
  end;
  defpred T[Element of Funcs(N,LinPreorders A),Element of LinPreorders A] means
  ex p st R[$1,p] & f.p = $2;
A14: for q ex o9 st T[q,o9]
  proof
    let q;
    consider p such that
A15: R[q,p] by A11;
    take f.p;
    thus thesis by A15;
  end;
consider f9 being Function of Funcs(N,LinPreorders A),LinPreorders A such that
A16: for q holds T[q,f9.q] from FUNCT_2:sch 3(A14);
A17: for q,a,b st for i holds a <_q.i, b holds a <_f9.q, b
  proof
    let q,a,b;
    assume
A18: for i holds a <_q.i, b;
    consider p such that
A19: R[q,p] and
A20: f.p = f9.q by A16;
 now
      let i;
  not O[q.i,b,a] by A18;
      hence a <_p.i, b by A19;
    end;
    hence thesis by A1,A20;
  end;
 now
    let q,q9,a,b;
    assume
A21: for i holds (a <_q.i, b iff a <_q9.i, b) & (b <_q.i, a iff b <_q9.i, a);
    consider p such that
A22: R[q,p] and
A23: f.p = f9.q by A16;
    consider p9 such that
A24: R[q9,p9] and
A25: f.p9 = f9.q9 by A16;
 for i holds a <_p.i, b iff a <_p9.i, b
    proof
      let i;
  O[q.i,b,a] iff O[q9.i,b,a] by A21;
      hence thesis by A22,A24;
    end;
    hence a <_f9.q, b iff a <_f9.q9, b by A2,A23,A25;
  end;
  then consider n such that
A26: for q,a,b st a <_q.n, b holds a <_f9.q, b by A3,A17,Th14;
  take n;
  let p;
 now
 rng p c= LinOrders A by RELAT_1:def 19;
then  dom p = N & rng p c= LinPreorders A by FUNCT_2:def 1,XBOOLE_1:1;
    then
reconsider q = p as Element of Funcs(N,LinPreorders A) by FUNCT_2:def 2
    ;
A27: R[q,p]
    proof
      let i;
      let a,b;
  a <_p.i, b or a = b or a >_p.i, b by Th6;
      hence thesis by Th4;
    end;
A28: ex p9 st ( R[q,p9])& f.p9 = f9.q by A16;
    let a,b;
    assume a <_p.n, b;
then  a <_f9.q, b by A26;
    hence a <_f.p, b by A7,A27,A28;
  end;
  hence thesis by Th13;
end;