:: Kuratowski - Zorn Lemma
::  by Wojciech A. Trybulec and Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2019 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 STRUCT_0, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, ORDERS_1,
      SUBSET_1, XXREAL_0, ARYTM_3, TREES_2, TARSKI, WELLORD1, FUNCT_1,
      ZFMISC_1, ORDERS_2, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
      RELSET_1, PARTFUN1, CARD_1, WELLORD1, DOMAIN_1, STRUCT_0, ORDERS_1;
 constructors RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_1, PRE_TOPC,
      RELSET_1, SETFAM_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, CARD_1,
      RELAT_2;
 requirements BOOLE, SUBSET, NUMERALS;
 definitions RELAT_2, TARSKI, WELLORD1, STRUCT_0, XBOOLE_0, ORDERS_1;
 equalities RELAT_1, WELLORD1, STRUCT_0, ORDERS_1;
 expansions RELAT_2, TARSKI, WELLORD1, XBOOLE_0, ORDERS_1;
 theorems RELAT_1, RELAT_2, TARSKI, WELLORD1, ZFMISC_1, XBOOLE_0, XBOOLE_1,
      PARTFUN1, ORDERS_1, XTUPLE_0;
 schemes XFAMILY;

begin :: Original ORDERS_1

reserve X,Y,x,y for set;

definition
  struct(1-sorted) RelStr (# carrier -> set, InternalRel -> Relation of the
    carrier #);
end;

registration
  let X be non empty set;
  let R be Relation of X;
  cluster RelStr(#X,R#) -> non empty;
  coherence;
end;

definition
  let A be RelStr;

  attr A is total means
  :Def1:
  the InternalRel of A is total;
  attr A is reflexive means
  :Def2:
  the InternalRel of A is_reflexive_in the carrier of A;
  attr A is transitive means
  :Def3:
  the InternalRel of A is_transitive_in the carrier of A;
  attr A is antisymmetric means
  :Def4:
  the InternalRel of A is_antisymmetric_in the carrier of A;
end;

registration
  cluster reflexive transitive antisymmetric strict total 1-element for RelStr;
  existence
  proof
    set R = the Order of {{}};
    take L = RelStr(#{{}},R#);
A1: field R = the carrier of L by ORDERS_1:12;
    hence the InternalRel of L is_reflexive_in the carrier of L by
RELAT_2:def 9;
    thus the InternalRel of L is_transitive_in the carrier of L by A1,
RELAT_2:def 16;
    thus the InternalRel of L is_antisymmetric_in the carrier of L by A1,
RELAT_2:def 12;
    thus L is strict;
    thus the InternalRel of L is total;
   thus the carrier of L is 1-element;
  end;
end;

registration
  cluster reflexive -> total for RelStr;
  coherence
  proof
    let L be RelStr;
    assume L is reflexive;
    then the InternalRel of L is_reflexive_in the carrier of L;
    then dom the InternalRel of L = the carrier of L by ORDERS_1:13;
    hence the InternalRel of L is total by PARTFUN1:def 2;
  end;
end;

definition
  mode Poset is reflexive transitive antisymmetric RelStr;
end;

registration
  let A be total RelStr;
  cluster the InternalRel of A -> total;
  coherence by Def1;
end;

registration
  let A be reflexive RelStr;
  cluster the InternalRel of A -> reflexive;
  coherence
  proof
    set R = the InternalRel of A;
    R is_reflexive_in the carrier of A by Def2;
    then
A1: field R = the carrier of A by ORDERS_1:13;
    the InternalRel of A is_reflexive_in the carrier of A by Def2;
    hence thesis by A1;
  end;
end;

registration
  let A be total antisymmetric RelStr;
  cluster the InternalRel of A -> antisymmetric;
  coherence
  proof
    set R = the InternalRel of A;
    field R = the carrier of A & the InternalRel of A is_antisymmetric_in
    the carrier of A by Def4,ORDERS_1:12;
    hence thesis;
  end;
end;

registration
  let A be total transitive RelStr;
  cluster the InternalRel of A -> transitive;
  coherence
  proof
    set R = the InternalRel of A;
    field R = the carrier of A & the InternalRel of A is_transitive_in the
    carrier of A by Def3,ORDERS_1:12;
    hence thesis;
  end;
end;

registration
  let X be set;
  let O be total reflexive Relation of X;
  cluster RelStr(#X,O#) -> reflexive;
  coherence
  proof
    set A = RelStr(#X,O#);
    field O = X by ORDERS_1:12;
    hence the InternalRel of A is_reflexive_in the carrier of A by
RELAT_2:def 9;
  end;
end;

registration
  let X be set;
  let O be total transitive Relation of X;
  cluster RelStr(#X,O#) -> transitive;
  coherence
  proof
    set A = RelStr(#X,O#);
    field O = X by ORDERS_1:12;
    hence the InternalRel of A is_transitive_in the carrier of A by
RELAT_2:def 16;
  end;
end;

registration
  let X be set;
  let O be total antisymmetric Relation of X;
  cluster RelStr(#X,O#) -> antisymmetric;
  coherence
  proof
    set A = RelStr(#X,O#);
    field O = X by ORDERS_1:12;
    hence the InternalRel of A is_antisymmetric_in the carrier of A by
RELAT_2:def 12;
  end;
end;

reserve A for non empty Poset;
reserve a,a1,a2,a3,b,c for Element of A;
reserve S,T for Subset of A;

Lm1: x in S implies x is Element of A;

definition
  let A be RelStr;
  let a1,a2 be Element of A;

  pred a1 <= a2 means

  [a1,a2] in the InternalRel of A;
end;

notation
  let A be RelStr;
  let a1,a2 be Element of A;
  synonym a2 >= a1 for a1 <= a2;
end;

definition
  let A be RelStr;
  let a1,a2 be Element of A;
  pred a1 < a2 means

  a1 <= a2 & a1 <> a2;
  irreflexivity;
end;

notation
  let A be RelStr;
  let a1,a2 be Element of A;
  synonym a2 > a1 for a1 < a2;
end;

theorem Th1:
  for A being reflexive non empty RelStr, a being Element of A holds a <= a
proof
  let A be reflexive non empty RelStr, a be Element of A;
  the InternalRel of A is_reflexive_in the carrier of A by Def2;
  then [a,a] in the InternalRel of A;
  hence thesis;
end;

definition
  let A be reflexive non empty RelStr;
  let a1,a2 be Element of A;
  redefine pred a1 <= a2;
  reflexivity by Th1;
end;

theorem Th2:
  for A being antisymmetric RelStr, a1,a2 being Element of A st a1
  <= a2 & a2 <= a1 holds a1 = a2
proof
  let A be antisymmetric RelStr, a1,a2 be Element of A;
  assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a1] in the InternalRel of A;
A3: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
  a1 in the carrier of A by A1,ZFMISC_1:87;
  hence thesis by A1,A2,A3;
end;

theorem Th3:
  for A being transitive RelStr, a1,a2,a3 being Element of A holds
  a1 <= a2 & a2 <= a3 implies a1 <= a3
proof
  let A be transitive RelStr, a1,a2,a3 be Element of A;
  assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a3] in the InternalRel of A;
A3: the InternalRel of A is_transitive_in the carrier of A by Def3;
  a1 in the carrier of A by A1,ZFMISC_1:87;
  hence [a1,a3] in the InternalRel of A by A1,A2,A3;
end;

theorem Th4:
  for A being antisymmetric RelStr, a1,a2 being Element of A holds
  not(a1 < a2 & a2 < a1)
by Th2;

theorem Th5:
  for A being transitive antisymmetric RelStr for a1,a2,a3 being
  Element of A holds a1 < a2 & a2 < a3 implies a1 < a3
by Th3,Th4;

theorem Th6:
  for A being antisymmetric RelStr, a1,a2 being Element of A holds
  a1 <= a2 implies not a2 < a1
by Th2;

theorem Th7:
  for A being transitive antisymmetric RelStr for a1,a2,a3 being
  Element of A holds a1 < a2 & a2 <= a3 or a1 <= a2 & a2 < a3 implies a1 < a3
by Th2,Th3;

::
::  Chains.
::

definition
  let A be RelStr;
  let IT be Subset of A;
  attr IT is strongly_connected means
  :Def7:
  the InternalRel of A is_strongly_connected_in IT;
end;

registration
  let A be RelStr;
  cluster empty -> strongly_connected for Subset of A;
  coherence
  proof let S be Subset of A;
    assume S is empty;
    then
A1:  S = {}A;
    let x1,x2 be object;
    thus thesis by A1;
  end;
end;

registration
  let A be RelStr;
  cluster strongly_connected for Subset of A;
  existence
  proof
    take {}A;
    thus thesis;
  end;
end;

definition
  let A be RelStr;
  mode Chain of A is strongly_connected Subset of A;
end;

theorem Th8:
  for A being non empty reflexive RelStr for a being Element of A
  holds {a} is Chain of A
proof
  let A be non empty reflexive RelStr, a be Element of A;
A1: the InternalRel of A is_reflexive_in the carrier of A by Def2;
  {a} is strongly_connected
  proof
    let x1,x2 be object;
    assume x1 in {a} & x2 in {a};
    then x1 = a & x2 = a by TARSKI:def 1;
    hence thesis by A1;
  end;
  hence thesis;
end;

theorem Th9:
  for A being non empty reflexive RelStr, a1,a2 being Element of A
  holds {a1,a2} is Chain of A iff a1 <= a2 or a2 <= a1
proof
  let A be non empty reflexive RelStr, a1,a2 be Element of A;
A1: a2 <= a2;
  thus {a1,a2} is Chain of A implies a1 <= a2 or a2 <= a1
  proof
    assume {a1,a2} is Chain of A;
    then
A2: the InternalRel of A is_strongly_connected_in {a1,a2} by Def7;
    a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
    then
    [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by A2;
    hence thesis;
  end;
  assume
A3: a1 <= a2 or a2 <= a1;
A4: a1 <= a1;
  {a1,a2} is strongly_connected
  proof
    let x,y be object;
    assume
A5: x in {a1,a2} & y in {a1,a2};
    now
      per cases by A5,TARSKI:def 2;
      suppose
        x = a1 & y = a1;
        hence thesis by A4;
      end;
      suppose
        x = a1 & y = a2;
        hence thesis by A3;
      end;
      suppose
        x = a2 & y = a1;
        hence thesis by A3;
      end;
      suppose
        x = a2 & y = a2;
        hence thesis by A1;
      end;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  for A being RelStr, C being Chain of A, S being Subset of A holds S c=
  C implies S is Chain of A
proof
  let A be RelStr, C be Chain of A, S be Subset of A;
  assume
A1: S c= C;
  the InternalRel of A is_strongly_connected_in C by Def7;
  then the InternalRel of A is_strongly_connected_in S by A1;
  hence thesis by Def7;
end;

theorem Th11:
  for A being reflexive RelStr, a1,a2 being Element of A holds (ex
  C being Chain of A st a1 in C & a2 in C) iff a1 <= a2 or a2 <= a1
proof
  let A be reflexive RelStr;
  let a1,a2 be Element of A;
  thus (ex C being Chain of A st a1 in C & a2 in C) implies a1 <= a2 or a2 <=
  a1
  proof
    given C being Chain of A such that
A1: a1 in C & a2 in C;
    the InternalRel of A is_strongly_connected_in C by Def7;
    then
    [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by A1;
    hence thesis;
  end;
  assume
A2: a1 <= a2 or a2 <= a1;
  then
  [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A;
  then reconsider B = A as non empty reflexive RelStr;
  reconsider b1 = a1, b2 = a2 as Element of B;
  reconsider Y = {b1,b2} as Chain of A by A2,Th9;
  take Y;
  thus thesis by TARSKI:def 2;
end;

theorem Th12:
  for A being reflexive antisymmetric RelStr, a1,a2 being Element
of A holds (ex C being Chain of A st a1 in C & a2 in C) iff (a1 < a2 iff not a2
  <= a1)
by Th6,Th11;

theorem Th13:
  for A being RelStr, T being Subset of A holds the InternalRel of
  A well_orders T implies T is Chain of A
by ORDERS_1:7,Def7;

::
::  Upper and lower cones.
::

definition
  let A;
  let S;
  func UpperCone(S) -> Subset of A equals
  {a1 : for a2 st a2 in S holds a2 <
  a1};
  coherence
  proof
    set T = {a1 : for a2 st a2 in S holds a2 < a1};
    T c= the carrier of A
    proof
      let x be object;
      assume x in T;
      then ex a1 st x = a1 & for a2 st a2 in S holds a2 < a1;
      hence thesis;
    end;
    hence thesis;
  end;
end;

definition
  let A;
  let S;
  func LowerCone(S) -> Subset of A equals
  {a1 : for a2 st a2 in S holds a1 <
  a2};
  coherence
  proof
    set T = {a1 : for a2 st a2 in S holds a1 < a2};
    T c= the carrier of A
    proof
      let x be object;
      assume x in T;
      then ex a1 st x = a1 & for a2 st a2 in S holds a1 < a2;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem Th14:
  UpperCone({}(A)) = the carrier of A
proof
  thus UpperCone({}(A)) c= the carrier of A;
  let x be object;
  assume x in the carrier of A;
  then reconsider a = x as Element of A;
  for a2 st a2 in {}(A) holds a2 < a;
  hence thesis;
end;

theorem
  UpperCone([#](A)) = {}
proof
  thus UpperCone([#](A)) c= {}
  proof
    let x be object;
    assume x in UpperCone([#](A));
    then ex a st x = a & for a2 st a2 in [#](A) holds a2 < a;
    hence thesis;
  end;
  thus thesis;
end;

theorem
  LowerCone({}(A)) = the carrier of A
proof
  thus LowerCone({}(A)) c= the carrier of A;
  let x be object;
  assume x in the carrier of A;
  then reconsider a = x as Element of A;
  for a2 st a2 in {}(A) holds a < a2;
  hence thesis;
end;

theorem
  LowerCone([#](A)) = {}
proof
  thus LowerCone([#](A)) c= {}
  proof
    let x be object;
    assume x in LowerCone([#](A));
    then ex a st x = a & for a2 st a2 in [#](A) holds a < a2;
    hence thesis;
  end;
  thus thesis;
end;

theorem Th18:
  a in S implies not a in UpperCone(S)
proof
  assume that
A1: a in S and
A2: a in UpperCone(S);
  ex a1 st a1 = a & for a2 st a2 in S holds a2 < a1 by A2;
  hence thesis by A1;
end;

theorem
  not a in UpperCone{a}
proof
  a in {a} by TARSKI:def 1;
  hence thesis by Th18;
end;

theorem Th20:
  a in S implies not a in LowerCone(S)
proof
  assume that
A1: a in S and
A2: a in LowerCone(S);
  ex a1 st a1 = a & for a2 st a2 in S holds a1 < a2 by A2;
  hence thesis by A1;
end;

theorem Th21:
  not a in LowerCone{a}
proof
  a in {a} by TARSKI:def 1;
  hence thesis by Th20;
end;

theorem
  c < a iff a in UpperCone{c}
proof
  thus c < a implies a in UpperCone{c}
  proof
    assume c < a;
    then for b holds b in {c} implies b < a by TARSKI:def 1;
    hence thesis;
  end;
  assume a in UpperCone{c};
  then
A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a2 < a1;
  c in {c} by TARSKI:def 1;
  hence thesis by A1;
end;

theorem Th23:
  a < c iff a in LowerCone{c}
proof
  thus a < c implies a in LowerCone{c}
  proof
    assume a < c;
    then for b holds b in {c} implies a < b by TARSKI:def 1;
    hence thesis;
  end;
  assume a in LowerCone{c};
  then
A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a1 < a2;
  c in {c} by TARSKI:def 1;
  hence thesis by A1;
end;

::
::  Initial segments.
::

definition
  let A;
  let S;
  let a;
  func InitSegm(S,a) -> Subset of A equals
  LowerCone{a} /\ S;
  correctness;
end;

definition
  let A;
  let S;
  mode Initial_Segm of S -> Subset of A means
    :Def11:
    ex a st a in S & it = InitSegm(S,a) if S <> {} otherwise it = {};
  existence
  proof
    now
      set x = the Element of S;
      assume S <> {};
      then reconsider x as Element of A by Lm1;
      take T = InitSegm(S,x);
      thus S <> {} implies ex a st a in S & T = InitSegm(S,a);
      thus S = {} implies T = {};
    end;
    hence thesis;
  end;
  consistency;
end;

theorem Th24:
  a in InitSegm(S,b) iff a < b & a in S
proof
  a in InitSegm(S,b) iff a in LowerCone{b} & a in S by XBOOLE_0:def 4;
  hence thesis by Th23;
end;

theorem
  InitSegm({}(A),a) = {};

theorem Th26:
  not a in InitSegm(S,a)
proof
  assume not thesis;
  then a in LowerCone{a} by XBOOLE_0:def 4;
  then
A1: ex a1 st a = a1 & for a2 st a2 in {a} holds a1 < a2;
  a in {a} by TARSKI:def 1;
  hence thesis by A1;
end;

theorem
  a1 < a2 implies InitSegm(S,a1) c= InitSegm(S,a2)
proof
  assume
A1: a1 < a2;
  let x be object;
  assume
A2: x in InitSegm(S,a1);
  then x in LowerCone{a1} by XBOOLE_0:def 4;
  then consider a such that
A3: a = x and
A4: for b st b in {a1} holds a < b;
  a1 in {a1} by TARSKI:def 1;
  then a < a1 by A4;
  then a < a2 by A1,Th5;
  then for b holds b in {a2} implies a < b by TARSKI:def 1;
  then
A5: x in LowerCone{a2} by A3;
  x in S by A2,XBOOLE_0:def 4;
  hence thesis by A5,XBOOLE_0:def 4;
end;

theorem Th28:
  S c= T implies InitSegm(S,a) c= InitSegm(T,a)
proof
  assume
A1: S c= T;
  let x be object;
  assume x in InitSegm(S,a);
  then x in S & x in LowerCone{a} by XBOOLE_0:def 4;
  hence thesis by A1,XBOOLE_0:def 4;
end;

theorem Th29:
  for I being Initial_Segm of S holds I c= S
proof
  let I be Initial_Segm of S;
  per cases;
  suppose
    S = {};
    hence thesis by Def11;
  end;
  suppose
    S <> {};
    then ex a st a in S & I = InitSegm(S,a) by Def11;
    hence thesis by XBOOLE_1:17;
  end;
end;

theorem Th30:
  S <> {} iff not S is Initial_Segm of S
proof
  thus S <> {} implies not S is Initial_Segm of S
  proof
    assume S <> {} & S is Initial_Segm of S;
    then consider a such that
A1: a in S & S = InitSegm(S,a) by Def11;
    a in LowerCone{a} by A1,XBOOLE_0:def 4;
    hence thesis by Th21;
  end;
  thus thesis by Def11;
end;

theorem Th31:
  S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S
proof
  assume that
A1: S <> {} and
A2: S is Initial_Segm of T and
A3: T is Initial_Segm of S;
  now
    per cases;
    suppose
      S = {};
      hence thesis by A1;
    end;
    suppose
      T = {};
      hence thesis by A1,A2,Def11;
    end;
    suppose
A4:   S <> {} & T <> {};
      then consider a2 such that
A5:   a2 in T and
A6:   S = InitSegm(T,a2) by A2,Def11;
      consider a1 such that
A7:   a1 in S and
A8:   T = InitSegm(S,a1) by A3,A4,Def11;
      a1 in LowerCone{a2} by A7,A6,XBOOLE_0:def 4;
      then
A9:   ex a st a = a1 & for b st b in {a2} holds a < b;
      a2 in LowerCone{a1} by A8,A5,XBOOLE_0:def 4;
      then
A10:  ex a3 st a3 = a2 & for b st b in {a1} holds a3 < b;
      a1 in {a1} by TARSKI:def 1;
      then
A11:  a2 < a1 by A10;
      a2 in {a2} by TARSKI:def 1;
      then a1 < a2 by A9;
      hence thesis by A11,Th4;
    end;
  end;
  hence thesis;
end;

theorem Th32:
  a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T
proof
  assume that
A1: a1 < a2 and
A2: a1 in S and
A3: a2 in T and
A4: T is Initial_Segm of S;
  consider a such that
  a in S and
A5: T = InitSegm(S,a) by A2,A4,Def11;
  now
    let b;
    assume b in {a};
    then
A6: b = a by TARSKI:def 1;
    a2 in LowerCone{a} by A3,A5,XBOOLE_0:def 4;
    then
A7: ex a3 st a3 = a2 & for c st c in {a} holds a3 < c;
    a in {a} by TARSKI:def 1;
    then a2 < a by A7;
    hence a1 < b by A1,A6,Th5;
  end;
  then a1 in LowerCone{a};
  hence thesis by A2,A5,XBOOLE_0:def 4;
end;

theorem Th33:
  a in S & S is Initial_Segm of T implies InitSegm(S,a) = InitSegm (T,a)
proof
  assume that
A1: a in S and
A2: S is Initial_Segm of T;
A3: S c= T by A2,Th29;
  thus InitSegm(S,a) c= InitSegm(T,a)
  proof
    let x be object;
    assume x in InitSegm(S,a);
    then x in LowerCone{a} & x in S by XBOOLE_0:def 4;
    hence thesis by A3,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A4: x in InitSegm(T,a);
  then
A5: x in LowerCone{a} by XBOOLE_0:def 4;
  then consider a1 such that
A6: x = a1 and
A7: for a2 st a2 in {a} holds a1 < a2;
A8: a1 in T by A4,A6,XBOOLE_0:def 4;
  a in {a} by TARSKI:def 1;
  then a1 < a by A7;
  then x in S by A1,A2,A6,A8,Th32;
  hence thesis by A5,XBOOLE_0:def 4;
end;

theorem
  S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S &
  a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T
proof
  assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1,a2 st a2 in S & a1 < a2 holds a1 in S and
A4: S <> T;
  per cases;
  case
    T <> {};
    set Y = T \ S;
    not T c= S by A1,A4;
    then Y <> {} by XBOOLE_1:37;
    then consider x being object such that
A5: x in Y and
A6: for y being object st y in Y holds [x,y] in the InternalRel of A
by A2,WELLORD1:5
,XBOOLE_1:36;
    reconsider x as Element of A by A5;
    take x;
    thus
A7: x in T by A5,XBOOLE_0:def 5;
    S = LowerCone{x} /\ T
    proof
      thus S c= LowerCone{x} /\ T
      proof
        let y be object;
        assume
A8:     y in S;
        then reconsider a = y as Element of A;
        now
          let a1;
          assume that
A9:       a1 in {x} and
A10:      not a < a1;
A11:      a1 = x by A9,TARSKI:def 1;
          then
A12:      a1 <> a by A5,A8,XBOOLE_0:def 5;
          T is Chain of A by A2,Th13;
          then a1 <= a by A1,A7,A8,A10,A11,Th12;
          then a1 < a by A12;
          then a1 in S by A3,A8;
          hence contradiction by A5,A11,XBOOLE_0:def 5;
        end;
        then y in {a1 : for a2 st a2 in {x} holds a1 < a2};
        hence thesis by A1,A8,XBOOLE_0:def 4;
      end;
      let y be object;
      assume
A13:  y in LowerCone{x} /\ T;
      then y in LowerCone{x} by XBOOLE_0:def 4;
      then consider a such that
A14:  a = y and
A15:  for a2 st a2 in {x} holds a < a2;
A16:  now
        assume y in Y;
        then [x,y] in the InternalRel of A by A6;
        then
A17:    x <= a by A14;
        x in {x} by TARSKI:def 1;
        hence contradiction by A15,A17,Th6;
      end;
      y in T by A13,XBOOLE_0:def 4;
      hence thesis by A16,XBOOLE_0:def 5;
    end;
    hence thesis;
  end;
  case
    T = {};
    hence thesis by A1;
  end;
end;

theorem Th35:
  S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2
in S & a1 in T & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T
proof
  assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1,a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S and
A4: S <> T;
  per cases;
  case
    T <> {};
    set Y = T \ S;
    not T c= S by A1,A4;
    then Y <> {} by XBOOLE_1:37;
    then consider x being object such that
A5: x in Y and
A6: for y being object st y in Y holds [x,y] in the InternalRel of A
by A2,WELLORD1:5
,XBOOLE_1:36;
    reconsider x as Element of A by A5;
    take x;
    thus
A7: x in T by A5,XBOOLE_0:def 5;
    S = LowerCone{x} /\ T
    proof
      thus S c= LowerCone{x} /\ T
      proof
        let y be object;
        assume
A8:     y in S;
        then reconsider a = y as Element of A;
        now
          let a1;
          assume that
A9:       a1 in {x} and
A10:      not a < a1;
A11:      a1 = x by A9,TARSKI:def 1;
          then
A12:      a1 <> a by A5,A8,XBOOLE_0:def 5;
          T is Chain of A by A2,Th13;
          then a1 <= a by A1,A7,A8,A10,A11,Th12;
          then a1 < a by A12;
          then a1 in S by A3,A7,A8,A11;
          hence contradiction by A5,A11,XBOOLE_0:def 5;
        end;
        then y in {a1 : for a2 st a2 in {x} holds a1 < a2};
        hence thesis by A1,A8,XBOOLE_0:def 4;
      end;
      let y be object;
      assume
A13:  y in LowerCone{x} /\ T;
      then y in LowerCone{x} by XBOOLE_0:def 4;
      then consider a such that
A14:  a = y and
A15:  for a2 st a2 in {x} holds a < a2;
A16:  now
        assume y in Y;
        then [x,y] in the InternalRel of A by A6;
        then
A17:    x <= a by A14;
        x in {x} by TARSKI:def 1;
        hence contradiction by A15,A17,Th6;
      end;
      y in T by A13,XBOOLE_0:def 4;
      hence thesis by A16,XBOOLE_0:def 5;
    end;
    hence thesis;
  end;
  case
    T = {};
    hence thesis by A1;
  end;
end;

::
::  Chains of choice function of BOOL of partially ordered sets.
::

reserve f for Choice_Function of BOOL(the carrier of A);

definition
  let A;
  let f;
  mode Chain of f -> Chain of A means
    :Def12:
    it <> {} & the InternalRel of A
    well_orders it & for a st a in it holds f.UpperCone(InitSegm(it,a)) = a;
  existence
  proof
    set AC = the carrier of A;
    AC in BOOL AC & not {} in BOOL AC by ORDERS_1:1,2;
    then reconsider aa = f.AC as Element of A by ORDERS_1:89;
    reconsider X = {aa} as Chain of A by Th8;
    take X;
    thus X <> {};
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
    the InternalRel of A is_reflexive_in the carrier of A & the
    InternalRel of A is_transitive_in the carrier of A by Def2,Def3;
    hence the InternalRel of A is_reflexive_in X & the InternalRel of A
    is_transitive_in X & the InternalRel of A is_antisymmetric_in X by A1;
    the InternalRel of A is_strongly_connected_in X by Def7;
    hence the InternalRel of A is_connected_in X;
    thus the InternalRel of A is_well_founded_in X
    proof
      reconsider x = aa as set;
      let Y;
      assume that
A2:   Y c= X and
A3:   Y <> {};
      take x;
      Y = X by A2,A3,ZFMISC_1:33;
      hence x in Y by TARSKI:def 1;
      thus (the InternalRel of A)-Seg(x) /\ Y c= {}
      proof
        let y be object;
        assume
A4:     y in (the InternalRel of A)-Seg(x) /\ Y;
        then y in Y by XBOOLE_0:def 4;
        then
A5:     y = aa by A2,TARSKI:def 1;
        y in (the InternalRel of A)-Seg(x) by A4,XBOOLE_0:def 4;
        hence thesis by A5,WELLORD1:1;
      end;
      thus thesis;
    end;
    let a;
    assume a in X;
    then
A6: a = aa by TARSKI:def 1;
    LowerCone{a} /\ X c= {}(A)
    proof
      let x be object;
      assume
A7:   x in LowerCone{a} /\ X;
      then x in LowerCone{a} by XBOOLE_0:def 4;
      then
A8:   ex a1 st x = a1 & for a2 st a2 in {a} holds a1 < a2;
      x in X by A7,XBOOLE_0:def 4;
      hence thesis by A6,A8;
    end;
    then LowerCone{a} /\ X = {}(A);
    hence thesis by A6,Th14;
  end;
end;

reserve fC,fC1,fC2 for Chain of f;

theorem Th36:
  {f.(the carrier of A)} is Chain of f
proof
  set AC = the carrier of A;
  AC in BOOL AC & not {} in BOOL AC by ORDERS_1:1,2;
  then reconsider aa = f.AC as Element of A by ORDERS_1:89;
  reconsider X = {aa} as Chain of A by Th8;
A1: the InternalRel of A is_well_founded_in X
  proof
    reconsider x = aa as set;
    let Y;
    assume that
A2: Y c= X and
A3: Y <> {};
    take x;
    Y = X by A2,A3,ZFMISC_1:33;
    hence x in Y by TARSKI:def 1;
    thus (the InternalRel of A)-Seg(x) /\ Y c= {}
    proof
      let y be object;
      assume
A4:   y in (the InternalRel of A)-Seg(x) /\ Y;
      then y in Y by XBOOLE_0:def 4;
      then
A5:   y = aa by A2,TARSKI:def 1;
      y in (the InternalRel of A)-Seg(x) by A4,XBOOLE_0:def 4;
      hence thesis by A5,WELLORD1:1;
    end;
    thus thesis;
  end;
A6: for a st a in X holds f.UpperCone(InitSegm(X,a)) = a
  proof
    let a;
    assume a in X;
    then
A7: a = aa by TARSKI:def 1;
    LowerCone{a} /\ X c= {}(A)
    proof
      let x be object;
      assume
A8:   x in LowerCone{a} /\ X;
      then x in LowerCone{a} by XBOOLE_0:def 4;
      then
A9:   ex a1 st x = a1 & for a2 st a2 in {a} holds a1 < a2;
      x in X by A8,XBOOLE_0:def 4;
      hence thesis by A7,A9;
    end;
    then LowerCone{a} /\ X = {}(A);
    hence thesis by A7,Th14;
  end;
  the InternalRel of A is_strongly_connected_in X by Def7;
  then
A10: the InternalRel of A is_connected_in X;
  the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
  then
A11: the InternalRel of A is_antisymmetric_in X;
  the InternalRel of A is_transitive_in the carrier of A by Def3;
  then
A12: the InternalRel of A is_transitive_in X;
  the InternalRel of A is_reflexive_in the carrier of A by Def2;
  then the InternalRel of A is_reflexive_in X;
  then the InternalRel of A well_orders X by A12,A11,A10,A1;
  hence thesis by A6,Def12;
end;

theorem Th37:
  f.(the carrier of A) in fC
proof
  the InternalRel of A well_orders fC & fC <> {} by Def12;
  then consider x being object such that
A1: x in fC and
A2: for y being object st y in fC holds [x,y] in the InternalRel of A
by WELLORD1:5;
  reconsider x as Element of A by A1;
A3: now
    set y = the Element of LowerCone{x} /\ fC;
    assume
A4: LowerCone{x} /\ fC <> {}(A);
    then reconsider a = y as Element of A by Lm1;
    a in LowerCone{x} by A4,XBOOLE_0:def 4;
    then
A5: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2;
    y in fC by A4,XBOOLE_0:def 4;
    then [x,y] in the InternalRel of A by A2;
    then
A6: x <= a;
    x in {x} by TARSKI:def 1;
    hence contradiction by A6,A5,Th6;
  end;
  LowerCone{x} /\ fC = InitSegm(fC,x);
  then f.UpperCone(LowerCone{x} /\ fC) = x by A1,Def12;
  hence thesis by A1,A3,Th14;
end;

theorem Th38:
  a in fC & b = f.(the carrier of A) implies b <= a
proof
  assume that
A1: a in fC and
A2: b = f.(the carrier of A);
  the InternalRel of A well_orders fC & fC <> {} by Def12;
  then consider x being object such that
A3: x in fC and
A4: for y being object st y in fC holds [x,y] in the InternalRel of A
by WELLORD1:5;
  reconsider x as Element of A by A3;
A5: now
    set y = the Element of LowerCone{x} /\ fC;
    assume
A6: LowerCone{x} /\ fC <> {}(A);
    then reconsider a = y as Element of A by Lm1;
    a in LowerCone{x} by A6,XBOOLE_0:def 4;
    then
A7: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2;
    y in fC by A6,XBOOLE_0:def 4;
    then [x,y] in the InternalRel of A by A4;
    then
A8: x <= a;
    x in {x} by TARSKI:def 1;
    hence contradiction by A8,A7,Th6;
  end;
  LowerCone{x} /\ fC = InitSegm(fC,x);
  then f.UpperCone(LowerCone{x} /\ fC) = x by A3,Def12;
  then
A9: f.(the carrier of A) = x by A5,Th14;
  [x,a] in the InternalRel of A by A1,A4;
  hence thesis by A2,A9;
end;

theorem
  a = f.(the carrier of A) implies InitSegm(fC,a) = {}
proof
  set x = the Element of LowerCone{a} /\ fC;
  assume
A1: a = f.(the carrier of A);
  then
A2: a in fC by Th37;
  assume
A3: InitSegm(fC,a) <> {};
  then reconsider b = x as Element of A by Lm1;
  x in LowerCone{a} by A3,XBOOLE_0:def 4;
  then
A4: ex a1 st a1 = b & for a2 st a2 in {a} holds a1 < a2;
  a in {a} by TARSKI:def 1;
  then
A5: b < a by A4;
A6: x in fC by A3,XBOOLE_0:def 4;
  then a <= b by A1,Th38;
  hence contradiction by A2,A6,A5,Th12;
end;

theorem
  fC1 meets fC2
proof
  f.(the carrier of A) in fC1 & f.(the carrier of A) in fC2 by Th37;
  hence thesis by XBOOLE_0:3;
end;

theorem Th41:
  fC1 <> fC2 implies (fC1 is Initial_Segm of fC2 iff not fC2 is
  Initial_Segm of fC1)
proof
  assume
A1: fC1 <> fC2;
  set N = {a : a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a)};
A2: N c= fC1
  proof
    let x be object;
    assume x in N;
    then
    ex a st a = x & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a);
    hence thesis by XBOOLE_0:def 4;
  end;
  then reconsider N as Subset of A by XBOOLE_1:1;
A3: N c= fC2
  proof
    let x be object;
    assume x in N;
    then ex a st a = x & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a);
    hence thesis by XBOOLE_0:def 4;
  end;
A4: now
    let a1,a2;
    assume that
A5: a2 in N and
A6: a1 in fC1 and
A7: a1 < a2;
A8: ex a st a = a2 & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a) by A5;
A9: InitSegm(fC1,a1) = InitSegm(fC2,a1)
    proof
      thus InitSegm(fC1,a1) c= InitSegm(fC2,a1)
      proof
        let x be object;
        assume
A10:    x in InitSegm(fC1,a1);
        then reconsider b = x as Element of A;
A11:    b in fC1 by A10,Th24;
A12:    b < a1 by A10,Th24;
        then b < a2 by A7,Th5;
        then b in InitSegm(fC1,a2) by A11,Th24;
        then b in fC2 by A8,Th24;
        hence thesis by A12,Th24;
      end;
      let x be object;
      assume
A13:  x in InitSegm(fC2,a1);
      then reconsider b = x as Element of A;
A14:  b in fC2 by A13,Th24;
A15:  b < a1 by A13,Th24;
      then b < a2 by A7,Th5;
      then b in InitSegm(fC2,a2) by A14,Th24;
      then b in fC1 by A8,Th24;
      hence thesis by A15,Th24;
    end;
    a1 in InitSegm(fC2,a2) by A6,A7,A8,Th24;
    then a1 in fC2 by XBOOLE_0:def 4;
    then a1 in fC1 /\ fC2 by A6,XBOOLE_0:def 4;
    hence a1 in N by A9;
  end;
A16: now
    let a1,a2;
    assume that
A17: a2 in N and
A18: a1 in fC2 and
A19: a1 < a2;
A20: ex a st a = a2 & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a)
    by A17;
A21: InitSegm(fC1,a1) = InitSegm(fC2,a1)
    proof
      thus InitSegm(fC1,a1) c= InitSegm(fC2,a1)
      proof
        let x be object;
        assume
A22:    x in InitSegm(fC1,a1);
        then reconsider b = x as Element of A;
A23:    b in fC1 by A22,Th24;
A24:    b < a1 by A22,Th24;
        then b < a2 by A19,Th5;
        then b in InitSegm(fC1,a2) by A23,Th24;
        then b in fC2 by A20,Th24;
        hence thesis by A24,Th24;
      end;
      let x be object;
      assume
A25:  x in InitSegm(fC2,a1);
      then reconsider b = x as Element of A;
A26:  b in fC2 by A25,Th24;
A27:  b < a1 by A25,Th24;
      then b < a2 by A19,Th5;
      then b in InitSegm(fC2,a2) by A26,Th24;
      then b in fC1 by A20,Th24;
      hence thesis by A27,Th24;
    end;
    a1 in InitSegm(fC1,a2) by A18,A19,A20,Th24;
    then a1 in fC1 by XBOOLE_0:def 4;
    then a1 in fC1 /\ fC2 by A18,XBOOLE_0:def 4;
    hence a1 in N by A21;
  end;
A28: the InternalRel of A well_orders fC1 & the InternalRel of A well_orders
  fC2 by Def12;
  now
    per cases by A2,A4,A28,A3,A16,Th35;
    suppose
A29:  N is Initial_Segm of fC1 & N = fC2;
      fC1 <> {} by Def12;
      hence thesis by A29,Th31;
    end;
    suppose
A30:  N is Initial_Segm of fC2 & N = fC1;
      fC2 <> {} by Def12;
      hence thesis by A30,Th31;
    end;
    suppose
      N = fC1 & N = fC2;
      hence thesis by A1;
    end;
    suppose
A31:  N is Initial_Segm of fC1 & N is Initial_Segm of fC2;
      fC2 <> {} by Def12;
      then consider b such that
A32:  b in fC2 and
A33:  N = InitSegm(fC2,b) by A31,Def11;
      fC1 <> {} by Def12;
      then consider a such that
A34:  a in fC1 and
A35:  N = InitSegm(fC1,a) by A31,Def11;
A36:  a = f.UpperCone(InitSegm(fC2,b)) by A34,A35,A33,Def12
        .= b by A32,Def12;
      then a in fC1 /\ fC2 by A34,A32,XBOOLE_0:def 4;
      then a in N by A35,A33,A36;
      hence thesis by A35,Th26;
    end;
  end;
  hence thesis;
end;

theorem Th42:
  fC1 c< fC2 iff fC1 is Initial_Segm of fC2
proof
  thus fC1 c< fC2 implies fC1 is Initial_Segm of fC2
  proof
    assume
A1: fC1 c< fC2;
    now
      assume
A2:   fC2 is Initial_Segm of fC1;
      fC1 <> {} by Def12;
      then ex a st a in fC1 & fC2 = InitSegm(fC1,a) by A2,Def11;
      then fC2 c= fC1 by XBOOLE_1:17;
      hence contradiction by A1,XBOOLE_0:def 8;
    end;
    hence thesis by A1,Th41;
  end;
  assume
A3: fC1 is Initial_Segm of fC2;
A4: fC2 <> {} by Def12;
  then ex a st a in fC2 & fC1 = InitSegm(fC2,a) by A3,Def11;
  then
A5: fC1 c= fC2 by XBOOLE_1:17;
  fC1 <> fC2 by A3,A4,Th30;
  hence thesis by A5;
end;

definition
  let A;
  let f;
  func Chains f -> set means
  :Def13:
  x in it iff x is Chain of f;
  existence
  proof
    defpred P[set] means $1 is Chain of f;
    consider X such that
A1: for x holds x in X iff x in bool(the carrier of A) & P[x] from
    XFAMILY:sch 1;
    take X;
    let x;
    thus x in X implies x is Chain of f by A1;
    assume x is Chain of f;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let D1,D2 be set;
    assume
A2: for x holds x in D1 iff x is Chain of f;
    assume
A3: for x holds x in D2 iff x is Chain of f;
    thus D1 c= D2
    proof
      let x be object;
      assume x in D1;
      then x is Chain of f by A2;
      hence thesis by A3;
    end;
    let x be object;
    assume x in D2;
    then x is Chain of f by A3;
    hence thesis by A2;
  end;
end;

registration
  let A;
  let f;
  cluster Chains f -> non empty;
  coherence
  proof
    set x = the Chain of f;
    x in Chains f by Def13;
    hence thesis;
  end;
end;

Lm2: union(Chains(f)) is Subset of A
proof
  now
    let X;
    assume X in Chains(f);
    then X is Chain of f by Def13;
    hence X c= the carrier of A;
  end;
  hence thesis by ZFMISC_1:76;
end;

Lm3: union(Chains(f)) is Chain of A
proof
  reconsider C = union(Chains(f)) as Subset of A by Lm2;
  the InternalRel of A is_strongly_connected_in C
  proof
    let x,y be object;
    assume that
A1: x in C and
A2: y in C;
    consider X such that
A3: x in X and
A4: X in Chains(f) by A1,TARSKI:def 4;
    consider Y such that
A5: y in Y and
A6: Y in Chains(f) by A2,TARSKI:def 4;
    reconsider X,Y as Chain of f by A4,A6,Def13;
A7: the InternalRel of A is_strongly_connected_in X by Def7;
A8: the InternalRel of A is_strongly_connected_in Y by Def7;
    now
      per cases;
      suppose
        X = Y;
        hence thesis by A3,A5,A7;
      end;
      suppose
A9:     X <> Y;
        now
          per cases by A9,Th41;
          suppose
            X is Initial_Segm of Y;
            then X c< Y by Th42;
            then X c= Y;
            hence thesis by A3,A5,A8;
          end;
          suppose
            Y is Initial_Segm of X;
            then Y c< X by Th42;
            then Y c= X;
            hence thesis by A3,A5,A7;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  hence thesis by Def7;
end;

theorem Th43:
  union(Chains(f)) <> {}
proof
  {f.(the carrier of A)} is Chain of f by Th36;
  then {f.(the carrier of A)} in Chains(f) by Def13;
  hence thesis by ORDERS_1:6;
end;

theorem Th44:
  fC <> union(Chains(f)) & S = union(Chains(f)) implies fC is Initial_Segm of S
proof
  assume that
A1: fC <> union(Chains(f)) and
A2: S = union(Chains(f));
  set x = the Element of S \ fC;
  fC in Chains(f) by Def13;
  then fC c= union(Chains(f)) by ZFMISC_1:74;
  then not union(Chains(f)) c= fC by A1;
  then
A3: S \ fC <> {} by A2,XBOOLE_1:37;
  then
A4: not x in fC by XBOOLE_0:def 5;
  x in S by A3,XBOOLE_0:def 5;
  then consider X such that
A5: x in X and
A6: X in Chains(f) by A2,TARSKI:def 4;
  reconsider X as Chain of f by A6,Def13;
  not X c= fC by A3,A5,XBOOLE_0:def 5;
  then not X c< fC;
  then not X is Initial_Segm of fC by Th42;
  then fC is Initial_Segm of X by A5,A4,Th41;
  then consider a such that
A7: a in X and
A8: fC = InitSegm(X,a) by A5,Def11;
A9: X c= S by A2,A6,ZFMISC_1:74;
  InitSegm(S,a) = InitSegm(X,a)
  proof
    thus InitSegm(S,a) c= InitSegm(X,a)
    proof
      let x be object;
      assume
A10:  x in InitSegm(S,a);
      then
A11:  x in LowerCone{a} by XBOOLE_0:def 4;
      then consider b such that
A12:  b = x and
A13:  for a2 st a2 in {a} holds b < a2;
      b in S by A10,A12,XBOOLE_0:def 4;
      then consider Y such that
A14:  b in Y and
A15:  Y in Chains(f) by A2,TARSKI:def 4;
      reconsider Y as Chain of f by A15,Def13;
      a in {a} by TARSKI:def 1;
      then
A16:  b < a by A13;
      now
        per cases;
        suppose
          X = Y;
          hence thesis by A11,A12,A14,XBOOLE_0:def 4;
        end;
        suppose
A17:      X <> Y;
          now
            per cases by A17,Th41;
            suppose
              X is Initial_Segm of Y;
              then x in X by A7,A12,A16,A14,Th32;
              hence thesis by A11,XBOOLE_0:def 4;
            end;
            suppose
              Y is Initial_Segm of X;
              then Y c< X by Th42;
              then Y c= X;
              hence thesis by A11,A12,A14,XBOOLE_0:def 4;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    let x be object;
    assume x in InitSegm(X,a);
    then x in LowerCone{a} & x in X by XBOOLE_0:def 4;
    hence thesis by A9,XBOOLE_0:def 4;
  end;
  hence thesis by A7,A8,A9,Def11;
end;

theorem Th45:
  union(Chains(f)) is Chain of f
proof
  reconsider C = union(Chains(f)) as Chain of A by Lm3;
A1: now
    let a;
    assume a in C;
    then consider X such that
A2: a in X and
A3: X in Chains(f) by TARSKI:def 4;
    reconsider X as Chain of f by A3,Def13;
    now
        InitSegm(C,a) = InitSegm(X,a) by A2,Th33,Th44;
        hence f.UpperCone(InitSegm(C,a)) = a by A2,Def12;
    end;
    hence f.UpperCone(InitSegm(C,a)) = a;
  end;
A4: the InternalRel of A well_orders C
  proof
A5: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
    the InternalRel of A is_reflexive_in the carrier of A & the
    InternalRel of A is_transitive_in the carrier of A by Def2,Def3;
    hence the InternalRel of A is_reflexive_in C & the InternalRel of A
    is_transitive_in C & the InternalRel of A is_antisymmetric_in C by A5;
    the InternalRel of A is_strongly_connected_in C by Def7;
    hence the InternalRel of A is_connected_in C;
    let Y;
    set x = the Element of Y;
    assume that
A6: Y c= C and
A7: Y <> {};
    x in C by A6,A7;
    then consider X such that
A8: x in X and
A9: X in Chains(f) by TARSKI:def 4;
    reconsider X as Chain of f by A9,Def13;
A10: the InternalRel of A well_orders X by Def12;
    X /\ Y <> {} by A7,A8,XBOOLE_0:def 4;
    then consider a being object such that
A11: a in X /\ Y and
A12: for x being object st x in X /\ Y holds [a,x] in the InternalRel of A
by A10,WELLORD1:5
,XBOOLE_1:17;
    take a;
    thus a in Y by A11,XBOOLE_0:def 4;
    reconsider aa = a as Element of A by A11;
    thus (the InternalRel of A)-Seg(a) /\ Y c= {}
    proof
      let y be object;
      assume
A13:  y in (the InternalRel of A)-Seg(a) /\ Y;
      then
A14:  y in Y by XBOOLE_0:def 4;
      then y in C by A6;
      then reconsider b = y as Element of A;
A15:  y in (the InternalRel of A)-Seg(a) by A13,XBOOLE_0:def 4;
      then
A16:  y <> a by WELLORD1:1;
      [y,a] in the InternalRel of A by A15,WELLORD1:1;
      then
A17:  b <= aa;
      now
        per cases;
        suppose
A18:      X <> C;
          a in X & b < aa by A11,A16,A17,XBOOLE_0:def 4;
          hence y in X by A6,A14,A18,Th32,Th44;
        end;
        suppose
          X = C;
          hence y in X by A6,A14;
        end;
      end;
      then y in X /\ Y by A14,XBOOLE_0:def 4;
      then [a,y] in the InternalRel of A by A12;
      then aa <= b;
      hence thesis by A16,A17,Th2;
    end;
    thus thesis;
  end;
  C <> {} by Th43;
  hence thesis by A4,A1,Def12;
end;

begin :: From original ORDERS_2

reserve R for Relation,
  A for non empty Poset,
  C for Chain of A,
  S for Subset of A,
  a,a1,a2,b,c1,c2 for Element of A;

::
::  Orders.
::

theorem Th46:
  field((the InternalRel of A) |_2 S) = S
proof
  set P = (the InternalRel of A) |_2 S;
  thus field P c= S by WELLORD1:13;
  thus S c= field P
  proof
    let x be object;
    assume
A1: x in S;
    then
A2: [x,x] in [:S,S:] by ZFMISC_1:87;
    the InternalRel of A is_reflexive_in the carrier of A by Def2;
    then [x,x] in the InternalRel of A by A1;
    then [x,x] in P by A2,XBOOLE_0:def 4;
    then x in dom P by XTUPLE_0:def 12;
    hence thesis by XBOOLE_0:def 3;
  end;
end;

theorem
  (the InternalRel of A) |_2 S is being_linear-order implies S is Chain of A
proof
  assume (the InternalRel of A) |_2 S is being_linear-order;
  then
A1: (the InternalRel of A) |_2 S is connected;
  field((the InternalRel of A) |_2 S) = S by Th46;
  then
A2: (the InternalRel of A) |_2 S is_connected_in S by A1;
  S is strongly_connected
  proof
    let x,y be object;
    assume
A3: x in S & y in S;
    then reconsider a = x, b = y as Element of A;
    now
      per cases;
      suppose
        x = y;
        then a <= b;
        hence thesis;
      end;
      suppose
        x <> y;
        then [x,y] in (the InternalRel of A) |_2 S or [y,x] in (the
        InternalRel of A) |_2 S by A2,A3;
        hence thesis by XBOOLE_0:def 4;
      end;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  (the InternalRel of A) |_2 C is being_linear-order
proof
  set P = (the InternalRel of A) |_2 C;
A1: P is_connected_in C
  proof
    let x,y be object;
    assume
A2: x in C & y in C;
    then
A3: [x,y] in [:C,C:] & [y,x] in [:C,C:] by ZFMISC_1:87;
    the InternalRel of A is_strongly_connected_in C by Def7;
    then
    [x,y] in the InternalRel of A or [y,x] in the InternalRel of A by A2;
    hence thesis by A3,XBOOLE_0:def 4;
  end;
  the InternalRel of A is being_partial-order;
  then P is being_partial-order by ORDERS_1:26;
  hence P is reflexive & P is transitive & P is antisymmetric;
  C = field P by Th46;
  hence thesis by A1;
end;

theorem
  the InternalRel of A linearly_orders S implies S is Chain of A
by ORDERS_1:7,Def7;

theorem
  the InternalRel of A linearly_orders C
proof
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
  the InternalRel of A is_reflexive_in the carrier of A & the InternalRel
  of A is_transitive_in the carrier of A by Def2,Def3;
  hence the InternalRel of A is_reflexive_in C & the InternalRel of A
  is_transitive_in C & the InternalRel of A is_antisymmetric_in C by A1;
  the InternalRel of A is_strongly_connected_in C by Def7;
  hence thesis;
end;

theorem
  a is_minimal_in the InternalRel of A iff for b holds not b < a
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
  thus a is_minimal_in the InternalRel of A implies for b holds not b < a
  proof
    assume
A2: a is_minimal_in the InternalRel of A;
    let b;
    a = b or not [b,a] in the InternalRel of A by A1,A2;
    then a = b or not b <= a;
    hence thesis;
  end;
  assume
A3: for b holds not b < a;
  thus a in field(the InternalRel of A) by A1;
  let y;
  assume that
A4: y in field(the InternalRel of A) and
A5: y <> a and
A6: [y,a] in the InternalRel of A;
  reconsider b = y as Element of A by A4,ORDERS_1:15;
  b <= a by A6;
  then b < a by A5;
  hence thesis by A3;
end;

theorem
  a is_maximal_in the InternalRel of A iff for b holds not a < b
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
  thus a is_maximal_in the InternalRel of A implies for b holds not a < b
  proof
    assume
A2: a is_maximal_in the InternalRel of A;
    let b;
    a = b or not [a,b] in the InternalRel of A by A1,A2;
    then a = b or not a <= b;
    hence thesis;
  end;
  assume
A3: for b holds not a < b;
  thus a in field(the InternalRel of A) by A1;
  let y;
  assume that
A4: y in field(the InternalRel of A) and
A5: y <> a and
A6: [a,y] in the InternalRel of A;
  reconsider b = y as Element of A by A4,ORDERS_1:15;
  a <= b by A6;
  then a < b by A5;
  hence thesis by A3;
end;

theorem
  a is_superior_of the InternalRel of A iff for b st a <> b holds b < a
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
  thus a is_superior_of the InternalRel of A implies for b st a <> b holds b <
  a
  proof
    assume
A2: a is_superior_of the InternalRel of A;
    let b;
    assume
A3: a <> b;
    then [b,a] in the InternalRel of A by A1,A2;
    then b <= a;
    hence thesis by A3;
  end;
  assume
A4: for b st a <> b holds b < a;
  thus a in field(the InternalRel of A) by A1;
  let y;
  assume y in field(the InternalRel of A);
  then reconsider b = y as Element of A by ORDERS_1:15;
  assume y <> a;
  then b < a by A4;
  then b <= a;
  hence thesis;
end;

theorem
  a is_inferior_of the InternalRel of A iff for b st a <> b holds a < b
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
  thus a is_inferior_of the InternalRel of A implies for b st a <> b holds a <
  b
  proof
    assume
A2: a is_inferior_of the InternalRel of A;
    let b;
    assume
A3: a <> b;
    then [a,b] in the InternalRel of A by A1,A2;
    then a <= b;
    hence thesis by A3;
  end;
  assume
A4: for b st a <> b holds a < b;
  thus a in field(the InternalRel of A) by A1;
  let y;
  assume y in field(the InternalRel of A);
  then reconsider b = y as Element of A by ORDERS_1:15;
  assume y <> a;
  then a < b by A4;
  then a <= b;
  hence thesis;
end;

Lm4: R well_orders X & Y c= X implies R well_orders Y
proof
  assume that
A1: R well_orders X and
A2: Y c= X;
A3: R is_antisymmetric_in X & R is_connected_in X by A1;
A4: R is_well_founded_in X by A1;
  R is_reflexive_in X & R is_transitive_in X by A1;
  hence R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y &
  R is_connected_in Y by A2,A3;
  let Z be set;
  assume that
A5: Z c= Y and
A6: Z <> {};
  Z c= X by A2,A5;
  hence thesis by A6,A4;
end;

::
::  Kuratowski - Zorn Lemma.
::

theorem Th55:
  (for C ex a st for b st b in C holds b <= a) implies ex a st
  for b holds not a < b
proof
  set f = the Choice_Function of BOOL(the carrier of A);
  reconsider F = union(Chains(f)) as Chain of f by Th45;
  assume for C ex a st for b st b in C holds b <= a;
  then consider a such that
A1: for b st b in F holds b <= a;
  take a;
  let b;
  assume
A2: a < b;
  now
    let a1;
    assume a1 in F;
    then a1 <= a by A1;
    hence a1 < b by A2,Th7;
  end;
  then b in {a1 : for a2 st a2 in F holds a2 < a1};
  then not UpperCone(F) in {{}} by TARSKI:def 1;
  then
A3: UpperCone(F) in BOOL(the carrier of A) by XBOOLE_0:def 5;
  not {} in BOOL(the carrier of A) by ORDERS_1:1;
  then
A4: f.UpperCone(F) in UpperCone(F) by A3,ORDERS_1:89;
  then reconsider c = f.UpperCone(F) as Element of A;
  reconsider Z = F \/ {c} as Subset of A;
A5: ex c11 being Element of A st c11 = c & for a2 st a2 in F holds a2 < c11
  by A4;
A6: the InternalRel of A is_connected_in Z
  proof
    let x,y be object;
    assume
A7: x in Z & y in Z;
    then reconsider x1 = x, y1 = y as Element of A;
    now
      per cases by A7,XBOOLE_0:def 3;
      suppose
        x1 in F & y1 in F;
        then x1 <= y1 or y1 <= x1 by Th11;
        hence thesis;
      end;
      suppose
A8:     x1 in F & y1 in {c};
        then y1 = c by TARSKI:def 1;
        then x1 < y1 by A5,A8;
        then x1 <= y1;
        hence thesis;
      end;
      suppose
A9:     x1 in {c} & y1 in F;
        then x1 = c by TARSKI:def 1;
        then y1 < x1 by A5,A9;
        then y1 <= x1;
        hence thesis;
      end;
      suppose
A10:    x1 in {c} & y1 in {c};
        then x1 = c by TARSKI:def 1;
        hence thesis by A10,TARSKI:def 1;
      end;
    end;
    hence thesis;
  end;
A11: now
    let a1;
    assume
A12: a1 in Z;
    now
      per cases;
      suppose
A13:    a1 = c;
        InitSegm(Z,c) = F
        proof
          thus InitSegm(Z,c) c= F
          proof
            let x be object;
            assume that
A14:        x in InitSegm(Z,c) and
A15:        not x in F;
            x in Z by A14,XBOOLE_0:def 4;
            then x in {c} by A15,XBOOLE_0:def 3;
            then
A16:        x = c by TARSKI:def 1;
            x in LowerCone{c} by A14,XBOOLE_0:def 4;
            hence contradiction by A16,Th21;
          end;
          let x be object;
          assume
A17:      x in F;
          then reconsider y = x as Element of A;
          y < c by A5,A17;
          then
A18:      x in LowerCone{c} by Th23;
          x in Z by A17,XBOOLE_0:def 3;
          hence thesis by A18,XBOOLE_0:def 4;
        end;
        hence f.UpperCone(InitSegm(Z,a1)) = a1 by A13;
      end;
      suppose
        a1 <> c;
        then not a1 in {c} by TARSKI:def 1;
        then
A19:    a1 in F by A12,XBOOLE_0:def 3;
A20:    InitSegm(Z,a1) c= InitSegm(F,a1)
        proof
          let x be object;
          assume
A21:      x in InitSegm(Z,a1);
          then
A22:      x in LowerCone{a1} by XBOOLE_0:def 4;
          now
            assume
A23:        not x in F;
            x in Z by A21,XBOOLE_0:def 4;
            then x in {c} by A23,XBOOLE_0:def 3;
            then x = c by TARSKI:def 1;
            then
A24:        ex c1 st c1 = c & for c2 st c2 in {a1} holds c1 < c2 by A22;
A25:        a1 < c by A5,A19;
            a1 in {a1} by TARSKI:def 1;
            then c < a1 by A24;
            hence contradiction by A25,Th4;
          end;
          hence thesis by A22,XBOOLE_0:def 4;
        end;
        InitSegm(F,a1) c= InitSegm(Z,a1) by Th28,XBOOLE_1:7;
        then InitSegm(Z,a1) = InitSegm(F,a1) by A20;
        hence f.UpperCone(InitSegm(Z,a1)) = a1 by A19,Def12;
      end;
    end;
    hence f.UpperCone(InitSegm(Z,a1)) = a1;
  end;
  the InternalRel of A is_reflexive_in the carrier of A by Def2;
  then
A26: the InternalRel of A is_reflexive_in Z;
  then the InternalRel of A is_strongly_connected_in Z by A6,ORDERS_1:7;
  then
A27: Z is Chain of A by Def7;
A28: the InternalRel of A is_well_founded_in Z
  proof
    let Y;
    assume that
A29: Y c= Z and
A30: Y <> {};
    now
      per cases;
      case
A31:    Y = {c};
        take x = c;
        thus x in Y by A31,TARSKI:def 1;
        assume (the InternalRel of A)-Seg(x) meets Y;
        then consider x9 being object such that
A32:    x9 in (the InternalRel of A)-Seg(x) and
A33:    x9 in Y by XBOOLE_0:3;
        x9 = c by A31,A33,TARSKI:def 1;
        hence contradiction by A32,WELLORD1:1;
      end;
      case
A34:    Y <> {c};
        set X = Y \ {c};
A35:    now
          assume X = {};
          then Y c= {c} by XBOOLE_1:37;
          hence contradiction by A30,A34,ZFMISC_1:33;
        end;
A36:    X c= F
        proof
          let x be object;
          assume that
A37:      x in X and
A38:      not x in F;
          x in Y by A37;
          then x in {c} by A29,A38,XBOOLE_0:def 3;
          hence thesis by A37,XBOOLE_0:def 5;
        end;
        the InternalRel of A well_orders F by Def12;
        then the InternalRel of A well_orders X by A36,Lm4;
        then the InternalRel of A is_well_founded_in X;
        then consider x being object such that
A39:    x in X and
A40:    (the InternalRel of A)-Seg(x) misses X by A35;
        take x9 = x;
        thus x9 in Y by A39;
A41:    (the InternalRel of A)-Seg(x) /\ X = {} by A40;
        now
          per cases;
          suppose
A42:        c in Y;
A43:        now
              x9 in F by A36,A39;
              then reconsider x99 = x9 as Element of A;
              assume
A44:          c in (the InternalRel of A)-Seg(x9);
              then [c,x9] in the InternalRel of A by WELLORD1:1;
              then
A45:          c <= x99;
A46:          x99 < c by A5,A36,A39;
              c <> x99 by A44,WELLORD1:1;
              then c < x99 by A45;
              hence contradiction by A46,Th4;
            end;
A47:        now
              set x = the Element of (the InternalRel of A)-Seg(x9) /\ {c };
              assume
A48:          (the InternalRel of A)-Seg(x9) /\ {c} <> {};
              then x in {c} by XBOOLE_0:def 4;
              then x = c by TARSKI:def 1;
              hence contradiction by A43,A48,XBOOLE_0:def 4;
            end;
            {c} c= Y by A42,ZFMISC_1:31;
            then Y = X \/ {c} by XBOOLE_1:45;
            then (the InternalRel of A)-Seg(x9) /\ Y = {} \/ {} by A41,A47,
XBOOLE_1:23
              .= {};
            hence (the InternalRel of A)-Seg(x9) misses Y;
          end;
          suppose
            not c in Y;
            then Y misses {c} by ZFMISC_1:50;
            hence (the InternalRel of A)-Seg(x9) misses Y by A40,XBOOLE_1:83;
          end;
        end;
        hence (the InternalRel of A)-Seg(x9) misses Y;
      end;
    end;
    hence thesis;
  end;
  the InternalRel of A is_transitive_in the carrier of A by Def3;
  then
A49: the InternalRel of A is_transitive_in Z;
  the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
  then the InternalRel of A is_antisymmetric_in Z;
  then the InternalRel of A well_orders Z by A26,A49,A6,A28;
  then reconsider Z as Chain of f by A27,A11,Def12;
  c in {c} by TARSKI:def 1;
  then
A50: c in Z by XBOOLE_0:def 3;
  Z in Chains(f) by Def13;
  then c in F by A50,TARSKI:def 4;
  hence thesis by A5;
end;

theorem
  (for C ex a st for b st b in C holds a <= b) implies ex a st for b
  holds not b < a
proof
  set X = the carrier of A;
  set R = (the InternalRel of A)~;
A1: dom R = dom the InternalRel of A by RELAT_2:12
    .= X by PARTFUN1:def 2;
A2: for a,b being Element of A holds [a,b] in R iff b <= a
  by RELAT_1:def 7;
  reconsider R as Order of the carrier of A by A1,PARTFUN1:def 2;
  set B = RelStr (# the carrier of A, R #);
  assume
A3: for C ex a st for b st b in C holds a <= b;
  for E being Chain of B ex e being Element of B st for f being Element of
  B st f in E holds f <= e
  proof
    let E be Chain of B;
    reconsider C = E as Subset of A;
    the InternalRel of A is_strongly_connected_in C
    proof
      let x,y be object;
      assume
A4:   x in C & y in C;
      then reconsider e = x, f = y as Element of B;
      reconsider e1 = e, f1 = f as Element of A;
A5:   e <= f or f <= e by A4,Th11;
      now
        per cases by A5;
        suppose
          [e,f] in R;
          then f1 <= e1 by A2;
          hence thesis;
        end;
        suppose
          [f,e] in R;
          then e1 <= f1 by A2;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    then reconsider C as Chain of A by Def7;
    consider a such that
A6: for b st b in C holds a <= b by A3;
    reconsider e = a as Element of B;
    take e;
    let f be Element of B;
    reconsider b = f as Element of A;
    assume f in E;
    then a <= b by A6;
    then [f,e] in R by A2;
    hence thesis;
  end;
  then consider e being Element of B such that
A7: for f being Element of B holds not e < f by Th55;
  reconsider d = e as Element of A;
  take d;
  let b;
  reconsider f = b as Element of B;
  assume
A8: b < d;
  then b <= d;
  then [e,f] in R by A2;
  then e <= f;
  then e < f by A8;
  hence thesis by A7;
end;

:: from YELLOW14, 2009.07.26, A.T.

registration
  cluster strict empty for RelStr;
  existence
  proof
    take R = RelStr (#{},the Relation of {}#);
    thus R is strict;
    thus the carrier of R is empty;
  end;
end;