:: Dickson's lemma
::  by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-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 FUNCT_1, RELAT_1, FUNCOP_1, NAT_1, TARSKI, ARYTM_3, XBOOLE_0,
      SUBSET_1, NUMBERS, XXREAL_0, FINSET_1, CARD_1, ORDERS_2, REARRAN1,
      RELAT_2, STRUCT_0, WELLORD1, WAYBEL_4, WAYBEL20, EQREL_1, ORDERS_1,
      ZFMISC_1, WELLFND1, SETFAM_1, VALUED_0, ORDINAL2, MCART_1, CAT_1,
      YELLOW_1, PBOOLE, CARD_3, RLVECT_2, YELLOW_6, WAYBEL_3, FUNCT_4,
      YELLOW_3, DICKSON;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      PBOOLE, RELSET_1, XXREAL_2, SEQ_4, PARTFUN1, FUNCT_2, CARD_3, ORDINAL1,
      NAT_1, STRUCT_0, RELAT_2, XXREAL_0, FUNCT_4, FUNCOP_1, DOMAIN_1,
      FINSET_1, XTUPLE_0, MCART_1, WELLORD1, ORDERS_2, ORDERS_1, EQREL_1,
      WELLFND1, WAYBEL_0, CARD_1, NUMBERS, WAYBEL_4, VALUED_0, PRALG_1,
      YELLOW_3, WAYBEL_1, YELLOW_1, WAYBEL_3, YELLOW_6;
 constructors WELLORD1, DOMAIN_1, PRALG_1, ORDERS_3, WAYBEL_1, YELLOW_3,
      WAYBEL_3, WAYBEL_4, WELLFND1, SEQ_4, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FUNCOP_1, FINSET_1, XXREAL_0, NAT_1, MEMBERED, EQREL_1, PRE_CIRC,
      STRUCT_0, ORDERS_2, YELLOW_1, YELLOW_3, WAYBEL18, WAYBEL_3, VALUED_0,
      CARD_1, XXREAL_2, CARD_3, ZFMISC_1, RELSET_1, XTUPLE_0;
 requirements BOOLE, SUBSET, NUMERALS;
 definitions TARSKI, RELAT_2, ORDERS_2, ORDERS_1, FUNCOP_1, XTUPLE_0;
 theorems WELLORD1, ORDERS_1, SUBSET_1, TARSKI, RELAT_1, RELAT_2, RELSET_1,
      ZFMISC_1, EQREL_1, WAYBEL_0, ORDERS_2, NAT_1, FUNCT_1, FUNCT_2, CARD_2,
      CARD_1, NORMSP_1, SEQM_3, FINSET_1, AXIOMS, YELLOW_3, WAYBEL_1, WAYBEL20,
      YELLOW_1, CARD_3, FUNCOP_1, WAYBEL_3, MCART_1, FUNCT_4, WELLFND1,
      WAYBEL_4, PRALG_1, YELLOW_6, AFINSQ_1, XBOOLE_0, XBOOLE_1, PARTFUN1,
      XXREAL_0, ORDINAL1, XXREAL_2, VALUED_0, XTUPLE_0;
 schemes PRE_CIRC, RECDEF_1, NAT_1, FUNCT_2, DOMAIN_1, FRAENKEL, FINSEQ_1,
      FUNCT_1, RELSET_1;

begin :: Preliminaries

theorem Th1:
  for g being Function, x being set st dom g = {x} holds g = x .--> g.x
proof
  let g be Function, x be set such that
A1: dom g = {x};
  now
    let a,b be set;
A2: dom (x .-->g.x) = {x} by FUNCOP_1:13;
    hereby
      assume
A3:   [a,b] in g;
      then
A4:   a in {x} by A1,FUNCT_1:1;
      then
A5:   a = x by TARSKI:def 1;
      then b = g.x by A3,FUNCT_1:1;
      then (x.-->g.x).a = b by A5,FUNCOP_1:72;
      hence [a,b] in x.-->g.x by A2,A4,FUNCT_1:1;
    end;
    assume
A6: [a,b] in x.-->g.x;
    then
A7: a in {x} by A2,FUNCT_1:1;
    then
A8: a = x by TARSKI:def 1;
    b = (x.-->g.x).a by A6,FUNCT_1:1
      .= g.a by A8,FUNCOP_1:72;
    hence [a,b] in g by A1,A7,FUNCT_1:1;
  end;
  hence thesis by RELAT_1:def 2;
end;

theorem Th2:
  for n being Nat holds n c= n+1
proof
  let n be Nat;
  n+1 = n \/ {n} by AFINSQ_1:2;
  hence thesis by XBOOLE_1:7;
end;

scheme FinSegRng2{m, n() -> Element of NAT, F(set)->set, P[set]}:
  {F(i) where i is Element of NAT : m()<i & i<=n() & P[i]} is finite
proof
  set F1 = {F(i) where i is Element of NAT: m()<=i & i<=n() & P[i]};
  set F2 = {F(i) where i is Element of NAT: m()< i & i<=n() & P[i]};
A1: F1 is finite from FINSEQ_1:sch 6;
  F2 c= F1
  proof
    let x be set;
    assume x in F2;
    then ex i being Element of NAT st ( F(i) = x)&( m()< i)&( i<=n())& ( P[i]);
    hence thesis;
  end;
  hence thesis by A1;
end;

theorem Th3:
  for X being infinite set ex f being Function of NAT, X st f is one-to-one
proof
  let X be infinite set;
  card NAT c= card X by CARD_1:47,CARD_3:85;
  then consider f being Function such that
A1: f is one-to-one and
A2: dom f = NAT and
A3: rng f c= X by CARD_1:10;
  now
    let x be set;
    assume x in NAT;
    then f.x in rng f by A2,FUNCT_1:3;
    hence f.x in X by A3;
  end;
  then reconsider f as Function of NAT, X by A2,FUNCT_2:3;
  take f;
  thus thesis by A1;
end;

definition
  let R be RelStr, f be sequence of R;
  attr f is ascending means
  for n being Element of NAT
  holds f.(n+1) <> f.n & [f.n, f.(n+1)] in the InternalRel of R;
end;

definition
  let R be RelStr, f be sequence of R;
  attr f is weakly-ascending means
  :Def2:
  for n being Element of NAT holds [f.n, f.(n+1)] in the InternalRel of R;
end;

theorem Th4:
  for R being non empty transitive RelStr, f being sequence of R
  st f is weakly-ascending
  holds for i,j being Element of NAT st i < j holds f.i <= f.j
proof
  let R be non empty transitive RelStr, f be sequence of R such that
A1: f is weakly-ascending;
  let i be Element of NAT;
  defpred P[Element of NAT] means i < $1 implies f.i <= f.$1;
A2: P[ 0 ] by NAT_1:2;
A3: for j being Element of NAT st P[j] holds P[j+1]
  proof
    let j be Element of NAT such that
A4: P[j] and
A5: i < j+1;
    reconsider fj1 = f.(j+1) as Element of R;
A6: [f.j, f.(j+1)] in the InternalRel of R by A1,Def2;
    then
A7: f.j <= fj1 by ORDERS_2:def 5;
A8: i <= j by A5,NAT_1:13;
    per cases by A8,XXREAL_0:1;
    suppose i < j;
      hence thesis by A4,A7,ORDERS_2:3;
    end;
    suppose i = j;
      hence thesis by A6,ORDERS_2:def 5;
    end;
  end;
  thus for j being Element of NAT holds P[j] from NAT_1:sch 1(A2,A3);
end;

theorem Th5:
  for R being non empty RelStr holds R is connected iff
  the InternalRel of R is_strongly_connected_in the carrier of R
proof
  let R be non empty RelStr;
  set IR = the InternalRel of R, CR = the carrier of R;
  hereby
    assume
A1: R is connected;
    now
      let x, y be set such that
A2:   x in CR and
A3:   y in CR;
      reconsider x9=x, y9=y as Element of R by A2,A3;
      x9 <= y9 or y9 <= x9 by A1,WAYBEL_0:def 29;
      hence [x,y] in IR or [y,x] in IR by ORDERS_2:def 5;
    end;
    hence IR is_strongly_connected_in CR by RELAT_2:def 7;
  end;
  assume
A4: IR is_strongly_connected_in CR;
  now
    let x, y be Element of R;
    [x,y] in IR or [y,x] in IR by A4,RELAT_2:def 7;
    hence x <= y or y <= x by ORDERS_2:def 5;
  end;
  hence thesis by WAYBEL_0:def 29;
end;

theorem Th6:
  for L being RelStr, Y being set, a being set
  holds (the InternalRel of L)-Seg(a) misses Y & a in Y iff
  a is_minimal_wrt Y, the InternalRel of L
proof
  let L be RelStr, Y be set, a be set;
  set IR = the InternalRel of L;
  hereby
    assume that
A1: IR-Seg(a) misses Y and
A2: a in Y;
A3: IR-Seg(a) /\ Y = {} by A1,XBOOLE_0:def 7;
    now
      assume ex y being set st y in Y & y<>a & [y,a] in IR;
      then consider y being set such that
A4:   y in Y and
A5:   y <> a and
A6:   [y,a] in IR;
      y in IR-Seg(a) by A5,A6,WELLORD1:1;
      hence contradiction by A3,A4,XBOOLE_0:def 4;
    end;
    hence a is_minimal_wrt Y, IR by A2,WAYBEL_4:def 25;
  end;
  assume
A7: a is_minimal_wrt Y, IR;
  now
    assume not IR-Seg(a) misses Y;
    then IR-Seg(a) /\ Y <> {} by XBOOLE_0:def 7;
    then consider y being set such that
A8: y in IR-Seg(a) /\ Y by XBOOLE_0:def 1;
A9: y in IR-Seg(a) by A8,XBOOLE_0:def 4;
A10: y in Y by A8,XBOOLE_0:def 4;
A11: y <> a by A9,WELLORD1:1;
    [y,a] in IR by A9,WELLORD1:1;
    hence contradiction by A7,A10,A11,WAYBEL_4:def 25;
  end;
  hence IR-Seg(a) misses Y;
  thus thesis by A7,WAYBEL_4:def 25;
end;

theorem Th7:
  for L being non empty transitive antisymmetric RelStr,
  x being Element of L, a, N being set
  st a is_minimal_wrt (the InternalRel of L)-Seg(x) /\ N,(the InternalRel of L)
  holds a is_minimal_wrt N, (the InternalRel of L)
proof
  let L be non empty transitive antisymmetric RelStr,
  x be Element of L, a,N be set such that
  A1: a
 is_minimal_wrt (the InternalRel of L)-Seg(x) /\ N,(the InternalRel of L);
  set IR = the InternalRel of L, CR = the carrier of L;
A2: IR is_transitive_in CR by ORDERS_2:def 3;
  now
A3: a in IR-Seg(x) /\ N by A1,WAYBEL_4:def 25;
    then
A4: a in IR-Seg(x) by XBOOLE_0:def 4;
    then
A5: a <> x by WELLORD1:1;
A6: [a,x] in IR by A4,WELLORD1:1;
    then reconsider a9 = a as Element of L by ZFMISC_1:87;
    thus a in N by A3,XBOOLE_0:def 4;
    now
      assume ex y being set st y in N & y <> a & [y,a] in IR;
      then consider y being set such that
A7:   y in N and
A8:   y <> a and
A9:   [y,a] in IR;
A10:  a in CR by A9,ZFMISC_1:87;
      y in CR by A9,ZFMISC_1:87;
      then
A11:  [y,x] in IR by A2,A6,A9,A10,RELAT_2:def 8;
      per cases;
      suppose x = y;
        then
A12:    x <= a9 by A9,ORDERS_2:def 5;
        a9 <= x by A6,ORDERS_2:def 5;
        hence contradiction by A5,A12,ORDERS_2:2;
      end;
      suppose x <> y;
        then y in IR-Seg(x) by A11,WELLORD1:1;
        then y in IR-Seg(x) /\ N by A7,XBOOLE_0:def 4;
        hence contradiction by A1,A8,A9,WAYBEL_4:def 25;
      end;
    end;
    hence not ex y being set st y in N & y <> a & [y,a] in IR;
  end;
  hence thesis by WAYBEL_4:def 25;
end;

begin :: Chapter 4.2

definition
  let R be RelStr; :: Def 4.19 (ix)
  attr R is quasi_ordered means
  :Def3:
  R is reflexive transitive;
end;

definition :: Lemma 4.24.i
  let R be RelStr such that
B1: R is quasi_ordered;
  func EqRel R -> Equivalence_Relation of the carrier of R equals
  :Def4:
  (the InternalRel of R) /\ (the InternalRel of R)~;
  coherence
  proof
    set IR = the InternalRel of R, CR = the carrier of R;
    R is reflexive by B1,Def3;
    then
A1: IR is_reflexive_in CR by ORDERS_2:def 2;
    R is transitive by B1,Def3;
    then
A2: IR is_transitive_in CR by ORDERS_2:def 3;
    then
A3: IR quasi_orders CR by A1,ORDERS_1:def 6;
A4: IR /\ IR~ is_reflexive_in CR
    proof
      let x be set;
      assume x in CR;
      then
A5:   [x,x] in IR by A1,RELAT_2:def 1;
      then [x,x] in IR~ by RELAT_1:def 7;
      hence thesis by A5,XBOOLE_0:def 4;
    end;
    then
A6: dom(IR /\ IR~) = CR by ORDERS_1:13;
A7: field(IR /\ IR~) = CR by A4,ORDERS_1:13;
A8: IR /\ IR~ is_symmetric_in CR
    proof
      let x,y be set such that x in CR and y in CR and
A9:  [x,y] in IR /\ IR~;
A10:  [x,y] in IR by A9,XBOOLE_0:def 4;
A11:  [x,y] in IR~ by A9,XBOOLE_0:def 4;
A12:  [y,x] in IR~ by A10,RELAT_1:def 7;
      [y,x] in IR by A11,RELAT_1:def 7;
      hence thesis by A12,XBOOLE_0:def 4;
    end;
    IR /\ IR~ is_transitive_in CR
    proof
      let x, y, z be set such that
A13:  x in CR and
A14:  y in CR and
A15:  z in CR and
A16:  [x,y] in IR /\ IR~ and
A17:  [y,z] in IR /\ IR~;
A18:  [x,y] in IR by A16,XBOOLE_0:def 4;
A19:  [x,y] in IR~ by A16,XBOOLE_0:def 4;
A20:  [y,z] in IR by A17,XBOOLE_0:def 4;
A21:  [y,z] in IR~ by A17,XBOOLE_0:def 4;
A22:  [x,z] in IR by A2,A13,A14,A15,A18,A20,RELAT_2:def 8;
      IR~ quasi_orders CR by A3,ORDERS_1:40;
      then IR~ is_transitive_in CR by ORDERS_1:def 6;
      then [x,z] in IR~ by A13,A14,A15,A19,A21,RELAT_2:def 8;
      hence thesis by A22,XBOOLE_0:def 4;
    end;
    hence thesis by A6,A7,A8,PARTFUN1:def 2,RELAT_2:def 11,def 16;
  end;
end;

theorem Th8:
  for R being RelStr, x,y being Element of R
  st R is quasi_ordered holds x in Class(EqRel R, y) iff x <= y & y <= x
proof
  let R be RelStr, x,y be Element of R such that
A1: R is quasi_ordered;
  set IR = the InternalRel of R;
  hereby
    assume x in Class(EqRel R,y);
    then [x,y] in EqRel R by EQREL_1:19;
    then
A2: [x,y] in IR /\ IR~ by A1,Def4;
    then
A3: [x,y] in IR by XBOOLE_0:def 4;
A4: [x,y] in IR~ by A2,XBOOLE_0:def 4;
    thus x <= y by A3,ORDERS_2:def 5;
    [y,x] in IR by A4,RELAT_1:def 7;
    hence y <= x by ORDERS_2:def 5;
  end;
  assume that
A5: x <= y and
A6: y <= x;
A7: [y,x] in IR by A6,ORDERS_2:def 5;
A8: [x,y] in IR by A5,ORDERS_2:def 5;
  [x,y] in IR~ by A7,RELAT_1:def 7;
  then [x,y] in IR /\ IR~ by A8,XBOOLE_0:def 4;
  then [x,y] in EqRel R by A1,Def4;
  hence thesis by EQREL_1:19;
end;

definition :: Lemma 4.24, (the InternalRel of R) / EqRel R
  let R be RelStr;
  func <=E R -> Relation of Class EqRel R means
  :Def5:
  for A, B being set holds [A,B] in it iff ex a, b being Element of R
  st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
  existence
  proof
    set IR = the InternalRel of R, CR = the carrier of R;
    per cases;
    suppose
A1:   CR = {};
      reconsider IT = {} as Relation of Class(EqRel R) by RELSET_1:12;
      take IT;
      let A, B be set;
      thus [A,B] in IT implies ex a, b being Element of R
      st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
      given a, b being Element of R such that
      A = Class(EqRel R, a) and B = Class(EqRel R, b) and
A2:   a <= b;
      IR = {} by A1;
      hence thesis by A2,ORDERS_2:def 5;
    end;
    suppose CR is non empty;
      then reconsider R9 = R as non empty RelStr;
      set IT = {[Class(EqRel R, a), Class(EqRel R, b)]
      where a,b is Element of R9 : a <= b};
      set Y = Class(EqRel R);
      IT c= [:Y,Y:]
      proof
        let x be set;
        assume x in IT;
        then consider a, b being Element of R9 such that
A3:     x = [Class(EqRel R, a), Class(EqRel R, b)] and a <= b;
A4:     Class(EqRel R, a) in Y by EQREL_1:def 3;
        Class(EqRel R, b) in Y by EQREL_1:def 3;
        hence thesis by A3,A4,ZFMISC_1:def 2;
      end;
      then reconsider IT as Relation of Class(EqRel R);
      take IT;
      let A, B be set;
      hereby
        assume [A,B] in IT;
        then consider a,b being Element of R such that
A5:     [A,B] = [Class(EqRel R, a), Class(EqRel R, b)] and
A6:     a <= b;
        reconsider a9 = a, b9 = b as Element of R;
        take a9, b9;
        thus A = Class(EqRel R, a9) & B = Class(EqRel R, b9) &
        a9 <= b9 by A5,A6,XTUPLE_0:1;
      end;
      given a, b being Element of R such that
A7:   A = Class(EqRel R, a) and
A8:   B = Class(EqRel R, b) and
A9:   a <= b;
      thus thesis by A7,A8,A9;
    end;
  end;
  uniqueness
  proof
    let IT1, IT2 be Relation of Class(EqRel R) such that
A10: for A, B being set holds [A,B] in IT1 iff ex a, b being Element of R
    st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b and
A11: for A, B being set holds [A,B] in IT2 iff ex a, b being Element of R
    st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
    now
      let x be set;
      hereby
        assume
A12:    x in IT1;
        set Y = Class(EqRel R);
        consider A, B being set such that A in Y and B in Y and
A13:    x = [A,B] by A12,ZFMISC_1:def 2;
        ex a, b being Element of R st ( A = Class(EqRel R, a))&( B =
        Class(EqRel R, b))&( a <= b) by A10,A12,A13;
        hence x in IT2 by A11,A13;
      end;
      assume
A14:  x in IT2;
      set Y = Class(EqRel R);
      consider A, B being set such that A in Y and B in Y and
A15:  x = [A,B] by A14,ZFMISC_1:def 2;
      ex a, b being Element of R st ( A = Class(EqRel R, a))&( B =
      Class(EqRel R, b))&( a <= b) by A11,A14,A15;
      hence x in IT1 by A10,A15;
    end;
    hence IT1 = IT2 by TARSKI:1;
  end;
end;

theorem Th9: :: Lemma 4.24.ii
  for R being RelStr
  st R is quasi_ordered holds <=E R partially_orders Class(EqRel R)
proof
  let R be RelStr;
  set CR = the carrier of R;
  set IR = the InternalRel of R;
  assume
A1: R is quasi_ordered;
  then R is transitive by Def3;
  then
A2: IR is_transitive_in CR by ORDERS_2:def 3;
  thus <=E R is_reflexive_in Class(EqRel R)
  proof
    let x be set;
    assume x in Class(EqRel R);
    then consider a being set such that
A3: a in CR and
A4: x = Class(EqRel R,a) by EQREL_1:def 3;
    R is reflexive by A1,Def3;
    then IR is_reflexive_in CR by ORDERS_2:def 2;
    then
A5: [a,a] in IR by A3,RELAT_2:def 1;
    reconsider a9= a as Element of R by A3;
    a9 <= a9 by A5,ORDERS_2:def 5;
    hence thesis by A4,Def5;
  end;
  thus <=E R is_transitive_in Class(EqRel R)
  proof
    let x,y,z be set such that
A6: x in Class(EqRel R) and y in Class(EqRel R)
    and z in Class(EqRel R) and
A7: [x,y] in <=E R and
A8: [y,z] in <=E R;
    consider a,b being Element of R such that
A9: x = Class(EqRel R, a) and
A10: y = Class(EqRel R, b) and
A11: a <= b by A7,Def5;
    consider c,d being Element of R such that
A12: y = Class(EqRel R,c) and
A13: z = Class(EqRel R,d) and
A14: c <= d by A8,Def5;
A15: [a,b] in IR by A11,ORDERS_2:def 5;
A16: [c,d] in IR by A14,ORDERS_2:def 5;
A17: ex x1 being set st ( x1 in CR)&( x = Class(EqRel R, x1)) by A6,
EQREL_1:def 3;
    then b in Class(EqRel R, c) by A10,A12,EQREL_1:23;
    then [b,c] in EqRel R by EQREL_1:19;
    then [b,c] in IR/\ IR~ by A1,Def4;
    then [b,c] in IR by XBOOLE_0:def 4;
    then [a,c] in IR by A2,A15,A17,RELAT_2:def 8;
    then [a,d] in IR by A2,A16,A17,RELAT_2:def 8;
    then a<=d by ORDERS_2:def 5;
    hence thesis by A9,A13,Def5;
  end;
  thus <=E R is_antisymmetric_in Class(EqRel R)
  proof
    let x,y be set such that
A18: x in Class(EqRel R) and y in Class(EqRel R) and
A19: [x,y] in <=E R and
A20: [y,x] in <=E R;
    consider a,b being Element of R such that
A21: x = Class(EqRel R, a) and
A22: y = Class(EqRel R, b) and
A23: a <= b by A19,Def5;
    consider c,d being Element of R such that
A24: y = Class(EqRel R, c) and
A25: x = Class(EqRel R, d) and
A26: c <= d by A20,Def5;
A27: [a,b] in IR by A23,ORDERS_2:def 5;
A28: [c,d] in IR by A26,ORDERS_2:def 5;
A29: ex x1 being set st ( x1 in CR)&( x = Class(EqRel R, x1)) by A18,
EQREL_1:def 3;
    then
A30: d in Class(EqRel R, a) by A21,A25,EQREL_1:23;
    a in Class(EqRel R, a) by A29,EQREL_1:20;
    then
A31: [a,d] in EqRel R by A30,EQREL_1:22;
A32: c in Class(EqRel R, b) by A22,A24,A29,EQREL_1:23;
    b in Class(EqRel R, b) by A29,EQREL_1:20;
    then
A33: [b,c] in EqRel R by A32,EQREL_1:22;
    [a,d] in IR /\ IR~ by A1,A31,Def4;
    then [a,d] in IR~ by XBOOLE_0:def 4;
    then
A34: [d,a] in IR by RELAT_1:def 7;
    [b,c] in IR /\ IR~ by A1,A33,Def4;
    then [b,c] in IR by XBOOLE_0:def 4;
    then [b,d] in IR by A2,A28,A29,RELAT_2:def 8;
    then
A35: [b,a] in IR by A2,A29,A34,RELAT_2:def 8;
    [b,a] in IR~ by A27,RELAT_1:def 7;
    then [b,a] in IR /\ IR~ by A35,XBOOLE_0:def 4;
    then [b,a] in EqRel R by A1,Def4;
    then b in Class(EqRel R, a) by EQREL_1:19;
    hence thesis by A21,A22,EQREL_1:23;
  end;
end;

theorem ::Lemma 4.24.iii
  for R being non empty RelStr st R is quasi_ordered & R is connected
  holds <=E R linearly_orders Class(EqRel R)
proof
  let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: R is connected;
A3: <=E R partially_orders Class(EqRel R) by A1,Th9;
  hence <=E R is_reflexive_in Class(EqRel R) by ORDERS_1:def 7;
  thus <=E R is_transitive_in Class(EqRel R) by A3,ORDERS_1:def 7;
  thus <=E R is_antisymmetric_in Class(EqRel R) by A3,ORDERS_1:def 7;
  thus <=E R is_connected_in Class(EqRel R)
  proof
    set CR = the carrier of R;
    let x, y be set such that
A4: x in Class(EqRel R) and
A5: y in Class(EqRel R) and x <> y and
A6: not [x,y] in <=E R;
    consider a being set such that
A7: a in CR and
A8: x = Class(EqRel R, a) by A4,EQREL_1:def 3;
    consider b being set such that
A9: b in CR and
A10: y = Class(EqRel R, b) by A5,EQREL_1:def 3;
    reconsider a9=a,b9=b as Element of R by A7,A9;
    not a9 <= b9 by A6,A8,A10,Def5;
    then b9 <= a9 by A2,WAYBEL_0:def 29;
    hence thesis by A8,A10,Def5;
  end;
end;

definition :: "strict part" of a relation, p. 155
  let R be Relation;
  func R\~ -> Relation equals
  R \ R~;
  correctness;
end;

registration
  let R be Relation;
  cluster R \~ -> asymmetric;
  coherence
  proof
    now
      let x,y be set such that x in field (R\~) and
      y in field (R\~) and
A1:   [x,y] in R\~;
      not [x,y] in R~ by A1,XBOOLE_0:def 5;
      hence not [y,x] in R\~ by RELAT_1:def 7;
    end;
    then R \~ is_asymmetric_in field (R\~) by RELAT_2:def 5;
    hence thesis by RELAT_2:def 13;
  end;
end;

definition
  let X be set, R be Relation of X;
  redefine func R\~ -> Relation of X;
  coherence
  proof
    R\~ = R \ R~;
    hence thesis;
  end;
end;

definition
  let R be RelStr;
  func R\~ -> strict RelStr equals
  RelStr(# the carrier of R, (the InternalRel of R)\~ #);
  correctness;
end;

registration
  let R be non empty RelStr;
  cluster R\~ -> non empty;
  coherence;
end;

registration
  let R be transitive RelStr;
  cluster R\~ -> transitive;
  coherence
  proof
    set IR = the InternalRel of R, CR = the carrier of R;
    set IR9= the InternalRel of R\~, CR9 = the carrier of R\~;
A1: IR is_transitive_in CR by ORDERS_2:def 3;
    now
      let x,y,z be set such that
A2:   x in CR9 and
A3:   y in CR9 and
A4:   z in CR9 and
A5:   [x,y] in IR9 and
A6:   [y,z] in IR9;
A7:   not [x,y] in IR~ by A5,XBOOLE_0:def 5;
A8:   [x,z] in IR by A1,A2,A3,A4,A5,A6,RELAT_2:def 8;
      now
        assume [x,z] in IR~;
        then [z, x] in IR by RELAT_1:def 7;
        then [y, x] in IR by A1,A2,A3,A4,A6,RELAT_2:def 8;
        hence contradiction by A7,RELAT_1:def 7;
      end;
      hence [x,z] in IR9 by A8,XBOOLE_0:def 5;
    end;
    then IR9 is_transitive_in CR9 by RELAT_2:def 8;
    hence thesis by ORDERS_2:def 3;
  end;
end;

registration
  let R be RelStr;
  cluster R\~ -> antisymmetric;
  coherence
  proof
    set IR = the InternalRel of R;
    set IR9= the InternalRel of R\~, CR9 = the carrier of R\~;
    now
      let x, y be set such that x in CR9 and y in CR9 and
A1:   [x,y] in IR9 and
A2:   [y,x] in IR9;
      not [x,y] in IR~ by A1,XBOOLE_0:def 5;
      hence x = y by A2,RELAT_1:def 7;
    end;
    then IR9 is_antisymmetric_in CR9 by RELAT_2:def 4;
    hence thesis by ORDERS_2:def 4;
  end;
end;

theorem ::Exercise 4.27:
  for R being non empty Poset, x being Element of R
  holds Class(EqRel R, x) = {x}
proof
  let R be non empty Poset;
  set IR = the InternalRel of R, CR = the carrier of R;
  let x be Element of CR;
A1: R is quasi_ordered by Def3;
A2: IR is_antisymmetric_in CR by ORDERS_2:def 4;
  now
    let z be set;
    hereby
      assume z in Class(EqRel R, x);
      then [z,x] in EqRel R by EQREL_1:19;
      then
A3:   [z,x] in IR /\ IR~ by A1,Def4;
      then
A4:   [z,x] in IR by XBOOLE_0:def 4;
      [z,x] in IR~ by A3,XBOOLE_0:def 4;
      then
A5:   [x,z] in IR by RELAT_1:def 7;
      z in dom IR by A4,XTUPLE_0:def 12;
      then z = x by A2,A4,A5,RELAT_2:def 4;
      hence z in {x} by TARSKI:def 1;
    end;
    assume z in {x};
    then z = x by TARSKI:def 1;
    hence z in Class(EqRel R, x) by EQREL_1:20;
  end;
  hence thesis by TARSKI:1;
end;

theorem :: Exercise 4.29.i
  for R being Relation holds R = R\~ iff R is asymmetric
proof
  let R be Relation;
  thus R = R\~ implies R is asymmetric;
  assume R is asymmetric;
  then
A1: R is_asymmetric_in field R by RELAT_2:def 13;
  now
    let a,b be set;
    hereby
      assume
A2:   [a,b] in R;
      then
A3:   a in field R by RELAT_1:15;
      b in field R by A2,RELAT_1:15;
      then not [b,a] in R by A1,A2,A3,RELAT_2:def 5;
      then not [a,b] in R~ by RELAT_1:def 7;
      hence [a,b] in R\~ by A2,XBOOLE_0:def 5;
    end;
    assume [a,b] in R\~;
    hence [a,b] in R;
  end;
  hence thesis by RELAT_1:def 2;
end;

theorem :: Exercise 4.29.ii
  for R being Relation st R is transitive holds R\~ is transitive
proof
  let R be Relation;
  assume R is transitive;
  then
A1: R is_transitive_in field R by RELAT_2:def 16;
  now
    let x, y, z be set such that
    x in field (R\~) and y in field (R\~)
    and z in field (R\~) and
A2: [x,y] in R\~ and
A3: [y,z] in R\~;
A4: x in field R by A2,RELAT_1:15;
A5: y in field R by A2,RELAT_1:15;
A6: z in field R by A3,RELAT_1:15;
    then
A7: [x,z] in R by A1,A2,A3,A4,A5,RELAT_2:def 8;
    not [x,y] in R~ by A2,XBOOLE_0:def 5;
    then not [y,x] in R by RELAT_1:def 7;
    then not [z,x] in R by A1,A3,A4,A5,A6,RELAT_2:def 8;
    then not [x,z] in R~ by RELAT_1:def 7;
    hence [x,z] in R\~ by A7,XBOOLE_0:def 5;
  end;
  then R\~ is_transitive_in field (R\~) by RELAT_2:def 8;
  hence thesis by RELAT_2:def 16;
end;

theorem :: Exercise 4.29.iii
  for R being Relation, a, b being set st R is antisymmetric
  holds [a,b] in R\~ iff [a,b] in R & a <> b
proof
  let R be Relation, a, b be set;
  assume R is antisymmetric;
  then
A1: R is_antisymmetric_in field R by RELAT_2:def 12;
A2: R\~ is_asymmetric_in field (R\~) by RELAT_2:def 13;
  hereby
    assume
A3: [a,b] in R\~;
    hence [a,b] in R;
    now
      assume
A4:   a = b;
      a in field (R\~) by A3,RELAT_1:15;
      hence contradiction by A2,A3,A4,RELAT_2:def 5;
    end;
    hence a <> b;
  end;
  assume that
A5: [a,b] in R and
A6: a <> b;
A7: a in field R by A5,RELAT_1:15;
  b in field R by A5,RELAT_1:15;
  then not [b,a] in R by A1,A5,A6,A7,RELAT_2:def 4;
  then not [a,b] in R~ by RELAT_1:def 7;
  hence thesis by A5,XBOOLE_0:def 5;
end;

theorem Th15: :: Exercise 4.29 (addition)
  for R being RelStr st R is well_founded holds R\~ is well_founded
proof
  let R be RelStr such that
A1: R is well_founded;
  set IR = the InternalRel of R, CR = the carrier of R;
  set IR9 = the InternalRel of R\~, CR9 = the carrier of R\~;
A2: IR is_well_founded_in CR by A1,WELLFND1:def 2;
  now
    let Y be set such that
A3: Y c= CR9 and
A4: Y <> {};
    consider a being set such that
A5: a in Y and
A6: IR-Seg(a) misses Y by A2,A3,A4,WELLORD1:def 3;
A7: IR-Seg(a) /\ Y = {} by A6,XBOOLE_0:def 7;
    take a;
    thus a in Y by A5;
    now
      assume ex z being set st z in IR9-Seg(a) /\ Y;
      then consider z being set such that
A8:   z in IR9-Seg(a) /\ Y;
A9:   z in IR9-Seg(a) by A8,XBOOLE_0:def 4;
A10:  z in Y by A8,XBOOLE_0:def 4;
A11:  z <> a by A9,WELLORD1:1;
      [z,a] in IR9 by A9,WELLORD1:1;
      then z in IR-Seg(a) by A11,WELLORD1:1;
      hence contradiction by A7,A10,XBOOLE_0:def 4;
    end;
    then IR9-Seg(a) /\ Y = {} by XBOOLE_0:def 1;
    hence IR9-Seg(a) misses Y by XBOOLE_0:def 7;
  end;
  then IR9 is_well_founded_in CR9 by WELLORD1:def 3;
  hence thesis by WELLFND1:def 2;
end;

theorem Th16: :: Exercise 4.29 (addition)
  for R being RelStr
  st R\~ is well_founded & R is antisymmetric holds R is well_founded
proof
  let R be RelStr such that
A1: R\~ is well_founded and
A2: R is antisymmetric;
  set IR = the InternalRel of R, CR = the carrier of R;
  set IR9 = the InternalRel of R\~;
A3: IR is_antisymmetric_in CR by A2,ORDERS_2:def 4;
A4: IR9 is_well_founded_in CR by A1,WELLFND1:def 2;
  now
    let Y be set such that
A5: Y c= CR and
A6: Y <> {};
    consider a being set such that
A7: a in Y and
A8: IR9-Seg(a) misses Y by A4,A5,A6,WELLORD1:def 3;
A9: IR9-Seg(a) /\ Y = {} by A8,XBOOLE_0:def 7;
    take a;
    thus a in Y by A7;
    now
      assume IR-Seg(a) /\ Y <> {};
      then consider z being set such that
A10:  z in IR-Seg(a) /\ Y by XBOOLE_0:def 1;
A11:  z in IR-Seg(a) by A10,XBOOLE_0:def 4;
A12:  z in Y by A10,XBOOLE_0:def 4;
A13:  z <> a by A11,WELLORD1:1;
A14:  [z,a] in IR by A11,WELLORD1:1;
      then not [a,z] in IR by A3,A5,A7,A12,A13,RELAT_2:def 4;
      then not [z,a] in IR~ by RELAT_1:def 7;
      then [z,a] in IR \ IR~ by A14,XBOOLE_0:def 5;
      then z in IR9-Seg(a) by A13,WELLORD1:1;
      hence contradiction by A9,A12,XBOOLE_0:def 4;
    end;
    hence IR-Seg(a) misses Y by XBOOLE_0:def 7;
  end;
  then IR is_well_founded_in CR by WELLORD1:def 3;
  hence thesis by WELLFND1:def 2;
end;

begin :: Chapter 4.3

theorem Th17: :: Def 4.30 (see WAYBEL_4:def 26)
  for L being RelStr, N being set, x being Element of L\~
  holds x is_minimal_wrt N, the InternalRel of (L\~) iff (x in N &
  for y being Element of L st y in N & [y,x] in the InternalRel of L
  holds [x,y] in the InternalRel of L)
proof
  let L be RelStr, N be set, x be Element of L\~;
  set IR = the InternalRel of L;
  set IR9 = the InternalRel of L\~;
  hereby
    assume
A1: x is_minimal_wrt N, the InternalRel of (L\~);
    hence x in N by WAYBEL_4:def 25;
    let y be Element of L such that
A2: y in N;
    assume
A3: [y,x] in IR;
    now per cases;
      suppose x = y;
        hence [x,y] in IR by A3;
      end;
      suppose x <> y;
        then not [y,x] in IR9 by A1,A2,WAYBEL_4:def 25;
        then [y,x] in IR~ by A3,XBOOLE_0:def 5;
        hence [x,y] in IR by RELAT_1:def 7;
      end;
    end;
    hence [x,y] in the InternalRel of L;
  end;
  assume that
A4: x in N and
A5: for y being Element of L st y in N holds [y,x] in (the InternalRel
  of L) implies [x,y] in (the InternalRel of L);
  now
    assume ex y being set st y in N & y <> x & [y,x] in IR9;
    then consider y being set such that
A6: y in N and y <> x and
A7: [y,x] in IR9;
    reconsider y9=y as Element of L by A7,ZFMISC_1:87;
A8: not [y,x] in IR~ by A7,XBOOLE_0:def 5;
    [y9,x] in IR implies [x,y9] in IR by A5,A6;
    hence contradiction by A7,A8,RELAT_1:def 7;
  end;
  hence thesis by A4,WAYBEL_4:def 25;
end;

:: Proposition 4.31 - see WELLFND1:15
:: Omitting Example 4.32, Exercise 4.33, Exercise 4.34

theorem ::L_4_35: :: Lemma 4.35
  for R, S being non empty RelStr, m being Function of R,S
  st R is quasi_ordered & S is antisymmetric & S\~ is well_founded &
  for a,b being Element of R holds
  (a <= b implies m.a <= m.b) & (m.a = m.b implies [a,b] in EqRel R)
  holds R\~ is well_founded
proof
  let R, S be non empty RelStr, m be Function of R, S such that
A1: R is quasi_ordered and
A2: S is antisymmetric and
A3: S\~ is well_founded and
A4: for a,b being Element of R holds (a <= b implies m.a <= m.b) &
  (m.a = m.b implies [a,b] in EqRel R);
  set IR = the InternalRel of R, IS = the InternalRel of S;
A5: IS is_antisymmetric_in the carrier of S by A2,ORDERS_2:def 4;
  now
    assume ex f being sequence of R\~ st f is descending;
    then consider f being sequence of R\~ such that
A6: f is descending;
    reconsider f9=f as sequence of R;
    deffunc F(Element of NAT) = m.(f9.$1);
    consider g9 being Function of NAT, the carrier of S such that
A7: for k being Element of NAT holds g9.k = F(k) from FUNCT_2:sch 4;
    reconsider g=g9 as sequence of S\~;
    now
      let n be Nat;
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A8:   [f.(n+1), f.n] in the InternalRel of R\~ by A6,WELLFND1:def 6;
A9:   [f.(n+1), f.n] in IR \ IR~ by A6,WELLFND1:def 6;
A10:  not [f.(n+1), f.n] in IR~ by A8,XBOOLE_0:def 5;
A11:  g.n1 = m.(f.n1) by A7;
A12:  now
        assume g.(n+1) = g.n;
        then m.(f.(n+1)) = m.(f.n) by A7,A11;
        then [f9.(n+1), f9.n] in EqRel R by A4;
        then [f.(n+1), f.n] in (IR /\ IR~) by A1,Def4;
        hence contradiction by A10,XBOOLE_0:def 4;
      end;
      hence g.(n+1) <> g.n;
      reconsider fn1 = f.(n+1) as Element of R;
      reconsider fn = f.n as Element of R;
A13:  fn1 <= fn by A9,ORDERS_2:def 5;
A14:  g9.(n+1) = m.fn1 by A7;
      g9.n1 = m.fn by A7;
      then g9.(n+1) <= g9.n by A4,A13,A14;
      then
A15:  [g.(n+1), g.n] in IS by ORDERS_2:def 5;
      then not [g.n, g.(n+1)] in IS by A5,A12,RELAT_2:def 4;
      then not [g.(n+1), g.n] in IS~ by RELAT_1:def 7;
      hence [g.(n+1), g.n] in the InternalRel of S\~ by A15,XBOOLE_0:def 5;
    end;
    then g is descending by WELLFND1:def 6;
    hence contradiction by A3,WELLFND1:14;
  end;
  hence thesis by WELLFND1:14;
end;

definition :: p. 158, restricted eq classes
  let R be non empty RelStr, N be Subset of R;
  func min-classes N -> Subset-Family of R means
  :Def8:
  for x being set holds x in it iff ex y being Element of R\~
  st y is_minimal_wrt N, the InternalRel of (R\~) & x = Class(EqRel R,y) /\ N;
  existence
  proof
    set IR9 = the InternalRel of R\~;
    set C = {x /\ N where x is Element of Class(EqRel R) :
    ex y being Element of R\~ st x = Class(EqRel R, y) &
    y is_minimal_wrt N, IR9};
    now
      let x be set;
      assume x in C;
      then ex xx being Element of Class(EqRel R) st ( x = xx /\ N)&( ex
y being Element of R\~ st xx = Class(EqRel R, y) & y is_minimal_wrt N, IR9);
      hence x in bool the carrier of R;
    end;
    then reconsider C as Subset-Family of R by TARSKI:def 3;
    take C;
    let x be set;
    hereby
      assume x in C;
      then ex xx being Element of Class(EqRel R) st ( x = xx /\ N)&( ex
y being Element of R\~ st xx = Class(EqRel R, y) & y is_minimal_wrt N, IR9);
      hence ex y being Element of R\~ st y is_minimal_wrt N, IR9 &
      x = Class(EqRel R,y) /\ N;
    end;
    given y being Element of R\~ such that
A1: y is_minimal_wrt N, IR9 and
A2: x = Class(EqRel R,y) /\ N;
    reconsider y9 = y as Element of R;
    EqClass(EqRel R, y9) in Class(EqRel R);
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    set IR = the InternalRel of R\~;
    let IT1, IT2 be Subset-Family of R such that
A3: for x being set holds x in IT1 iff
    ex y being Element of R\~ st y is_minimal_wrt N, IR &
    x = Class(EqRel R,y) /\ N and
A4: for x being set holds x in IT2 iff
    ex y being Element of R\~ st y is_minimal_wrt N, IR &
    x = Class(EqRel R, y) /\ N;
    now
      let x be set;
      hereby
        assume x in IT1;
        then ex y being Element of R\~ st y is_minimal_wrt N, IR &
        x = Class(EqRel R,y) /\ N by A3;
        hence x in IT2 by A4;
      end;
      assume x in IT2;
      then ex y being Element of R\~ st y is_minimal_wrt N, IR &
      x = Class(EqRel R,y) /\ N by A4;
      hence x in IT1 by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th19: :: Lemma 4.36
  for R being non empty RelStr, N being Subset of R, x being set
  st R is quasi_ordered & x in min-classes N
  holds for y being Element of R\~ st y in x
  holds y is_minimal_wrt N, the InternalRel of R\~
proof
  let R be non empty RelStr, N be Subset of R, x be set such that
A1: R is quasi_ordered and
A2: x in min-classes N;
  set IR = the InternalRel of R, CR = the carrier of R;
  set IR9 = the InternalRel of R\~;
  let c be Element of R\~ such that
A3: c in x;
  consider b being Element of R\~ such that
A4: b is_minimal_wrt N, IR9 and
A5: x = Class(EqRel R, b) /\ N by A2,Def8;
  c in Class(EqRel R, b) by A3,A5,XBOOLE_0:def 4;
  then [c,b] in EqRel R by EQREL_1:19;
  then [c,b] in IR /\ IR~ by A1,Def4;
  then
A6: [c,b] in IR by XBOOLE_0:def 4;
A7: now
    assume ex d being set st d in N & d <> c & [d,c] in IR9;
    then consider d being set such that
A8: d in N and d <> c and
A9: [d,c] in IR9;
A10: not [d,c] in IR~ by A9,XBOOLE_0:def 5;
    R is transitive by A1,Def3;
    then
A11: IR is_transitive_in CR by ORDERS_2:def 3;
    then
A12: [d,b] in IR by A6,A8,A9,RELAT_2:def 8;
    now
      assume [d,b] in IR~;
      then [b,d] in IR by RELAT_1:def 7;
      then [c,d] in IR by A6,A8,A11,RELAT_2:def 8;
      hence contradiction by A10,RELAT_1:def 7;
    end;
    then
A13: [d,b] in IR9 by A12,XBOOLE_0:def 5;
    b <> d by A6,A10,RELAT_1:def 7;
    hence contradiction by A4,A8,A13,WAYBEL_4:def 25;
  end;
  c in N by A3,A5,XBOOLE_0:def 4;
  hence thesis by A7,WAYBEL_4:def 25;
end;

theorem Th20:
  for R being non empty RelStr holds R\~ is well_founded iff
  for N being Subset of R st N <> {} ex x being set st x in min-classes N
proof
  let R be non empty RelStr;
  set CR = the carrier of R;
  set IR9= the InternalRel of R\~, CR9 = the carrier of R\~;
  hereby
    assume R\~ is well_founded;
    then
A1: IR9 is_well_founded_in CR9 by WELLFND1:def 2;
    let N be Subset of CR such that
A2: N <> {};
    reconsider N9=N as Subset of CR9;
    consider y being set such that
A3: y in N9 and
A4: IR9-Seg(y) misses N9 by A1,A2,WELLORD1:def 3;
A5: IR9-Seg(y) /\ N9 = {} by A4,XBOOLE_0:def 7;
    reconsider y as Element of R\~ by A3;
    set x = Class(EqRel R, y) /\ N;
    now
      assume ex z being set st z in N & z <> y & [z,y] in IR9;
      then consider z being set such that
A6:   z in N and
A7:   z <> y and
A8:   [z,y] in IR9;
      z in IR9-Seg(y) by A7,A8,WELLORD1:1;
      hence contradiction by A5,A6,XBOOLE_0:def 4;
    end;
    then y is_minimal_wrt N, IR9 by A3,WAYBEL_4:def 25;
    then x in min-classes N by Def8;
    hence ex x being set st x in min-classes N;
  end;
  assume
A9: for N being Subset of R st N <> {} ex x being set st x in min-classes N;
  now
    let N be set such that
A10: N c= CR9 and
A11: N <> {};
    reconsider N9=N as Subset of R by A10;
    consider x being set such that
A12: x in min-classes N9 by A9,A11;
    consider a being Element of R\~ such that
A13: a is_minimal_wrt N9, IR9 and x = Class(EqRel R, a) /\ N9 by A12,Def8;
    reconsider a9=a as set;
    take a9;
    thus a9 in N by A13,WAYBEL_4:def 25;
    now
      assume IR9-Seg(a9) /\ N <> {};
      then consider z being set such that
A14:  z in IR9-Seg(a9) /\ N by XBOOLE_0:def 1;
A15:  z in IR9-Seg(a9) by A14,XBOOLE_0:def 4;
A16:  z in N by A14,XBOOLE_0:def 4;
      then reconsider z as Element of R\~ by A10;
A17:  z <> a9 by A15,WELLORD1:1;
      [z,a] in IR9 by A15,WELLORD1:1;
      hence contradiction by A13,A16,A17,WAYBEL_4:def 25;
    end;
    hence IR9-Seg(a9) misses N by XBOOLE_0:def 7;
  end;
  then IR9 is_well_founded_in CR9 by WELLORD1:def 3;
  hence thesis by WELLFND1:def 2;
end;

theorem Th21:
  for R being non empty RelStr, N being Subset of R, y being Element of R\~
  st y is_minimal_wrt N, the InternalRel of (R\~)
  holds min-classes N is non empty
proof
  let R be non empty RelStr, N be Subset of R, y be Element of R\~ such that
A1: y is_minimal_wrt N, the InternalRel of (R\~);
  ex x being set st ( x = Class(EqRel R,y) /\ N);
  hence thesis by A1,Def8;
end;

theorem Th22:
  for R being non empty RelStr, N being Subset of R, x being set st
  x in min-classes N holds x is non empty
proof
  let R be non empty RelStr, N be Subset of R, x be set;
  assume x in min-classes N;
  then consider y being Element of R\~ such that
A1: y is_minimal_wrt N, the InternalRel of R\~ and
A2: x = Class(EqRel R, y) /\ N by Def8;
A3: y in N by A1,WAYBEL_4:def 25;
  y in Class(EqRel R, y) by EQREL_1:20;
  hence thesis by A2,A3,XBOOLE_0:def 4;
end;

theorem Th23: :: Lemma 4.37
  for R being non empty RelStr st R is quasi_ordered
  holds R is connected & R\~ is well_founded iff
  for N being non empty Subset of R holds card min-classes N = 1
proof
  let R be non empty RelStr such that
A1: R is quasi_ordered;
  set IR = the InternalRel of R, CR = the carrier of R;
  set IR9 = the InternalRel of R\~;
  hereby
    assume that
A2: R is connected and
A3: R\~ is well_founded;
    let N be non empty Subset of CR;
    consider x being set such that
A4: x in min-classes N by A3,Th20;
    consider a being Element of R\~ such that
A5: a is_minimal_wrt N, the InternalRel of (R\~) and
A6: x = Class(EqRel R, a) /\ N by A4,Def8;
A7: a in N by A5,WAYBEL_4:def 25;
    now
      let y be set;
      hereby
        assume y in min-classes N;
        then consider b being Element of R\~ such that
A8:     b is_minimal_wrt N, IR9 and
A9:     y = Class(EqRel R, b) /\ N by Def8;
A10:    b in N by A8,WAYBEL_4:def 25;
        reconsider a9=a as Element of R;
        reconsider b9=b as Element of R;
A11:    now per cases by A2,WAYBEL_0:def 29;
          suppose
A12:        a9 <= b9;
            then
A13:        [a, b] in IR by ORDERS_2:def 5;
            now per cases;
              suppose a = b;
                hence [b,a] in IR by A12,ORDERS_2:def 5;
              end;
              suppose
A14:            a <> b;
                now
                  assume not [b,a] in IR;
                  then not [a,b] in IR~ by RELAT_1:def 7;
                  then [a,b] in IR \ IR~ by A13,XBOOLE_0:def 5;
                  hence contradiction by A7,A8,A14,WAYBEL_4:def 25;
                end;
                hence [b,a] in IR;
              end;
            end;
            hence [a,b] in IR & [b,a] in IR by A12,ORDERS_2:def 5;
          end;
          suppose
A15:        b9 <= a9;
            then
A16:        [b, a] in IR by ORDERS_2:def 5;
            now per cases;
              suppose a = b;
                hence [a,b] in IR by A15,ORDERS_2:def 5;
              end;
              suppose
A17:            a <> b;
                now
                  assume not [a,b] in IR;
                  then not [b,a] in IR~ by RELAT_1:def 7;
                  then [b,a] in IR \ IR~ by A16,XBOOLE_0:def 5;
                  hence contradiction by A5,A10,A17,WAYBEL_4:def 25;
                end;
                hence [a,b] in IR;
              end;
            end;
            hence [a,b] in IR & [b,a] in IR by A15,ORDERS_2:def 5;
          end;
        end;
        then [b,a] in IR~ by RELAT_1:def 7;
        then [b,a] in IR /\ IR~ by A11,XBOOLE_0:def 4;
        then [b,a] in EqRel R by A1,Def4;
        then b in Class(EqRel R, a) by EQREL_1:19;
        then Class(EqRel R, b) = Class(EqRel R, a) by EQREL_1:23;
        hence y in {x} by A6,A9,TARSKI:def 1;
      end;
      assume y in {x};
      then y = Class(EqRel R, a) /\ N by A6,TARSKI:def 1;
      hence y in min-classes N by A5,Def8;
    end;
    then min-classes N = {x} by TARSKI:1;
    hence card min-classes N = 1 by CARD_1:30;
  end;
  assume
A18: for N being non empty Subset of R holds card min-classes N = 1;
  now
    let a,b be Element of R;
    assume that
A19: not a <= b and
A20: not a >= b;
A21: not [a,b] in IR by A19,ORDERS_2:def 5;
    then
A22: not [b,a] in IR~ by RELAT_1:def 7;
    not [b,a] in IR by A20,ORDERS_2:def 5;
    then
A23: not [a,b] in IR~ by RELAT_1:def 7;
    set N9 = {a,b};
    set MCN = {{a},{b}};
    now
      let x be set;
      hereby
        assume x in min-classes N9;
        then consider y being Element of R\~ such that
A24:    y is_minimal_wrt N9, IR9 and
A25:    x = Class(EqRel R, y) /\ N9 by Def8;
A26:    y in N9 by A24,WAYBEL_4:def 25;
        per cases by A26,TARSKI:def 2;
        suppose
A27:      y = a;
          now
            let z be set;
            hereby
              assume
A28:          z in x;
              then
A29:          z in Class(EqRel R,a) by A25,A27,XBOOLE_0:def 4;
A30:          z in N9 by A25,A28,XBOOLE_0:def 4;
              now per cases by A30,TARSKI:def 2;
                suppose z = a;
                  hence z in {a} by TARSKI:def 1;
                end;
                suppose z = b;
                  then [b,a] in EqRel R by A29,EQREL_1:19;
                  then [b,a] in IR /\ IR~ by A1,Def4;
                  hence z in {a} by A22,XBOOLE_0:def 4;
                end;
              end;
              hence z in {a};
            end;
            assume z in {a};
            then
A31:        z = a by TARSKI:def 1;
            then
A32:        z in N9 by TARSKI:def 2;
            z in Class(EqRel R, a) by A31,EQREL_1:20;
            hence z in x by A25,A27,A32,XBOOLE_0:def 4;
          end;
          then x = {a} by TARSKI:1;
          hence x in MCN by TARSKI:def 2;
        end;
        suppose
A33:      y = b;
          now
            let z be set;
            hereby
              assume
A34:          z in x;
              then
A35:          z in Class(EqRel R,b) by A25,A33,XBOOLE_0:def 4;
A36:          z in N9 by A25,A34,XBOOLE_0:def 4;
              now per cases by A36,TARSKI:def 2;
                suppose z = b;
                  hence z in {b} by TARSKI:def 1;
                end;
                suppose z = a;
                  then [a,b] in EqRel R by A35,EQREL_1:19;
                  then [a,b] in IR /\ IR~ by A1,Def4;
                  hence z in {b} by A21,XBOOLE_0:def 4;
                end;
              end;
              hence z in {b};
            end;
            assume z in {b};
            then
A37:        z = b by TARSKI:def 1;
            then
A38:        z in N9 by TARSKI:def 2;
            z in Class(EqRel R, b) by A37,EQREL_1:20;
            hence z in x by A25,A33,A38,XBOOLE_0:def 4;
          end;
          then x = {b} by TARSKI:1;
          hence x in MCN by TARSKI:def 2;
        end;
      end;
      assume
A39:  x in MCN;
      per cases by A39,TARSKI:def 2;
      suppose
A40:    x = {a};
        now reconsider a9=a as Element of R\~;
          take a9;
A41:      a9 in N9 by TARSKI:def 2;
          now
            assume ex y being set st y in N9 & y <> a9 & [y,a9] in IR9;
            then consider y being set such that
A42:        y in N9 and
A43:        y <> a9 and
A44:        [y,a9] in IR9;
            y = b by A42,A43,TARSKI:def 2;
            hence contradiction by A20,A44,ORDERS_2:def 5;
          end;
          hence a9 is_minimal_wrt N9, the InternalRel of (R\~)
          by A41,WAYBEL_4:def 25;
          now
            let z be set;
            hereby
              assume z in x;
              then
A45:          z = a by A40,TARSKI:def 1;
              then z in Class(EqRel R, a) by EQREL_1:20;
              hence z in Class(EqRel R, a) /\ N9 by A41,A45,XBOOLE_0:def 4;
            end;
            assume
A46:        z in Class(EqRel R, a) /\ N9;
            then
A47:        z in Class(EqRel R, a) by XBOOLE_0:def 4;
A48:        z in N9 by A46,XBOOLE_0:def 4;
            per cases by A48,TARSKI:def 2;
            suppose z = a;
              hence z in x by A40,TARSKI:def 1;
            end;
            suppose z = b;
              then [b,a] in EqRel R by A47,EQREL_1:19;
              then [b,a] in IR /\ IR~ by A1,Def4;
              hence z in x by A22,XBOOLE_0:def 4;
            end;
          end;
          hence x = Class(EqRel R, a9) /\ N9 by TARSKI:1;
        end;
        hence x in min-classes N9 by Def8;
      end;
      suppose
A49:    x = {b};
        now reconsider b9=b as Element of R\~;
          take b9;
A50:      b9 in N9 by TARSKI:def 2;
          now
            assume ex y being set st y in N9 & y <> b9 & [y,b9] in IR9;
            then consider y being set such that
A51:        y in N9 and
A52:        y <> b9 and
A53:        [y,b9] in IR9;
            y = a by A51,A52,TARSKI:def 2;
            hence contradiction by A19,A53,ORDERS_2:def 5;
          end;
          hence b9 is_minimal_wrt N9, the InternalRel of (R\~)
          by A50,WAYBEL_4:def 25;
          now
            let z be set;
            hereby
              assume z in x;
              then
A54:          z = b by A49,TARSKI:def 1;
              then z in Class(EqRel R, b) by EQREL_1:20;
              hence z in Class(EqRel R, b) /\ N9 by A50,A54,XBOOLE_0:def 4;
            end;
            assume
A55:        z in Class(EqRel R, b) /\ N9;
            then
A56:        z in Class(EqRel R, b) by XBOOLE_0:def 4;
A57:        z in N9 by A55,XBOOLE_0:def 4;
            per cases by A57,TARSKI:def 2;
            suppose z = b;
              hence z in x by A49,TARSKI:def 1;
            end;
            suppose z = a;
              then [a,b] in EqRel R by A56,EQREL_1:19;
              then [a,b] in IR /\ IR~ by A1,Def4;
              hence z in x by A23,XBOOLE_0:def 4;
            end;
          end;
          hence x = Class(EqRel R, b9) /\ N9 by TARSKI:1;
        end;
        hence x in min-classes N9 by Def8;
      end;
    end;
    then min-classes N9 = MCN by TARSKI:1;
    then
A58: card MCN = 1 by A18;
    now
      assume {a} = {b};
      then
A59:  a = b by ZFMISC_1:3;
      R is reflexive by A1,Def3;
      then IR is_reflexive_in CR by ORDERS_2:def 2;
      hence contradiction by A21,A59,RELAT_2:def 1;
    end;
    hence contradiction by A58,CARD_2:57;
  end;
  hence R is connected by WAYBEL_0:def 29;
  now
    let N be Subset of R;
    assume N <> {};
    then card min-classes N = 1 by A18;
    then min-classes N <> {};
    hence ex x being set st x in min-classes N by XBOOLE_0:def 1;
  end;
  hence thesis by Th20;
end;

theorem :: Lemma 4.38
  for R being non empty Poset
  holds the InternalRel of R well_orders the carrier of R iff
  for N being non empty Subset of R holds card min-classes N = 1
proof
  let R be non empty Poset;
  set IR = the InternalRel of R, CR = the carrier of R;
A1: R is quasi_ordered by Def3;
  hereby
    assume
A2: IR well_orders CR;
    then
A3: IR is_reflexive_in CR by WELLORD1:def 5;
A4: IR is_connected_in CR by A2,WELLORD1:def 5;
A5: IR is_well_founded_in CR by A2,WELLORD1:def 5;
    IR is_strongly_connected_in CR by A3,A4,ORDERS_1:7;
    then
A6: R is connected by Th5;
    R is well_founded by A5,WELLFND1:def 2;
    then R\~ is well_founded by Th15;
    hence for N being non empty Subset of R holds
    card min-classes N = 1 by A1,A6,Th23;
  end;
  assume
A7: for N being non empty Subset of R holds card min-classes N = 1;
  then
A8: R is connected by A1,Th23;
A9: R\~ is well_founded by A1,A7,Th23;
A10: IR is_strongly_connected_in CR by A8,Th5;
A11: R is well_founded by A9,Th16;
A12: IR is_reflexive_in CR by ORDERS_2:def 2;
A13: IR is_transitive_in CR by ORDERS_2:def 3;
A14: IR is_antisymmetric_in CR by ORDERS_2:def 4;
A15: IR is_connected_in CR by A10,ORDERS_1:7;
  IR is_well_founded_in CR by A11,WELLFND1:def 2;
  hence thesis by A12,A13,A14,A15,WELLORD1:def 5;
end;

definition :: Def 4.39
  let R be RelStr, N be Subset of R, B be set;
  pred B is_Dickson-basis_of N,R means
  :Def9:
  B c= N & for a being Element of R st a in N
  ex b being Element of R st b in B & b <= a;
end;

theorem Th25:
  for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R, R
proof
  let R be RelStr;
  set N = {} the carrier of R;
  thus {} c= N;
  thus thesis;
end;

theorem Th26:
  for R being non empty RelStr, N being non empty Subset of R, B being set
  st B is_Dickson-basis_of N,R holds B is non empty
proof
  let R be non empty RelStr, N be non empty Subset of R, B be set;
  assume
A1: B is_Dickson-basis_of N,R;
  set a = the Element of N;
  ex b being Element of R st ( b in B)&( b <= a) by A1,Def9;
  hence thesis;
end;

definition :: Def 4.39
  let R be RelStr;
  attr R is Dickson means
  :Def10:
  for N being Subset of R
  ex B being set st B is_Dickson-basis_of N,R & B is finite;
end;

theorem Th27: :: Lemma 4:40
  for R being non empty RelStr
  st R\~ is well_founded & R is connected holds R is Dickson
proof
  let R be non empty RelStr such that
A1: R\~ is well_founded and
A2: R is connected;
  set IR9 = the InternalRel of R\~, CR9 = the carrier of R\~;
  set IR = the InternalRel of R, CR = the carrier of R;
  let N be Subset of CR;
  per cases;
  suppose
A3: N = {} CR;
    take B = {};
    thus B is_Dickson-basis_of N,R by A3,Th25;
    thus thesis;
  end;
  suppose
A4: N <> {} CR;
    IR9 is_well_founded_in CR9 by A1,WELLFND1:def 2;
    then consider b being set such that
A5: b in N and
A6: IR9-Seg(b) misses N by A4,WELLORD1:def 3;
A7: IR9-Seg(b) /\ N = {} by A6,XBOOLE_0:def 7;
    take B = {b};
    reconsider b as Element of N by A5;
    thus B is_Dickson-basis_of N,R
    proof
      {b} is Subset of N by A4,SUBSET_1:33;
      hence B c= N;
      let a be Element of R such that
A8:   a in N;
      reconsider b as Element of R by A5;
      take b;
      thus b in B by TARSKI:def 1;
      per cases by A2,WAYBEL_0:def 29;
      suppose b <= a;
        hence thesis;
      end;
      suppose
A9:     a <= b;
        then
A10:    [a,b] in IR by ORDERS_2:def 5;
        now per cases;
          suppose a = b;
            hence thesis by A9;
          end;
          suppose
A11:        not a = b;
            now per cases;
              suppose [a,b] in IR9;
                then a in IR9-Seg(b) by A11,WELLORD1:1;
                hence thesis by A7,A8,XBOOLE_0:def 4;
              end;
              suppose not [a,b] in IR9;
                then [a,b] in IR~ by A10,XBOOLE_0:def 5;
                then [b,a] in IR by RELAT_1:def 7;
                hence thesis by ORDERS_2:def 5;
              end;
            end;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
    end;
    thus thesis;
  end;
end;

theorem Th28: :: Exercise 4.41
  for R, S being RelStr st (the InternalRel of R) c= (the InternalRel of S) &
  R is Dickson & (the carrier of R) = (the carrier of S) holds S is Dickson
proof
  let r, s be RelStr such that
A1: the InternalRel of r c= the InternalRel of s and
A2: r is Dickson and
A3: the carrier of r = the carrier of s;
  let N be Subset of s;
  reconsider N9 = N as Subset of r by A3;
  consider B being set such that
A4: B is_Dickson-basis_of N9,r and
A5: B is finite by A2,Def10;
  take B;
  thus B c= N by A4,Def9;
  hereby
    let a be Element of s such that
A6: a in N;
    reconsider a9 = a as Element of r by A3;
    consider b being Element of r such that
A7: b in B and
A8: b <= a9 by A4,A6,Def9;
    reconsider b9 = b as Element of s by A3;
    take b9;
    [b,a9] in the InternalRel of r by A8,ORDERS_2:def 5;
    hence b9 in B & b9 <= a by A1,A7,ORDERS_2:def 5;
  end;
  thus thesis by A5;
end;

definition
  let f be Function, b be set such that
B1: dom f = NAT and
B2: b in rng f;
  func f mindex b -> Element of NAT means
  :Def11:
  f.it = b & for i being Element of NAT st f.i = b holds it <= i;
  existence
  proof
    set N = {i where i is Element of NAT : f.i = b};
    consider x being set such that
A1: x in NAT and
A2: f.x = b by B1,B2,FUNCT_1:def 3;
    reconsider x as Element of NAT by A1;
A3: x in N by A2;
    now
      let x be set;
      assume x in N;
      then ex i being Element of NAT st ( x = i)&( f.i = b);
      hence x in NAT;
    end;
    then reconsider N as non empty Subset of NAT by A3,TARSKI:def 3;
    take I = min N;
    I in N by XXREAL_2:def 7;
    then ex II being Element of NAT st ( II = I)&( f.II = b);
    hence f.I = b;
    let i be Element of NAT;
    assume f.i = b;
    then i in N;
    hence thesis by XXREAL_2:def 7;
  end;
  uniqueness
  proof
    let IT1, IT2 be Element of NAT such that
A4: f.IT1 = b and
A5: for i being Element of NAT st f.i = b holds IT1 <= i and
A6: f.IT2 = b and
A7: for i being Element of NAT st f.i = b holds IT2 <= i;
    assume
A8: IT1 <> IT2;
    per cases by A8,XXREAL_0:1;
    suppose IT1 < IT2;
      hence contradiction by A4,A7;
    end;
    suppose IT1 > IT2;
      hence contradiction by A5,A6;
    end;
  end;
end;

definition
  let R be non empty 1-sorted, f be sequence of R, b be set,
  m be Element of NAT;
  assume
A1: ex j being Element of NAT st m < j & f.j = b;
  func f mindex (b,m) -> Element of NAT means
  : Def12:
  f.it = b & m < it & for i being Element of NAT st m < i & f.i = b
  holds it <= i;
  existence
  proof
    set N = {i where i is Element of NAT : m < i & f.i = b};
    consider j being Element of NAT such that
A2: m < j and
A3: f.j = b by A1;
A4: j in N by A2,A3;
    now
      let x be set;
      assume x in N;
      then ex i being Element of NAT st ( x = i)&( m < i)&( f.i = b);
      hence x in NAT;
    end;
    then reconsider N as non empty Subset of NAT by A4,TARSKI:def 3;
    take I = min N;
    I in N by XXREAL_2:def 7;
    then ex II being Element of NAT st ( II = I)&( m < II)&( f.II = b);
    hence f.I = b & m < I;
    let i be Element of NAT such that
A5: m < i and
A6: f.i = b;
    i in N by A5,A6;
    hence thesis by XXREAL_2:def 7;
  end;
  uniqueness
  proof
    let IT1, IT2 be Element of NAT such that
A7: f.IT1 = b and
A8: m < IT1 and
A9: for i being Element of NAT st m < i & f.i = b holds IT1 <= i and
A10: f.IT2 = b and
A11: m < IT2 and
A12: for i being Element of NAT st m < i & f.i = b holds IT2 <= i;
    assume
A13: IT1 <> IT2;
    per cases by A13,XXREAL_0:1;
    suppose IT1 < IT2;
      hence contradiction by A7,A8,A12;
    end;
    suppose IT1 > IT2;
      hence contradiction by A9,A10,A11;
    end;
  end;
end;

theorem Th29: :: Prop 4.42 (i) -> (ii)
  for R being non empty RelStr st R is Dickson
  for f being sequence of R ex i,j being Element of NAT st i < j & f.i <= f.j
proof
  let R be non empty RelStr such that
A1: R is Dickson;
  let f be sequence of R;
  set N = rng f;
A2: dom f = NAT by FUNCT_2:def 1;
  consider B being set such that
A3: B is_Dickson-basis_of N,R and
A4: B is finite by A1,Def10;
  reconsider B as finite non empty set by A3,A4,Th26;
  defpred P[set] means not contradiction;
  deffunc F(set) = f mindex $1;
  set BI = { F(b) where b is Element of B : P[b] };
A5: BI is finite from PRE_CIRC:sch 1;
  set b = the Element of B;
A6: f mindex b in BI;
  now
    let x be set;
    assume x in BI;
    then ex b being Element of B st ( x = f mindex b);
    hence x in NAT;
  end;
  then reconsider BI as finite non empty Subset of NAT by A5,A6,TARSKI:def 3;
  reconsider mB = max BI as Element of NAT by ORDINAL1:def 12;
  set j = mB+1;
  reconsider fj = f.j as Element of R;
  fj in N by A2,FUNCT_1:3;
  then consider b being Element of R such that
A7: b in B and
A8: b <= fj by A3,Def9;
A9: B c= N by A3,Def9;
  take i = f mindex b;
  take j;
  i in BI by A7;
  then i <= max(BI) by XXREAL_2:def 8;
  hence i < j by NAT_1:13;
  dom f = NAT by NORMSP_1:12;
  hence thesis by A7,A8,A9,Def11;
end;

theorem Th30:
  for R being RelStr, N being Subset of R, x being Element of R\~
  st R is quasi_ordered & x in N &
  ((the InternalRel of R)-Seg(x)) /\ N c= Class(EqRel R,x)
  holds x is_minimal_wrt N, the InternalRel of R\~
proof
  let R be RelStr, N be Subset of R, x be Element of R\~ such that
A1: R is quasi_ordered and
A2: x in N and
A3: ((the InternalRel of R)-Seg(x)) /\ N c= Class(EqRel R,x);
  set IR = the InternalRel of R;
  set IR9= the InternalRel of R\~;
  now
    assume ex y being set st y in N & y<>x & [y,x] in IR9;
    then consider y being set such that
A4: y in N and
A5: y <> x and
A6: [y,x] in IR9;
A7: not [y,x] in IR~ by A6,XBOOLE_0:def 5;
    y in IR-Seg(x) by A5,A6,WELLORD1:1;
    then y in IR-Seg(x) /\ N by A4,XBOOLE_0:def 4;
    then [y,x] in EqRel R by A3,EQREL_1:19;
    then [y,x] in IR /\ IR~ by A1,Def4;
    hence contradiction by A7,XBOOLE_0:def 4;
  end;
  hence thesis by A2,WAYBEL_4:def 25;
end;

theorem Th31: :: Prop 4.42 (ii) -> (iii)
  for R being non empty RelStr st R is quasi_ordered &
  (for f being sequence of R
  ex i,j being Element of NAT st i < j & f.i <= f.j)
  holds for N being non empty Subset of R
  holds min-classes N is finite & min-classes N is non empty
proof
  let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: for f being sequence of R
  ex i,j being Element of NAT st i < j & f.i <= f.j;
  set IR = the InternalRel of R;
  set IR9= the InternalRel of R\~;
A3: R is transitive by A1,Def3;
  let N be non empty Subset of R such that
A4: not (min-classes N is finite & min-classes N is non empty);
  per cases by A4;
  suppose
A5: min-classes N is infinite;
    then reconsider MCN = min-classes N as infinite set;
    consider f being Function of NAT, min-classes N such that
A6: f is one-to-one by A5,Th3;
    deffunc F(set) = choose(f.$1);
A7: now
      let x be set;
      assume x in NAT;
      then reconsider x9 = x as Element of NAT;
      f.x9 is Element of min-classes N;
      then
A8:   f.x in MCN;
      then f.x is non empty by Th22;
      then choose(f.x9) in f.x;
      hence F(x) in the carrier of R by A8;
    end;
    consider g being Function of NAT,the carrier of R such that
A9: for x being set st x in NAT holds g.x = F(x) from FUNCT_2:sch 2(A7);
    reconsider g as sequence of R;
    consider i,j being Element of NAT such that
A10: i < j and
A11: g.i <= g.j by A2;
    reconsider gi = g.i, gj= g.j as Element of R\~;
A12: [gi, gj] in IR by A11,ORDERS_2:def 5;
A13: f.i in MCN;
    then
A14: f.i is non empty by Th22;
A15: f.j in MCN;
    then
A16: f.j is non empty by Th22;
A17: g.j = choose f.j by A9;
A18: g.i = choose f.i by A9;
A19: gj is_minimal_wrt N, the InternalRel of R\~ by A1,A15,A16,A17,Th19;
    gi is_minimal_wrt N, the InternalRel of R\~ by A1,A13,A14,A18,Th19;
    then
A20: gi in N by WAYBEL_4:def 25;
A21: now per cases;
      suppose gi = gj;
        hence [gi, gj] in IR~ by A12,RELAT_1:def 7;
      end;
      suppose
A22:    gi <> gj;
        now
          assume not [gi, gj] in IR~;
          then [gi, gj] in IR \ IR~ by A12,XBOOLE_0:def 5;
          hence contradiction by A19,A20,A22,WAYBEL_4:def 25;
        end;
        hence [gi, gj] in IR~;
      end;
    end;
    [gi,gj] in IR by A11,ORDERS_2:def 5;
    then [gi,gj] in IR /\ IR~ by A21,XBOOLE_0:def 4;
    then [gi,gj] in EqRel R by A1,Def4;
    then gi in Class(EqRel R, gj) by EQREL_1:19;
    then
A23: Class(EqRel R, gj) = Class(EqRel R, gi) by EQREL_1:23;
    consider mj being Element of R\~ such that
    mj is_minimal_wrt N, IR9 and
A24: f.j = Class(EqRel R,mj) /\ N by A15,Def8;
    consider mi being Element of R\~ such that
    mi is_minimal_wrt N, IR9 and
A25: f.i = Class(EqRel R,mi) /\ N by A13,Def8;
    gj in Class(EqRel R, mj) by A16,A17,A24,XBOOLE_0:def 4;
    then
A26: Class(EqRel R, gj) = Class(EqRel R, mj) by EQREL_1:23;
    gi in Class(EqRel R, mi) by A14,A18,A25,XBOOLE_0:def 4;
    then f.i = f.j by A23,A24,A25,A26,EQREL_1:23;
    hence contradiction by A5,A6,A10,FUNCT_2:19;
  end;
  suppose
A27: min-classes N is empty;
    deffunc F(set,set) = choose (IR-Seg($2) /\ N\Class(EqRel R,$2));
    consider f being Function such that
A28: dom f = NAT and
A29: f.0 = choose N and
A30: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
    defpred P[Nat] means f.$1 in N;
A31: P[ 0 ] by A29;
A32: now
      let i be Element of NAT such that
A33:  P[i];
      reconsider fi = f.i as Element of R\~ by A33;
      set IC = IR-Seg(fi) /\ N\Class(EqRel R,fi);
A34:  f.(i+1) = choose (IR-Seg(f.i) /\ N\Class(EqRel R,f.i)) by A30;
      now
        assume IC is empty;
        then IR-Seg(fi) /\ N c= Class(EqRel R,fi) by XBOOLE_1:37;
        hence contradiction by A1,A27,A33,Th21,Th30;
      end;
      then f.(i+1) in IR-Seg(f.i) /\ N by A34,XBOOLE_0:def 5;
      hence P[i+1] by XBOOLE_0:def 4;
    end;
A35: for i being Element of NAT holds P[i] from NAT_1:sch 1(A31,A32);
    now
      let x being set;
      assume x in NAT;
      then f.x in N by A35;
      hence f.x in the carrier of R;
    end;
    then reconsider f as sequence of R by A28,FUNCT_2:3;
A36: now
      let i be Element of NAT;
      defpred P[Element of NAT] means i < $1 implies f.i >= f.$1;
A37:  P[ 0 ] by NAT_1:2;
A38:  for j being Element of NAT st P[j] holds P[j+1]
      proof
        let j be Element of NAT such that
A39:    i < j implies f.i >= f.j and
A40:    i < j+1;
A41:    i <= j by A40,NAT_1:13;
        reconsider fj = f.j, fj1 = f.(j+1) as Element of R\~;
        set IC = IR-Seg(fj) /\ N\Class(EqRel R,fj);
A42:    fj in N by A35;
A43:    fj1 = choose IC by A30;
        now
          assume IC is empty;
          then IR-Seg(fj) /\ N c= Class(EqRel R,fj) by XBOOLE_1:37;
          hence contradiction by A1,A27,A42,Th21,Th30;
        end;
        then fj1 in IR-Seg(fj) /\ N by A43,XBOOLE_0:def 5;
        then fj1 in IR-Seg(fj) by XBOOLE_0:def 4;
        then
A44:    [fj1, fj] in IR by WELLORD1:1;
        then
A45:    f.j >= f.(j+1) by ORDERS_2:def 5;
        per cases by A41,XXREAL_0:1;
        suppose i < j;
          hence thesis by A3,A39,A45,ORDERS_2:3;
        end;
        suppose i = j;
          hence thesis by A44,ORDERS_2:def 5;
        end;
      end;
      thus for j being Element of NAT holds P[j] from NAT_1:sch 1(A37,
      A38);
    end;
    now
      let i be Element of NAT;
      defpred P[Element of NAT] means i < $1 implies not f.i <= f.$1;
A46:  P[ 0 ] by NAT_1:2;
A47:  for j being Element of NAT st P[j] holds P[j+1]
      proof
        let j be Element of NAT such that
        i < j implies not f.i <= f.j and
A48:    i < j+1;
A49:    i <= j by A48,NAT_1:13;
        reconsider fj = f.j, fj1 = f.(j+1) as Element of R\~;
A50:    fj in N by A35;
        per cases by A49,XXREAL_0:1;
        suppose
A51:      i < j;
          assume
A52:      f.i <= f.(j+1);
          j < j+1 by NAT_1:13;
          then
A53:      f.j >= f.(j+1) by A36;
          f.i >= f.j by A36,A51;
          then f.j <= f.(j+1) by A3,A52,ORDERS_2:3;
          then
A54:      fj1 in Class(EqRel R, fj) by A1,A53,Th8;
          set IC = IR-Seg(fj) /\ N\Class(EqRel R,fj);
A55:      fj1 = choose IC by A30;
          now
            assume IC is empty;
            then IR-Seg(fj) /\ N c= Class(EqRel R,fj) by XBOOLE_1:37;
            hence contradiction by A1,A27,A50,Th21,Th30;
          end;
          hence contradiction by A54,A55,XBOOLE_0:def 5;
        end;
        suppose
A56:      i = j;
          assume
A57:      f.i <= f.(j+1);
          j < j+1 by NAT_1:13;
          then f.(j+1) <= f.j by A36;
          then
A58:      fj1 in Class(EqRel R, fj) by A1,A56,A57,Th8;
          set IC = IR-Seg(fj) /\ N\Class(EqRel R,fj);
A59:      fj1 = choose IC by A30;
          now
            assume IC is empty;
            then IR-Seg(fj) /\ N c= Class(EqRel R,fj) by XBOOLE_1:37;
            hence contradiction by A1,A27,A50,Th21,Th30;
          end;
          hence contradiction by A58,A59,XBOOLE_0:def 5;
        end;
      end;
      thus for j being Element of NAT holds P[j] from NAT_1:sch 1(A46,
      A47);
    end;
    hence contradiction by A2;
  end;
end;

theorem Th32: :: Prop (iii) -> (i)
  for R being non empty RelStr st R is quasi_ordered &
  (for N being non empty Subset of R
  holds min-classes N is finite & min-classes N is non empty)
  holds R is Dickson
proof
  let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: for N being non empty Subset of R
  holds min-classes N is finite & min-classes N is non empty;
A3: R is transitive by A1,Def3;
A4: R is reflexive by A1,Def3;
  set IR = the InternalRel of R, CR = the carrier of R;
  set IR9 = the InternalRel of R\~;
  let N be Subset of CR;
  per cases;
  suppose
A5: N = {} CR;
    take B = {};
    thus B is_Dickson-basis_of N,R by A5,Th25;
    thus thesis;
  end;
  suppose not N is empty;
    then reconsider N9=N as non empty Subset of CR;
    reconsider MCN9 = min-classes N9 as finite non empty Subset-Family of CR
    by A2;
    take B = {choose x where x is Element of MCN9 : not contradiction };
    thus B is_Dickson-basis_of N,R
    proof
      now
        let x be set;
        assume x in B;
        then consider y being Element of MCN9 such that
A6:     x = choose(y);
A7:     ex z being Element of R\~ st ( z is_minimal_wrt N, IR9)&( y
        = Class(EqRel R, z) /\ N) by Def8;
        y is non empty by Th22;
        hence x in N by A6,A7,XBOOLE_0:def 4;
      end;
      hence B c= N by TARSKI:def 3;
      let a be Element of R such that
A8:   a in N;
      defpred P[Element of R] means $1 <= a;
      set NN9 = {d where d is Element of N9 : P[d]};
A9:   NN9 is Subset of N9 from DOMAIN_1:sch 7;
      a <= a by A4,ORDERS_2:1;
      then a in NN9 by A8;
      then reconsider NN9 as non empty Subset of CR by A9,XBOOLE_1:1;
      set m = the Element of min-classes NN9;
A10:  min-classes NN9 is non empty by A2;
      then reconsider m9 = m as non empty set by Th22;
      set c = the Element of m9;
      consider y being Element of R\~ such that
      y is_minimal_wrt NN9, IR9 and
A11:  m9 = Class(EqRel R, y) /\ NN9 by A10,Def8;
A12:  c in Class(EqRel R, y) by A11,XBOOLE_0:def 4;
A13:  c in NN9 by A11,XBOOLE_0:def 4;
      reconsider c as Element of R\~ by A12;
      reconsider c9=c as Element of R;
A14:  ex d being Element of N9 st ( c = d)&( d <= a) by A13;
A15:  c is_minimal_wrt NN9, IR9 by A1,A10,Th19;
      now
        assume not c is_minimal_wrt N, IR9;
        then consider w being set such that
A16:    w in N and
A17:    w <> c and
A18:    [w,c] in IR9 by A14,WAYBEL_4:def 25;
        reconsider w9 = w as Element of R by A18,ZFMISC_1:87;
        w9 <= c9 by A18,ORDERS_2:def 5;
        then w9 <= a by A3,A14,ORDERS_2:3;
        then w9 in NN9 by A16;
        hence contradiction by A15,A17,A18,WAYBEL_4:def 25;
      end;
      then
A19:  Class(EqRel R, c) /\ N in min-classes N by Def8;
      then
A20:  Class(EqRel R, c) /\ N is non empty by Th22;
      set t = choose( Class(EqRel R, c) /\ N );
      t in N by A20,XBOOLE_0:def 4;
      then reconsider t as Element of R;
      take t;
      thus t in B by A19;
      t in Class(EqRel R, c) by A20,XBOOLE_0:def 4;
      then [t,c] in EqRel R by EQREL_1:19;
      then [t,c] in IR /\ IR~ by A1,Def4;
      then [t,c] in IR by XBOOLE_0:def 4;
      then t <= c9 by ORDERS_2:def 5;
      hence thesis by A3,A14,ORDERS_2:3;
    end;
    deffunc F(set) = choose $1;
    defpred P[set] means not contradiction;
    {F(x) where x is Element of MCN9 : P[x]} is finite from PRE_CIRC: sch 1;
    hence thesis;
  end;
end;

theorem Th33: :: Corollary 4.44
  for R being non empty RelStr st R is quasi_ordered & R is Dickson
  holds R\~ is well_founded
proof
  let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: R is Dickson;
  A3: for
 f being sequence of R ex i,j being Element of NAT st i < j & f.i <= f.j
  by A2,Th29;
  now
    let N be Subset of R;
    assume N <> {};
    then min-classes N is non empty by A1,A3,Th31;
    hence ex x being set st x in min-classes N by XBOOLE_0:def 1;
  end;
  hence thesis by Th20;
end;

theorem :: Corollary 4.43
  for R being non empty Poset, N being non empty Subset of R st R is Dickson
  holds ex B being set st B is_Dickson-basis_of N, R &
  for C being set st C is_Dickson-basis_of N, R holds B c= C
proof
  let R be non empty Poset, N be non empty Subset of R such that
A1: R is Dickson;
  set IR=the InternalRel of R, CR = the carrier of R;
  set IR9=the InternalRel of R\~;
  set B = {b where b is Element of R\~ : b is_minimal_wrt N, IR9};
A2: R is quasi_ordered by Def3;
  for f being sequence of R ex i,j being Element of NAT
  st i < j & f.i <= f.j by A1,Th29;
  then min-classes N is non empty by A2,Th31;
  then consider x being set such that
A3: x in min-classes N by XBOOLE_0:def 1;
  consider y being Element of R\~ such that
A4: y is_minimal_wrt N, IR9 and x = Class(EqRel R, y) /\ N by A3,Def8;
  y in B by A4;
  then reconsider B as non empty set;
  take B;
A5: now
    let x be set;
    assume x in B;
    then ex b being Element of R\~ st ( x = b)&( b is_minimal_wrt N, IR9);
    hence x in N by WAYBEL_4:def 25;
  end;
  then
A6: B c= N by TARSKI:def 3;
  thus B is_Dickson-basis_of N, R
  proof
    thus B c= N by A5,TARSKI:def 3;
    let a be Element of R such that
A7: a in N;
    reconsider a9=a as Element of R\~;
    now
      assume
A8:   not ex b being Element of R st b in B & b <= a;
      per cases;
      suppose IR9-Seg(a) /\ N = {};
        then IR9-Seg(a) misses N by XBOOLE_0:def 7;
        then a9 is_minimal_wrt N, IR9 by A7,Th6;
        then a in B;
        hence contradiction by A8;
      end;
      suppose
A9:     IR9-Seg(a) /\ N <> {};
        R\~ is well_founded by A1,A2,Th33;
        then IR9 is_well_founded_in CR by WELLFND1:def 2;
        then consider z being set such that
A10:    z in IR9-Seg(a) /\ N and
A11:    IR9-Seg(z) misses (IR9-Seg(a) /\ N) by A9,WELLORD1:def 3;
A12:    z in IR9-Seg(a) by A10,XBOOLE_0:def 4;
        then [z,a] in IR9 by WELLORD1:1;
        then z in dom IR9 by XTUPLE_0:def 12;
        then reconsider z as Element of R\~;
        reconsider z9 = z as Element of R;
        z is_minimal_wrt IR9-Seg(a9) /\ N, IR9 by A10,A11,Th6;
        then z is_minimal_wrt N, IR9 by Th7;
        then
A13:    z in B;
        [z,a] in IR \ IR~ by A12,WELLORD1:1;
        then z9 <= a by ORDERS_2:def 5;
        hence contradiction by A8,A13;
      end;
    end;
    hence ex b being Element of R st b in B & b <= a;
  end;
  let C be set such that
A14: C is_Dickson-basis_of N, R;
A15: C c= N by A14,Def9;
  now
    let b be set such that
A16: b in B;
    b in N by A5,A16;
    then reconsider b9=b as Element of R;
    consider c being Element of R such that
A17: c in C and
A18: c <= b9 by A6,A14,A16,Def9;
A19: ex b99 being Element of R\~ st ( b99 = b)&( b99
    is_minimal_wrt N, IR9) by A16;
A20: [c,b] in IR by A18,ORDERS_2:def 5;
A21: IR is_antisymmetric_in CR by ORDERS_2:def 4;
    [b,c] in IR by A15,A17,A19,A20,Th17;
    hence b in C by A17,A18,A20,A21,RELAT_2:def 4;
  end;
  hence thesis by TARSKI:def 3;
end;

definition
  let R be non empty RelStr, N be Subset of R such that
B1: R is Dickson;
  func Dickson-bases (N,R) -> non empty Subset-Family of R means
  :Def13:
  for B being set holds B in it iff B is_Dickson-basis_of N,R;
  existence
  proof
    set BB = {b where b is Subset of N: b is_Dickson-basis_of N,R};
    set CR = the carrier of R;
    consider bp being set such that
A1: bp is_Dickson-basis_of N,R and bp is finite by B1,Def10;
    bp c= N by A1,Def9;
    then
A2: bp in BB by A1;
    now
      let x be set;
      assume x in BB;
      then consider b being Subset of N such that
A3:   x = b and b is_Dickson-basis_of N,R;
      b c= CR by XBOOLE_1:1;
      hence x in bool CR by A3;
    end;
    then reconsider BB as non empty Subset-Family of CR by A2,TARSKI:def 3;
    take BB;
    let B be set;
    hereby
      assume B in BB;
      then ex b being Subset of N st ( b = B)&( b is_Dickson-basis_of N,R);
      hence B is_Dickson-basis_of N,R;
    end;
    assume
A4: B is_Dickson-basis_of N,R;
    then B c= N by Def9;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let IT1, IT2 be non empty Subset-Family of R such that
A5: for B being set holds B in IT1 iff B is_Dickson-basis_of N, R and
A6: for B being set holds B in IT2 iff B is_Dickson-basis_of N, R;
    now
      let x be set;
      hereby
        assume x in IT1;
        then x is_Dickson-basis_of N, R by A5;
        hence x in IT2 by A6;
      end;
      assume x in IT2;
      then x is_Dickson-basis_of N, R by A6;
      hence x in IT1 by A5;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th35: :: Proposition 4.45
  for R being non empty RelStr, s being sequence of R st R is Dickson
  ex t being sequence of R st t is subsequence of s & t is weakly-ascending
proof
  let R be non empty RelStr, s be sequence of R such that
A1: R is Dickson;
  set CR = the carrier of R;
  deffunc Bi(Element of rng s, Element of NAT)
  = {n where n is Element of NAT : $1 <= s.n & $2 < n};
  deffunc Bi2(Element of rng s) = {n where n is Element of NAT : $1 <= s.n};
  defpred P[set,Element of NAT,set] means
  ex N being Subset of CR, B being non empty Subset of CR
  st N = {s.w where w is Element of NAT : s.$2 <= s.w & $2 < w} &
  { w where w is Element of NAT : s.$2 <= s.w & $2 < w} is infinite &
  B = choose {BB where BB is Element of Dickson-bases(N,R): BB is finite} &
  $3 = s mindex ( choose {b where b is Element of B :
  ex b9 being Element of rng s st b9=b & Bi(b9,$2) is infinite}, $2);
  defpred Q[set,Element of NAT,set] means
  {w where w is Element of NAT : s.$2 <= s.w & $2 < w} is infinite
  implies P[$1,$2,$3];
A2: for n being Element of NAT for x being Element of NAT
  ex y being Element of NAT st Q[n,x,y]
  proof
    let n be Element of NAT, x be Element of NAT;
    set N = {s.w where w is Element of NAT : s.x <= s.w & x < w};
    now
      let y be set;
      assume y in N;
      then ex w being Element of NAT st ( y = s.w)&( s.x <= s.w)&( x < w);
      hence y in CR;
    end;
    then reconsider N as Subset of CR by TARSKI:def 3;
    set W = {w where w is Element of NAT : s.x <= s.w & x < w};
    per cases;
    suppose
A3:   N is empty;
      take 1;
      assume W is infinite;
      then consider ww being set such that
A4:   ww in W by XBOOLE_0:def 1;
      consider www being Element of NAT such that www = ww and
A5:   s.x <= s.www and
A6:   x < www by A4;
      s.www in N by A5,A6;
      hence thesis by A3;
    end;
    suppose
A7:   N is non empty;
      set BBX = {BB where BB is Element of Dickson-bases(N,R): BB is finite};
      set B = choose BBX;
      consider BD1 being set such that
A8:   BD1 is_Dickson-basis_of N,R and
A9:   BD1 is finite by A1,Def10;
      BD1 in Dickson-bases(N,R) by A1,A8,Def13;
      then BD1 in BBX by A9;
      then B in BBX;
      then ex BBB being Element of Dickson-bases(N,R) st ( B = BBB)&(
      BBB is finite);
      then
A10:  B is_Dickson-basis_of N,R by A1,Def13;
      then B c= N by Def9;
      then reconsider B as non empty Subset of CR by A7,A10,Th26,XBOOLE_1:1;
      set y = s mindex ( choose {b where b is Element of B :
      ex b9 being Element of rng s st b9=b & Bi(b9,x) is infinite}, x);
      take y;
      set W = {w where w is Element of NAT : s.x <= s.w & x < w};
      assume
A11:  W is infinite;
      take N;
      reconsider B as non empty Subset of CR;
      take B;
      thus N = {s.w where w is Element of NAT : s.x <= s.w & x < w};
      thus { w where w is Element of NAT : s.x <= s.w & x < w}
      is infinite by A11;
      thus B = choose {BB where BB is Element of Dickson-bases(N,R):
      BB is finite};
      thus thesis;
    end;
  end;
  consider B being set such that
A12: B is_Dickson-basis_of rng s, R and
A13: B is finite by A1,Def10;
  reconsider B as non empty set by A12,Th26;
  set BALL = {b where b is Element of B :
  ex b9 being Element of rng s st b9=b & Bi2(b9) is infinite};
  set b1 = choose BALL;
  consider f being Function of NAT,NAT such that
A14: f.0 = s mindex b1 and
A15: for n being Element of NAT holds Q[n, f.n, f.(n+1)]
  from RECDEF_1:sch 2(A2);
A16: dom f = NAT by FUNCT_2:def 1;
A17: rng f c= NAT;
  now
A18: B is finite by A13;
    assume
A19: for b being Element of rng s st b in B holds Bi2(b) is finite;
    set Ball = {Bi2(b) where b is Element of rng s: b in B};
A20: Ball is finite from FRAENKEL:sch 21(A18);
    now
      let X be set;
      assume X in Ball;
      then ex b being Element of rng s st ( X = Bi2(b))&( b in B);
      hence X is finite by A19;
    end;
    then
A21: union Ball is finite by A20,FINSET_1:7;
    now
      let x be set;
      assume x in NAT;
      then reconsider x9= x as Element of NAT;
      dom s = NAT by FUNCT_2:def 1;
      then x9 in dom s;
      then
A22:  s.x in rng s by FUNCT_1:3;
      then reconsider sx = s.x as Element of R;
      consider b being Element of R such that
A23:  b in B and
A24:  b <= sx by A12,A22,Def9;
      B c= rng s by A12,Def9;
      then reconsider b as Element of rng s by A23;
A25:  x9 in Bi2(b) by A24;
      Bi2(b) in Ball by A23;
      hence x in union Ball by A25,TARSKI:def 4;
    end;
    then NAT c= union Ball by TARSKI:def 3;
    hence contradiction by A21;
  end;
  then consider tb being Element of rng s such that
A26: tb in B and
A27: Bi2(tb) is infinite;
A28: tb in BALL by A26,A27;
  then b1 in BALL;
  then
A29: ex bt being Element of B st ( b1 = bt)&( ex b9 being
  Element of rng s st b9 = bt & Bi2(b9) is infinite);
  dom s = NAT by NORMSP_1:12;
  then
A30: s.(f.0) = b1 by A14,A29,Def11;
  b1 in BALL by A28;
  then
A31: ex eb being Element of B st ( b1 = eb)&( ex eb9 being
  Element of rng s st eb9=eb & Bi2(eb9) is infinite);
  deffunc F(set) = $1;
  defpred P[Element of NAT] means s.(f.0) <= s.$1;
  set W1 = {w where w is Element of NAT: s.(f.0) <= s.w};
  set W2 = {w where w is Element of NAT: s.(f.0) <= s.w & f.0 < w};
  set W3 = {F(w) where w is Element of NAT: 0 <= w & w <= f.0 & P[w]};
A32: W3 is finite from FINSEQ_1:sch 6;
  now
    let x be set;
    hereby
      assume x in W1;
      then consider w being Element of NAT such that
A33:  x = w and
A34:  s.(f.0) <= s.w;
A35:  0 <= w by NAT_1:2;
      w <= f.0 or w > f.0;
      then x in W2 or x in W3 by A33,A34,A35;
      hence x in W2 \/ W3 by XBOOLE_0:def 3;
    end;
    assume
A36: x in W2 \/ W3;
    per cases by A36,XBOOLE_0:def 3;
    suppose x in W2;
      then ex w being Element of NAT st ( x = w)&( s.(f.0) <= s.w)&( f .0 < w);
      hence x in W1;
    end;
    suppose x in W3;
      then ex w being Element of NAT st ( x = w)&( 0 <= w)&( w <= f.0)
      &( s.(f.0) <= s.w);
      hence x in W1;
    end;
  end;
  then
A37: W2 is infinite by A30,A31,A32,TARSKI:1;
  defpred R[Element of NAT] means P[$1, f.$1, f.($1+1)];
A38: R[ 0 ] by A15,A37;
A39: now
    let k be Element of NAT;
    assume R[k];
    then consider
    N being Subset of CR, B being non empty Subset of CR such that
A40: N = {s.w where w is Element of NAT : s.(f.k) <= s.w & f.k < w} and
A41: {w where w is Element of NAT : s.(f.k) <= s.w & f.k < w} is infinite and
A42: B = choose {BB where BB is Element of Dickson-bases(N, R) :
    BB is finite} and
A43: f.(k+1)=s mindex (choose {b where b is Element of B :
    ex b9 being Element of rng s
    st b9=b & Bi(b9,f.k) is infinite},f.k);
    set BALL={b where b is Element of B: ex b9 being Element of rng s
    st b9=b & Bi(b9,f.k) is infinite};
    set BBX ={BB where BB is Element of Dickson-bases(N, R): BB is finite};
    set iN = {w where w is Element of NAT : s.(f.k) <= s.w & f.k < w};
    consider BD being set such that
A44: BD is_Dickson-basis_of N,R and
A45: BD is finite by A1,Def10;
    BD in Dickson-bases(N,R) by A1,A44,Def13;
    then BD in BBX by A45;
    then B in BBX by A42;
    then
A46: ex BB being Element of Dickson-bases(N,R) st ( B = BB)&( BB is finite);
    then
A47: B is_Dickson-basis_of N,R by A1,Def13;
    now
      deffunc F(Element of rng s) = Bi($1, f.k);
A48:  B is finite by A46;
      assume
A49:  for b being Element of rng s st b in B holds Bi(b, f.k) is finite;
      set Ball = {F(b) where b is Element of rng s : b in B };
A50:  Ball is finite from FRAENKEL:sch 21(A48);
      now
        let X be set;
        assume X in Ball;
        then ex b being Element of rng s st ( X = Bi(b, f.k))&( b in B);
        hence X is finite by A49;
      end;
      then
A51:  union Ball is finite by A50,FINSET_1:7;
      iN c= union Ball
      proof
        let x be set;
        assume x in iN;
        then consider w being Element of NAT such that
A52:    x = w and
A53:    s.(f.k) <= s.w and
A54:    f.k < w;
A55:    s.w in N by A40,A53,A54;
        reconsider sw = s.w as Element of R;
        consider b being Element of R such that
A56:    b in B and
A57:    b <= sw by A47,A55,Def9;
A58:    B c= N by A47,Def9;
        N c= rng s
        proof
          let x be set;
          assume x in N;
          then
A59:      ex u being Element of NAT st ( x = s.u)&( s.(f.k) <= s.u)&(
          f.k < u) by A40;
          dom s = NAT by FUNCT_2:def 1;
          hence thesis by A59,FUNCT_1:3;
        end;
        then B c= rng s by A58,XBOOLE_1:1;
        then reconsider b as Element of rng s by A56;
A60:    w in Bi(b, f.k) by A54,A57;
        Bi(b, f.k) in Ball by A56;
        hence thesis by A52,A60,TARSKI:def 4;
      end;
      hence contradiction by A41,A51;
    end;
    then consider b being Element of rng s such that
A61: b in B and
A62: Bi(b, f.k) is infinite;
    b in BALL by A61,A62;
    then choose BALL in BALL;
    then consider b being Element of B such that
A63: b = choose BALL and
A64: ex b9 being Element of rng s st b9=b & Bi(b9,f.k) is infinite;
A65: b in B;
    B c= N by A47,Def9;
    then b in N by A65;
    then
A66: ex w being Element of NAT st ( b = s.w)&( s.(f.k) <= s.w)&(
    f.k < w) by A40;
    then
A67: s.(f.(k+1)) = choose BALL by A43,A63,Def12;
A68: f.k < f.(k+1) by A43,A63,A66,Def12;
    deffunc F(set) = $1;
    defpred P[Element of NAT] means s.(f.(k+1)) <= s.$1;
    set W1 = {w1 where w1 is Element of NAT : s.(f.(k+1)) <= s.w1 & f.k < w1};
    set W2 = {w1 where w1 is Element of NAT :
    s.(f.(k+1)) <= s.w1 & f.(k+1) < w1};
    set W3 = {F(w1) where w1 is Element of NAT :
    f.k < w1 & w1 <= f.(k+1) & P[w1]};
A69: W3 is finite from FinSegRng2;
    now
      let x be set;
      hereby
        assume x in W1;
        then consider w being Element of NAT such that
A70:    x = w and
A71:    s.(f.(k+1)) <= s.w and
A72:    f.k < w;
        w <= f.(k+1) or w > f.(k+1);
        then x in W2 or x in W3 by A70,A71,A72;
        hence x in W2 \/ W3 by XBOOLE_0:def 3;
      end;
      assume
A73:  x in W2 \/ W3;
      per cases by A73,XBOOLE_0:def 3;
      suppose x in W2;
        then consider w being Element of NAT such that
A74:    x = w and
A75:    s.(f.(k+1)) <= s.w and
A76:    f.(k+1) < w;
        f.k < w by A68,A76,XXREAL_0:2;
        hence x in W1 by A74,A75;
      end;
      suppose x in W3;
        then ex w being Element of NAT st ( x = w)&( f.k < w)&( w <= f.(
        k+1))&( s.(f.(k+1)) <= s.w);
        hence x in W1;
      end;
    end;
    then W2 is infinite by A63,A64,A67,A69,TARSKI:1;
    hence R[k+1] by A15;
  end;
A77: for n being Element of NAT holds R[n] from NAT_1:sch 1(A38,A39);
  set t = s * f;
  take t;
  reconsider f as Function of NAT, REAL by FUNCT_2:7;
  now
    now
      let n be Element of NAT;
      f.n in rng f by A16,FUNCT_1:def 3;
      then reconsider fn = f.n as Element of NAT by A17;
      consider N being Subset of CR, B being non empty Subset of CR such that
A78:  N = {s.w where w is Element of NAT : s.(fn) <= s.w & fn < w} and
A79:  {w where w is Element of NAT : s.(fn) <= s.w & fn < w} is infinite and
A80:  B = choose {BB where BB is Element of Dickson-bases(N, R):
      BB is finite} and
A81:  f.(n+1) = s mindex (choose {b where b is Element of B :
      ex b9 being Element of rng s st b9=b & Bi(b9,fn) is infinite}, fn)
      by A77;
      set BBX = {BB where BB is Element of Dickson-bases(N, R): BB is finite};
      set BJ = {b where b is Element of B : ex b9 being Element of rng s
      st b9=b & Bi(b9,fn) is infinite};
      set BC = choose BJ;
      consider BD being set such that
A82:  BD is_Dickson-basis_of N,R and
A83:  BD is finite by A1,Def10;
      BD in Dickson-bases(N,R) by A1,A82,Def13;
      then BD in BBX by A83;
      then B in BBX by A80;
      then
A84:  ex BB being Element of Dickson-bases(N,R) st ( B = BB)&( BB is finite);
      then
A85:  B is_Dickson-basis_of N,R by A1,Def13;
      then
A86:  B c= N by Def9;
      now
A87:    B is finite by A84;
        assume
A88:    for b being Element of rng s st b in B holds Bi(b, fn) is finite;
        deffunc F(Element of rng s) = Bi($1, fn);
        set Ball = {F(b) where b is Element of rng s : b in B};
        set iN = {w where w is Element of NAT : s.(fn) <= s.w & fn < w};
A89:    Ball is finite from FRAENKEL:sch 21(A87);
        now
          let X be set;
          assume X in Ball;
          then ex b being Element of rng s st ( X = Bi(b, fn))&( b in B);
          hence X is finite by A88;
        end;
        then
A90:    union Ball is finite by A89,FINSET_1:7;
        iN c= union Ball
        proof
          let x be set;
          assume x in iN;
          then consider w being Element of NAT such that
A91:      x = w and
A92:      s.(fn) <= s.w and
A93:      f.n < w;
A94:      s.w in N by A78,A92,A93;
          reconsider sw = s.w as Element of R;
          consider b being Element of R such that
A95:      b in B and
A96:      b <= sw by A85,A94,Def9;
A97:      B c= N by A85,Def9;
          N c= rng s
          proof
            let x be set;
            assume x in N;
            then
A98:        ex u being Element of NAT st ( x = s.u)&( s.(fn) <= s.u)&(
            fn < u) by A78;
            dom s = NAT by FUNCT_2:def 1;
            hence thesis by A98,FUNCT_1:3;
          end;
          then B c= rng s by A97,XBOOLE_1:1;
          then reconsider b as Element of rng s by A95;
A99:      w in Bi(b, fn) by A93,A96;
          Bi(b, fn) in Ball by A95;
          hence thesis by A91,A99,TARSKI:def 4;
        end;
        hence contradiction by A79,A90;
      end;
      then consider b being Element of rng s such that
A100: b in B and
A101: Bi(b, fn) is infinite;
      b in BJ by A100,A101;
      then BC in BJ;
      then ex b being Element of B st ( BC = b)&( ex b9 being Element
      of rng s st b9=b & Bi(b9,fn) is infinite);
      then BC in N by A86,TARSKI:def 3;
      then ex j being Element of NAT st ( BC = s.j)&( s.(fn) <= s.j)&(
      fn < j) by A78;
      hence f.n < f.(n+1) by A81,Def12;
    end;
    hence f is increasing by SEQM_3:def 6;
    let n be Element of NAT;
    f.n in rng f by A16,FUNCT_1:def 3;
    hence f.n is Element of NAT by A17;
  end;
  then reconsider f as increasing sequence of NAT;
  t = s * f;
  hence t is subsequence of s;
  let n be Element of NAT;
A102: t.n = s.(f.n) by A16,FUNCT_1:13;
A103: t.(n+1) = s.(f.(n+1)) by A16,FUNCT_1:13;
  consider N being Subset of CR, B being non empty Subset of CR such that
A104: N = {s.w where w is Element of NAT : s.(f.n) <= s.w & f.n < w} and
A105: {w where w is Element of NAT: s.(f.n) <= s.w & f.n < w} is infinite and
A106: B = choose{BB where BB is Element of Dickson-bases(N, R):BB is finite}
  and
A107: f.(n+1) = s mindex ( choose {b where b is Element of B :
  ex b9 being Element of rng s st b9=b & Bi(b9,f.n) is infinite}, f.n) by A77;
  set BX = {b where b is Element of B : ex b9 being Element of rng s
  st b9=b & Bi(b9,f.n) is infinite};
  set sfn1 = choose BX;
  set BBX = {BB where BB is Element of Dickson-bases(N, R):BB is finite};
  consider BD being set such that
A108: BD is_Dickson-basis_of N,R and
A109: BD is finite by A1,Def10;
  BD in Dickson-bases(N,R) by A1,A108,Def13;
  then BD in BBX by A109;
  then B in BBX by A106;
  then
A110: ex BB being Element of Dickson-bases(N, R) st ( BB = B)&( BB is finite);
  then
A111: B is_Dickson-basis_of N,R by A1,Def13;
  now
A112: B is finite by A110;
    assume
A113: for b being Element of rng s st b in B holds Bi(b, f.n) is finite;
    deffunc F(Element of rng s) = Bi($1, f.n);
    set Ball = {F(b) where b is Element of rng s : b in B };
    set iN = {w where w is Element of NAT : s.(f.n) <= s.w & f.n < w};
A114: Ball is finite from FRAENKEL:sch 21(A112);
    now
      let X be set;
      assume X in Ball;
      then ex b being Element of rng s st ( X = Bi(b, f.n))&( b in B);
      hence X is finite by A113;
    end;
    then
A115: union Ball is finite by A114,FINSET_1:7;
    iN c= union Ball
    proof
      let x be set;
      assume x in iN;
      then consider w being Element of NAT such that
A116: x = w and
A117: s.(f.n) <= s.w and
A118: f.n < w;
A119: s.w in N by A104,A117,A118;
      reconsider sw = s.w as Element of R;
      consider b being Element of R such that
A120: b in B and
A121: b <= sw by A111,A119,Def9;
A122: B c= N by A111,Def9;
      N c= rng s
      proof
        let x be set;
        assume x in N;
        then
A123:   ex u being Element of NAT st ( x = s.u)&( s.(f.n) <= s.u)&(
        f.n < u) by A104;
        dom s = NAT by FUNCT_2:def 1;
        hence thesis by A123,FUNCT_1:3;
      end;
      then B c= rng s by A122,XBOOLE_1:1;
      then reconsider b as Element of rng s by A120;
A124: w in Bi(b, f.n) by A118,A121;
      Bi(b, f.n) in Ball by A120;
      hence thesis by A116,A124,TARSKI:def 4;
    end;
    hence contradiction by A105,A115;
  end;
  then consider b being Element of rng s such that
A125: b in B and
A126: Bi(b, f.n) is infinite;
  b in BX by A125,A126;
  then sfn1 in BX;
  then ex b being Element of B st ( b = sfn1)&( ex b9 being
  Element of rng s st b9 = b & Bi(b9,f.n) is infinite);
  then
A127: sfn1 in B;
  B c= N by A111,Def9;
  then sfn1 in N by A127;
  then ex w being Element of NAT st ( sfn1 = s.w)&( s.(f.n) <= s.w
  )&( f.n < w) by A104;
  then t.n <= t.(n+1) by A102,A103,A107,Def12;
  hence [t.n, t.(n+1)] in the InternalRel of R by ORDERS_2:def 5;
end;

theorem Th36:
  for R being RelStr st R is empty holds R is Dickson
proof
  let R be RelStr such that
A1: R is empty;
  now
    let N be Subset of R;
    take B = {};
    N = {} the carrier of R by A1;
    hence B is_Dickson-basis_of N,R by Th25;
    thus B is finite;
  end;
  hence thesis by Def10;
end;

theorem Th37:  :: Theorem 4.46
  for M, N be RelStr
  st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered
  holds [:M,N:] is quasi_ordered & [:M,N:] is Dickson
proof
  let M,N be RelStr such that
A1: M is Dickson and
A2: N is Dickson and
A3: M is quasi_ordered and
A4: N is quasi_ordered;
  reconsider M9 = M as reflexive transitive RelStr by A3,Def3;
  reconsider N9 = N as reflexive transitive RelStr by A4,Def3;
  [:M9,N9:] is reflexive;
  hence
A5: [:M,N:] is quasi_ordered by Def3;
  per cases;
  suppose M is non empty & N is non empty;
    then reconsider Me=M,Ne=N as non empty RelStr;
    set CPMN = [:Me,Ne:];
    for f being sequence of [:Me,Ne:]
    ex i,j being Element of NAT st i < j & f.i <= f.j
    proof
      let f be sequence of [:Me,Ne:];
      deffunc F(Element of NAT) = (f.$1)`1;
      consider a being Function of NAT, the carrier of Me such that
A6:   for x being Element of NAT holds a.x = F(x) from FUNCT_2:sch 4;
      reconsider a as sequence of Me;
      consider sa being sequence of Me such that
A7:   sa is subsequence of a and
A8:   sa is weakly-ascending by A1,Th35;
      consider NS being increasing sequence of NAT such that
A9:   sa = a * NS by A7,VALUED_0:def 17;
      deffunc G(Element of NAT) = (f.(NS.$1))`2;
      consider b being Function of NAT, the carrier of Ne such that
A10:  for x being Element of NAT holds b.x = G(x) from FUNCT_2:sch 4;
      reconsider b as sequence of Ne;
      consider i,j being Element of NAT such that
A11:  i < j and
A12:  b.i <= b.j by A2,Th29;
      take NS.i, NS.j;
      dom NS = NAT by FUNCT_2:def 1;
      hence NS.i < NS.j by A11,VALUED_0:def 13;
      reconsider x = f.(NS.i), y = f.(NS.j) as Element of [:Me,Ne:];
A13:  dom sa = NAT by FUNCT_2:def 1;
      then
A14:  sa.i = a.(NS.i) by A9,FUNCT_1:12
        .= (f.(NS.i))`1 by A6;
A15:  sa.j = a.(NS.j) by A9,A13,FUNCT_1:12
        .= (f.(NS.j))`1 by A6;
      M is transitive by A3,Def3;
      then
A16:  x`1 <= y`1 by A8,A11,A14,A15,Th4;
A17:  b.i = x`2 by A10;
      b.j =y`2 by A10;
      hence thesis by A12,A16,A17,YELLOW_3:12;
    end;
    then for N being non empty Subset of CPMN
    holds min-classes N is finite & min-classes N is non empty by A5,Th31;
    hence thesis by A5,Th32;
  end;
  suppose
A18: not (M is non empty & N is non empty);
    now per cases by A18;
      suppose M is empty;
        then reconsider M2 = the carrier of M as empty set;
        [: M2, the carrier of N:] is empty;
        hence [:the carrier of M, the carrier of N:] is empty;
      end;
      suppose N is empty;
        then reconsider N2 = the carrier of N as empty set;
        [:the carrier of M, N2 :] is empty;
        hence [:the carrier of M, the carrier of N:] is empty;
      end;
    end;
    then [:M,N:] is empty by YELLOW_3:def 2;
    hence thesis by Th36;
  end;
end;

theorem Th38:
for R, S being RelStr st R,S are_isomorphic & R is Dickson & R is quasi_ordered
  holds S is quasi_ordered & S is Dickson
proof
  let R, S be RelStr such that
A1: R,S are_isomorphic and
A2: R is Dickson and
A3: R is quasi_ordered;
  set CRS = the carrier of S, IRS = the InternalRel of S;
  per cases;
  suppose R is not empty & S is not empty;
    then reconsider Re = R, Se = S as non empty RelStr;
    consider f being Function of Re,Se such that
A4: f is isomorphic by A1,WAYBEL_1:def 8;
A5: f is one-to-one by A4,WAYBEL_0:66;
A6: rng f = the carrier of Se by A4,WAYBEL_0:66;
A7: Re is reflexive by A3,Def3;
A8: Re is transitive by A3,Def3;
A9: Se is reflexive by A1,A7,WAYBEL20:15;
    Se is transitive by A1,A8,WAYBEL20:16;
    hence
A10: S is quasi_ordered by A9,Def3;
    now
      let t be sequence of Se;
      reconsider fi = f" as Function of the carrier of Se,
      the carrier of Re by A5,A6,FUNCT_2:25;
      deffunc F(Element of NAT) = fi.(t.$1);
      consider sr being Function of NAT, the carrier of Re such that
A11:  for x being Element of NAT holds sr.x = F(x) from FUNCT_2:sch 4;
      reconsider sr as sequence of Re;
      consider i,j being Element of NAT such that
A12:  i < j and
A13:  sr.i <= sr.j by A2,Th29;
      take i,j;
      thus i < j by A12;
A14:  f.(sr.i) = f.(f".(t.i)) by A11
        .= t.i by A5,A6,FUNCT_1:35;
      f.(sr.j) = f.(f".(t.j)) by A11
        .= t.j by A5,A6,FUNCT_1:35;
      hence t.i <= t.j by A4,A13,A14,WAYBEL_0:66;
    end;
    then for N being non empty Subset of Se
    holds min-classes N is finite & min-classes N is non empty by A10,Th31;
    hence thesis by A10,Th32;
  end;
  suppose
A15: not(R is not empty & S is not empty);
A16: now per cases by A15;
      suppose
A17:    R is empty;
        ex f being Function of R,S st ( f is isomorphic) by A1,WAYBEL_1:def 8;
        hence S is empty by A17,WAYBEL_0:def 38;
      end;
      suppose S is empty;
        hence S is empty;
      end;
    end;
    then for x being set st x in CRS holds [x,x] in IRS;
    then
A18: IRS is_reflexive_in CRS by RELAT_2:def 1;
    for x,y,z be set
    st x in CRS & y in CRS & z in CRS & [x,y] in IRS & [y,z] in IRS
    holds [x,z] in IRS by A16;
    then
A19: IRS is_transitive_in CRS by RELAT_2:def 8;
A20: S is reflexive by A18,ORDERS_2:def 2;
    S is transitive by A19,ORDERS_2:def 3;
    hence S is quasi_ordered by A20,Def3;
    thus thesis by A16,Th36;
  end;
end;

theorem Th39:
  for p being RelStr-yielding ManySortedSet of 1, z being Element of 1
  holds p.z, product p are_isomorphic
proof
  let p be RelStr-yielding ManySortedSet of 1, z be Element of 1;
  deffunc F(set) = 0 .--> $1;
  consider f being Function such that
A1: dom f = the carrier of p.z and
A2: for x being set st x in the carrier of p.z holds f.x = F(x) from
  FUNCT_1:sch 3;
A3: z = 0 by CARD_1:49,TARSKI:def 1;
A4: 0 in 1 by CARD_1:49,TARSKI:def 1;
  now
    let x be set;
    assume
A5: x in the carrier of p.z;
    then
A6: f.x = 0.-->x by A2;
    set g = 0 .--> x;
A7: dom g = {0} by FUNCOP_1:13
      .= dom Carrier p by CARD_1:49,PARTFUN1:def 2;
    now
      let y be set;
      assume y in dom Carrier p;
      then
A8:   y in 1;
      then
A9:   y = 0 by CARD_1:49,TARSKI:def 1;
      ex R being 1-sorted st ( R = p.y)&( (Carrier p).y = the
      carrier of R) by A8,PRALG_1:def 13;
      hence g.y in (Carrier p).y by A3,A5,A9,FUNCOP_1:72;
    end;
    then f.x in product Carrier p by A6,A7,CARD_3:def 5;
    hence f.x in the carrier of product p by YELLOW_1:def 4;
  end;
  then reconsider f as Function of p.z, product p by A1,FUNCT_2:3;
  now
    per cases;
    suppose
A10:  p.z is empty;
      now
        assume the carrier of product p is not empty;
        then
A11:    product Carrier p is non empty by YELLOW_1:def 4;
        set x = the Element of product Carrier p;
A12:    ex g being Function st ( x = g)&( dom g = dom (Carrier p))&
( for y being set st y in dom Carrier p holds g.y in (Carrier p).y) by A11,
CARD_3:def 5;
A13:    0 in dom Carrier p by A4,PARTFUN1:def 2;
        consider R being 1-sorted such that
A14:    R = p.0 and
A15:    (Carrier p).0 = the carrier of R by A4,PRALG_1:def 13;
        R is empty by A10,A14,CARD_1:49,TARSKI:def 1;
        hence contradiction by A12,A13,A15;
      end;
      then product p is empty;
      hence f is isomorphic by A10,WAYBEL_0:def 38;
    end;
    suppose
A16:  p.z is non empty;
      then reconsider pz = p.z as non empty RelStr;
      now
        let i be set;
        assume i in rng p;
        then consider x being set such that
A17:    x in dom p and
A18:    i = p.x by FUNCT_1:def 3;
        x in 1 by A17;
        then i = p.0 by A18,CARD_1:49,TARSKI:def 1;
        hence i is non empty 1-sorted by A16,CARD_1:49,TARSKI:def 1;
      end;
      then reconsider np = p as yielding_non-empty_carriers
      RelStr-yielding ManySortedSet of 1 by YELLOW_6:def 2;
      product np is non empty;
      then reconsider pp = product p as non empty RelStr;
      now
        let x1, x2 be set such that
A19:    x1 in dom f and
A20:    x2 in dom f and
A21:    f.x1 = f.x2;
A22:    f.x1 = 0 .--> x1 by A2,A19
          .= [:{0}, {x1}:];
A23:    f.x2 = 0 .--> x2 by A2,A20
          .= [:{0}, {x2}:];
A24:    0 in {0} by TARSKI:def 1;
        x1 in {x1} by TARSKI:def 1;
        then [0, x1] in f.x2 by A21,A22,A24,ZFMISC_1:def 2;
        then ex xa,ya being set st ( xa in {0})&( ya in {x2})&( [0,x1] =
        [xa,ya]) by A23,ZFMISC_1:def 2;
        then x1 in {x2} by XTUPLE_0:1;
        hence x1 = x2 by TARSKI:def 1;
      end;
      then
A25:  f is one-to-one by FUNCT_1:def 4;
      now
        let y be set;
        thus y in rng f implies y in the carrier of product p;
        assume y in the carrier of product p;
        then y in product Carrier p by YELLOW_1:def 4;
        then consider g being Function such that
A26:    y = g and
A27:    dom g = dom (Carrier p) and
A28:    for x being set st x in dom Carrier p holds g.x in (Carrier p).x
        by CARD_3:def 5;
A29:    dom g = {0} by A27,CARD_1:49,PARTFUN1:def 2;
A30:    0 in dom Carrier p by A4,PARTFUN1:def 2;
A31:    ex R being 1-sorted st ( R = p.0)&( (Carrier p).0 = the
        carrier of R) by A4,PRALG_1:def 13;
A32:    g = 0 .--> g.0 by A29,Th1;
A33:    f.(g.0) = 0 .--> g.0 by A2,A3,A28,A30,A31;
        g.0 in dom f by A1,A3,A28,A30,A31;
        hence y in rng f by A26,A32,A33,FUNCT_1:def 3;
      end;
      then
A34:  rng f = the carrier of product p by TARSKI:1;
      reconsider f9 = f as Function of pz, pp;
      now
        let x, y be Element of pz;
        product np is non empty;
        then
A35:    product Carrier p is non empty by YELLOW_1:def 4;
A36:    f9.x is Element of product Carrier p by YELLOW_1:def 4;
        hereby
          assume
A37:      x <= y;
          ex f1,g1 being Function st f1 = f9.x & g1 = f9.y &
          for i be set st i in 1 ex R being RelStr, xi,yi being Element of R
          st R = p.i & xi = f1.i & yi = g1.i & xi <= yi
          proof
            set f1 = 0 .--> x;
            set g1 = 0 .--> y;
            reconsider f1 as Function;
            reconsider g1 as Function;
            take f1, g1;
            thus f1 = f9.x by A2;
            thus g1 = f9.y by A2;
            let i be set such that
A38:        i in 1;
A39:        i = 0 by A38,CARD_1:49,TARSKI:def 1;
            0 in dom p by A4,PARTFUN1:def 2;
            then p.0 in rng p by FUNCT_1:def 3;
            then reconsider p0 = p.0 as RelStr by YELLOW_1:def 3;
            set R = p0;
            reconsider x9=x as Element of R by CARD_1:49,TARSKI:def 1;
            reconsider y9=y as Element of R by CARD_1:49,TARSKI:def 1;
            take R, x9, y9;
            thus R = p.i by A38,CARD_1:49,TARSKI:def 1;
            thus x9 = f1.i by A39,FUNCOP_1:72;
            thus y9 = g1.i by A39,FUNCOP_1:72;
            thus thesis by A37,CARD_1:49,TARSKI:def 1;
          end;
          hence f9.x <= f9.y by A35,A36,YELLOW_1:def 4;
        end;
        assume f9.x <= f9.y;
        then consider f1, g1 being Function such that
A40:    f1 = f9.x and
A41:    g1 = f9.y and
        A42:    for
 i being set st i in 1 ex R being RelStr, xi, yi being Element of R
        st R = p.i & xi = f1.i & yi = g1.i & xi <= yi
        by A35,A36,YELLOW_1:def 4;
        consider R being RelStr, xi, yi being Element of R such that
A43:    R = p.0 and
A44:    xi = f1.0 and
A45:    yi = g1.0 and
A46:    xi <= yi by A4,A42;
        f1 = 0 .--> x by A2,A40;
        then
A47:    xi = x by A44,FUNCOP_1:72;
A48:    g1 = 0 .--> y by A2,A41;
        R = pz by A43,CARD_1:49,TARSKI:def 1;
        hence x <= y by A45,A46,A47,A48,FUNCOP_1:72;
      end;
      hence f is isomorphic by A25,A34,WAYBEL_0:66;
    end;
  end;
  hence thesis by WAYBEL_1:def 8;
end;

registration
  let X be set, p be RelStr-yielding ManySortedSet of X, Y be Subset of X;
  cluster p|Y -> RelStr-yielding;
  coherence
  proof
    now
      let v be set;
      assume v in rng (p|Y);
      then consider x being set such that
A1:   x in dom (p|Y) and
A2:   v = (p|Y).x by FUNCT_1:def 3;
A3:   x in Y by A1;
      then
A4:   (p|Y).x = p.x by FUNCT_1:49;
      x in X by A3;
      then x in dom p by PARTFUN1:def 2;
      then p.x in rng p by FUNCT_1:3;
      hence v is RelStr by A2,A4,YELLOW_1:def 3;
    end;
    hence thesis by YELLOW_1:def 3;
  end;
end;

theorem Th40:
  for n being non empty Nat, p being RelStr-yielding ManySortedSet of n
  holds product p is non empty iff p is non-Empty
proof
  let n be non empty Nat, p be RelStr-yielding ManySortedSet of n;
  hereby
    assume product p is non empty;
    then product Carrier p is non empty by YELLOW_1:def 4;
    then consider z being set such that
A1: z in product Carrier p by XBOOLE_0:def 1;
A2: ex g being Function st ( z = g)&( dom g = dom (Carrier p))&
( for i being set st i in dom (Carrier p) holds g.i in (Carrier p).i) by A1,
CARD_3:def 5;
    now
      let S be 1-sorted;
      assume S in rng p;
      then consider x being set such that
A3:   x in dom p and
A4:   S = p.x by FUNCT_1:def 3;
A5:   x in n by A3;
      then
A6:   x in dom (Carrier p) by PARTFUN1:def 2;
      ex R being 1-sorted st ( R = p.x)&( (Carrier p).x = the
      carrier of R) by A5,PRALG_1:def 13;
      hence S is non empty by A2,A4,A6;
    end;
    hence p is non-Empty by WAYBEL_3:def 7;
  end;
  assume
A7: p is non-Empty;
A8: dom Carrier p = n by PARTFUN1:def 2;
  deffunc F(set) = choose (Carrier p).$1;
  consider g being Function such that
A9: dom g = dom Carrier p and
  A10: for
 i being set st i in dom Carrier p holds g.i = F(i) from FUNCT_1:sch 3;
  set x = g;
  now
    take g;
    thus x = g;
    thus dom g = dom Carrier p by A9;
    thus
    for i being set st i in dom Carrier p holds g.i in (Carrier p).i
    proof
      let i be set such that
A11:  i in dom Carrier p;
      i in dom p by A8,A11,PARTFUN1:def 2;
      then
A12:  p.i in rng p by FUNCT_1:def 3;
      then reconsider pi1 = p.i as RelStr by YELLOW_1:def 3;
      pi1 is non empty by A7,A12,WAYBEL_3:def 7;
      then
A13:  the carrier of pi1 is non empty;
      i in n by A11;
      then
A14:  ex R being 1-sorted st ( R = p.i)&( (Carrier p).i = the
      carrier of R) by PRALG_1:def 13;
      g.i = choose (Carrier p).i by A10,A11;
      hence thesis by A13,A14;
    end;
  end;
  then product Carrier p is non empty by CARD_3:def 5;
  hence thesis by YELLOW_1:def 4;
end;

theorem Th41:
  for n being non empty Nat, p being RelStr-yielding ManySortedSet of n+1,
  ns being Subset of n+1, ne being Element of n+1
  st ns = n & ne = n holds [:product(p|ns), p.ne:], product p are_isomorphic
proof
  let n be non empty Nat,
  p be RelStr-yielding ManySortedSet of n+1,
  ns be Subset of n+1, ne be Element of n+1 such that
A1: ns = n and
A2: ne = n;
  set S = [: product (p|ns), p.ne:];
  set T = product p;
  set CP = [: the carrier of product (p|ns), the carrier of p.ne:];
  set CPP = the carrier of product p;
A3: dom Carrier (p|ns) = n by A1,PARTFUN1:def 2;
  per cases;
  suppose
A4: the carrier of product p is empty;
    then
A5: T is empty;
    not p is non-Empty by A4;
    then consider r1 being 1-sorted such that
A6: r1 in rng p and
A7: r1 is empty by WAYBEL_3:def 7;
    consider x being set such that
A8: x in dom p and
A9: r1 = p.x by A6,FUNCT_1:def 3;
    x in n+1 by A8;
    then
A10: x in n \/ {n} by AFINSQ_1:2;
A11: S is empty
    proof
      per cases by A10,XBOOLE_0:def 3;
      suppose
A12:    x in n;
        then
A13:    (p|ns).x = p.x by A1,FUNCT_1:49;
        x in dom(p|ns) by A1,A12,PARTFUN1:def 2;
        then p.x in rng (p|ns) by A13,FUNCT_1:def 3;
        then not (p|ns) is non-Empty by A7,A9,WAYBEL_3:def 7;
        then reconsider
        ptemp = the carrier of product (p|ns) as empty set by A1,Th40;
        [: ptemp, the carrier of p.ne :] is empty;
        hence thesis by YELLOW_3:def 2;
      end;
      suppose x in {n};
        then p.ne is empty by A2,A7,A9,TARSKI:def 1;
        then reconsider pne = the carrier of p.ne as empty set;
        reconsider ptemp = the carrier of product (p|ns) as set;
        [: ptemp, pne :] is empty;
        hence thesis by YELLOW_3:def 2;
      end;
    end;
then A14: dom {} = the carrier of S;
    for x being set st x in {} holds {}.x in the carrier of T;
    then reconsider f = {} as Function of S, T by A14,FUNCT_2:3;
    f is isomorphic by A5,A11,WAYBEL_0:def 38;
    hence thesis by WAYBEL_1:def 8;
  end;
  suppose
A15: the carrier of product p is non empty;
    then reconsider CPP as non empty set;
    reconsider T as non empty RelStr by A15;
A16: p is non-Empty by A15,Th40;
    reconsider p9=p as RelStr-yielding non-Empty ManySortedSet of n+1
    by A15,Th40;
    p9.ne is non empty;
    then reconsider pne2 = the carrier of p.ne as non empty set;
    now
      let S be 1-sorted;
      assume S in rng (p|ns);
      then consider x being set such that
A17:  x in dom (p|ns) and
A18:  S = (p|ns).x by FUNCT_1:def 3;
      x in ns by A17;
      then x in n+1;
      then
A19:  x in dom p by PARTFUN1:def 2;
      S = p.x by A17,A18,FUNCT_1:47;
      then S in rng p by A19,FUNCT_1:def 3;
      hence S is non empty by A16,WAYBEL_3:def 7;
    end;
    then
A20: p|ns is non-Empty by WAYBEL_3:def 7;
    then
A21: product (p|ns) is non empty;
    reconsider ppns2 = the carrier of product (p|ns) as non empty set
    by A20;
    CP = [: ppns2, pne2 :];
    then reconsider S as non empty RelStr by YELLOW_3:def 2;
    CP = the carrier of S by YELLOW_3:def 2;
    then reconsider CP9 = CP as non empty set;
    defpred P[set,set] means ex a being Function, b being Element of pne2
    st a in ppns2 & $1 = [a,b] & $2 = a +* (n.-->b);
A22: for x being Element of CP9 ex y being Element of CPP st P[x,y]
    proof
      let x be Element of CP9;
      reconsider xx = x as Element of [: ppns2, pne2 :];
      set a = xx`1, b = xx`2;
      reconsider a as Element of ppns2 by MCART_1:10;
      reconsider b as Element of pne2 by MCART_1:10;
A23:  product Carrier (p|ns) is non empty by A21,YELLOW_1:def 4;
A24:  a is Element of product Carrier (p|ns) by YELLOW_1:def 4;
      then
A25:  ex g being Function st ( a = g)&( dom g = dom Carrier (p|ns
))&( for i being set st i in dom Carrier (p|ns) holds g.i in (Carrier (p|ns)).i
      ) by A23,CARD_3:def 5;
      reconsider a as Function by A24;
      set y = a +* (n.-->b);
      now
        set g1 = y;
        reconsider g1 as Function;
        take g1;
        thus y = g1;
A26:    dom a = ns by A25,PARTFUN1:def 2;
        thus dom g1 = dom a \/ dom (n.-->b) by FUNCT_4:def 1
          .= n \/ {n} by A1,A26,FUNCOP_1:13
          .= n+1 by AFINSQ_1:2
          .= dom (Carrier p) by PARTFUN1:def 2;
        let x be set;
        assume x in dom (Carrier p);
        then
A27:    x in n+1;
        then
A28:    x in n \/ {n} by AFINSQ_1:2;
        per cases by A28,XBOOLE_0:def 3;
        suppose
A29:      x in n;
          then x <> n;
          then not x in dom(n.-->b) by TARSKI:def 1;
          then
A30:      g1.x = a.x by FUNCT_4:11;
A31:      x in dom(Carrier (p|ns)) by A1,A29,PARTFUN1:def 2;
A32:      ex R being 1-sorted st ( R = (p|ns).x)&( (Carrier (p|ns)).x
          = the carrier of R) by A1,A29,PRALG_1:def 13;
          ex R2 being 1-sorted st ( R2 = p.x)&( (Carrier p).x = the
          carrier of R2) by A27,PRALG_1:def 13;
          then (Carrier (p|ns)).x = (Carrier p).x by A1,A29,A32,FUNCT_1:49;
          hence g1.x in (Carrier p).x by A25,A30,A31;
        end;
        suppose
A33:      x in {n};
          then
A34:      x = n by TARSKI:def 1;
          x in dom (n.-->b) by A33,FUNCOP_1:13;
          then
A35:      g1.x = (n.-->b).n by A34,FUNCT_4:13
            .= b by FUNCOP_1:72;
          ex R being 1-sorted st ( R = p.ne)&( (Carrier p).ne = the
          carrier of R) by PRALG_1:def 13;
          hence g1.x in (Carrier p).x by A2,A34,A35;
        end;
      end;
      then y in product Carrier p by CARD_3:def 5;
      then reconsider y as Element of CPP by YELLOW_1:def 4;
      take y,a,b;
      thus a in ppns2;
      thus x = [a,b] by MCART_1:21;
      thus thesis;
    end;
    consider f being Function of CP9, CPP such that
A36: for x being Element of CP9 holds P[x,f.x] from FUNCT_2:sch 3(A22);
    now
      the carrier of [:product(p|ns), p.ne :] =
      [:the carrier of product(p|ns),the carrier of p.ne:] by YELLOW_3:def 2;
      then reconsider f as Function of [:product (p|ns), p.ne:], product p;
      reconsider f9=f as Function of S, T;
      take f;
      now
        let x1,x2 be set such that
A37:    x1 in dom f and
A38:    x2 in dom f and
A39:    f.x1 = f.x2;
        x1 is Element of [:the carrier of product (p|ns),
        the carrier of p.ne :] by A37,YELLOW_3:def 2;
        then consider a1 being Function, b1 being Element of pne2 such that
A40:    a1 in ppns2 and
A41:    x1 = [a1, b1] and
A42:    f.x1 = a1 +* (n.-->b1) by A36;
        x2 is Element of [: the carrier of product (p|ns),
        the carrier of p.ne :] by A38,YELLOW_3:def 2;
        then consider a2 being Function, b2 being Element of pne2 such that
A43:    a2 in ppns2 and
A44:    x2 = [a2, b2] and
A45:    f.x2 = a2 +* (n.-->b2) by A36;
        a1 in product Carrier (p|ns) by A40,YELLOW_1:def 4;
        then
A46:    ex g1 being Function st ( a1 = g1)&( dom g1 = dom Carrier (
p|ns))&( for x being set st x in dom Carrier (p|ns) holds g1.x in (Carrier (p|
        ns)).x) by CARD_3:def 5;
        a2 in product Carrier (p|ns) by A43,YELLOW_1:def 4;
        then
A47:    ex g2 being Function st ( a2 = g2)&( dom g2 = dom Carrier (
p|ns))&( for x being set st x in dom Carrier (p|ns) holds g2.x in (Carrier (p|
        ns)).x) by CARD_3:def 5;
A48:    dom (n .--> b1) = {n} by FUNCOP_1:13;
        then
A49:    dom (n .--> b1) = dom (n.-->b2) by FUNCOP_1:13;
A50:    dom a1 = n by A1,A46,PARTFUN1:def 2;
A51:    now
          assume not n misses {n};
          then n /\ {n} <> {} by XBOOLE_0:def 7;
          then consider x being set such that
A52:      x in n /\ {n} by XBOOLE_0:def 1;
A53:      x in n by A52,XBOOLE_0:def 4;
          x in {n} by A52,XBOOLE_0:def 4;
          then x = n by TARSKI:def 1;
          hence contradiction by A53;
        end;
        then
A54:    dom a1 misses dom (n.-->b1) by A50,FUNCOP_1:13;
A55:    dom a2 misses dom (n.-->b2) by A46,A47,A50,A51,FUNCOP_1:13;
A56:    now
          let a, b be set;
          hereby
            assume
A57:        [a,b] in a1;
            then
A58:        a in dom a1 by FUNCT_1:1;
A59:        b = a1.a by A57,FUNCT_1:1;
A60:        a in dom a1 \/ dom (n.-->b1) by A58,XBOOLE_0:def 3;
            then not a in dom (n.-->b1) by A54,A58,XBOOLE_0:5;
            then
A61:        (a2+*(n.-->b2)).a = a1.a by A39,A42,A45,A60,FUNCT_4:def 1;
A62:        a in dom a2 \/ dom (n.-->b2) by A46,A47,A58,XBOOLE_0:def 3;
A63:        a in dom a2 by A46,A47,A57,FUNCT_1:1;
            then not a in dom (n.-->b2) by A55,A62,XBOOLE_0:5;
            then b = a2.a by A59,A61,A62,FUNCT_4:def 1;
            hence [a,b] in a2 by A63,FUNCT_1:1;
          end;
          assume
A64:      [a,b] in a2;
          then
A65:      a in dom a2 by FUNCT_1:1;
A66:      b = a2.a by A64,FUNCT_1:1;
A67:      a in dom a2 \/ dom (n.-->b2) by A65,XBOOLE_0:def 3;
          then not a in dom (n.-->b2) by A55,A65,XBOOLE_0:5;
          then
A68:      (a1 +* (n.-->b1)).a = a2.a by A39,A42,A45,A67,FUNCT_4:def 1;
A69:      a in dom a1 \/ dom (n.-->b1) by A46,A47,A65,XBOOLE_0:def 3;
A70:      a in dom a1 by A46,A47,A64,FUNCT_1:1;
          then not a in dom (n.-->b1) by A54,A69,XBOOLE_0:5;
          then b = a1.a by A66,A68,A69,FUNCT_4:def 1;
          hence [a,b] in a1 by A70,FUNCT_1:1;
        end;
A71:    n in dom (n.-->b1) by A48,TARSKI:def 1;
        then
A72:    n in dom a1 \/ dom (n.-->b1) by XBOOLE_0:def 3;
A73:    n in dom (n.-->b2) by A48,A49,TARSKI:def 1;
        then n in dom a2 \/ dom (n.-->b2) by XBOOLE_0:def 3;
        then (a1 +* (n.-->b1)).n = (n.-->b2).n by A39,A42,A45,A73,FUNCT_4:def 1
          .= b2 by FUNCOP_1:72;
        then b2 = (n.-->b1).n by A71,A72,FUNCT_4:def 1
          .= b1 by FUNCOP_1:72;
        hence x1 = x2 by A41,A44,A56,RELAT_1:def 2;
      end;
      then
A74:  f is one-to-one by FUNCT_1:def 4;
      now
        let y be set;
        thus y in rng f implies y in the carrier of product p;
        assume y in the carrier of product p;
        then y in product Carrier p by YELLOW_1:def 4;
        then consider g being Function such that
A75:    y = g and
A76:    dom g = dom (Carrier p) and
A77:    for x being set st x in dom Carrier p holds g.x in (Carrier p).x
        by CARD_3:def 5;
A78:    dom Carrier p = n+1 by PARTFUN1:def 2;
A79:    n+1 = {i where i is Element of NAT : i < n+1} by AXIOMS:4;
A80:    n in NAT by ORDINAL1:def 12;
        n < n+1 by NAT_1:13;
        then
A81:    n in n+1 by A79,A80;
        set a = g|n, b = g.n;
        set x = [a,b];
A82:    dom (Carrier (p|ns)) = ns by PARTFUN1:def 2;
A83:    dom a = dom g /\ n by RELAT_1:61
          .= (n+1) /\ n by A76,PARTFUN1:def 2;
        then
A84:    dom a = n by Th2,XBOOLE_1:28;
A85:    dom a = dom (Carrier (p|ns)) by A1,A82,A83,XBOOLE_1:28;
        now
          let x be set;
          assume x in dom (Carrier (p|ns));
          then
A86:      x in n by A1;
A87:      n c= n+1 by Th2;
A88:      a.x = g.x by A86,FUNCT_1:49;
A89:      g.x in (Carrier p).x by A77,A78,A86,A87;
A90:      ex R1 being 1-sorted st ( R1 = p.x)&( (Carrier p).x = the
          carrier of R1) by A86,A87,PRALG_1:def 13;
          ex R2 being 1-sorted st ( R2 = (p|ns).x)&( (Carrier (p|ns))
          .x = the carrier of R2) by A1,A86,PRALG_1:def 13;
          hence a.x in (Carrier (p|ns)).x by A1,A86,A88,A89,A90,FUNCT_1:49;
        end;
        then a in product (Carrier (p|ns)) by A85,CARD_3:9;
        then
A91:    a in the carrier of product(p|ns) by YELLOW_1:def 4;
        ex R1 being 1-sorted st ( R1 = p.n)&( (Carrier p).n = the
        carrier of R1) by A81,PRALG_1:def 13;
        then
A92:    b in the carrier of p.ne by A2,A77,A78;
        then [a,b] in [:the carrier of product(p|ns), the carrier of p.ne :]
        by A91,ZFMISC_1:87;
        then
A93:    x in dom f by FUNCT_2:def 1;
        x is Element of CP9 by A91,A92,ZFMISC_1:87;
        then consider ta being Function, tb being Element of pne2 such that
        ta in ppns2 and
A94:    x = [ta, tb] and
A95:    f.x = ta +* (n.-->tb) by A36;
A96:    ta = a by A94,XTUPLE_0:1;
A97:    tb = b by A94,XTUPLE_0:1;
        now
          let i, j be set;
          hereby
            assume
A98:        [i,j] in (a+*(n.-->b));
            then i in dom (a +* (n.-->b)) by FUNCT_1:1;
            then
A99:       i in ((dom a) \/ dom ((n.-->b))) by FUNCT_4:def 1;
            then
A100:       i in n \/ {n} by A84,FUNCOP_1:13;
A101:       (a+*(n.-->b)).i = j by A98,FUNCT_1:1;
            per cases;
            suppose
A102:         i in dom ((n.-->b));
              then i in {n};
              then
A103:         i = n by TARSKI:def 1;
              (a+*(n.-->b)).i = (n.-->b).i by A99,A102,FUNCT_4:def 1
                .= b by A103,FUNCOP_1:72;
              then
A104:         g.i = j by A98,A103,FUNCT_1:1;
              i in dom g by A76,A78,A100,AFINSQ_1:2;
              hence [i,j] in g by A104,FUNCT_1:1;
            end;
            suppose
A105:         not i in dom ((n.-->b));
              then not i in {n} by FUNCOP_1:13;
              then
A106:         i in n by A100,XBOOLE_0:def 3;
              (a +* (n.-->b)).i = a.i by A99,A105,FUNCT_4:def 1;
              then
A107:         g.i = j by A101,A106,FUNCT_1:49;
              i in dom g by A76,A78,A100,AFINSQ_1:2;
              hence [i,j] in g by A107,FUNCT_1:1;
            end;
          end;
          assume
A108:     [i,j] in g;
          then
A109:     i in n+1 by A76,A78,FUNCT_1:1;
          then
A110:     i in n \/ {n} by AFINSQ_1:2;
          dom (a+* (n.-->b)) = dom a \/ dom (n.-->b) by FUNCT_4:def 1
            .= n \/ {n} by A84,FUNCOP_1:13;
          then
A111:     i in dom (a+*(n.-->b)) by A109,AFINSQ_1:2;
          then
A112:     i in dom a \/ dom (n.-->b) by FUNCT_4:def 1;
          per cases;
          suppose
A113:       i in dom (n.-->b);
            then i in {n};
            then
A114:       i = n by TARSKI:def 1;
            (a+* (n.-->b)).i = (n.-->b).i by A112,A113,FUNCT_4:def 1
              .= b by A114,FUNCOP_1:72
              .= j by A108,A114,FUNCT_1:1;
            hence [i,j] in (a+*(n.-->b)) by A111,FUNCT_1:1;
          end;
          suppose
A115:       not i in dom (n.-->b);
            then not i in {n} by FUNCOP_1:13;
            then
A116:       i in n by A110,XBOOLE_0:def 3;
            (a+*(n.-->b)).i = a.i by A112,A115,FUNCT_4:def 1
              .= g.i by A116,FUNCT_1:49
              .= j by A108,FUNCT_1:1;
            hence [i,j] in (a+*(n.-->b)) by A111,FUNCT_1:1;
          end;
        end;
        then f.x = y by A75,A95,A96,A97,RELAT_1:def 2;
        hence y in rng f by A93,FUNCT_1:def 3;
      end;
      then
A117: rng f = the carrier of product p by TARSKI:1;
      now
        let x, y be Element of S;
A118:   x is Element of CP by YELLOW_3:def 2;
        then consider xa being Function, xb being Element of pne2 such that
A119:   xa in ppns2 and
A120:   x = [xa,xb] and
A121:   f.x = xa +* (n.-->xb) by A36;
        dom f = CP9 by FUNCT_2:def 1;
        then f.x in the carrier of product p by A117,A118,FUNCT_1:def 3;
        then
A122:   f9.x in product Carrier p by YELLOW_1:def 4;
        y is Element of CP by YELLOW_3:def 2;
        then consider ya being Function, yb being Element of pne2 such that
A123:   ya in ppns2 and
A124:   y = [ya,yb] and
A125:   f.y = ya +* (n.-->yb) by A36;
A126:   [xa,xb]`1 = xa;
A127:   [xa,xb]`2 = xb;
A128:   xa in product Carrier (p|ns) by A119,YELLOW_1:def 4;
        then
A129:   ex gx being Function st ( xa = gx)&( dom gx = dom Carrier (
p|ns))&( for x being set st x in dom Carrier (p|ns) holds gx.x in (Carrier (p|
        ns)).x) by CARD_3:def 5;
        then
A130:   dom xa = n by A1,PARTFUN1:def 2;
        then
A131:   dom xa \/ dom (n.-->xb) = n \/ {n} by FUNCOP_1:13;
        ya in product Carrier(p|ns) by A123,YELLOW_1:def 4;
        then
A132:   ex gy being Function st ( ya = gy)&( dom gy = dom Carrier (
p|ns))&( for x being set st x in dom Carrier (p|ns) holds gy.x in (Carrier (p|
        ns)).x) by CARD_3:def 5;
        then
A133:   dom ya = n by A1,PARTFUN1:def 2;
        then
A134:   dom ya \/ dom (n.-->yb) = n \/ {n} by FUNCOP_1:13;
        reconsider xa9=xa as Element of product(p|ns) by A119;
        reconsider ya9=ya as Element of product(p|ns) by A123;
        hereby
          assume x <= y;
          then [x,y] in the InternalRel of S by ORDERS_2:def 5;
          then
A135:     [x,y] in ["the InternalRel of product(p|ns),
          the InternalRel of p.ne"] by YELLOW_3:def 2;
          then
A136:     [[x,y]`1`1,[x,y]`2`1] in the InternalRel of product(p| ns ) by
YELLOW_3:10;
A137:     [[x,y]`1`2,[x,y]`2`2] in the InternalRel of p.ne by A135,YELLOW_3:10;
          [ya,yb]`1 = ya;
          then
A138:     [xa,ya] in the InternalRel of product(p|ns)
          by A124,A126,A136,A120;
A139:     xa in product Carrier(p|ns) by A119,YELLOW_1:def 4;
          xa9 <= ya9 by A138,ORDERS_2:def 5;
          then consider ffx,ggx being Function such that
A140:     ffx = xa and
A141:     ggx = ya and
A142:     for i being set st i in n
          ex RR being RelStr, xxi, yyi being Element of RR
          st RR = (p|ns).i & xxi = ffx.i & yyi = ggx.i & xxi <= yyi
          by A1,A139,YELLOW_1:def 4;
          [ya,yb]`2 = yb;
          then
A143:     [xb,yb] in the InternalRel of p.ne
            by A124,A127,A137,A120;
          reconsider xb9=xb as Element of p.ne;
          reconsider yb9=yb as Element of p.ne;
A144:     xb9 <= yb9 by A143,ORDERS_2:def 5;
          ex f1,g1 being Function st f1 = f.x & g1 = f.y &
          for i being set st i in n+1
          ex R being RelStr, xi, yi being Element of R
          st R = p.i & xi = f1.i & yi = g1.i & xi <= yi
          proof
            set f1 = xa +* (n.-->xb), g1 = ya +* (n.-->yb);
            take f1, g1;
            thus f1 = f.x by A121;
            thus g1 = f.y by A125;
            let i be set such that
A145:       i in n+1;
A146:       i in n \/ {n} by A145,AFINSQ_1:2;
            set R = p.i;
            set xi = f1.i;
            set yi = g1.i;
            i in dom p by A145,PARTFUN1:def 2;
            then p.i in rng p by FUNCT_1:def 3;
            then reconsider R as RelStr by YELLOW_1:def 3;
A147:       i in dom xa \/ dom (n.-->xb) by A131,A145,AFINSQ_1:2;
            now per cases;
              suppose
A148:           i in dom(n.-->xb);
                then i in {n};
                then
A149:           i = n by TARSKI:def 1;
                f1.i = (n.-->xb).i by A147,A148,FUNCT_4:def 1;
                hence xi is Element of R by A2,A149,FUNCOP_1:72;
              end;
              suppose
A150:           not i in dom(n.-->xb);
                then
A151:           not i in {n} by FUNCOP_1:13;
                then
A152:           i in n by A146,XBOOLE_0:def 3;
A153:           i in dom Carrier (p|ns) by A3,A146,A151,XBOOLE_0:def 3;
                f1.i = xa.i by A147,A150,FUNCT_4:def 1;
                then
A154:           xi in (Carrier (p|ns)).i by A129,A153;
                ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
                i =the carrier of R2) by A1,A152,PRALG_1:def 13;
                hence xi is Element of R by A1,A152,A154,FUNCT_1:49;
              end;
            end;
            then reconsider xi as Element of R;
A155:       i in dom ya \/ dom (n.-->yb) by A134,A145,AFINSQ_1:2;
            now per cases;
              suppose
A156:           i in dom(n.-->yb);
                then i in {n};
                then
A157:           i = n by TARSKI:def 1;
                g1.i = (n.-->yb).i by A155,A156,FUNCT_4:def 1;
                hence yi is Element of R by A2,A157,FUNCOP_1:72;
              end;
              suppose
A158:           not i in dom(n.-->yb);
                then
A159:           not i in {n} by FUNCOP_1:13;
                then
A160:           i in n by A146,XBOOLE_0:def 3;
A161:           i in dom Carrier (p|ns) by A3,A146,A159,XBOOLE_0:def 3;
                g1.i = ya.i by A155,A158,FUNCT_4:def 1;
                then
A162:           yi in (Carrier (p|ns)).i by A132,A161;
                ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
                i=the carrier of R2) by A1,A160,PRALG_1:def 13;
                hence yi is Element of R by A1,A160,A162,FUNCT_1:49;
              end;
            end;
            then reconsider yi as Element of R;
            take R,xi,yi;
            thus R = p.i;
            thus xi = f1.i;
            thus yi = g1.i;
            per cases by A146,XBOOLE_0:def 3;
            suppose
A163:         i in n;
A164:         not i in {n}
              proof
                assume i in {n};
                then n in n by A163,TARSKI:def 1;
                hence contradiction;
              end;
              then
A165:         not i in dom (n.-->xb);
              not i in dom (n.-->yb) by A164;
              then
A166:         yi = ya.i by A155,FUNCT_4:def 1;
              consider RR being RelStr, xxi, yyi being Element of RR such that
A167:         RR = (p|ns).i and
A168:         xxi = ffx.i and
A169:         yyi = ggx.i and
A170:         xxi <= yyi by A142,A163;
              RR = R by A1,A163,A167,FUNCT_1:49;
              hence thesis by A140,A141,A147,A165,A166,A168,A169,A170,
FUNCT_4:def 1;
            end;
            suppose
A171:         i in {n};
              then
A172:         i = n by TARSKI:def 1;
A173:         i in dom (n.-->xb) by A171,FUNCOP_1:13;
A174:         i in dom (n.-->yb) by A171,FUNCOP_1:13;
A175:         xi = (n.-->xb).i by A147,A173,FUNCT_4:def 1
                .= xb by A172,FUNCOP_1:72;
              yi = (n.-->yb).i by A155,A174,FUNCT_4:def 1
                .= yb by A172,FUNCOP_1:72;
              hence thesis by A2,A144,A171,A175,TARSKI:def 1;
            end;
          end;
          hence f9.x <= f9.y by A122,YELLOW_1:def 4;
        end;
        assume f9.x <= f9.y;
        then consider f1, g1 being Function such that
A176:   f1 = f.x and
A177:   g1 = f.y and
A178:   for i be set st i in n+1 ex R being RelStr, xi,yi being Element of R
        st R = p.i & xi = f1.i & yi = g1.i & xi <= yi by A122,YELLOW_1:def 4;
        now
          set f2 = xa9, g2 = ya9;
          reconsider f2, g2 as Function;
          take f2, g2;
          thus f2 = xa9 & g2 = ya9;
          let i be set such that
A179:     i in ns;
A180:     not i in {n}
          proof
            assume i in {n};
            then i = n by TARSKI:def 1;
            hence contradiction by A1,A179;
          end;
          then
A181:     not i in dom (n.-->yb);
A182:     not i in dom (n.-->xb) by A180;
          set R = (p|ns).i;
          i in dom (p|ns) by A179,PARTFUN1:def 2;
          then (p|ns).i in rng (p|ns) by FUNCT_1:def 3;
          then reconsider R as RelStr by YELLOW_1:def 3;
          take R;
          set xi = xa.i, yi = ya.i;
A183:     i in dom xa \/ dom (n.-->xb) by A1,A130,A179,XBOOLE_0:def 3;
A184:     i in dom Carrier(p|ns) by A179,PARTFUN1:def 2;
          ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
          i = the carrier of R2) by A179,PRALG_1:def 13;
          then reconsider xi as Element of R by A129,A184;
A185:     i in dom ya \/ dom (n.-->yb) by A1,A133,A179,XBOOLE_0:def 3;
          ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
          i = the carrier of R2) by A179,PRALG_1:def 13;
          then reconsider yi as Element of R by A132,A184;
          take xi, yi;
          thus R = (p|ns).i & xi = f2.i & yi = g2.i;
          consider R2 being RelStr, xi2, yi2 being Element of R2 such that
A186:     R2 = p.i and
A187:     xi2 = f1.i and
A188:     yi2 = g1.i and
A189:     xi2 <= yi2 by A178,A179;
A190:     R2 = R by A179,A186,FUNCT_1:49;
          (xa +* (n.-->xb)).i = xi by A182,A183,FUNCT_4:def 1;
          hence xi <= yi by A121,A125,A176,A177,A181,A185,A187,A188,A189,A190,
FUNCT_4:def 1;
        end;
        then xa9 <= ya9 by A128,YELLOW_1:def 4;
        then
A191:    [xa,ya] in the InternalRel of product(p|ns) by ORDERS_2:def 5;
        [ya,yb]`1 = ya;
          then
A192:   [[x,y]`1`1, [x,y]`2`1] in the InternalRel of product(p|ns)
        by A124,A126,A120,A191;
        consider Rn being RelStr, xni, yni being Element of Rn such that
A193:   Rn = p.ne and
A194:   xni = f1.n and
A195:   yni = g1.n and
A196:   xni <= yni by A2,A178;
A197:   [xni, yni] in the InternalRel of p.ne by A193,A196,ORDERS_2:def 5;
        dom (n.-->xb) = {n} by FUNCOP_1:13;
        then
A198:   n in dom (n.-->xb) by TARSKI:def 1;
        then n in dom xa \/ dom (n.-->xb) by XBOOLE_0:def 3;
        then
A199:   (xa +* (n.-->xb)).n = (n.-->xb).n by A198,FUNCT_4:def 1
          .= xb by FUNCOP_1:72;
        dom (n.-->yb) = {n} by FUNCOP_1:13;
        then
A200:   n in dom (n.-->yb) by TARSKI:def 1;
        then n in dom ya \/ dom (n.-->yb) by XBOOLE_0:def 3;
        then
A201:    (ya +* (n.-->yb)).n = (n.-->yb).n by A200,FUNCT_4:def 1
          .= yb by FUNCOP_1:72;
        [ya,yb]`2 = yb;
          then
A202:   [[x,y]`1`2, [x,y]`2`2] in the InternalRel of p.ne
        by A121,A124,A125,A127,A176,A177,A194,A195,A197,A199,A201
,A120;
A203:   [x,y]`1 = [xa,xb] by A120;
        [x,y]`2 = [ya,yb] by A124;
        then [x,y] in ["the InternalRel of product (p|ns),
        the InternalRel of p.ne"] by A192,A202,A203,YELLOW_3:10;
        then [x,y] in the InternalRel of S by YELLOW_3:def 2;
        hence x <= y by ORDERS_2:def 5;
      end;
      hence f is isomorphic by A74,A117,WAYBEL_0:66;
    end;
    hence thesis by WAYBEL_1:def 8;
  end;
end;

theorem Th42: :: Corollary 4.47
  for n being non empty Nat, p being RelStr-yielding ManySortedSet of n
  st for i being Element of n holds p.i is Dickson & p.i is quasi_ordered
  holds product p is quasi_ordered & product p is Dickson
proof
  defpred P[non empty Nat] means
  for p being RelStr-yielding ManySortedSet of $1
  st for i being Element of $1 holds p.i is Dickson & p.i is quasi_ordered
  holds product p is quasi_ordered & product p is Dickson;
A1: P[1]
  proof
    let p be RelStr-yielding ManySortedSet of 1 such that
A2: for i being Element of 1 holds p.i is Dickson & p.i is quasi_ordered;
    reconsider z = 0 as Element of 1 by CARD_1:49,TARSKI:def 1;
A3: p.z is Dickson by A2;
A4: p.z is quasi_ordered by A2;
    p.z,product p are_isomorphic by Th39;
    hence thesis by A3,A4,Th38;
  end;
A5: now
    let n be non empty Nat;
    assume
A6: P[n];
    thus P[n+1]
    proof
      let p be RelStr-yielding ManySortedSet of n+1;
      assume
      A7:   for
 i being Element of (n+1) holds p.i is Dickson & p.i is quasi_ordered;
      n <= n+1 by NAT_1:11;
      then reconsider ns = n as Subset of n+1 by NAT_1:39;
A8:   n+1 = {k where k is Element of NAT : k < n+1} by AXIOMS:4;
A9:   n in NAT by ORDINAL1:def 12;
      n < n+1 by NAT_1:13;
      then n in n+1 by A8,A9;
      then reconsider ne = n as Element of n+1;
      reconsider pns = p|ns as RelStr-yielding ManySortedSet of n;
      A10:  for
 i being Element of n holds pns.i is Dickson & pns.i is quasi_ordered
      proof
        let i be Element of n;
A11:    (pns.i) = p.i by FUNCT_1:49;
A12:    n = {k where k is Element of NAT : k < n} by AXIOMS:4;
        i in n;
        then consider k being Element of NAT such that
A13:    k = i and
A14:    k < n by A12;
        k < n+1 by A14,NAT_1:13;
        then i in n+1 by A8,A13;
        then reconsider i9=i as Element of n+1;
        i9 = i;
        hence thesis by A7,A11;
      end;
      then
A15:  product(pns) is Dickson by A6;
A16:  product(pns) is quasi_ordered by A6,A10;
A17:  p.ne is Dickson by A7;
A18:  p.ne is quasi_ordered by A7;
      then
A19:  [:product(p|ns), p.ne:] is Dickson by A15,A16,A17,Th37;
A20:  [:product(p|ns), p.ne:] is quasi_ordered by A15,A16,A17,A18,Th37;
      [:product(p|ns),p.ne:], product p are_isomorphic by Th41;
      hence thesis by A19,A20,Th38;
    end;
  end;
  thus for n being non empty Nat holds P[n] from NAT_1:sch 10(A1,
  A5);
end;

Lm1: for p being RelStr-yielding ManySortedSet of {}
holds product p is non empty &
product p is quasi_ordered & product p is Dickson & product p is antisymmetric
proof
  let p be RelStr-yielding ManySortedSet of {};
A1: product p = RelStr (# {{}}, id {{}} #) by YELLOW_1:26;
  set pp = product p, cpp = the carrier of pp, ipp = the InternalRel of pp;
A2: ipp = id {{}} by YELLOW_1:26;
  thus pp is non empty by YELLOW_1:26;
  thus pp is quasi_ordered
  proof
    thus pp is reflexive by YELLOW_1:26;
    let x, y, z be set;
    assume that x in cpp and y in cpp
    and z in cpp and
A3: [x,y] in ipp and
A4: [y,z] in ipp;
    thus thesis by A2,A3,A4,RELAT_1:def 10;
  end;
  thus pp is Dickson
  proof
    let N be Subset of cpp;
    per cases by A1,ZFMISC_1:33;
    suppose
A5:   N = {};
      take B = {};
      N = {} cpp by A5;
      hence B is_Dickson-basis_of N,pp by Th25;
      thus thesis;
    end;
    suppose
A6:   N = {{}};
      take B = {{}};
      thus B is_Dickson-basis_of N,pp
      proof
        thus B c= N by A6;
        let a be Element of pp;
        assume
A7:     a in N;
        take b = a;
        thus b in B by A6,A7;
        [b,a] in id {{}} by A6,A7,RELAT_1:def 10;
        hence thesis by A2,ORDERS_2:def 5;
      end;
      thus thesis;
    end;
  end;
  thus thesis by YELLOW_1:26;
end;

registration
  let p be RelStr-yielding ManySortedSet of {};
  cluster product p -> non empty;
  coherence by Lm1;
  cluster product p -> antisymmetric;
  coherence by Lm1;
  cluster product p -> quasi_ordered;
  coherence by Lm1;
::$N Dickson Lemma
  cluster product p -> Dickson;
  coherence by Lm1;
end;

definition
  func NATOrd -> Relation of NAT equals
  {[x,y] where x, y is Element of NAT : x <= y};
  correctness
  proof
    set NO = {[x,y] where x, y is Element of NAT : x <= y};
    now
      let z be set;
      assume z in NO;
      then ex x, y being Element of NAT st ( z = [x,y])&( x <= y);
      hence z in [:NAT, NAT:];
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th43:
  NATOrd is_reflexive_in NAT
proof
  let x be set;
  assume x in NAT;
  then reconsider x9 = x as Element of NAT;
  x9 <= x9;
  hence thesis;
end;

theorem Th44:
  NATOrd is_antisymmetric_in NAT
proof
  let x, y be set such that x in NAT and y in NAT and
A1: [x,y] in NATOrd and
A2: [y,x] in NATOrd;
  consider x9, y9 being Element of NAT such that
A3: [x,y] = [x9,y9] and
A4: x9 <= y9 by A1;
A5: x = x9 by A3,XTUPLE_0:1;
A6: y = y9 by A3,XTUPLE_0:1;
  consider y2, x2 being Element of NAT such that
A7: [y,x] = [y2,x2] and
A8: y2 <= x2 by A2;
A9: y2 = y9 by A6,A7,XTUPLE_0:1;
  x2 = x9 by A5,A7,XTUPLE_0:1;
  hence thesis by A4,A5,A6,A8,A9,XXREAL_0:1;
end;

theorem Th45:
  NATOrd is_strongly_connected_in NAT
proof
  now
    let x, y be set such that
A1: x in NAT and
A2: y in NAT;
    thus [x,y] in NATOrd or [y,x] in NATOrd
    proof
      assume that
A3:   not [x,y] in NATOrd and
A4:   not [y,x] in NATOrd;
      reconsider x,y as Element of NAT by A1,A2;
      per cases;
      suppose x <= y;
        hence contradiction by A3;
      end;
      suppose y <= x;
        hence contradiction by A4;
      end;
    end;
  end;
  hence thesis by RELAT_2:def 7;
end;

theorem Th46:
  NATOrd is_transitive_in NAT
proof
  let x, y, z be set such that x in NAT and y in NAT
  and z in NAT and
A1: [x,y] in NATOrd and
A2: [y,z] in NATOrd;
  consider x1,y1 being Element of NAT such that
A3: [x,y] = [x1,y1] and
A4: x1 <= y1 by A1;
A5: x = x1 by A3,XTUPLE_0:1;
A6: y = y1 by A3,XTUPLE_0:1;
  consider y2, z2 being Element of NAT such that
A7: [y,z] = [y2,z2] and
A8: y2 <= z2 by A2;
A9: y = y2 by A7,XTUPLE_0:1;
A10: z = z2 by A7,XTUPLE_0:1;
  x1 <= z2 by A4,A6,A8,A9,XXREAL_0:2;
  hence thesis by A5,A10;
end;

definition
  func OrderedNAT -> non empty RelStr equals
  RelStr(# NAT, NATOrd #);
  correctness;
end;

Lm2: now now
    let x, y be Element of OrderedNAT;
    assume not x <= y;
    then not [x,y] in NATOrd by ORDERS_2:def 5;
    then [y,x] in NATOrd by Th45,RELAT_2:def 7;
    hence y <= x by ORDERS_2:def 5;
  end;
  hence OrderedNAT is connected by WAYBEL_0:def 29;
end;

registration
  cluster OrderedNAT -> connected;
  coherence by Lm2;
  cluster OrderedNAT -> Dickson;
  coherence
  proof
    set IR9 = the InternalRel of OrderedNAT\~,CR9 =the carrier of OrderedNAT\~;
    now
      let N be set such that
A1:   N c= CR9 and
A2:   N <> {};
A3:   ex k being set st ( k in N) by A2,XBOOLE_0:def 1;
      defpred P[Nat] means $1 in N;
A4:   ex k being Nat st P[k] by A1,A3;
      consider m being Nat such that
A5:   P[m] and
A6:   for n being Nat st P[n] holds m <= n from NAT_1:sch 5(A4);
      reconsider m as Element of OrderedNAT by ORDINAL1:def 12;
      thus ex m being set st m in N & IR9-Seg(m) misses N
      proof
        take m;
        thus m in N by A5;
        now
          assume IR9-Seg(m) /\ N <> {};
          then consider z being set such that
A7:       z in IR9-Seg(m) /\ N by XBOOLE_0:def 1;
A8:       z in IR9-Seg(m) by A7,XBOOLE_0:def 4;
A9:       z in N by A7,XBOOLE_0:def 4;
A10:      z <> m by A8,WELLORD1:1;
A11:      [z,m] in IR9 by A8,WELLORD1:1;
          then [z,m] in NATOrd;
          then consider x,y being Element of NAT such that
A12:      [z,m] = [x,y] and x <= y;
A13:      z = x by A12,XTUPLE_0:1;
A14:      m = y by A12,XTUPLE_0:1;
          then y <= x by A6,A9,A13;
          then [y,x] in NATOrd;
          hence contradiction by A10,A11,A13,A14,Th44,RELAT_2:def 4;
        end;
        hence thesis by XBOOLE_0:def 7;
      end;
    end;
    then IR9 is_well_founded_in CR9 by WELLORD1:def 3;
    then OrderedNAT\~ is well_founded by WELLFND1:def 2;
    hence thesis by Th27;
  end;
  cluster OrderedNAT -> quasi_ordered;
  coherence
  proof
A15: OrderedNAT is reflexive by Th43,ORDERS_2:def 2;
    OrderedNAT is transitive by Th46,ORDERS_2:def 3;
    hence thesis by A15,Def3;
  end;
  cluster OrderedNAT -> antisymmetric;
  coherence by Th44,ORDERS_2:def 4;
  cluster OrderedNAT -> transitive;
  coherence by Th46,ORDERS_2:def 3;
  cluster OrderedNAT -> well_founded;
  coherence
  proof
    set ir = the InternalRel of OrderedNAT;
    now
      given f being sequence of OrderedNAT such that
A16:  f is descending;
A17:  dom f = NAT by FUNCT_2:def 1;
      reconsider rf = rng f as non empty Subset of NAT;
      set m = min rf;
      m in rng f by XXREAL_2:def 7;
      then consider d being set such that
A18:  d in dom f and
A19:  m = f.d by FUNCT_1:def 3;
      reconsider d as Element of NAT by A18;
A20:  f.(d+1) <> f.d by A16,WELLFND1:def 6;
      [f.(d+1),f.d] in ir by A16,WELLFND1:def 6;
      then consider x, y being Element of NAT such that
A21:  [f.(d+1),f.d] = [x,y] and
A22:  x <= y;
      reconsider fd1 = f.(d+1), fd = f.d as Element of NAT;
A23:  f.(d+1) = x by A21,XTUPLE_0:1;
      f.d = y by A21,XTUPLE_0:1;
      then
A24:  fd1 < fd by A20,A22,A23,XXREAL_0:1;
      f.(d+1) in rf by A17,FUNCT_1:3;
      hence contradiction by A19,A24,XXREAL_2:def 7;
    end;
    hence thesis by WELLFND1:14;
  end;
end;

Lm3: now
  let n be Element of NAT;
  set pp = product (n --> OrderedNAT);
  per cases;
  suppose n is empty;
    hence pp is non empty & pp is Dickson & pp is quasi_ordered &
    pp is antisymmetric;
  end;
  suppose n is non empty;
    then reconsider n9 = n as non empty Element of NAT;
    set p = (n9 --> OrderedNAT);
    thus product (n --> OrderedNAT) is non empty;
    for i being Element of n9
    holds p.i is Dickson & p.i is quasi_ordered by FUNCOP_1:7;
    hence product (n --> OrderedNAT) is Dickson &
    product (n --> OrderedNAT) is quasi_ordered by Th42;
    product p is antisymmetric;
    hence product (n --> OrderedNAT) is antisymmetric;
  end;
end;

registration :: 4.48 Dickson's Lemma
  let n be Element of NAT;
  cluster product (n --> OrderedNAT) -> non empty;
  coherence;
  cluster product (n --> OrderedNAT) -> Dickson;
  coherence by Lm3;
  cluster product (n --> OrderedNAT) -> quasi_ordered;
  coherence by Lm3;
  cluster product (n --> OrderedNAT) -> antisymmetric;
  coherence by Lm3;
end;

theorem :: Proposition 4.49, in B&W proven without axiom of choice (4.46)
  for M be RelStr st M is Dickson & M is quasi_ordered
  holds [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson
  by Th37;

:: Omitting Exercise 4.50

theorem Th48: :: Lemma 4.51
  for R, S being non empty RelStr st R is Dickson & S is quasi_ordered &
  the InternalRel of R c= the InternalRel of S &
  (the carrier of R) = (the carrier of S) holds S\~ is well_founded
proof
  let R, S be non empty RelStr such that
A1: R is Dickson and
A2: S is quasi_ordered and
A3: the InternalRel of R c= the InternalRel of S and
A4: the carrier of R = the carrier of S;
  S is Dickson by A1,A3,A4,Th28;
  hence thesis by A2,Th33;
end;

theorem :: Lemma 4.52
  for R being non empty RelStr st R is quasi_ordered holds R is Dickson iff
  for S being non empty RelStr
  st S is quasi_ordered & the InternalRel of R c= the InternalRel of S &
  the carrier of R = the carrier of S holds S\~ is well_founded
proof
  let R be non empty RelStr such that
A1: R is quasi_ordered;
A2: R is reflexive by A1,Def3;
A3: R is transitive by A1,Def3;
  set IR = the InternalRel of R, CR = the carrier of R;
  thus R is Dickson implies for S being non empty RelStr st
  S is quasi_ordered & IR c= the InternalRel of S & CR = the carrier of S
  holds S\~ is well_founded by Th48;
  assume
A4: for S being non empty RelStr st S is quasi_ordered &
  IR c= the InternalRel of S & CR = the carrier of S
  holds S\~ is well_founded;
  now
    assume not R is Dickson;
    then not (for N being non empty Subset of R
    holds min-classes N is finite & min-classes N is non empty) by A1,Th32;
    then consider f being sequence of R such that
A5: for i,j being Element of NAT st i < j holds not f.i <= f.j by A1,Th31;
    defpred P[set,set] means
    [$1,$2] in IR or ex i,j being Element of NAT st i < j &
    [$1, f.j] in IR & [f.i, $2] in IR;
    consider QOE being Relation of CR,CR such that
A6: for x,y being set holds [x,y] in QOE iff x in CR & y in CR & P[x,y]
    from RELSET_1:sch 1;
    set S = RelStr(# CR, QOE #);
    now
      let x,y be set such that
A7:   [x,y] in IR;
A8:   x in dom IR by A7,XTUPLE_0:def 12;
      y in rng IR by A7,XTUPLE_0:def 13;
      hence [x,y] in QOE by A6,A7,A8;
    end;
    then
A9: IR c= the InternalRel of S by RELAT_1:def 3;
A10: IR is_reflexive_in CR by A2,ORDERS_2:def 2;
    now
      let x be set such that
A11:  x in CR;
      [x,x] in IR by A10,A11,RELAT_2:def 1;
      hence [x,x] in QOE by A6,A11;
    end;
    then QOE is_reflexive_in CR by RELAT_2:def 1;
    then
A12: S is reflexive by ORDERS_2:def 2;
A13: IR is_transitive_in CR by A3,ORDERS_2:def 3;
    now
      let x,y,z be set such that
A14:  x in CR and
A15:  y in CR and
A16:  z in CR and
A17:  [x,y] in QOE and
A18:  [y,z] in QOE;
      now per cases by A6,A17;
        suppose
A19:      [x,y] in IR;
          now per cases by A6,A18;
            suppose [y,z] in IR;
              then [x,z] in IR by A13,A14,A15,A16,A19,RELAT_2:def 8;
              hence [x,z] in QOE by A6,A14,A16;
            end;
            suppose ex i,j being Element of NAT
              st i<j & [y,f.j] in IR & [f.i, z] in IR;
              then consider i,j being Element of NAT such that
A20:          i < j and
A21:          [y,f.j] in IR and
A22:          [f.i, z] in IR;
              [x,f.j] in IR by A13,A14,A15,A19,A21,RELAT_2:def 8;
              hence [x,z] in QOE by A6,A14,A16,A20,A22;
            end;
          end;
          hence [x,z] in QOE;
        end;
        suppose ex i,j being Element of NAT
          st i < j & [x, f.j] in IR & [f.i, y] in IR;
          then consider i, j being Element of NAT such that
A23:      i < j and
A24:      [x, f.j] in IR and
A25:      [f.i, y] in IR;
          now per cases by A6,A18;
            suppose [y,z] in IR;
              then [f.i, z] in IR by A13,A15,A16,A25,RELAT_2:def 8;
              hence [x,z] in QOE by A6,A14,A16,A23,A24;
            end;
            suppose ex a,b being Element of NAT
              st a<b & [y,f.b] in IR & [f.a,z] in IR;
              then consider a,b being Element of NAT such that
A26:          a < b and
A27:          [y,f.b] in IR and
A28:          [f.a, z] in IR;
              [f.i, f.b] in IR by A13,A15,A25,A27,RELAT_2:def 8;
              then f.i <= f.b by ORDERS_2:def 5;
              then not i < b by A5;
              then a <= i by A26,XXREAL_0:2;
              then a < j by A23,XXREAL_0:2;
              hence [x,z] in QOE by A6,A14,A16,A24,A28;
            end;
          end;
          hence [x,z] in QOE;
        end;
      end;
      hence [x,z] in QOE;
    end;
    then QOE is_transitive_in CR by RELAT_2:def 8;
    then S is transitive by ORDERS_2:def 3;
    then S is quasi_ordered by A12,Def3;
    then
A29: S\~ is well_founded by A4,A9;
    reconsider f9=f as sequence of S\~;
    now
      let n be Nat;
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A30:  n < n+1 by NAT_1:13;
      then not f.n1 <= f.(n1+1) by A5;
      then
A31:  not [f.n, f.(n+1)] in IR by ORDERS_2:def 5;
      hence f9.(n+1) <> f9.n by A10,RELAT_2:def 1;
A32:  [f9.(n+1), f9.(n+1)] in IR by A10,RELAT_2:def 1;
A33:  [f9.n, f9.n] in IR by A10,RELAT_2:def 1;
A34:  now
        assume [f9.n, f9.(n+1)] in QOE;
        then ex i,j being Element of NAT st i < j &
        [f9.n, f.j] in IR & [f.i, f9.(n+1)] in IR by A6,A31;
        then consider l,k being Element of NAT such that
A35:    k < l and
A36:    [f9.n, f.l] in IR and
A37:    [f.k, f9.(n+1)] in IR;
A38:    f.n <= f.l by A36,ORDERS_2:def 5;
A39:    f.k <= f.(n+1) by A37,ORDERS_2:def 5;
A40:    l <= n1 by A5,A38;
A41:    n+1 <= k by A5,A39;
        l < n+1 by A40,NAT_1:13;
        hence contradiction by A35,A41,XXREAL_0:2;
      end;
A42:  [f9.(n1+1),f9.n1] in QOE by A6,A30,A32,A33;
      not [f9.(n+1),f9.n] in QOE~ by A34,RELAT_1:def 7;
      hence [f9.(n+1), f9.n] in the InternalRel of S\~ by A42,XBOOLE_0:def 5;
    end;
    then f9 is descending by WELLFND1:def 6;
    hence contradiction by A29,WELLFND1:14;
  end;
  hence thesis;
end;