:: Fix-point Theorem for Continuous Functions on Chain-complete Posets
::  by Kazuhisa Ishida and Yasunari Shidama
::
:: Received November 10, 2009
:: Copyright (c) 2009-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 POSET_1, ORDERS_1, RELAT_1, RELAT_2, XBOOLE_0, FUNCT_1, FUNCT_2,
      ORDINAL2, FUNCOP_1, SEQM_3, LATTICES, LATTICE3, YELLOW_0, WAYBEL_0,
      ABIAN, TARSKI, CARD_1, FUNCT_7, NAT_1, SUBSET_1, ORDERS_2, XXREAL_0,
      STRUCT_0, ARYTM_3, TREES_2, EQREL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, ORDERS_1,
      RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ORDERS_2, ORDERS_3, NUMBERS,
      ORDINAL1, FUNCT_7, XXREAL_0, XCMPLX_0, YELLOW_2, LATTICE3, YELLOW_0,
      WAYBEL_0, ABIAN;
 constructors ORDERS_3, NAT_1, DOMAIN_1, ABIAN, LATTICE3, YELLOW_2, RELSET_1;
 registrations XBOOLE_0, ORDINAL1, FUNCT_1, PARTFUN1, STRUCT_0, ORDERS_2,
      XREAL_0, NAT_1, WAYBEL10, YELLOW_0, WAYBEL24, FUNCT_7, RELSET_1,
      RELAT_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions RELAT_1, LATTICE3, STRUCT_0;
 theorems RELAT_1, RELSET_1, RELAT_2, ORDERS_2, TARSKI, FUNCT_1, FUNCT_2,
      XBOOLE_0, XBOOLE_1, ORDERS_1, ORDERS_3, FUNCOP_1, FUNCT_7, NAT_1,
      LATTICE3, YELLOW_0, ABIAN, YELLOW_2, WAYBEL_0;
 schemes NAT_1, RELSET_1, FUNCT_2;

begin

:: 1. Monotone function, chain and chain-complete Poset

Lm1: for f being Function st rng f c= dom f holds iter (f,0) = id(dom f)
proof
  let f be Function;
  assume rng f c= dom f;
  then field f = dom f by XBOOLE_1:12;
  hence thesis by FUNCT_7:68;
end;

Lm2: for f being Function, n be Nat st
  rng f c= dom f holds dom iter(f,n) = dom f & rng iter(f,n) c= dom f
proof
  let f be Function, n be Nat;
  defpred U[Nat] means
  dom iter(f,$1) = dom f & rng iter(f,$1) c= dom f;
  assume rng f c= dom f;
  then iter(f,0) = id dom f by Lm1;
  then
A1: U[ 0] by RELAT_1:45;
A2: for k be Nat holds U[k] implies U[k+1]
  proof
    let k be Nat;
    assume
A3: dom iter(f,k) = dom f & rng iter(f,k) c= dom f;
    iter(f,k+1) = f*iter(f,k) & iter(f,k+1) = iter(f,k)*f
                                          by FUNCT_7:69,71;
    then dom iter(f,k+1) = dom iter(f,k) &
    rng iter(f,k+1) c= rng iter(f,k) by A3,RELAT_1:26,27;
    hence thesis by A3,XBOOLE_1:1;
  end;
  for k be Nat holds U[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

Lm3:
  for X be set, f being Function of X,X, n be Nat holds
    iter(f,n) is Function of X,X
proof
  let X be set, f be Function of X,X, n be Nat;
A1: X = {} implies X = {}; then
A2: dom f = X & rng f c= X by FUNCT_2:def 1;
  then dom iter(f,n) = X & rng iter(f,n) c= X by Lm2;
  then reconsider R = iter(f,n) as Relation of X,X by RELSET_1:4;
  dom R = X & rng R c= X by A2,Lm2;
  hence thesis by A1,FUNCT_2:def 1;
end;

registration let P be non empty Poset; :: move to ORDERS_2
  cluster non empty for Chain of P;
  existence
  proof
    ex L being Chain of P st L is non empty
    proof
      set z = the Element of P;
      set IT={z};
      reconsider IT as Chain of P by ORDERS_2:8;
      IT is non empty;
      hence thesis;
    end;
    hence thesis;
  end;
end;

Lm4:
  for A being non empty RelStr, a being Element of A holds
  a is_<=_than the carrier of A iff for x being Element of A holds a <= x
proof
  let A be non empty RelStr, a be Element of A;
  (for x being Element of A holds a <= x) implies a is_<=_than the carrier of A
  proof
    assume A1:for x being Element of A holds a <= x;
    a is_<=_than the carrier of A
    proof
      let x be Element of A;
      thus thesis by A1;
    end;
    hence thesis;
  end;
  hence thesis by LATTICE3:def 8;
end;

definition let IT be RelStr;
  attr IT is chain-complete means :Def1:
  IT is lower-bounded &
  for L being Chain of IT st L is non empty holds ex_sup_of L,IT;
end;

theorem Th1:
  for P1, P2 being non empty Poset, K being non empty Chain of P1,
      h being monotone Function of P1, P2 holds
    h.:K is non empty Chain of P2
  proof
  let P1, P2 be non empty Poset,
      K be non empty Chain of P1,
      h be monotone Function of P1, P2;
  set R = the InternalRel of P2;
  set K2 = h.:K;
  for x, y be set st x in K2 & y in K2 & x <>y holds [x,y] in R or [y,x] in R
  proof
    let x, y be set;
    assume A1:x in K2 & y in K2 & x <>y;
    then reconsider x,y as Element of P2;
    consider a be set such that A2: a in dom h & a in K & x = h.a
                                            by A1,FUNCT_1:def 6;
    consider b be set such that A3: b in dom h & b in K & y = h.b
                                            by A1,FUNCT_1:def 6;
    reconsider a,b as Element of P1 by A2,A3;
    a<=b or b<=a by A2,A3,ORDERS_2:11;
    then x<=y or y<=x by A2,A3,ORDERS_3:def 5;
    hence thesis by ORDERS_2:def 5;
  end;
  then A4:R is_connected_in K2 by RELAT_2:def 6;
  for x be set st x in K2 holds [x,x] in R
  proof
    let x be set;
    assume x in K2;
    then reconsider x as Element of P2;
    x<=x;
    hence thesis by ORDERS_2:def 5;
  end;
  then R is_reflexive_in K2 by RELAT_2:def 1;
  then R is_strongly_connected_in K2 by A4,ORDERS_1:7;
  then reconsider K2 as Chain of P2 by ORDERS_2:def 7;
  consider a be set such that A5:a in K by XBOOLE_0:7;
  a in the carrier of P1 by A5;
  then a in dom h by FUNCT_2:def 1;
  then h.a in K2 by A5,FUNCT_1:def 6;
  hence thesis;
  end;

registration
  cluster strict chain-complete non empty for Poset;
  existence
  proof
    set z = the set;
    set A = {z};
    reconsider R = id A as Relation of A;
    reconsider R as Order of A;
    take IT = RelStr(#A,R#);
    reconsider z as Element of IT by TARSKI:def 1;
    for L being Chain of IT st L is non empty holds ex_sup_of L,IT
      proof
      let L be Chain of IT;
      assume L is non empty;
      for x being Element of IT st x in L holds x <= z by TARSKI:def 1;
      then A1: L is_<=_than z by LATTICE3:def 9;
      for y being Element of IT holds
            L is_<=_than y implies z <= y by TARSKI:def 1;
      hence thesis by A1,YELLOW_0:15;
    end;
    hence thesis by Def1;
  end;
end;

registration
  cluster chain-complete -> lower-bounded for RelStr;
  coherence by Def1;
end;

reserve n,m,k for Nat;
reserve x,y,z,X for set;
reserve P,Q for strict chain-complete non empty Poset;
reserve L for non empty Chain of P;
reserve M for non empty Chain of Q;
reserve p,p1,p2,p3,p4 for Element of P;
reserve q,q1,q2 for Element of Q;
reserve f for monotone Function of P,Q;
reserve g,g1,g2 for monotone Function of P,P;

:: Minimum and sup.

theorem Th2:
  sup (f.:L) <= f.(sup L)
  proof
  reconsider M=f.:L as non empty Chain of Q by Th1;
  set r = sup L;
  set u = f.(sup L);
  A1:ex_sup_of L,P & ex_sup_of M,Q by Def1;
  for q st q in M holds q <= u
    proof
    let q;
    assume q in M;
    then consider x such that
A2: x in dom f & x in L & q = f.x by FUNCT_1:def 6;
    reconsider x as Element of P by A2;
    L is_<=_than r by A1,YELLOW_0:def 9;
    then x <= r by A2,LATTICE3:def 9;
    hence thesis by A2,ORDERS_3:def 5;
    end;
  then M is_<=_than u by LATTICE3:def 9;
  hence thesis by A1,YELLOW_0:def 9;
  end;

begin

:: 2. Fix-point theorem for continuous function on chain-complete Poset
:: Primaries--Iteration of monotone functions

Lm5:
  for P be non empty Poset, g be monotone Function of P, P,
      p be Element of P holds
  iter(g,0).p=p
  proof
    let P be non empty Poset,
        g be monotone Function of P, P,
        p be Element of P;
    set X = the carrier of P;
    iter(g,0).p = (id X).p by FUNCT_7:84
              .= p by FUNCT_1:18;
    hence thesis;
  end;

definition let P be non empty Poset,
               g be monotone Function of P, P,
               p be Element of P;
  func iterSet(g,p) -> non empty set equals
    {x where x is Element of P : ex n being Nat st x = iter(g,n).p};
  correctness
  proof
    set IT = {x where x is Element of P
                        : ex n being Nat st x = iter(g,n).p};
    IT is non empty
    proof
      iter(g,0).p = p by Lm5;
      then p in IT;
      hence thesis;
    end;
    hence thesis;
  end;
end;

Lm6:
  iter(g,n).p is Element of P
  proof
    set X = the carrier of P;
    reconsider g1 = iter(g,n) as Function of X,X by Lm3;
    g1.p in X;
    hence thesis;
  end;

Lm7:
  (g*iter(g,n)).p = g.(iter(g,n).p) & (iter(g,n)*g).p = iter(g,n).(g.p)
  proof
    set X = the carrier of P;
    reconsider g1 = iter(g,n) as Function of X,X by Lm3;
    (g*g1).p = g.(g1.p) & (g1*g).p = g1.(g.p) by FUNCT_2:15;
    hence thesis;
  end;

Lm8:
  p<=p3 & p1=iter(g,n).p & p4= iter(g,n).p3 implies p1 <= p4
  proof
  defpred U[Nat] means
  for p,p3,p1,p4 holds
  p<=p3 & p1=iter(g,$1).p & p4= iter(g,$1).p3 implies p1 <= p4;
  A1:U[0]
    proof
    let p,p3,p1,p4;
    assume p<=p3 & p1=iter(g,0).p & p4= iter(g,0).p3;
    then p<=p3 & p1=p & p4=p3 by Lm5;
    hence thesis;
    end;
  A2: U[k] implies U[k+1]
    proof
    assume
    A3: for p,p3,p1,p4 holds
              p<=p3 & p1=iter(g,k).p & p4= iter(g,k).p3 implies p1 <= p4;
    U[k+1]
     proof
     let p,p3,p1,p4;
     assume A4:p<=p3 & p1=iter(g,k+1).p & p4= iter(g,k+1).p3;
     reconsider x1=iter(g,k).p as Element of P by Lm6;
     reconsider y1=iter(g,k).p3 as Element of P by Lm6;
     A5:x1<=y1 by A4,A3;
     iter(g,k+1) = g*iter(g,k) by FUNCT_7:71;
     then p1 = g.(iter(g,k).p) & p4 = g.(iter(g,k).p3) by Lm7,A4;
     hence thesis by A5,ORDERS_3:def 5;
     end;
    hence thesis;
    end;
  U[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
  end;

Lm9:
  p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+k).p implies p1 <= p4
  proof
  defpred U[Nat] means
  for p,p3,p1,p4 holds
       p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+$1).p implies p1 <= p4;
  A1:U[0];
  A2:for k be Nat st U[k] holds U[k+1]
    proof
    let k;
    assume
    A3: for p,p3,p1,p4 holds
          p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+k).p
                           implies p1 <= p4;
    U[k+1]
     proof
     let p,p3,p1,p4;
     assume A4:p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+(k+1)).p;
     reconsider y1=iter(g,n+k).p as Element of P by Lm6;
     A5:p1<=y1 by A4,A3;
     iter(g,n+(k+1)) = iter(g,(n+k)+1).=iter(g,n+k)*g by FUNCT_7:69;
     then p4 = iter(g,n+k).p3 by Lm7,A4;
     then y1<=p4 by A4,Lm8;
     hence thesis by A5,ORDERS_2:3;
     end;
    hence thesis;
    end;
  for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
  end;

Lm10:
  n<=m & p3 = g.p & p<=p3 & p1=iter(g,n).p & p4 = iter(g,m).p implies p1 <= p4
proof
  assume A1:n<=m & p3= g.p & p<=p3 & p1=iter(g,n).p & p4 = iter(g,m).p;
  then consider k such that A2:m=n+k by NAT_1:10;
  thus thesis by A1,A2,Lm9;
end;

Lm11:
  p is_a_fixpoint_of g implies iter(g,n).p = p
  proof
  defpred U[Nat] means
  for p holds p is_a_fixpoint_of g implies iter(g,$1).p = p;
  A1:U[0] by Lm5;
  A2:for k be Nat st U[k] holds U[k+1]
    proof
    let k;
    assume A3:U[k];
    U[k+1]
     proof
     let p;
     assume A4:p is_a_fixpoint_of g;
     iter(g,k+1) = g*iter(g,k) by FUNCT_7:71;
     then iter(g,k+1).p = g.(iter(g,k).p) by Lm7
                       .= g.p by A4,A3
                       .= p by A4,ABIAN:def 3;
     hence thesis;
     end;
    hence thesis;
    end;
  for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
  end;

Lm12:
  g1 <= g2 & p1 = iter(g1,n).p & p2 = iter(g2,n).p implies p1 <= p2
  proof
  defpred U[Nat] means
  for p,p1,p2 holds
       g1 <= g2 & p1 = iter(g1,$1).p & p2 = iter(g2,$1).p
             implies p1 <= p2;
  A1:U[0]
  proof
     let p,p1,p2;
     assume g1 <= g2 & p1 = iter(g1,0).p & p2 = iter(g2,0).p;
     then p1 = p & p2 = p by Lm5;
     hence thesis;
     end;
  A2:for k be Nat st U[k] holds U[k+1]
    proof
    let k;
    assume A3:U[k];
    U[k+1]
      proof
      let p,p1,p2;
      assume A4:g1 <= g2 & p1 = iter(g1,k+1).p & p2 = iter(g2,k+1).p;
      reconsider q1 = iter(g1,k).p as Element of P by Lm6;
      reconsider q2 = iter(g2,k).p as Element of P by Lm6;
      set r = g1.q2;
A5:   q1 <= q2 by A4,A3;
  iter(g1,k+1) = g1*iter(g1,k) by FUNCT_7:71;
then A6:   p1 = g1.q1 by Lm7,A4;
  iter(g2,k+1) = g2*iter(g2,k) by FUNCT_7:71;
then A7:   p2 = g2.q2 by Lm7,A4;
A8:   p1 <= r by A5,A6,ORDERS_3:def 5;
      r <= p2 by A4,A7,YELLOW_2:9;
      hence thesis by A8,ORDERS_2:3;
      end;
    hence thesis;
    end;
  for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
  end;

theorem Th3:
  iterSet(g,Bottom P) is non empty Chain of P
  proof
  set a = Bottom P;
  set R = the InternalRel of P;
  set L=iterSet(g,a);
  A1:x in L implies x is Element of P
    proof
    assume x in L;
    then consider y being Element of P such that
A2: x=y & ex n being Nat st y = iter(g,n).a;
    thus thesis by A2;
    end;
  x in L implies x in the carrier of P
    proof
    assume x in L;
    then x is Element of the carrier of P by A1;
    hence thesis;
    end;
  then reconsider L as Subset of P by TARSKI:def 3;
  x in L & y in L & x <>y implies [x,y] in R  or [y,x] in R
    proof
    assume A3:x in L & y in L & x <>y;
    then reconsider x,y as Element of P;
    consider p such that A4: x=p & ex n st p = iter(g,n).a by A3;
    consider p1 such that A5: y=p1 & ex m st p1 = iter(g,m).a by A3;
    consider n such that A6:p = iter(g,n).a by A4;
    consider m such that A7:p1 = iter(g,m).a by A5;
    p<=p1 or p1<=p
      proof
      set a1 = iter(g,1).a;
      A8:a1=g.a by FUNCT_7:70;
      per cases;
        suppose n<=m;
          hence thesis by A6,A7,A8,Lm10,YELLOW_0:44;
          end;
        suppose m<=n;
          hence thesis by A6,A7,A8,Lm10,YELLOW_0:44;
          end;
      end;
    hence thesis by A4,A5,ORDERS_2:def 5;
    end;
  then A9:R is_connected_in L by RELAT_2:def 6;
  x in L implies [x,x] in R
    proof
    assume x in L;
    then reconsider x as Element of P;
    x<=x;
    hence thesis by ORDERS_2:def 5;
    end;
  then R is_reflexive_in L by RELAT_2:def 1;
  then R is_strongly_connected_in L by A9,ORDERS_1:7;
  then reconsider L as Chain of P by ORDERS_2:def 7;
  L is non empty Chain of P;
  hence thesis;
end;

definition let P; let g be monotone Function of P,P;
  func iter_min(g) -> non empty Chain of P equals
    iterSet(g,Bottom P);
  correctness by Th3;
end;

theorem Th4:
  sup iter_min(g) = sup (g.:iter_min(g))
  proof
  reconsider L=g.:iter_min(g) as non empty Chain of P by Th1;
  A1:ex_sup_of iter_min(g),P & ex_sup_of L,P by Def1;
  set a = Bottom P;
  set s1=sup iter_min(g);
  set s2=sup L;
  A2:iter_min(g) is_<=_than s1 by A1,YELLOW_0:def 9;
  A3:L is_<=_than s2 by A1,YELLOW_0:def 9;
  for x being Element of P st x in iter_min(g) holds x <= s2
    proof
    let x be Element of P;
    assume x in iter_min(g);
    then consider p such that A4:x=p & ex n st p = iter(g,n).a;
    consider n such that A5:p=iter(g,n).a by A4;
    A6:1<=n implies p in L
      proof
      assume 1<=n;
      then consider k such that A7:n=1+k by NAT_1:10;
      reconsider z=iter(g,k).a as Element of P by Lm6;
      z in the carrier of P; then
A8:   z in dom g & z in iter_min(g) by FUNCT_2:def 1;
      p = (g*iter(g,k)).a by A5,A7,FUNCT_7:71
       .= g.z by Lm7;
      hence thesis by A8,FUNCT_1:def 6;
      end;
    n=0 implies p=a by A5,Lm5;
    hence thesis by A6,A4,A3,LATTICE3:def 9,NAT_1:14,YELLOW_0:44;
    end;
  then iter_min(g) is_<=_than s2 by LATTICE3:def 9;
  then A9:s1<=s2 by A1,YELLOW_0:30;
  for x being Element of P st x in L holds x <= s1
    proof
    let x be Element of P;
    assume x in L;
    then consider z such that
A10: z in dom g & z in iter_min(g) & x = g.z by FUNCT_1:def 6;
    consider z1 be Element of P such that
               A11:z=z1 & ex n st z1 = iter(g,n).a by A10;
    consider n such that A12:z1=iter(g,n).a by A11;
    set n1=n+1;
    g.z = (g*iter(g,n)).a by Lm7,A11,A12
       .= iter(g,n1).a by FUNCT_7:71;
    then x in iterSet(g,a) by A10;
    hence thesis by A2,LATTICE3:def 9;
    end;
  then L is_<=_than s1 by LATTICE3:def 9;
  then s2<=s1 by A1,YELLOW_0:def 9;
  hence thesis by A9,ORDERS_2:2;
  end;

theorem Th5:
  g1 <= g2 implies sup iter_min(g1) <= sup iter_min(g2)
  proof
  assume A1:g1 <= g2;
  set p2 = sup iter_min(g2);
  set a = Bottom P;
  A2:ex_sup_of iter_min(g1),P & ex_sup_of iter_min(g2),P by Def1;
  then A3:iter_min(g2) is_<=_than p2 by YELLOW_0:def 9;
  for x being Element of P st x in iter_min(g1) holds x <= p2
    proof
    let x be Element of P;
    assume x in iter_min(g1);
    then consider p such that A4:x=p & ex n st p = iter(g1,n).a;
    consider n such that A5:p=iter(g1,n).a by A4;
    reconsider y = iter(g2,n).a as Element of P by Lm6;
    y in iter_min(g2);
    then A6:y <= p2 by A3,LATTICE3:def 9;
    p <= y by A1,A5,Lm12;
    hence thesis by A4,A6,ORDERS_2:3;
    end;
  then iter_min(g1) is_<=_than p2 by LATTICE3:def 9;
  hence thesis by A2,YELLOW_0:30;
  end;

:: Continuous function on chain-complete Poset

definition let P,Q be non empty Poset;
  let f be Function of P,Q;
  attr f is continuous means :Def4:
  f is monotone & for L be non empty Chain of P holds f preserves_sup_of L;
end;

theorem Th6:
  for f being Function of P,Q holds f is continuous iff
          (f is monotone & for L holds f.(sup L) = sup (f.:L))
   proof
   let f be Function of P,Q;
   thus f is continuous implies
        (f is monotone & for L holds f.(sup L) = sup (f.:L))
     proof
     assume A1:f is continuous;
     for L holds f.(sup L) = sup (f.:L)
     proof
       let L;
    A2:f preserves_sup_of L by A1,Def4;
       ex_sup_of L,P by Def1;
       hence thesis by A2,WAYBEL_0:def 31;
     end;
     hence thesis by A1,Def4;
     end;
     assume that A3:f is monotone and
A4:  for L holds f.(sup L) = sup (f.:L);
     for L holds f preserves_sup_of L
     proof
       let L;
       reconsider M = f.:L as non empty Chain of Q by A3,Th1;
       ex_sup_of M,Q & f.(sup L) = sup M by Def1,A4;
       hence thesis by WAYBEL_0:def 31;
     end;
     hence thesis by A3,Def4;
   end;

theorem Th7:
  for z being Element of Q holds (P-->z) is continuous
  proof
    let z be Element of Q;
    set IT = P --> z;
    for L holds IT.(sup L) = sup (IT.:L)
      proof
      let L;
      set M = IT.:L;
      for x being Element of Q st x in M holds x <= z
        proof
        let x be Element of Q;
        assume x in M;
        then consider a be set such that
    A1: a in dom IT & a in L & x = IT.a by FUNCT_1:def 6;
        thus thesis by A1,FUNCOP_1:7;
        end;
      then A2:M is_<=_than z by LATTICE3:def 9;
      for y being Element of Q st M is_<=_than y holds z <= y
        proof
        let y be Element of Q;
        assume A3:M is_<=_than y;
        consider a be set such that A4:a in L by XBOOLE_0:def 1;
        a in the carrier of P by A4;
        then A5:a in dom IT by FUNCOP_1:13;
        IT.a = z by A4,FUNCOP_1:7;
        then z in M by A4,A5,FUNCT_1:def 6;
        hence thesis by A3,LATTICE3:def 9;
        end;
      then z = "\/"(M,Q) by A2,YELLOW_0:30;
      hence thesis by FUNCOP_1:7;
      end;
    hence thesis by Th6;
  end;

registration let P,Q;
  cluster continuous for Function of P, Q;
  existence
  proof
    set z = the Element of Q;
    take P-->z;
    thus thesis by Th7;
  end;
end;

registration let P,Q;
  cluster continuous -> monotone for Function of P, Q;
  correctness by Def4;
end;

theorem Th8:
  for f being monotone Function of P,Q holds
    (for L holds f.(sup L) <= sup (f.:L)) implies f is continuous
  proof
  let f be monotone Function of P,Q;
  assume A1:for L holds f.(sup L) <= sup (f.:L);
  for L holds f.(sup L) = sup (f.:L)
    proof
    let L;
    set a1=f.(sup L);
    set a2=sup (f.:L);
    A2:a2<=a1 by Th2;
    a1<=a2 by A1;
    hence thesis by A2,ORDERS_2:2;
    end;
  hence thesis by Th6;
  end;

:: Fix-point theorem for continuous function on chain-complete Poset

Lm13:
  g is continuous & p=sup iter_min(g) implies p is_a_fixpoint_of g
proof
A1:dom g = the carrier of P by FUNCT_2:def 1;
  reconsider L=g.:iter_min(g) as non empty Chain of P by Th1;
  assume A2:g is continuous & p=sup iter_min(g);
  then g.p = sup L by Th6
          .= p by A2,Th4;
  hence thesis by A1,ABIAN:def 3;
end;

Lm14:
  p4=sup iter_min(g) implies for p st p is_a_fixpoint_of g holds p4 <= p
proof
  assume A1:p4=sup iter_min(g);
  for p st p is_a_fixpoint_of g holds p4 <= p
  proof
    let p;
    assume A2:p is_a_fixpoint_of g;
    set M = iter_min(g);
    set a = Bottom P;
    A3:ex_sup_of M,P by Def1;
    for p1 st p1 in M holds p1 <= p
    proof
      let p1;
      assume p1 in M;
      then consider p2 such that A4:p1=p2 & ex n st p2 = iter(g,n).a;
      consider n such that A5:p1=iter(g,n).a by A4;
      reconsider q = iter(g,n).p as Element of P by Lm6;
      p1 <= q by A5,Lm8,YELLOW_0:44;
      hence thesis by A2,Lm11;
    end;
    then M is_<=_than p by LATTICE3:def 9;
    hence thesis by A3,A1,YELLOW_0:def 9;
  end;
  hence thesis;
end;

definition let P; let g be monotone Function of P,P;
  assume A1:g is continuous;
  func least_fix_point(g) -> Element of P means  :Def5:
    it is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds it <= p;
  existence
  proof
    set IT = sup iter_min(g);
    take IT;
    thus thesis by A1,Lm13,Lm14;
  end;
  uniqueness
  proof
    let p1,p2;
    assume (p1 is_a_fixpoint_of g &
               for p st p is_a_fixpoint_of g holds p1 <= p) &
           (p2 is_a_fixpoint_of g &
               for p st p is_a_fixpoint_of g holds p2 <= p);
    then p1 <=  p2 & p2 <= p1;
    hence thesis by ORDERS_2:2;
  end;
end;

theorem Th9:
  for g being continuous Function of P,P holds
    least_fix_point(g) = sup iter_min(g)
proof
  let g be continuous Function of P,P;
  set p = sup iter_min(g);
  set q = least_fix_point(g);
  p is_a_fixpoint_of g by Lm13;
  then A1:q <= p by Def5;
  q is_a_fixpoint_of g by Def5;
  then p <= q by Lm14;
  hence thesis by A1,ORDERS_2:2;
end;

theorem Th10:
  for g1,g2 being continuous Function of P,P st g1 <= g2 holds
    least_fix_point(g1) <= least_fix_point(g2)
proof
  let g1,g2 be continuous Function of P,P;
  assume A1: g1 <= g2;
  set p1 = sup iter_min(g1);
  set p2 = sup iter_min(g2);
  p1 = least_fix_point(g1) & p2 = least_fix_point(g2) by Th9;
  hence thesis by A1,Th5;
end;

begin

:: 3. Function space of continuous functions on chain-complete Posets

definition let P,Q;
  func ConFuncs (P,Q) -> non empty set equals
   {x where x is Element of Funcs(the carrier of P,the carrier of Q)
               :ex f be continuous Function of P,Q st f=x };
    correctness
    proof
    set IT = {x where x is Element of Funcs(the carrier of P,the carrier of Q)
               :ex f be continuous Function of P,Q st f=x };
    IT is non empty
    proof
      set z = the Element of Q;
      reconsider f = P-->z as continuous Function of P,Q by Th7;
      f is Element of Funcs(the carrier of P,the carrier of Q) by FUNCT_2:8;
      then f in IT;
      hence thesis;
    end;
    hence thesis;
    end;
  end;

Lm15:
  for f be Function of P,Q holds f <= f
proof
  let f be Function of P,Q;
  for p holds f.p <= f.p;
  hence thesis by YELLOW_2:9;
end;

Lm16:
  for f,g,h be Function of P,Q st f <= g & g <= h holds f <= h
  proof
  let f,g,h be Function of P,Q;
  assume A1:f <= g & g <= h;
  for p holds f.p <= h.p
    proof
    let p;
    q=f.p & q2=h.p implies q<=q2
      proof
      assume A2:q=f.p & q2=h.p;
      set q1=g.p;
      q<=q1 & q1<=q2 by A2,A1,YELLOW_2:9;
      hence thesis by ORDERS_2:3;
      end;
    hence thesis;
    end;
  hence thesis by YELLOW_2:9;
  end;

Lm17:
  for f,g be Function of P,Q st f <= g & g <= f holds f=g
proof
  let f,g be Function of P,Q;
  assume A1:f <= g & g <= f;
  for x st x in the carrier of P holds f.x =g.x
  proof
    let x;
    assume x in the carrier of P;
    then reconsider p=x as Element of P;
    set q1=f.p;
    set q2=g.p;
    A2:q1<=q2 by A1,YELLOW_2:9;
    q2<=q1 by A1,YELLOW_2:9;
    hence thesis by A2,ORDERS_2:2;
  end;
  hence thesis by FUNCT_2:12;
end;

definition let P,Q;
  func ConRelat(P,Q) -> Relation of ConFuncs(P,Q) means  :Def7:
   for x,y holds [x,y] in it iff (x in ConFuncs(P,Q) & y in ConFuncs(P,Q)
        & ex f,g being Function of P,Q st x=f & y=g & f <= g);
   existence
     proof
     defpred U[set,set] means ex f,g being Function of P,Q st
                                 $1=f & $2=g & f <= g;
     set X = ConFuncs(P,Q);
     consider IT being Relation of X,X such that
       A1:for x,y holds [x,y] in IT iff x in X & y in X & U[x,y]
                           from RELSET_1:sch 1;
     take IT;
     thus thesis by A1;
     end;
    uniqueness
     proof
     set X = ConFuncs(P,Q);
     let Y1,Y2 be Relation of X;
     defpred P1[set,set] means
       $1 in X & $2 in X
          & ex f,g being Function of P,Q st
                                 $1=f & $2=g & f <= g;
     (for x,y holds ([x,y] in Y1 iff P1[x,y]) &
      for x,y holds ([x,y] in Y2 iff P1[x,y]) )
          implies Y1=Y2
       proof
       assume A2:for x,y holds ([x,y] in Y1 iff P1[x,y]) &
                 for x,y holds ([x,y] in Y2 iff P1[x,y]);
       then A3:for x1 being Element of X, y1 being Element of X
            holds ([x1,y1] in Y1 iff P1[x1,y1] );
       A4:for x being Element of X, y being Element of X
            holds [x,y] in Y2 iff P1[x,y] by A2;
       thus thesis from RELSET_1:sch 4(A3,A4);
       end;
     hence thesis;
     end;
  end;

Lm18:
  field ConRelat(P,Q) c= ConFuncs(P,Q)
  proof
    ConFuncs(P,Q) \/ ConFuncs(P,Q) c= ConFuncs(P,Q);
    hence thesis by RELSET_1:8;
  end;

Lm19:
  ConRelat(P,Q) is_reflexive_in ConFuncs(P,Q)
  proof
    set R = ConRelat(P,Q);
    x in ConFuncs(P,Q) implies [x,x] in R
    proof
      assume A1:x in ConFuncs(P,Q);
      then consider x1 be Element of Funcs(the carrier of P,the carrier of Q)
         such that
   A2:x=x1 and A3: ex f be continuous Function of P,Q st f=x1;
      consider f be continuous Function of P,Q such that A4:f=x1 by A3;
      f <= f by Lm15;
      hence thesis by A1,A2,A4,Def7;
    end;
    hence thesis by RELAT_2:def 1;
  end;

Lm20:
  ConRelat(P,Q) is_transitive_in ConFuncs(P,Q)
  proof
    set X = ConFuncs(P,Q);
    set R = ConRelat(P,Q);
    x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
    proof
      assume A1:x in X & y in X & z in X & [x,y] in R & [y,z] in R;
      then consider f,g being Function of P,Q such that
      A2:x=f & y=g & f <= g by Def7;
      consider g1,h being Function of P,Q such that
      A3:y=g1 & z=h & g1 <= h by A1,Def7;
      f <= h by A3,A2,Lm16;
      hence thesis by A1,A2,A3,Def7;
    end;
    hence thesis by RELAT_2:def 8;
  end;

Lm21:
  ConRelat(P,Q) is_antisymmetric_in ConFuncs(P,Q)
  proof
    set X = ConFuncs(P,Q);
    reconsider R = ConRelat(P,Q) as Relation of ConFuncs(P,Q);
    x in X & y in X & [x,y] in R & [y,x] in R implies x = y
    proof
      assume A1:x in X & y in X & [x,y] in R & [y,x] in R;
      then consider f,g being Function of P,Q such that
      A2:x=f & y=g & f <= g by Def7;
      consider g1,f1 being Function of P,Q such that
      A3:y=g1 & x=f1 & g1 <= f1 by A1,Def7;
      thus thesis by A2,A3,Lm17;
    end;
    hence thesis by RELAT_2:def 4;
  end;

registration let P,Q;
  cluster ConRelat(P,Q) -> reflexive;
  coherence
  proof
    ConRelat(P,Q) is_reflexive_in field ConRelat(P,Q)
    proof
      reconsider R = ConRelat(P,Q)  as Relation of ConFuncs(P,Q);
      x in field R implies [x,x] in R
      proof
        assume A1:x in field R;
        A2:field R c= ConFuncs(P,Q) by Lm18;
        R is_reflexive_in ConFuncs(P,Q) by Lm19;
        hence thesis by A1,A2,RELAT_2:def 1;
      end;
      hence thesis by RELAT_2:def 1;
    end;
    hence thesis by RELAT_2:def 9;
  end;
  cluster ConRelat(P,Q) -> transitive;
  coherence
  proof
    ConRelat(P,Q) is_transitive_in field ConRelat(P,Q)
    proof
      set X = field ConRelat(P,Q);
      set R = ConRelat(P,Q);
      x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
      proof
        assume A3:x in X & y in X & z in X & [x,y] in R & [y,z] in R;
        set X1=ConFuncs(P,Q);
        A4:field R c= X1 by Lm18;
        R is_transitive_in X1 by Lm20;
        hence thesis by A3,A4,RELAT_2:def 8;
      end;
      hence thesis by RELAT_2:def 8;
    end;
    hence thesis by RELAT_2:def 16;
  end;
  cluster ConRelat(P,Q) -> antisymmetric;
  coherence
  proof
    ConRelat(P,Q) is_antisymmetric_in field ConRelat(P,Q)
      proof
      set X = field ConRelat(P,Q);
      reconsider R = ConRelat(P,Q) as Relation of ConFuncs(P,Q);
      x in X & y in X & [x,y] in R & [y,x] in R implies x = y
      proof
        assume A5:x in X & y in X & [x,y] in R & [y,x] in R;
        set X1=ConFuncs(P,Q);
        A6:field R c= X1 by Lm18;
        R is_antisymmetric_in X1 by Lm21;
        hence thesis by A5,A6,RELAT_2:def 4;
      end;
      hence thesis by RELAT_2:def 4;
    end;
    hence thesis by RELAT_2:def 12;
  end;
end;

definition let P,Q;
  func ConPoset(P,Q) -> strict non empty Poset equals
     RelStr(#ConFuncs(P,Q),ConRelat(P,Q)#);
  correctness
  proof
    set IT = RelStr(#ConFuncs(P,Q),ConRelat(P,Q)#);
A1: the InternalRel of IT is_reflexive_in the carrier of IT by Lm19;
A2: the InternalRel of IT is_transitive_in the carrier of IT by Lm20;
    the InternalRel of IT is_antisymmetric_in the carrier of IT
                                                            by Lm21;
    hence thesis by A1,A2,ORDERS_2:def 2,def 3,def 4;
  end;
end;

reserve F for non empty Chain of ConPoset(P,Q);

definition let P,Q,F,p;
  func F-image p -> non empty Chain of Q equals
    {x where x is Element of Q
        :ex f being continuous Function of P,Q st f in F & x=f.p};
  correctness
  proof
    set R = the InternalRel of Q;
    set IT = {x where x is Element of Q
            :ex f being continuous Function of P,Q st f in F & x=f.p};
    x in IT implies x in the carrier of Q
    proof
      assume x in IT;
      then consider a being Element of Q such that
      A1:x=a & ex f being continuous Function of P,Q st f in F & a=f.p;
      reconsider x as Element of the carrier of Q by A1;
      x in the carrier of Q;
      hence thesis;
    end;
    then reconsider IT as Subset of Q by TARSKI:def 3;
    x in IT & y in IT & x <>y implies [x,y] in R  or [y,x] in R
      proof
      assume A2:x in IT & y in IT & x <>y;
      then consider a being Element of Q such that
A3:   x=a & ex f being continuous Function of P,Q st f in F & a=f.p;
      consider f being continuous Function of P,Q such that
A4:   f in F & a=f.p by A3;
      consider b being Element of Q such that
A5:   y=b & ex g being continuous Function of P,Q st g in F & b=g.p by A2;
      consider g being continuous Function of P,Q such that
A6:   g in F & b=g.p by A5;
      set S =the InternalRel of ConPoset(P,Q);
      A7:S is_strongly_connected_in F by ORDERS_2:def 7;
      per cases by A7,A4,A6,RELAT_2:def 7;
        suppose [f,g] in S;
           then consider f1,g1 being Function of P,Q such that
        A8:f=f1 & g=g1 & f1 <= g1 by Def7;
           a <= b by A8,A4,A6,YELLOW_2:9;
           hence thesis by A3,A5,ORDERS_2:def 5;
           end;
        suppose [g,f] in S;
           then consider g1,f1 being Function of P,Q such that
              A9:g=g1 & f=f1 & g1 <= f1 by Def7;
           b<= a by A9,A4,A6,YELLOW_2:9;
           hence thesis by A3,A5,ORDERS_2:def 5;
           end;
        end;
    then A10:R is_connected_in IT by RELAT_2:def 6;
    x in IT implies [x,x] in R
      proof
      assume x in IT;
      then reconsider x as Element of Q;
      x<=x;
      hence thesis by ORDERS_2:def 5;
      end;
    then R is_reflexive_in IT by RELAT_2:def 1;
    then R is_strongly_connected_in IT by A10,ORDERS_1:7;
    then reconsider IT as Chain of Q by ORDERS_2:def 7;
    consider a be set such that A11:a in F by XBOOLE_0:7;
    a in ConFuncs(P,Q) by A11; then
    consider b being Element of Funcs(the carrier of P,the carrier of Q)
         such that
A12: a=b & ex f be continuous Function of P,Q st f=b;
    consider f be continuous Function of P,Q such that A13:f=b by A12;
    reconsider c = f.p as Element of Q;
    c in IT by A11,A12,A13;
    hence thesis;
    end;
  end;

definition let P,Q,F;
  func sup_func(F) -> Function of P,Q means  :Def10:
    for p,M holds M=F-image p implies it.p=sup M;
  existence
    proof
    set X = the carrier of P;
    set Y = the carrier of Q;
    defpred U[set,set] means for p,M holds p= $1 & M=F-image p
    implies $2=sup M;
    A1:for x st x in X ex y st y in Y & U[x,y]
      proof
      let x;
      assume x in X;
      then reconsider x as Element of P;
      reconsider a = F-image x as non empty Chain of Q;
      set y = sup a;
      take y;
      thus thesis;
      end;
    consider IT being Function of X,Y such that
A2: for x st x in X holds U[x,IT.x] from FUNCT_2:sch 1(A1);
    for p,M holds M=F-image p implies IT.p=sup M by A2;
    hence thesis;
    end;
  uniqueness
    proof
      let f,g be Function of P,Q;
      (for p,M holds M=F-image p implies f.p=sup M) &
      (for p,M holds M=F-image p implies g.p=sup M) implies f=g
        proof
        assume A3:(for p,M holds M=F-image p implies f.p=sup M) &
                  (for p,M holds M=F-image p implies g.p=sup M);
        set X = the carrier of P;
        for x st x in X holds f.x = g.x
        proof
          let x;
          assume x in X;
          then reconsider p= x as Element of P;
          reconsider M = F-image p as non empty Chain of Q;
          f.x = sup M by A3 .= g.x by A3;
          hence thesis;
        end;
        hence thesis by FUNCT_2:12;
      end;
      hence thesis;
    end;
end;

Lm22:
  sup_func(F) is monotone
  proof
  reconsider f=sup_func(F) as Function of P,Q;
  for p,p1 st p <= p1 for q,q1 st q = f.p & q1 = f.p1 holds q <= q1
    proof
    let p,p1;
    assume A1:p <= p1;
    for q,q1 st q = f.p & q1 = f.p1 holds q <= q1
    proof
      let q,q1;
      assume A2:q = f.p & q1 = f.p1;
      reconsider X= F-image p as non empty Chain of Q;
      reconsider X1= F-image p1 as non empty Chain of Q;
      A3:ex_sup_of X,Q & ex_sup_of X1,Q by Def1;
      A4:q=sup X by A2,Def10;
      q1=sup X1 by A2,Def10;
      then A5:X1 is_<=_than q1 by A3,YELLOW_0:def 9;
      for x being Element of Q st x in X holds x <= q1
        proof
        let x be Element of Q;
        assume x in X;
        then consider a being Element of Q such that
        A6:x=a & ex g being continuous Function of P,Q st g in F & a=g.p;
        consider g being continuous Function of P,Q such that
        A7: g in F & a=g.p by A6;
        reconsider b=g.p1 as Element of Q;
        A8:a <= b by A1,A7,ORDERS_3:def 5;
        b in X1 by A7;
        then b <= q1 by A5,LATTICE3:def 9;
        hence thesis by A6,A8,ORDERS_2:3;
      end;
      then X is_<=_than q1 by LATTICE3:def 9;
      hence thesis by A3,A4,YELLOW_0:def 9;
      end;
    hence thesis;
    end;
  hence thesis by ORDERS_3:def 5;
  end;

Lm23:
q in M implies q <= sup M
  proof
  assume A1:q in M;
  A2:ex_sup_of M,Q by Def1;
  set x = sup M;
  M is_<=_than x by A2,YELLOW_0:def 9;
  hence thesis by A1,LATTICE3:def 9;
  end;

Lm24:
(for q st q in M holds q<=q1) implies sup M <= q1
proof
  assume for q st q in M holds q<=q1;
  then A1:M is_<=_than q1 by LATTICE3:def 9;
  A2:ex_sup_of M,Q by Def1;
  thus thesis by A2,A1,YELLOW_0:def 9;
end;

Lm25:
  sup_func(F) is continuous
  proof
  reconsider f=sup_func(F) as monotone Function of P,Q by Lm22;
  for L holds f.(sup L) <= sup (f.:L)
    proof
    let L;
    reconsider M1 = f.:L as non empty Chain of Q by Th1;
    set q1 = sup M1;
    set a = sup L;
    set M = F-image a;
    A1:f.a = sup M by Def10;
    for q st q in M holds q <=q1
      proof
      let q;
      assume q in M;
      then consider q0 be Element of Q such that
   A2:q=q0 & ex g being continuous Function of P,Q st g in F & q0=g.a;
      consider g being continuous Function of P,Q such that
  A3: g in F & q0=g.a by A2;
      reconsider M2=g.:L as non empty Chain of Q by Th1;
   A4:q = sup M2 by Th6,A2,A3;
      for q2 st q2 in M2 holds q2 <= q1
      proof
        let q2;
        assume q2 in M2;
        then consider x such that A5: x in dom g & x in L & q2 = g.x
                                            by FUNCT_1:def 6;
        reconsider x as Element of P by A5;
        set Mx=F-image x;
        A6:f.x= sup Mx by Def10;
        set y = f.x;
        x in the carrier of P;
        then x in dom f by FUNCT_2:def 1;
        then y in M1 by A5,FUNCT_1:def 6;
        then A7:y <= q1 by Lm23;
        q2 in F-image x by A5,A3;
        then q2 <= sup Mx by Lm23;
        hence thesis by A7,A6,ORDERS_2:3;
      end;
      hence thesis by A4,Lm24;
    end;
    hence thesis by A1,Lm24;
    end;
  hence thesis by Th8;
  end;

registration let P,Q,F;
  cluster sup_func(F) -> continuous;
  correctness by Lm25;
end;

Lm26:
  sup_func(F) is Element of ConPoset(P,Q)
  proof
    set x = sup_func(F);
A1: x is Element of Funcs(the carrier of P,the carrier of Q) by FUNCT_2:8;
    reconsider x = sup_func(F) as continuous Function of P,Q;
    x in ConFuncs(P,Q) by A1;
    hence thesis;
  end;

Lm27:
for x st x in F holds ex g being continuous Function of P,Q st x=g
  proof
  let x;
  assume x in F;
  then x in ConFuncs(P,Q);
  then consider y be Element of Funcs(the carrier of P,the carrier of Q)
     such that A1:x = y & ex g be continuous Function of P,Q st g=y;
  thus thesis by A1;
  end;

theorem Th11:
  ex_sup_of F, ConPoset(P,Q) & sup_func(F) = "\/"(F,ConPoset(P,Q))
  proof
  set X = ConPoset(P,Q);
  set f1 = sup_func(F);
  reconsider f=f1 as Element of ConPoset(P,Q) by Lm26;
  for x being Element of X st x in F holds x <= f
    proof
    let x be Element of X;
    assume A1:x in F;
    then consider g1 being continuous Function of P,Q such that
A2: x = g1 by Lm27;
    reconsider g = g1 as Element of X by A2;
    for p holds g1.p <= f1.p
    proof
      let p;
      q1=g1.p & q2=f1.p implies q1<=q2
      proof
        assume A3:q1=g1.p & q2=f1.p;
        then A4:q1 in F-image p by A1,A2;
        reconsider M = F-image p as non empty Chain of Q;
        q2 = sup M by Def10,A3;
        hence thesis by A4,Lm23;
      end;
      hence thesis;
    end;
    then g1 <= f1 by YELLOW_2:9;
    then [g,f] in ConRelat(P,Q) by Def7;
    hence thesis by A2,ORDERS_2:def 5;
    end;
   then A5:F is_<=_than f by LATTICE3:def 9;
   for y being Element of X holds F is_<=_than y implies f <= y
    proof
    let y be Element of X;
    y in ConFuncs(P,Q);
    then consider y1 being Element of Funcs(the carrier of P,the carrier of Q)
        such that A6:y = y1 & ex gy be continuous Function of P,Q st gy =y1;
    consider gy being continuous Function of P,Q
        such that A7:gy = y1 by A6;
    F is_<=_than y implies f <= y
      proof
      assume A8:F is_<=_than y;
      for p holds f1.p <= gy.p
        proof
        let p;
        q1=f1.p & q2=gy.p implies q1<=q2
          proof
          assume A9:q1=f1.p & q2=gy.p;
          reconsider M=F-image p as non empty Chain of Q;
          for q st q in M holds q<=q2
            proof
            let q;
            assume q in M;
            then consider a being Element of Q such that
         A10:q=a & ex g being continuous Function of P,Q st g in F & a=g.p;
            consider g be continuous Function of P,Q such that
              A11: g in F & a=g.p by A10;
            reconsider g1 = g as Element of ConPoset(P,Q) by A11;
            g1 <= y by A8,A11,LATTICE3:def 9;
            then [g1,y] in ConRelat(P,Q) by ORDERS_2:def 5;
            then consider g2,g3 being Function of P,Q such that
         A12:g1=g2 & y=g3 & g2 <= g3 by Def7;
            thus thesis by A12,A6,A7,A10,A11,A9,YELLOW_2:9;
            end;
          then sup M <= q2 by Lm24;
          hence thesis by A9,Def10;
          end;
        hence thesis;
        end;
      then f1 <= gy by YELLOW_2:9;
      then [f,y] in ConRelat(P,Q) by A6,A7,Def7;
      hence thesis by ORDERS_2:def 5;
      end;
    hence thesis;
    end;
  hence thesis by A5,YELLOW_0:30;
  end;

definition let P,Q;
  func min_func(P,Q) -> Function of P,Q equals
    P --> Bottom Q;
  coherence;
end;

registration let P,Q;
  cluster min_func(P,Q) -> continuous;
  coherence by Th7;
end;

Lm28:
  min_func(P,Q) is Element of ConPoset(P,Q)
  proof
    reconsider f = min_func(P,Q) as continuous Function of P,Q;
    reconsider x = f as Element of Funcs(the carrier of P,the carrier of Q)
                                                     by FUNCT_2:8;
    x in ConFuncs(P,Q);
    hence thesis;
  end;

theorem Th12:
  for f being Element of ConPoset(P,Q) st f = min_func(P,Q)
    holds f is_<=_than the carrier of ConPoset(P,Q)
proof
  let f be Element of ConPoset(P,Q);
  assume A1:f = min_func(P,Q);
  set f1 = min_func(P,Q);
  for x being Element of ConPoset(P,Q) holds f<=x
    proof
    let x be Element of ConPoset(P,Q);
    x in ConFuncs(P,Q);
    then consider x1 being Element of Funcs(the carrier of P,the carrier of Q)
      such that
A2: x = x1 & ex g be continuous Function of P,Q st g=x1;
    consider g being continuous Function of P,Q such that
A3: g=x1 by A2;
    for p holds f1.p <= g.p
      proof
      let p;
      q1=f1.p & q2=g.p implies q1<=q2
        proof
        assume q1=f1.p & q2=g.p;
        then q1=Bottom Q by FUNCOP_1:7;
        hence thesis by YELLOW_0:44;
        end;
      hence thesis;
      end;
    then f1 <= g by YELLOW_2:9;
    then [f,x] in ConRelat(P,Q) by A2,A3,Def7,A1;
    hence thesis by ORDERS_2:def 5;
  end;
  hence thesis by Lm4;
end;

registration let P,Q;
  cluster ConPoset(P,Q) -> chain-complete;
  coherence
  proof
    set IT = ConPoset(P,Q);
    ex a being Element of IT st a is_<=_than the carrier of IT
    proof
    reconsider a = min_func(P,Q) as Element of ConPoset(P,Q)
      by Lm28;
    take a;
    thus thesis by Th12;
    end; then
A1: IT is lower-bounded by YELLOW_0:def 4;
    for L being Chain of IT st L is non empty holds ex_sup_of L,IT
      by Th11;
    hence thesis by Def1,A1;
  end;
end;

begin

:: 4. Continuity of fix-point function from ConPoset(P,P) to P

Lm29:
  x is Element of ConPoset(P,P) implies x is continuous Function of P,P
proof
  assume x is Element of ConPoset(P,P);
  then x in ConFuncs(P,P);
  then consider y be Element of Funcs(the carrier of P,the carrier of P)
  such that A1:x = y & ex g be continuous Function of P,P st g=y;
  thus thesis by A1;
end;

Lm30:
  g is continuous Function of P,P implies g is Element of ConPoset(P,P)
proof
  assume A1:g is continuous Function of P,P;
  reconsider g1 = g as Element of Funcs(the carrier of P,the carrier of P)
                                  by FUNCT_2:8;
  g1 in ConFuncs (P,P) by A1;
  hence thesis;
end;

definition let P;
  func fix_func(P) -> Function of ConPoset(P,P), P means  :Def12:
    for g being Element of ConPoset(P,P),
        h being continuous Function of P, P st g = h holds
    it.g = least_fix_point h;
  existence
  proof
    set X = the carrier of ConPoset(P,P);
    set Y = the carrier of P;
    defpred U[set,set] means
      for g being Element of ConPoset(P,P),
          h being continuous Function of P, P st
          g = h & g = $1 holds $2 = least_fix_point h;
A1: for x st x in X ex y st y in Y & U[x,y]
    proof
      let x;
      assume x in X;
      then reconsider x as Element of ConPoset(P,P);
      reconsider h = x as continuous Function of P, P by Lm29;
      take least_fix_point h;
      thus thesis;
    end;
    consider IT being Function of X,Y such that
A2: for x st x in X holds U[x,IT.x] from FUNCT_2:sch 1(A1);
    for g being Element of ConPoset(P,P),
        h being continuous Function of P, P st g = h holds
      IT.g = least_fix_point h by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let h1,h2 be Function of ConPoset(P,P),P such that
A3: (for g being Element of ConPoset(P,P),
         h being continuous Function of P, P st g = h holds
        h1.g = least_fix_point h) &
    (for g being Element of ConPoset(P,P),
        h being continuous Function of P, P st g = h holds
        h2.g = least_fix_point h);
    set X = the carrier of ConPoset(P,P);
    for x st x in X holds h1.x = h2.x
    proof
      let x;
      assume x in X;
      then reconsider g = x as Element of ConPoset(P,P);
      reconsider h = g as continuous Function of P, P by Lm29;
      h1.x = least_fix_point h by A3
          .= h2.x by A3;
      hence thesis;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

Lm31:
  for p1,p2 being Element of ConPoset(P,P) st p1 <= p2
    holds (p1 in ConFuncs(P,P) & p2 in ConFuncs(P,P) &
      ex g1,g2 being continuous Function of P,P st
                               p1=g1 & p2=g2 & g1 <= g2)
  proof
    let p1,p2 be Element of ConPoset(P,P);
    assume p1 <= p2;
    then A1:[p1,p2] in ConRelat(P,P) by ORDERS_2:def 5;
    ex g1,g2 being continuous Function of P,P st p1=g1 & p2=g2 & g1 <= g2
    proof
      consider g1,g2 being Function of P,P such that
A2:   p1=g1 & p2=g2 & g1 <= g2 by A1,Def7;
      reconsider h1 = p1, h2 = p2 as continuous Function of P, P
        by Lm29;
      g1 = h1 by A2;
      then reconsider g1 as continuous Function of P, P;
      g2 = h2 by A2;
      then reconsider g2 as continuous Function of P, P;
      take g1,g2;
      thus thesis by A2;
    end;
    hence thesis;
  end;

Lm32:
  fix_func(P) is monotone Function of ConPoset(P,P),P
  proof
    set IT = fix_func(P);
    for p1,p2 being Element of ConPoset(P,P) st p1 <= p2
    for a,b being Element of P
               st a = IT.p1 & b = IT.p2 holds a <= b
    proof
      let p1,p2 be Element of ConPoset(P,P);
      assume A1:p1 <= p2;
      let a, b be Element of P;
      assume A2:a = IT.p1 & b = IT.p2;
      consider g1,g2 being continuous Function of P,P such that
A3:   p1=g1 & p2=g2 & g1 <= g2 by A1,Lm31;
      a = least_fix_point(g1) & b = least_fix_point(g2) by A2,Def12,A3;
      hence thesis by A3,Th10;
    end;
    hence thesis by ORDERS_3:def 5;
  end;

Lm33:
for G being non empty Chain of ConPoset(P,P),n,X,x
    st X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
       & x in X
     holds ex p being Element of P,
              g being continuous Function of P,P
                           st x=p & g in G & p = iter(g,n).(Bottom P)
  proof
  let G be non empty Chain of ConPoset(P,P);
  let n,X,x;
  assume X = {p where p is Element of P : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
         & x in X;
  then consider p be Element of P such that
A1:x=p & ex g being Element of ConPoset(P,P),
            h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P);
  thus thesis by A1;
  end;

Lm34:
for G being non empty Chain of ConPoset(P,P) ,n, X
    st X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
   holds x in X implies x is Element of P
  proof
  let G be non empty Chain of ConPoset(P,P);
  let n,X;
  assume A1:X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)};
  x in X implies x is Element of P
    proof
    assume x in X;
    then consider p being Element of P such that
A2: x=p & ex g being Element of ConPoset(P,P),
             h being continuous Function of P,P
        st h = g & g in G & p = iter(h,n).(Bottom P) by A1;
    thus thesis by A2;
    end;
  hence thesis;
  end;

Lm35:
for G being non empty Chain of ConPoset(P,P), n, X
    st X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
   holds X is non empty Subset of P
  proof
  let G be non empty Chain of ConPoset(P,P);
  let n,X;
  assume A1:X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                  st h = g & g in G & p = iter(h,n).(Bottom P)};
  consider g be set such that A2:g in G by XBOOLE_0:def 1;
  reconsider g as Element of ConPoset(P,P) by A2;
  reconsider gg = g as continuous Function of P,P by Lm29;
  reconsider p = iter(gg,n).(Bottom P) as Element of P by Lm6;
  A3:p in X by A1,A2;
  x in X implies x in the carrier of P
  proof
    assume x in X;
    then x is Element of the carrier of P by Lm34,A1;
    hence thesis;
  end;
  hence thesis by A3,TARSKI:def 3;
end;

Lm36:
for G being non empty Chain of ConPoset(P,P),
    f,g being monotone Function of P,P st f in G & g in G
   holds f <= g or g <= f
  proof
  let G be non empty Chain of ConPoset(P,P);
  let f,g be monotone Function of P,P;
  assume A1: f in G & g in G;
  set S = the InternalRel of ConPoset(P,P);
  A2:S is_strongly_connected_in G by ORDERS_2:def 7;
  per cases by A2,A1,RELAT_2:def 7;
    suppose [f,g] in S;
      then consider f1,g1 being Function of P,P such that
      A3:f=f1 & g=g1 & f1 <= g1 by Def7;
      thus thesis by A3;
    end;
    suppose [g,f] in S;
      then consider g1,f1 being Function of P,P such that
      A4:g=g1 & f=f1 & g1 <= f1 by Def7;
      thus thesis by A4;
    end;
  end;

Lm37:
for G being non empty Chain of ConPoset(P,P) ,n, X
    st X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
   holds X is non empty Chain of P
  proof
  let G be non empty Chain of ConPoset(P,P);
  let n,X;
  assume A1: X = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)};
  set R = the InternalRel of P;
  reconsider X as non empty Subset of P by A1,Lm35;
  x in X & y in X & x <>y implies [x,y] in R or [y,x] in R
    proof
    assume A2:x in X & y in X & x <>y;
    then consider p1 being Element of P,
             g1 being continuous Function of P,P such that
A3: x=p1 & g1 in G & p1 = iter(g1,n).(Bottom P) by A1,Lm33;
    consider p2 being Element of P,
             g2 being continuous Function of P,P such that
A4: y=p2 & g2 in G & p2 = iter(g2,n).(Bottom P) by A1,A2,Lm33;
    per cases by A3,A4,Lm36;
    suppose g1 <= g2;
      then p1 <= p2 by Lm12,A3,A4;
      hence thesis by A3,A4,ORDERS_2:def 5;
    end;
    suppose g2 <= g1;
      then p2 <= p1 by Lm12,A3,A4;
      hence thesis by A3,A4,ORDERS_2:def 5;
    end;
  end;
  then A5:R is_connected_in X by RELAT_2:def 6;
  x in X implies [x,x] in R
    proof
    assume x in X;
    then reconsider x as Element of P;
    x<=x;
    hence thesis by ORDERS_2:def 5;
    end;
  then R is_reflexive_in X by RELAT_2:def 1;
  then R is_strongly_connected_in X by A5,ORDERS_1:7;
  hence thesis by ORDERS_2:def 7;
  end;

Lm38:
  for h being Function of ConPoset(P,P),P,
      G being non empty Chain of ConPoset(P,P),x
     holds x in G implies h.x in h.:G
   proof
   let h be Function of ConPoset(P,P),P;
   let G be non empty Chain of ConPoset(P,P);
   let x;
   assume A1:x in G;
   set X = the carrier of ConPoset(P,P);
   set Y = the carrier of P;
   reconsider h as Function of X,Y;
   x in X by A1; then
   x in dom h by FUNCT_2:def 1;
   hence thesis by A1,FUNCT_1:def 6;
   end;

Lm39:
for g being continuous Function of P,P ,p,p1,n
   holds p = (fix_func(P)).g & p1 = (iter(g,n)).(Bottom P)
                 implies p1 <= p
 proof
   let g be continuous Function of P,P;
   let p,p1,n;
   set a = Bottom P;
   assume A1: p = (fix_func(P)).g & p1 = (iter(g,n)).a;
   then A2:p1 in iterSet(g,a);
   reconsider g1 = g as Element of ConPoset(P,P) by Lm30;
   reconsider G1 = g1 as continuous Function of P,P;
   p = least_fix_point(G1) by Def12,A1
    .= sup iter_min(g) by Th9;
   hence thesis by Lm23,A2;
 end;

Lm40:
for G being non empty Chain of ConPoset(P,P), x being set, n being Nat,
    M being non empty Chain of P,
    g1 being monotone Function of P,P
    st M = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
       & x in g1.:M
   holds ex g being continuous Function of P,P
              st g in G & x = g1.(iter(g,n).(Bottom P))
   proof
   let G be non empty Chain of ConPoset(P,P);
   let x be set;
   let n be Nat;
   let M be non empty Chain of P;
   let g1 be monotone Function of P,P;
   assume A1:M = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n).(Bottom P)}
           & x in g1.:M;
   then ex y st y in dom g1 & y in M & x = g1.y by FUNCT_1:def 6;
   then consider y being Element of M such that
A2:y in M & x = g1.y;
   consider p being Element of P such that
A3:y = p & ex g being Element of ConPoset(P,P),
              h being continuous Function of P,P
     st h = g & g in G & p = iter(h,n).(Bottom P) by A1,A2;
   thus thesis by A2,A3;
   end;

Lm41:
for G being non empty Chain of ConPoset(P,P)
   holds (fix_func(P)).(sup G) <= sup ((fix_func(P)).:G)
   proof
   let G be non empty Chain of ConPoset(P,P);
   reconsider h = fix_func(P) as monotone Function of ConPoset(P,P),P
                                       by Lm32;
   h.(sup G) <= sup (h.:G)
     proof
     reconsider L = h.:G as non empty Chain of P by Th1;
     set g0 = sup G;
     set p0 = h.g0;
     reconsider G0 = g0 as continuous Function of P,P by Lm29;
  A1:p0 = least_fix_point(G0) by Def12;
  A2:sup G = sup_func(G) by Th11;
     then reconsider g0 as continuous Function of P,P;
     set a = Bottom P;
     reconsider I0 = iterSet(g0,a) as non empty Chain of P by Th3;
A3:  p0 = sup iter_min(g0) by Th9,A1
       .= sup I0;
  A4:ex_sup_of I0,P by Def1;
     for x being Element of P st x in I0 holds x <= sup L
       proof
       let x be Element of P;
       assume x in I0;
       then consider y being Element of P such that
   A5: x=y & ex n being Nat st y = iter(g0,n).a;
       consider n0 being Nat such that A6:x = iter(g0,n0).a by A5;
       set M0 = {p where p is Element of P
                  : ex g being Element of ConPoset(P,P),
                       h being continuous Function of P,P
                     st h = g & g in G & p = iter(h,n0).a};
       reconsider M0 as non empty Chain of P by Lm37;
       for p st p in M0 holds p <= sup L
         proof
         let p;
         assume p in M0;
         then consider p0 being Element of P,
         g being continuous Function of P,P such that
A7:      p=p0 & g in G & p0 = iter(g,n0).a by Lm33;
         set r = h.g;
         r in L by A7,Lm38;
         then reconsider r as Element of P;
      A8:r <= sup L by Lm23,A7,Lm38;
         p <= r by A7,Lm39;
         hence thesis by A8,ORDERS_2:3;
         end; then
     A9: sup M0 <= sup L by Lm24;
       defpred U[Nat] means
          for z being Element of P,M being non empty Chain of P
            st z = iter(g0,$1).a &
               M = {p where p is Element of P
                     :ex g being Element of ConPoset(P,P),
                         h being continuous Function of P,P
                        st h = g & g in G & p = iter(h,$1).a}
                holds z <= sup M;
       A10:U[0]
         proof
         let z be Element of P;
         let M be non empty Chain of P;
         assume z = iter(g0,0).a;
         then z = a by Lm5;
         hence thesis by YELLOW_0:44;
         end;
       A11: U[k] implies U[k+1]
         proof
         assume A12:U[k];
         for z1 being Element of P,M1 being non empty Chain of P
            st z1 = iter(g0,k+1).a &
               M1 = {p where p is Element of P
                     :ex g being Element of ConPoset(P,P),
                         h being continuous Function of P,P
                        st h = g & g in G & p = iter(h,k+1).a}
              holds z1 <= sup M1
           proof
           let z1 be Element of P;
           let M1 be non empty Chain of P;
           assume
        A13:z1 = iter(g0,k+1).a & M1 = {p where p is Element of P
                     :ex g being Element of ConPoset(P,P),
                         h being continuous Function of P,P
                        st h = g & g in G & p = iter(h,k+1).a};
            reconsider z = iter(g0,k).a as Element of P by Lm6;
            A14:z1 = (g0*iter(g0,k)).a by A13,FUNCT_7:71
                 .= g0.z by Lm7;
            reconsider M = {p where p is Element of P
                     :ex g being Element of ConPoset(P,P),
                         h being continuous Function of P,P
                        st h = g & g in G & p = iter(h,k).a}
                             as non empty Chain of P by Lm37;
            reconsider M0 = g0.:M as non empty Chain of P by Th1;
            A15:g0.(sup M) = sup M0 by Th6;
            A16:ex_sup_of M0,P by Def1;
            for q being Element of P st q in M0 holds q <= sup M1
              proof
              let q be Element of P;
              assume q in M0;
              then consider g being continuous Function of P,P such that
          A17: g in G & q = g0.(iter(g,k).a) by Lm40;
              reconsider a1 = iter(g,k).a as Element of P by Lm6;
              reconsider W = G-image a1 as non empty Chain of P;
              A18:q = sup W by A17,Def10,A2;
              A19:ex_sup_of W,P by Def1;
              for q1 being Element of P st q1 in W holds q1 <= sup M1
                proof
                let q1 be Element of P;
                assume q1 in W;
                then consider q2 being Element of P such that
           A20:q1 = q2 & ex g1 being continuous Function of P,P
                st g1 in G & q2=g1.a1;
                consider g1 be continuous Function of P,P
                such that A21:g1 in G & q1=g1.a1 by A20;
                per cases by A17,A21,Lm36;
                  suppose g1 <= g;
                  then A22:q1 <= g.a1 by A21,YELLOW_2:9;
                  set a2 = g.a1;
                  reconsider g2 = g as Element of ConPoset(P,P)
                                          by Lm30;
                  reconsider gg = g2 as continuous Function of P,P;
                  a2 = (g*iter(g,k)).a by Lm7
                    .= iter(gg,k+1).a by FUNCT_7:71;
                  then a2 in M1 by A13,A17;
                  then a2 <= sup M1 by Lm23;
                  hence thesis by A22,ORDERS_2:3;
                  end;
                  suppose A23:g <= g1;
                  reconsider a2 = iter(g1,k).a as Element of P by Lm6;
                  a1 <= a2 by A23,Lm12;
                  then A24:q1 <= g1.a2 by A21,ORDERS_3:def 5;
                  set a3 = g1.a2;
                  reconsider g2 = g1 as Element of ConPoset(P,P)
                                          by Lm30;
                  reconsider gg = g2 as continuous Function of P,P;
                  a3 = (g1*iter(g1,k)).a by Lm7
                    .= iter(gg,k+1).a by FUNCT_7:71;
                  then a3 in M1 by A13,A21;
                  then a3 <= sup M1 by Lm23;
                  hence thesis by A24,ORDERS_2:3;
                  end;
                end;
              then W is_<=_than sup M1 by LATTICE3:def 9;
              hence thesis by A18,A19,YELLOW_0:def 9;
              end;
            then M0 is_<=_than sup M1 by LATTICE3:def 9;
            then A25:sup M0 <= sup M1 by A16,YELLOW_0:def 9;
            z <= sup M by A12;
            then z1 <= sup M0 by A14,A15,ORDERS_3:def 5;
            hence thesis by A25,ORDERS_2:3;
            end;
         hence thesis;
         end;
       U[k] from NAT_1:sch 2(A10,A11);
       then x <= sup M0 by A6;
       hence thesis by A9,ORDERS_2:3;
       end;
     then I0 is_<=_than sup L by LATTICE3:def 9;
     hence thesis by A3,A4,YELLOW_0:def 9;
     end;
   hence thesis;
   end;

registration let P;
  cluster fix_func(P) -> continuous;
  coherence
  proof
    reconsider f = fix_func(P) as monotone Function of ConPoset(P,P),P
      by Lm32;
    for L be non empty Chain of ConPoset(P,P)
      holds f.(sup L) <= sup (f.:L) by Lm41;
    hence thesis by Th8;
  end;
end;