:: Fix-points in complete lattices
::  by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 16, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, XBOOLE_0, RELAT_1, FUNCT_4, SUBSET_1, NUMBERS, ABIAN,
      FUNCT_7, ARYTM_3, COHSP_1, TARSKI, FUNCOP_1, ZFMISC_1, SETFAM_1, FUNCT_2,
      LATTICES, STRUCT_0, ORDINAL1, ORDINAL2, EQREL_1, CARD_1, BINOP_1,
      LATTICE3, PBOOLE, FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1,
      ORDERS_2, XXREAL_0, REWRITE1, XXREAL_2, SEQM_3, KNASTER;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, NUMBERS, ORDINAL1,
      NAT_1, RELAT_1, RELAT_2, ORDERS_1, STRUCT_0, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, BINOP_1, FUNCOP_1, SETFAM_1, FUNCT_4, WELLORD1, ORDINAL2,
      COHSP_1, LATTICES, LATTICE3, QUANTAL1, ORDERS_2, ABIAN;
 constructors WELLORD1, WELLORD2, BINOP_1, DOMAIN_1, ORDINAL2, NAT_1, ABIAN,
      BOOLEALG, QUANTAL1, COHSP_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, CARD_1,
      STRUCT_0, LATTICES, LATTICE3, QUANTAL1;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, RELAT_1, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0,
      ABIAN, WELLORD1;
 theorems TARSKI, SETFAM_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_2,
      FUNCT_4, CARD_1, COHSP_1, LATTICES, LATTICE3, QUANTAL1, FILTER_0,
      FILTER_1, BOOLEALG, WELLORD1, RELSET_1, ORDERS_2, RELAT_2, ORDINAL1,
      CARD_3, XBOOLE_0, XBOOLE_1, FUNCT_7, PARTFUN1, ORDERS_1, ABIAN, NAT_1;
 schemes NAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, ORDINAL2;

begin :: Preliminaries

reserve f, g, h for Function;

theorem
  h = f \/ g & dom f misses dom g implies (h is one-to-one iff f is
  one-to-one & g is one-to-one & rng f misses rng g)
proof
  assume that
A1: h = f \/ g and
A2: dom f misses dom g;
A3: dom h = dom f \/ dom g by A1,RELAT_1:1;
  hereby
    assume
A4: h is one-to-one;
    thus f is one-to-one
    proof
      assume not f is one-to-one;
      then consider x1, x2 being set such that
A5:   x1 in dom f and
A6:   x2 in dom f and
A7:   f.x1 = f.x2 & x1<>x2 by FUNCT_1:def 4;
A8:   x2 in dom h by A3,A6,XBOOLE_0:def 3;
      [x2, f.x2] in f by A6,FUNCT_1:def 2;
      then [x2, f.x2] in h by A1,XBOOLE_0:def 3;
      then
A9:   f.x2 = h.x2 by A8,FUNCT_1:def 2;
A10:  x1 in dom h by A3,A5,XBOOLE_0:def 3;
      [x1, f.x1] in f by A5,FUNCT_1:def 2;
      then [x1, f.x1] in h by A1,XBOOLE_0:def 3;
      then f.x1 = h.x1 by A10,FUNCT_1:def 2;
      hence contradiction by A4,A7,A10,A8,A9,FUNCT_1:def 4;
    end;
    thus g is one-to-one
    proof
      assume not g is one-to-one;
      then consider x1, x2 being set such that
A11:  x1 in dom g and
A12:  x2 in dom g and
A13:  g.x1 = g.x2 & x1<>x2 by FUNCT_1:def 4;
A14:  x2 in dom h by A3,A12,XBOOLE_0:def 3;
      [x2, g.x2] in g by A12,FUNCT_1:def 2;
      then [x2, g.x2] in h by A1,XBOOLE_0:def 3;
      then
A15:  g.x2 = h.x2 by A14,FUNCT_1:def 2;
A16:  x1 in dom h by A3,A11,XBOOLE_0:def 3;
      [x1, g.x1] in g by A11,FUNCT_1:def 2;
      then [x1, g.x1] in h by A1,XBOOLE_0:def 3;
      then g.x1 = h.x1 by A16,FUNCT_1:def 2;
      hence contradiction by A4,A13,A16,A14,A15,FUNCT_1:def 4;
    end;
    thus rng f misses rng g
    proof
      assume not thesis;
      then consider hx being set such that
A17:  hx in rng f and
A18:  hx in rng g by XBOOLE_0:3;
      consider x1 being set such that
A19:  x1 in dom f and
A20:  hx = f.x1 by A17,FUNCT_1:def 3;
A21:  x1 in dom h by A3,A19,XBOOLE_0:def 3;
      consider x2 being set such that
A22:  x2 in dom g and
A23:  hx = g.x2 by A18,FUNCT_1:def 3;
A24:  x2 in dom h by A3,A22,XBOOLE_0:def 3;
      [x2, hx] in g by A22,A23,FUNCT_1:def 2;
      then [x2, hx] in h by A1,XBOOLE_0:def 3;
      then
A25:  h.x2 = hx by A24,FUNCT_1:def 2;
A26:  x1 <> x2 by A2,A19,A22,XBOOLE_0:3;
      [x1, hx] in f by A19,A20,FUNCT_1:def 2;
      then [x1, hx] in h by A1,XBOOLE_0:def 3;
      then h.x1 = hx by A21,FUNCT_1:def 2;
      hence contradiction by A4,A26,A21,A24,A25,FUNCT_1:def 4;
    end;
  end;
  assume
A27: f is one-to-one & g is one-to-one & rng f misses rng g;
  f \/ g = f+*g by A2,FUNCT_4:31;
  hence thesis by A1,A27,FUNCT_4:92;
end;

begin :: Fix points in general

reserve x, y, z, u, X for set,
  A for non empty set,
  n for Element of NAT,
  f for Function of X, X;

theorem Th2:
  x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f, n)
proof
  assume
A1: x is_a_fixpoint_of iter(f,n);
  then
A2: x in dom iter(f, n) by ABIAN:def 3;
A3: dom f = X by FUNCT_2:52;
  then dom iter(f, n) = X & f.x in rng f by A2,FUNCT_1:def 3,FUNCT_2:52;
  hence f.x in dom iter(f, n);
  x = iter(f, n).x by A1,ABIAN:def 3;
  hence f.x = (f*iter(f, n)).x by A2,FUNCT_1:13
    .= iter(f, n+1).x by FUNCT_7:71
    .= (iter(f, n)*f).x by FUNCT_7:69
    .= iter(f, n).(f.x) by A2,A3,FUNCT_1:13;
end;

theorem
  (ex n st x is_a_fixpoint_of iter(f,n) & for y st y is_a_fixpoint_of
  iter(f,n) holds x = y) implies x is_a_fixpoint_of f
proof
  given n such that
A1: x is_a_fixpoint_of iter(f, n) and
A2: for y st y is_a_fixpoint_of iter(f,n) holds x = y;
  dom f = X & dom iter(f, n) = X by FUNCT_2:52;
  hence x in dom f by A1,ABIAN:def 3;
  thus thesis by A1,A2,Th2;
end;

definition
  let A, B be non empty set, f be Function of A, B;

  redefine attr f is c=-monotone means
  :Def1:
  for x, y being Element of A st x c= y holds f.x c= f.y;
  compatibility
  proof
    dom f = A by FUNCT_2:def 1;
    hence f is c=-monotone implies for x, y being Element of A st x c= y holds
    f.x c= f.y by COHSP_1:def 11;
    assume
A1: for x, y being Element of A st x c= y holds f.x c= f.y;
    let x, y be set;
    assume x in dom f & y in dom f & x c= y;
    hence thesis by A1;
  end;
end;

registration
  let A be set, B be non empty set;
  cluster c=-monotone for Function of A, B;
  existence
  proof
    set b = the Element of B;
    reconsider f = A --> b as Function of A, B;
    take f;
    let x, y be set;
    assume that
A1: x in dom f and
A2: y in dom f and
    x c= y;
    f.x = b by A1,FUNCOP_1:7
      .= f.y by A2,FUNCOP_1:7;
    hence thesis;
  end;
end;

definition
  let X be set;
  let f be c=-monotone Function of bool X, bool X;
  func lfp (X, f) -> Subset of X equals
  meet {h where h is Subset of X : f.h c= h};
  coherence
  proof
    defpred P[set] means f.$1 c= $1;
    reconsider H = {h where h is Subset of X : P[h] } as Subset-Family of X
    from DOMAIN_1:sch 7;
    reconsider H as Subset-Family of X;
    meet H is Subset of X;
    hence thesis;
  end;
  func gfp (X, f) -> Subset of X equals
  union {h where h is Subset of X : h c= f.h };
  coherence
  proof
    defpred P[set] means $1 c= f.$1;
    reconsider H = {h where h is Subset of X : P[h] } as Subset-Family of X
    from DOMAIN_1:sch 7;
    union H is Subset of X;
    hence thesis;
  end;
end;

reserve f for c=-monotone Function of bool X, bool X,
  S for Subset of X;

theorem Th4:
  lfp(X, f) is_a_fixpoint_of f
proof
  defpred P[set] means f.$1 c= $1;
  reconsider H = { h where h is Subset of X : P[h] } as Subset-Family of X
  from DOMAIN_1:sch 7;
  reconsider H as Subset-Family of X;
  set A = meet H;
  now
    X c= X;
    then reconsider X9 = X as Subset of X;
    f.X9 c= X9;
    then X9 in H;
    hence H <> {};
    let h be set;
    assume
A1: h in H;
    then consider x being Subset of X such that
A2: x = h and
A3: f.x c= x;
    A c= h by A1,SETFAM_1:3;
    then f.A c= f.x by A2,Def1;
    hence f.A c= h by A2,A3,XBOOLE_1:1;
  end;
  then
A4: f.A c= A by SETFAM_1:5;
  then f.(f.A) c= f.A by Def1;
  then f.A in H;
  then A c= f.A by SETFAM_1:3;
  hence f.(lfp(X,f)) = lfp(X,f) by A4,XBOOLE_0:def 10;
end;

theorem Th5:
  gfp(X, f) is_a_fixpoint_of f
proof
  defpred P[set] means $1 c= f.$1;
  reconsider H = { h where h is Subset of X : P[h] } as Subset-Family of X
  from DOMAIN_1:sch 7;
  set A = union H;
  now
    let x be set;
    assume
A1: x in H;
    then consider h being Subset of X such that
A2: x = h and
A3: h c= f.h;
    h c= A by A1,A2,ZFMISC_1:74;
    then f.h c= f.A by Def1;
    hence x c= f.A by A2,A3,XBOOLE_1:1;
  end;
  then
A4: A c= f.A by ZFMISC_1:76;
  then f.A c= f.(f.A) by Def1;
  then f.A in H;
  then f.A c= A by ZFMISC_1:74;
  hence f.(gfp (X,f)) = gfp(X,f) by A4,XBOOLE_0:def 10;
end;

theorem Th6:
  f.S c= S implies lfp(X,f) c= S
proof
  set H = {h where h is Subset of X : f.h c= h };
  assume f.S c= S;
  then S in H;
  hence thesis by SETFAM_1:3;
end;

theorem Th7:
  S c= f.S implies S c= gfp(X,f)
proof
  set H = {h where h is Subset of X : h c= f.h };
  assume S c= f.S;
  then S in H;
  hence thesis by ZFMISC_1:74;
end;

theorem Th8:
  S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f)
proof
  assume S = f.S;
  hence thesis by Th6,Th7;
end;

::$N Knaster Theorem
scheme
  Knaster{A() -> set, F(set) -> set}: ex D being set st F(D) = D & D c= A()
provided
A1: for X, Y being set st X c= Y holds F(X) c= F(Y) and
A2: F(A()) c= A()
proof
  consider f being Function such that
A3: dom f = bool A() & for x being set st x in bool A() holds f.x = F(x)
  from FUNCT_1:sch 3;
  rng f c= bool A()
  proof
    let x be set;
    assume x in rng f;
    then consider y being set such that
A4: y in dom f and
A5: x = f.y by FUNCT_1:def 3;
    F(y) c= F(A()) by A1,A3,A4;
    then F(y) c= A() by A2,XBOOLE_1:1;
    then f.y c= A() by A3,A4;
    hence thesis by A5;
  end;
  then reconsider f as Function of bool A(), bool A() by A3,FUNCT_2:def 1
,RELSET_1:4;
  now
    let a, b be set;
    assume that
A6: a in dom f & b in dom f and
A7: a c= b;
    f.a = F(a) & f.b = F(b) by A3,A6;
    hence f.a c= f.b by A1,A7;
  end;
  then reconsider f as c=-monotone Function of bool A(), bool A() by
COHSP_1:def 11;
  take d = lfp(A(), f);
  d is_a_fixpoint_of f by Th4;
  then d = f.d by ABIAN:def 3;
  hence F(d) = d by A3;
  thus thesis;
end;

reserve X, Y for non empty set,
  f for Function of X, Y,
  g for Function of Y, X;

:: Banach decomposition

theorem Th9:
  ex Xa, Xb, Ya, Yb being set st Xa misses Xb & Ya misses Yb & Xa
  \/ Xb = X & Ya \/ Yb = Y & f.:Xa = Ya & g.:Yb = Xb
proof
  deffunc F(set)=X\g.:(Y\f.:$1);
A1: for x being set st x in bool X holds F(x) in bool X;
  consider h being Function of bool X, bool X such that
A2: for x being set st x in bool X holds h.x =F(x) from FUNCT_2:sch 2(A1);
  now
    let x, y be set;
    assume that
A3: x in dom h and
A4: y in dom h and
A5: x c= y;
    f.:x c= f.:y by A5,RELAT_1:123;
    then Y \ f.:y c= Y \ f.:x by XBOOLE_1:34;
    then g.:(Y \ f.:y) c= g.:(Y \ f.:x) by RELAT_1:123;
    then X \ g.:(Y \ f.:x) c= X \ g.:(Y \ f.:y) by XBOOLE_1:34;
    then h.x c= X \ g.:(Y \ f.:y) by A2,A3;
    hence h.x c= h.y by A2,A4;
  end;
  then reconsider h as c=-monotone Function of bool X, bool X by COHSP_1:def 11
;
  take Xa = lfp (X, h);
  take Xb = X \ Xa;
  take Ya = f.:Xa;
  take Yb = Y \ Ya;
  thus Xa misses Xb by XBOOLE_1:79;
  thus Ya misses Yb by XBOOLE_1:79;
  thus Xa \/ Xb = X by XBOOLE_1:45;
  thus Ya \/ Yb = Y by XBOOLE_1:45;
  thus f.:Xa = Ya;
A6: Xa is_a_fixpoint_of h by Th4;
  thus g.:Yb = X/\g.:(Y\f.:Xa) by XBOOLE_1:28
    .= X\(X\g.:(Y\f.:Xa)) by XBOOLE_1:48
    .= X\h.Xa by A2
    .= Xb by A6,ABIAN:def 3;
end;

::$N Schroeder Bernstein theorem
theorem Th10:
  for X, Y being non empty set,
      f being Function of X, Y,
      g being Function of Y, X st
    f is one-to-one & g is one-to-one holds
   ex h being Function of X,Y st h is bijective
proof
  let X, Y be non empty set,
      f be Function of X, Y,
      g be Function of Y, X;
  assume that
A1: f is one-to-one and
A2: g is one-to-one;
  consider Xa, Xb, Ya, Yb being set such that
A3: Xa misses Xb and
A4: Ya misses Yb and
A5: Xa \/ Xb = X and
A6: Ya \/ Yb = Y and
A7: f.:Xa = Ya and
A8: g.:Yb = Xb by Th9;
  set gYb = g|Yb;
A9: gYb is one-to-one by A2,FUNCT_1:52;
  set fXa = f|Xa;
  dom f = X by FUNCT_2:def 1;
  then
A10: dom fXa = Xa by A5,RELAT_1:62,XBOOLE_1:7;
  set h = fXa+*gYb";
  rng gYb = Xb by A8,RELAT_1:115;
  then
A11: dom (gYb") = Xb by A9,FUNCT_1:32;
  then
A12: X = dom h by A5,A10,FUNCT_4:def 1;
A13: rng fXa = Ya by A7,RELAT_1:115;
  dom g = Y by FUNCT_2:def 1;
  then dom gYb = Yb by A6,RELAT_1:62,XBOOLE_1:7;
  then
A14: rng (gYb") = Yb by A9,FUNCT_1:33;
  fXa \/ gYb" = h by A3,A10,A11,FUNCT_4:31;
  then
A15: rng h = Y by A6,A13,A14,RELAT_1:12;
  then reconsider h as Function of X, Y by A12,FUNCT_2:def 1,RELSET_1:4;
A16: h is onto by A15,FUNCT_2:def 3;
  take h;
  fXa is one-to-one by A1,FUNCT_1:52;
  then h is one-to-one by A4,A13,A9,A14,FUNCT_4:92;
  hence thesis by A16,FUNCT_2:def 4;
end;

theorem Th11: ::: EULER_1:12
  f is bijective implies X,Y are_equipotent
proof
  assume
A1: f is bijective;
  take h = f;
A2: h is one-to-one onto by A1,FUNCT_2:def 4;
  then
A3: rng h = Y by FUNCT_2:def 3;
  hereby
    let x;
    assume
A4: x in X;
    take y = h.x;
    thus y in Y by A3,A4,FUNCT_2:4;
    x in dom h by A4,FUNCT_2:def 1;
    hence [x,y] in h by FUNCT_1:1;
  end;
  hereby
    let y;
    assume y in Y;
    then consider x such that
A5: x in dom h & y = h.x by A3,FUNCT_1:def 3;
    take x;
    thus x in X & [x,y] in h by A5,FUNCT_1:1;
  end;
  let x,y,z,u;
  assume that
A6: [x,y] in h and
A7: [z,u] in h;
A8: z in dom h & u = h.z by A7,FUNCT_1:1;
  x in dom h & y = h.x by A6,FUNCT_1:1;
  hence thesis by A2,A8,FUNCT_1:def 4;
end;

theorem
  f is one-to-one & g is one-to-one implies X,Y are_equipotent
proof
  assume f is one-to-one & g is one-to-one;
  then ex h being Function of X,Y st h is bijective by Th10;
  hence thesis by Th11;
end;

begin :: The lattice of a lattice subset

definition
  let L be Lattice, f be Function of the carrier of L, the carrier of L, x be
  Element of L, O be Ordinal;
  func (f, O)+.x means
  :Def4:
  ex L0 being T-Sequence st it = last L0 & dom L0
= succ O & L0.{} = x & (for C being Ordinal st succ C in succ O holds L0.succ C
= f.(L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal
  holds L0.C = "\/"(rng(L0|C), L);
  correctness
  proof
    deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
    deffunc C(Ordinal,set)=f.$2;
    (ex z being set,S being T-Sequence st z = last S & dom S = succ O & S.
{} = x & (for C being Ordinal st succ C in succ O holds S.succ C = C(C,S.C)) &
for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds S.C = D
(C,S|C) ) & for x1,x2 being set st (ex L0 being T-Sequence st x1 = last L0 &
dom L0 = succ O & L0.{} = x & (for C being Ordinal st succ C in succ O holds L0
    .succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is
limit_ordinal holds L0.C = D(C,L0|C) ) & (ex L0 being T-Sequence st x2 = last
    L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal st succ C in succ O
holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C
is limit_ordinal holds L0.C = D(C,L0|C) ) holds x1 = x2 from ORDINAL2:sch 7;
    hence thesis;
  end;
  func (f, O)-.x means
  :Def5:
  ex L0 being T-Sequence st it = last L0 & dom L0
= succ O & L0.{} = x & (for C being Ordinal st succ C in succ O holds L0.succ C
= f.(L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal
  holds L0.C = "/\"(rng(L0|C) , L);
  correctness
  proof
    deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
    deffunc C(Ordinal,set)=f.$2;
    (ex z being set,S being T-Sequence st z = last S & dom S = succ O & S.
{} = x & (for C being Ordinal st succ C in succ O holds S.succ C = C(C,S.C)) &
for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds S.C = D
(C,S|C) ) & for x1,x2 being set st (ex L0 being T-Sequence st x1 = last L0 &
dom L0 = succ O & L0.{} = x & (for C being Ordinal st succ C in succ O holds L0
    .succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is
limit_ordinal holds L0.C = D(C,L0|C) ) & (ex L0 being T-Sequence st x2 = last
    L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal st succ C in succ O
holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in succ O & C <> {} & C
is limit_ordinal holds L0.C = D(C,L0|C) ) holds x1 = x2 from ORDINAL2:sch 7;
    hence thesis;
  end;
end;

reserve L for Lattice,
  f for Function of the carrier of L, the carrier of L,
  x for Element of L,
  O, O1, O2, O3, O4 for Ordinal,
  T for T-Sequence;

theorem Th13:
  (f, {})+.x = x
proof
  deffunc C(Ordinal,set)=f.$2;
  deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
  deffunc F(Ordinal)=(f, $1)+.x;
A1: for O being Ordinal, y being set holds y = F(O) iff ex L0 being
T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
  succ O & C <> {} & C is limit_ordinal holds L0.C = D(C,L0|C) by Def4;
  thus F({}) = x from ORDINAL2:sch 8(A1);
end;

theorem Th14:
  (f, {})-.x = x
proof
  deffunc C(Ordinal,set)=f.$2;
  deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
  deffunc F(Ordinal)=(f, $1)-.x;
A1: for O being Ordinal, y being set holds y = F(O) iff ex L0 being
T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
  succ O & C <> {} & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
  thus F({}) = x from ORDINAL2:sch 8(A1);
end;

theorem Th15:
  (f, succ O)+.x = f.(f, O)+.x
proof
  deffunc C(Ordinal,set)=f.$2;
  deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
  deffunc F(Ordinal)=(f, $1)+.x;
A1: for O being Ordinal, y being set holds y = F(O) iff ex L0 being
T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
  succ O & C <> {} & C is limit_ordinal holds L0.C = D(C,L0|C) by Def4;
  for O being Ordinal holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9( A1);
  hence thesis;
end;

theorem Th16:
  (f, succ O)-.x = f.(f, O)-.x
proof
  deffunc C(Ordinal,set)=f.$2;
  deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
  deffunc F(Ordinal)=(f, $1)-.x;
A1: for O being Ordinal, y being set holds y = F(O) iff ex L0 being
T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
  succ O & C <> {} & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
  for O being Ordinal holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9( A1);
  hence thesis;
end;

theorem Th17:
  O <> {} & O is limit_ordinal & dom T = O & (for A being Ordinal
  st A in O holds T.A = (f, A)+.x) implies (f, O)+.x = "\/"(rng T, L)
proof
  deffunc C(Ordinal,set)=f.$2;
  deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);
  deffunc F(Ordinal)=(f, $1)+.x;
  assume that
A1: O <> {} & O is limit_ordinal and
A2: dom T = O and
A3: for A being Ordinal st A in O holds T.A = F(A);
A4: for O being Ordinal, y being set holds y = F(O) iff ex L0 being
T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
  succ O & C <> {} & C is limit_ordinal holds L0.C = D(C,L0|C) by Def4;
  thus F(O) = D(O,T) from ORDINAL2:sch 10(A4, A1, A2, A3);
end;

theorem Th18:
  O <> {} & O is limit_ordinal & dom T = O & (for A being Ordinal
  st A in O holds T.A = (f, A)-.x) implies (f, O)-.x = "/\"(rng T, L)
proof
  deffunc C(Ordinal,set)=f.$2;
  deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);
  deffunc F(Ordinal)=(f, $1)-.x;
  assume that
A1: O <> {} & O is limit_ordinal and
A2: dom T = O and
A3: for A being Ordinal st A in O holds T.A = F(A);
A4: for O being Ordinal, y being set holds y = F(O) iff ex L0 being
T-Sequence st y = last L0 & dom L0 = succ O & L0.{} = x & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
  succ O & C <> {} & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
  thus F(O) = D(O,T) from ORDINAL2:sch 10(A4, A1, A2, A3);
end;

theorem
  iter(f, n).x = (f, n)+.x
proof
  defpred P[Element of NAT] means iter(f, $1).x = (f, $1)+.x;
A1: dom f = the carrier of L by FUNCT_2:def 1;
  then
A2: x in field f by XBOOLE_0:def 3;
A3: now
    let n be Element of NAT;
    assume
A4: P[n];
    rng f c= the carrier of L;
    then
A5: dom iter(f, n) = dom f by A1,FUNCT_7:74;
    iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:71
      .= f.(f, n)+.x by A1,A4,A5,FUNCT_1:13
      .= (f, succ n)+.x by Th15
      .= (f, n+1)+.x by NAT_1:38;
    hence P[n+1];
  end;
  iter(f, 0).x = id(field f).x by FUNCT_7:68
    .= x by A2,FUNCT_1:18
    .= (f, 0)+.x by Th13;
  then
A6: P[ 0 ];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A6, A3);
  hence thesis;
end;

theorem
  iter(f, n).x = (f, n)-.x
proof
  defpred P[Element of NAT] means iter(f, $1).x = (f, $1)-.x;
A1: dom f = the carrier of L by FUNCT_2:def 1;
  then
A2: x in field f by XBOOLE_0:def 3;
A3: now
    let n be Element of NAT;
    assume
A4: P[n];
    rng f c= the carrier of L;
    then
A5: dom iter(f, n) = dom f by A1,FUNCT_7:74;
    iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:71
      .= f.(f, n)-.x by A1,A4,A5,FUNCT_1:13
      .= (f, succ n)-.x by Th16
      .= (f, n+1)-.x by NAT_1:38;
    hence P[n+1];
  end;
  iter(f, 0).x = id(field f).x by FUNCT_7:68
    .= x by A2,FUNCT_1:18
    .= (f, 0)-.x by Th14;
  then
A6: P[ 0 ];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A6, A3);
  hence thesis;
end;

definition
  let L be Lattice, f be (UnOp of the carrier of L), a be Element of L, O be
  Ordinal;
  redefine func (f, O)+.a -> Element of L;
  coherence
  proof
    deffunc F(Ordinal)=(f, $1)+.a;
    defpred P[Ordinal] means (f, $1)+.a is Element of L;
A1: now
      let O1;
      assume P[O1];
      then reconsider fa = (f, O1)+.a as Element of L;
      f.fa = (f, succ O1)+.a by Th15;
      hence P[succ O1];
    end;
A2: now
      let O1;
      assume that
A3:   O1 <> {} & O1 is limit_ordinal and
      for O2 st O2 in O1 holds P[O2];
      consider Ls being T-Sequence such that
A4:   dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(
      O2) from ORDINAL2:sch 2;
      (f, O1)+.a = "\/"(rng Ls, L) by A3,A4,Th17;
      hence P[O1];
    end;
A5: P[{}] by Th13;
    for O holds P[O] from ORDINAL2:sch 1(A5, A1, A2);
    hence thesis;
  end;
end;

definition
  let L be Lattice, f be (UnOp of the carrier of L), a be Element of L, O be
  Ordinal;
  redefine func (f, O)-.a -> Element of L;
  coherence
  proof
    deffunc F(Ordinal)=(f, $1)-.a;
    defpred P[Ordinal] means (f, $1)-.a is Element of L;
A1: now
      let O1;
      assume P[O1];
      then reconsider fa = (f, O1)-.a as Element of L;
      f.fa = (f, succ O1)-.a by Th16;
      hence P[succ O1];
    end;
A2: now
      let O1;
      assume that
A3:   O1 <> {} & O1 is limit_ordinal and
      for O2 st O2 in O1 holds P[O2];
      consider Ls being T-Sequence such that
A4:   dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 =F(O2
      ) from ORDINAL2:sch 2;
      (f, O1)-.a = "/\"(rng Ls, L) by A3,A4,Th18;
      hence P[O1];
    end;
A5: P[{}] by Th14;
    for O holds P[O] from ORDINAL2:sch 1(A5, A1, A2);
    hence thesis;
  end;
end;

definition
  let L be non empty LattStr, P be Subset of L;
  attr P is with_suprema means
  :Def6:
  for x,y being Element of L st x in P & y
in P ex z being Element of L st z in P & x [= z & y [= z & for z9 being Element
  of L st z9 in P & x [= z9 & y [= z9 holds z [= z9;
  attr P is with_infima means
  :Def7:
  for x,y being Element of L st x in P & y
in P ex z being Element of L st z in P & z [= x & z [= y & for z9 being Element
  of L st z9 in P & z9 [= x & z9 [= y holds z9 [= z;
end;

registration
  let L be Lattice;
  cluster non empty with_suprema with_infima for Subset of L;
  existence
  proof
    the carrier of L c= the carrier of L;
    then reconsider P = the carrier of L as Subset of L;
    take P;
    thus P is non empty;
    thus P is with_suprema
    proof
      let x,y be Element of L such that
      x in P and
      y in P;
      take z = x"\/"y;
      thus z in P;
      thus x [= z & y [= z by LATTICES:5;
      let z9 be Element of L;
      assume that
      z9 in P and
A1:   x [= z9 & y [= z9;
      thus z [= z9 by A1,BOOLEALG:5;
    end;
    let x,y be Element of L such that
    x in P and
    y in P;
    take z = x"/\"y;
    thus z in P;
    thus z [= x & z [= y by LATTICES:6;
    let z9 be Element of L;
    assume that
    z9 in P and
A2: z9 [= x & z9 [= y;
    thus z9 [= z by A2,BOOLEALG:6;
  end;
end;

definition
  let L be Lattice, P be non empty with_suprema with_infima Subset of L;
  func latt P -> strict Lattice means
  :Def8:
  the carrier of it = P & for x, y
  being Element of it ex x9, y9 being Element of L st x = x9 & y = y9 & (x [= y
  iff x9 [= y9);
  existence
  proof
    set cL = the carrier of L;
    set LL = LattRel L;
    set LR = LL|_2 P;
    reconsider LR as Relation of P by XBOOLE_1:17;
    field LL = cL by FILTER_1:32;
    then
A1: LL is_reflexive_in cL by RELAT_2:def 9;
A2: field LR = P
    proof
      thus field LR c= P by WELLORD1:13;
      let x be set;
      assume x in P;
      then [x,x] in [:P, P:] & [x,x] in LL by A1,RELAT_2:def 1,ZFMISC_1:87;
      then [x, x] in LR by XBOOLE_0:def 4;
      hence thesis by RELAT_1:15;
    end;
    LR is reflexive by WELLORD1:15;
    then
A3: LR is_reflexive_in P by A2,RELAT_2:def 9;
    then
A4: dom LR = P by ORDERS_1:13;
    LR is transitive by WELLORD1:17;
    then
A5: LR is_transitive_in P by A2,RELAT_2:def 16;
    LR is antisymmetric by WELLORD1:18;
    then
A6: LR is_antisymmetric_in P by A2,RELAT_2:def 12;
    reconsider LR as Order of P by A4,PARTFUN1:def 2,WELLORD1:15,17,18;
    set RS = RelStr(#P, LR#);
    take IT = latt RS;
A7: RS is with_suprema
    proof
      let x,y be Element of RS;
      x in P & y in P;
      then reconsider xL = x, yL = y as Element of L;
      consider zL being Element of L such that
A8:   zL in P and
A9:   xL [= zL and
A10:  yL [= zL and
A11:  for z9 being Element of L st z9 in P & xL [= z9 & yL [= z9
      holds zL [= z9 by Def6;
      [yL,zL] in [:P,P:] & [yL,zL] in LL by A8,A10,FILTER_1:31,ZFMISC_1:87;
      then
A12:  [yL,zL] in LR by XBOOLE_0:def 4;
      reconsider z = zL as Element of RS by A8;
      take z;
      [xL,zL] in [:P,P:] & [xL,zL] in LL by A8,A9,FILTER_1:31,ZFMISC_1:87;
      then [xL,zL] in LR by XBOOLE_0:def 4;
      hence x <= z & y <= z by A12,ORDERS_2:def 5;
      let z9 be Element of RS;
      assume that
A13:  x <= z9 and
A14:  y <= z9;
      z9 in P;
      then reconsider z9L = z9 as Element of L;
      [y,z9] in LR by A14,ORDERS_2:def 5;
      then [y,z9] in LL by XBOOLE_0:def 4;
      then
A15:  yL [= z9L by FILTER_1:31;
      [x,z9] in LR by A13,ORDERS_2:def 5;
      then [x,z9] in LL by XBOOLE_0:def 4;
      then xL [= z9L by FILTER_1:31;
      then zL [= z9L by A11,A15;
      then
A16:  [zL,z9L] in LL by FILTER_1:31;
      [zL,z9L] in [:P, P:] by A8,ZFMISC_1:87;
      then [zL,z9L] in LR by A16,XBOOLE_0:def 4;
      hence thesis by ORDERS_2:def 5;
    end;
A17: RS is with_infima
    proof
      let x,y be Element of RS;
      x in P & y in P;
      then reconsider xL = x, yL = y as Element of L;
      consider zL being Element of L such that
A18:  zL in P and
A19:  zL [= xL and
A20:  zL [= yL and
A21:  for z9 being Element of L st z9 in P & z9 [= xL & z9 [= yL
      holds z9 [= zL by Def7;
      [zL,yL] in [:P,P:] & [zL,yL] in LL by A18,A20,FILTER_1:31,ZFMISC_1:87;
      then
A22:  [zL,yL] in LR by XBOOLE_0:def 4;
      reconsider z = zL as Element of RS by A18;
      take z;
      [zL,xL] in [:P,P:] & [zL,xL] in LL by A18,A19,FILTER_1:31,ZFMISC_1:87;
      then [zL,xL] in LR by XBOOLE_0:def 4;
      hence z <= x & z <= y by A22,ORDERS_2:def 5;
      let z9 be Element of RS;
      assume that
A23:  z9 <= x and
A24:  z9 <= y;
      z9 in P;
      then reconsider z9L = z9 as Element of L;
      [z9,y] in LR by A24,ORDERS_2:def 5;
      then [z9,y] in LL by XBOOLE_0:def 4;
      then
A25:  z9L [= yL by FILTER_1:31;
      [z9,x] in LR by A23,ORDERS_2:def 5;
      then [z9,x] in LL by XBOOLE_0:def 4;
      then z9L [= xL by FILTER_1:31;
      then z9L [= zL by A21,A25;
      then
A26:  [z9L,zL] in LL by FILTER_1:31;
      [z9L,zL] in [:P, P:] by A18,ZFMISC_1:87;
      then [z9L,zL] in LR by A26,XBOOLE_0:def 4;
      hence thesis by ORDERS_2:def 5;
    end;
A27: RS is Poset by A3,A6,A5,ORDERS_2:def 2,def 3,def 4;
    then
A28: RS = LattPOSet IT by A7,A17,LATTICE3:def 15;
    LattPOSet IT = RelStr(#the carrier of IT, LattRel IT#);
    hence the carrier of IT = P by A7,A17,A27,LATTICE3:def 15;
    let x, y be Element of IT;
    x in P & y in P by A28;
    then reconsider x9 = x, y9 = y as Element of L;
    take x9, y9;
    thus x = x9 & y = y9;
    hereby
      assume x [= y;
      then [x, y] in LR by A28,FILTER_1:31;
      then [x, y] in LattRel L by XBOOLE_0:def 4;
      hence x9 [= y9 by FILTER_1:31;
    end;
    assume x9 [= y9;
    then
A29: [x, y] in LattRel L by FILTER_1:31;
    [x, y] in [:P, P:] by A28,ZFMISC_1:87;
    then [x, y] in LattRel IT by A28,A29,XBOOLE_0:def 4;
    hence thesis by FILTER_1:31;
  end;
  uniqueness
  proof
    let it1, it2 be strict Lattice such that
A30: the carrier of it1 = P and
A31: for x, y being Element of it1 ex x9, y9 being Element of L st x =
    x9 & y = y9 & (x [= y iff x9 [= y9) and
A32: the carrier of it2 = P and
A33: for x, y being Element of it2 ex x9, y9 being Element of L st x =
    x9 & y = y9 & (x [= y iff x9 [= y9);
A34: LattRel it2 = { [p,q] where p is Element of it2, q is Element of it2:
    p [= q } by FILTER_1:def 8;
A35: LattRel it1 = { [p,q] where p is Element of it1, q is Element of it1:
    p [= q } by FILTER_1:def 8;
    now
      let a be set;
      hereby
        assume a in LattRel it1;
        then consider p1, q1 being Element of it1 such that
A36:    a = [p1, q1] & p1 [= q1 by A35;
        reconsider p1, q1 as Element of it1;
        reconsider p2 = p1, q2 = q1 as Element of it2 by A30,A32;
        (ex pl1, ql1 being Element of L st p1 = pl1 & q1 = ql1 &( p1 [=
q1 iff pl1 [= ql1))& ex pl2, ql2 being Element of L st p2 = pl2 & q2 = ql2 &(
        p2 [= q2 iff pl2 [= ql2) by A31,A33;
        hence a in LattRel it2 by A34,A36;
      end;
      assume a in LattRel it2;
      then consider p1, q1 being Element of it2 such that
A37:  a = [p1, q1] & p1 [= q1 by A34;
      reconsider p1, q1 as Element of it2;
      reconsider p2 = p1, q2 = q1 as Element of it1 by A30,A32;
      (ex pl1, ql1 being Element of L st p1 = pl1 & q1 = ql1 &( p1 [= q1
iff pl1 [= ql1))& ex pl2, ql2 being Element of L st p2 = pl2 & q2 = ql2 &( p2
      [= q2 iff pl2 [= ql2) by A31,A33;
      hence a in LattRel it1 by A35,A37;
    end;
    then
A38: LattRel it1 = LattRel it2 by TARSKI:1;
    LattPOSet it1 = RelStr(#the carrier of it1,LattRel it1#) & LattPOSet
    it2 = RelStr(#the carrier of it2,LattRel it2#);
    hence thesis by A30,A32,A38,LATTICE3:6;
  end;
end;

begin :: Complete lattices

registration
  cluster complete -> bounded for Lattice;
  coherence
  proof
    let L be Lattice;
    assume L is complete;
    then L is 0_Lattice & L is 1_Lattice by LATTICE3:49,50;
    hence thesis;
  end;
end;

reserve L for complete Lattice,
  f for monotone UnOp of L,
  a, b for Element of L;

theorem Th21:
  ex a st a is_a_fixpoint_of f
proof
  set H = {h where h is Element of L: h [= f.h};
  set fH = {f.h where h is Element of L: h [= f.h};
  set uH = "\/"(H, L);
  set fuH = "\/"(fH, L);
  take uH;
  now
    let fh be Element of L;
    assume fh in fH;
    then consider h being Element of L such that
A1: fh = f.h and
A2: h [= f.h;
    h in H by A2;
    then h [= uH by LATTICE3:38;
    hence fh [= f.uH by A1,QUANTAL1:def 12;
  end;
  then fH is_less_than f.uH by LATTICE3:def 17;
  then
A3: fuH [= f.uH by LATTICE3:def 21;
  now
    let a be Element of L;
    assume a in H;
    then consider h being Element of L such that
A4: a = h & h [= f.h;
    reconsider fh = f.h as Element of L;
    take fh;
    thus a [= fh & fh in fH by A4;
  end;
  then uH [= fuH by LATTICE3:47;
  then
A5: uH [= f.uH by A3,LATTICES:7;
  then f.uH [= f.(f.uH) by QUANTAL1:def 12;
  then f.uH in H;
  then f.uH [= uH by LATTICE3:38;
  hence uH = f.uH by A5,LATTICES:8;
end;

theorem Th22:
  for a st a [= f.a for O holds a [= (f, O)+.a
proof
  let a;
  defpred S[Ordinal] means a [= (f, $1)+.a;
  deffunc F(Ordinal)=(f, $1)+.a;
A1: now
    let O1;
    assume that
A2: O1 <> {} and
A3: O1 is limit_ordinal and
A4: for O2 st O2 in O1 holds S[O2];
    consider O2 being set such that
A5: O2 in O1 by A2,XBOOLE_0:def 1;
    reconsider O2 as Ordinal by A5;
A6: S[O2] by A4,A5;
    consider Ls being T-Sequence such that
A7: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2
    ) from ORDINAL2:sch 2;
    Ls.O2 = (f, O2)+.a & Ls.O2 in rng Ls by A7,A5,FUNCT_1:def 3;
    then (f, O2)+.a [= "\/"(rng Ls, L) by LATTICE3:38;
    then a [= "\/"(rng Ls, L) by A6,LATTICES:7;
    hence S[O1] by A2,A3,A7,Th17;
  end;
  assume
A8: a [= f.a;
A9: now
    let O1;
    assume S[O1];
    then f.a [= f.((f, O1)+.a) by QUANTAL1:def 12;
    then a [= f.((f, O1)+.a) by A8,LATTICES:7;
    hence S[succ O1] by Th15;
  end;
A10: S[{}] by Th13;
  thus for O holds S[O] from ORDINAL2:sch 1(A10, A9, A1);
end;

theorem Th23:
  for a st f.a [= a for O holds (f, O)-.a [= a
proof
  let a;
  defpred S[Ordinal] means (f, $1)-.a [= a;
  deffunc F(Ordinal)=(f, $1)-.a;
A1: now
    let O1;
    assume that
A2: O1 <> {} and
A3: O1 is limit_ordinal and
A4: for O2 st O2 in O1 holds S[O2];
    consider O2 being set such that
A5: O2 in O1 by A2,XBOOLE_0:def 1;
    reconsider O2 as Ordinal by A5;
A6: S[O2] by A4,A5;
    consider Ls being T-Sequence such that
A7: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2
    ) from ORDINAL2:sch 2;
    Ls.O2 = (f, O2)-.a & Ls.O2 in rng Ls by A7,A5,FUNCT_1:def 3;
    then "/\"(rng Ls, L) [= (f, O2)-.a by LATTICE3:38;
    then "/\"(rng Ls, L) [= a by A6,LATTICES:7;
    hence S[O1] by A2,A3,A7,Th18;
  end;
  assume
A8: f.a [= a;
A9: now
    let O1;
    assume S[O1];
    then f.((f, O1)-.a) [= f.a by QUANTAL1:def 12;
    then f.((f, O1)-.a) [= a by A8,LATTICES:7;
    hence S[succ O1] by Th16;
  end;
A10: S[{}] by Th14;
  thus for O holds S[O] from ORDINAL2:sch 1(A10, A9, A1);
end;

theorem Th24:
  for a st a [= f.a for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a
proof
  let a;
  defpred S[Ordinal] means for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O1)+.a
  [= (f, O2)+.a;
A1: now
    let O4;
    assume that
A2: O4 <> {} & O4 is limit_ordinal and
A3: for O3 st O3 in O4 holds S[O3];
    thus S[O4]
    proof
      let O1, O2;
      assume that
A4:   O1 c= O2 and
A5:   O2 c= O4;
A6:   O2 c< O4 iff O2 c= O4 & O2 <> O4 by XBOOLE_0:def 8;
A7:   O1 c< O2 iff O1 c= O2 & O1 <> O2 by XBOOLE_0:def 8;
      per cases by A5,A6,ORDINAL1:11;
      suppose
A8:     O2 = O4;
        thus (f, O1)+.a [= (f, O2)+.a
        proof
          per cases by A4,A7,ORDINAL1:11;
          suppose
            O1 = O2;
            hence thesis;
          end;
          suppose
A9:         O1 in O2;
            deffunc F(Ordinal)=(f, $1)+.a;
            consider L1 being T-Sequence such that
A10:        dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
            ORDINAL2:sch 2;
A11:        L1.O1 = (f, O1)+.a & L1.O1 in rng L1 by A9,A10,FUNCT_1:def 3;
            (f, O2)+.a = "\/"(rng L1, L) by A2,A8,A10,Th17;
            hence thesis by A11,LATTICE3:38;
          end;
        end;
      end;
      suppose
        O2 in O4;
        hence thesis by A3,A4;
      end;
    end;
  end;
  assume
A12: a [= f.a;
A13: now
    let O4;
    assume
A14: S[O4];
    thus S[succ O4]
    proof
      let O1, O2;
      assume that
A15:  O1 c= O2 and
A16:  O2 c= succ O4;
      per cases;
      suppose
        O1 = O2 & O2 <> succ O4;
        hence thesis;
      end;
      suppose
        O1 <> O2 & O2 <> succ O4;
        then O2 c< succ O4 by A16,XBOOLE_0:def 8;
        then O2 in succ O4 by ORDINAL1:11;
        then O2 c= O4 by ORDINAL1:22;
        hence thesis by A14,A15;
      end;
      suppose
        O1 = O2 & O2 = succ O4;
        hence thesis;
      end;
      suppose
A17:    O1 <> O2 & O2 = succ O4;
A18:    (f, O4)+.a [= (f, succ O4)+.a
        proof
          per cases by ORDINAL1:29;
          suppose
A19:        O4 is limit_ordinal;
            thus thesis
            proof
              per cases;
              suppose
                O4 = {};
                then (f, O4)+.a = a by Th13;
                hence thesis by A12,Th15;
              end;
              suppose
A20:            O4 <> {};
                deffunc F(Ordinal)=(f, $1)+.a;
                consider L1 being T-Sequence such that
A21:            dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
                from ORDINAL2:sch 2;
A22:            rng L1 is_less_than (f, succ O4)+.a
                proof
                  let q be Element of L;
                  assume q in rng L1;
                  then consider O3 being set such that
A23:              O3 in dom L1 and
A24:              q = L1.O3 by FUNCT_1:def 3;
                  reconsider O3 as Ordinal by A23;
                  O3 in succ O3 by ORDINAL1:6;
                  then
A25:              O3 c= succ O3 by ORDINAL1:def 2;
                  O3 c= O4 by A21,A23,ORDINAL1:def 2;
                  then (f, O3)+.a [= (f, O4)+.a by A14;
                  then f.(f, O3)+.a [= f.(f, O4)+.a by QUANTAL1:def 12;
                  then (f, succ O3)+.a [= f.(f, O4)+.a by Th15;
                  then
A26:              (f, succ O3)+.a [= (f, succ O4)+.a by Th15;
                  succ O3 c= O4 by A21,A23,ORDINAL1:21;
                  then
A27:              (f, O3)+.a [= (f, succ O3)+.a by A14,A25;
                  q = (f, O3)+.a by A21,A23,A24;
                  hence q [= (f, succ O4)+.a by A26,A27,LATTICES:7;
                end;
                (f, O4)+.a = "\/"(rng L1, L) by A19,A20,A21,Th17;
                hence thesis by A22,LATTICE3:def 21;
              end;
            end;
          end;
          suppose
            ex O3 st O4 = succ O3;
            then consider O3 such that
A28:        O4 = succ O3;
            succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
            then O3 c= O4 by A28,XBOOLE_1:7;
            then (f, O3)+.a [= (f, O4)+.a by A14;
            then f.((f, O3)+.a) [= f.((f, O4)+.a) by QUANTAL1:def 12;
            then (f, O4)+.a [= f.((f, O4)+.a) by A28,Th15;
            hence thesis by Th15;
          end;
        end;
        O1 c< O2 by A15,A17,XBOOLE_0:def 8;
        then O1 in O2 by ORDINAL1:11;
        then O1 c= O4 by A17,ORDINAL1:22;
        then (f, O1)+.a [= (f, O4)+.a by A14;
        hence thesis by A17,A18,LATTICES:7;
      end;
    end;
  end;
  let O1, O2;
  assume
A29: O1 c= O2;
A30: S[{}];
  for O4 holds S[O4] from ORDINAL2:sch 1(A30, A13, A1);
  hence thesis by A29;
end;

theorem Th25:
  for a st f.a [= a for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a
proof
  let a;
  defpred S[Ordinal] means for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O2)-.a
  [= (f, O1)-.a;
A1: now
    let O4;
    assume that
A2: O4 <> {} & O4 is limit_ordinal and
A3: for O3 st O3 in O4 holds S[O3];
    thus S[O4]
    proof
      let O1, O2;
      assume that
A4:   O1 c= O2 and
A5:   O2 c= O4;
A6:   O2 c< O4 iff O2 c= O4 & O2 <> O4 by XBOOLE_0:def 8;
A7:   O1 c< O2 iff O1 c= O2 & O1 <> O2 by XBOOLE_0:def 8;
      per cases by A5,A6,ORDINAL1:11;
      suppose
A8:     O2 = O4;
        thus (f, O2)-.a [= (f, O1)-.a
        proof
          per cases by A4,A7,ORDINAL1:11;
          suppose
            O1 = O2;
            hence thesis;
          end;
          suppose
A9:         O1 in O2;
            deffunc F(Ordinal)=(f, $1)-.a;
            consider L1 being T-Sequence such that
A10:        dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
            ORDINAL2:sch 2;
A11:        L1.O1 = (f, O1)-.a & L1.O1 in rng L1 by A9,A10,FUNCT_1:def 3;
            (f, O2)-.a = "/\"(rng L1, L) by A2,A8,A10,Th18;
            hence thesis by A11,LATTICE3:38;
          end;
        end;
      end;
      suppose
        O2 in O4;
        hence thesis by A3,A4;
      end;
    end;
  end;
  assume
A12: f.a [= a;
A13: now
    let O4;
    assume
A14: S[O4];
    thus S[succ O4]
    proof
      let O1, O2;
      assume that
A15:  O1 c= O2 and
A16:  O2 c= succ O4;
      per cases;
      suppose
        O1 = O2 & O2 <> succ O4;
        hence thesis;
      end;
      suppose
        O1 <> O2 & O2 <> succ O4;
        then O2 c< succ O4 by A16,XBOOLE_0:def 8;
        then O2 in succ O4 by ORDINAL1:11;
        then O2 c= O4 by ORDINAL1:22;
        hence thesis by A14,A15;
      end;
      suppose
        O1 = O2 & O2 = succ O4;
        hence thesis;
      end;
      suppose
A17:    O1 <> O2 & O2 = succ O4;
A18:    (f, succ O4)-.a [= (f, O4)-.a
        proof
          per cases by ORDINAL1:29;
          suppose
A19:        O4 is limit_ordinal;
            thus thesis
            proof
              per cases;
              suppose
                O4 = {};
                then (f, O4)-.a = a by Th14;
                hence thesis by A12,Th16;
              end;
              suppose
A20:            O4 <> {};
                deffunc F(Ordinal)=(f, $1)-.a;
                consider L1 being T-Sequence such that
A21:            dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
                from ORDINAL2:sch 2;
A22:            (f, succ O4)-.a is_less_than rng L1
                proof
                  let q be Element of L;
                  assume q in rng L1;
                  then consider O3 being set such that
A23:              O3 in dom L1 and
A24:              q = L1.O3 by FUNCT_1:def 3;
                  reconsider O3 as Ordinal by A23;
                  O3 in succ O3 by ORDINAL1:6;
                  then
A25:              O3 c= succ O3 by ORDINAL1:def 2;
                  O3 c= O4 by A21,A23,ORDINAL1:def 2;
                  then (f, O4)-.a [= (f, O3)-.a by A14;
                  then f.(f, O4)-.a [= f.(f, O3)-.a by QUANTAL1:def 12;
                  then (f, succ O4)-.a [= f.(f, O3)-.a by Th16;
                  then
A26:              (f, succ O4)-.a [= (f, succ O3)-.a by Th16;
                  succ O3 c= O4 by A21,A23,ORDINAL1:21;
                  then
A27:              (f, succ O3)-.a [= (f, O3)-.a by A14,A25;
                  q = (f, O3)-.a by A21,A23,A24;
                  hence (f, succ O4)-.a [= q by A26,A27,LATTICES:7;
                end;
                (f, O4)-.a = "/\"(rng L1, L) by A19,A20,A21,Th18;
                hence thesis by A22,LATTICE3:34;
              end;
            end;
          end;
          suppose
            ex O3 st O4 = succ O3;
            then consider O3 such that
A28:        O4 = succ O3;
            succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
            then O3 c= O4 by A28,XBOOLE_1:7;
            then (f, O4)-.a [= (f, O3)-.a by A14;
            then f.((f, O4)-.a) [= f.((f, O3)-.a) by QUANTAL1:def 12;
            then f.((f, O4)-.a) [= (f, O4)-.a by A28,Th16;
            hence thesis by Th16;
          end;
        end;
        O1 c< O2 by A15,A17,XBOOLE_0:def 8;
        then O1 in O2 by ORDINAL1:11;
        then O1 c= O4 by A17,ORDINAL1:22;
        then (f, O4)-.a [= (f, O1)-.a by A14;
        hence thesis by A17,A18,LATTICES:7;
      end;
    end;
  end;
  let O1, O2;
  assume
A29: O1 c= O2;
A30: S[{}];
  for O4 holds S[O4] from ORDINAL2:sch 1(A30, A13, A1);
  hence thesis by A29;
end;

theorem Th26:
  for a st a [= f.a for O1, O2 st O1 c< O2 & not (f, O2)+.a
  is_a_fixpoint_of f holds (f, O1)+.a <> (f, O2)+.a
proof
  let a;
  assume
A1: a [= f.a;
  let O1, O2;
  succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
  then
A2: (f, O1)+.a [= (f, succ O1)+.a by A1,Th24,XBOOLE_1:7;
  assume that
A3: O1 c< O2 and
A4: not (f, O2)+.a is_a_fixpoint_of f and
A5: (f, O1)+.a = (f, O2)+.a;
  O1 in O2 by A3,ORDINAL1:11;
  then succ O1 c= O2 by ORDINAL1:21;
  then (f, succ O1)+.a [= (f, O2)+.a by A1,Th24;
  then (f, O1)+.a = (f, succ O1)+.a by A5,A2,LATTICES:8;
  then (f, O1)+.a = f.(f, O1)+.a by Th15;
  hence contradiction by A4,A5,ABIAN:def 4;
end;

theorem Th27:
  for a st f.a [= a for O1, O2 st O1 c< O2 & not (f, O2)-.a
  is_a_fixpoint_of f holds (f, O1)-.a <> (f, O2)-.a
proof
  let a;
  assume
A1: f.a [= a;
  let O1, O2;
  succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
  then
A2: (f, succ O1)-.a [= (f, O1)-.a by A1,Th25,XBOOLE_1:7;
  assume that
A3: O1 c< O2 and
A4: not (f, O2)-.a is_a_fixpoint_of f and
A5: (f, O1)-.a = (f, O2)-.a;
  O1 in O2 by A3,ORDINAL1:11;
  then succ O1 c= O2 by ORDINAL1:21;
  then (f, O2)-.a [= (f, succ O1)-.a by A1,Th25;
  then (f, O1)-.a = (f, succ O1)-.a by A5,A2,LATTICES:8;
  then (f, O1)-.a = f.(f, O1)-.a by Th16;
  hence contradiction by A4,A5,ABIAN:def 4;
end;

theorem Th28:
  a [= f.a & (f, O1)+.a is_a_fixpoint_of f implies for O2 st O1 c=
  O2 holds (f, O1)+.a = (f, O2)+.a
proof
  assume that
A1: a [= f.a and
A2: (f, O1)+.a is_a_fixpoint_of f;
  set fa = (f, O1)+.a;
  defpred S[Ordinal] means O1 c= $1 implies fa = (f, $1)+.a;
A3: now
    let O2;
    assume that
A4: O2 <> {} & O2 is limit_ordinal and
A5: for O3 st O3 in O2 holds S[O3];
    thus S[O2]
    proof
      assume O1 c= O2;
      then
A6:   fa [= (f, O2)+.a by A1,Th24;
      deffunc F(Ordinal)=(f, $1)+.a;
      consider L1 being T-Sequence such that
A7:   dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
      ORDINAL2:sch 2;
A8:   rng L1 is_less_than fa
      proof
        let q be Element of L;
        assume q in rng L1;
        then consider O3 being set such that
A9:     O3 in dom L1 and
A10:    q = L1.O3 by FUNCT_1:def 3;
        reconsider O3 as Ordinal by A9;
        per cases;
        suppose
          O1 c= O3;
          then (f, O3)+.a [= fa by A5,A7,A9;
          hence q [= fa by A7,A9,A10;
        end;
        suppose
          O3 c= O1;
          then (f, O3)+.a [= fa by A1,Th24;
          hence q [= fa by A7,A9,A10;
        end;
      end;
      (f, O2)+.a = "\/"(rng L1, L) by A4,A7,Th17;
      then (f, O2)+.a [= fa by A8,LATTICE3:def 21;
      hence thesis by A6,LATTICES:8;
    end;
  end;
A11: now
    let O2;
    assume
A12: S[O2];
    thus S[succ O2]
    proof
      assume
A13:  O1 c= succ O2;
      per cases;
      suppose
        O1 = succ O2;
        hence thesis;
      end;
      suppose
        O1 <> succ O2;
        then O1 c< succ O2 by A13,XBOOLE_0:def 8;
        then O1 in succ O2 by ORDINAL1:11;
        hence fa = f.(f, O2)+.a by A2,A12,ABIAN:def 3,ORDINAL1:22
          .= (f, succ O2)+.a by Th15;
      end;
    end;
  end;
A14: S[{}];
  thus for O2 holds S[O2] from ORDINAL2:sch 1(A14, A11, A3);
end;

theorem Th29:
  f.a [= a & (f, O1)-.a is_a_fixpoint_of f implies for O2 st O1 c=
  O2 holds (f, O1)-.a = (f, O2)-.a
proof
  assume that
A1: f.a [= a and
A2: (f, O1)-.a is_a_fixpoint_of f;
  set fa = (f, O1)-.a;
  defpred S[Ordinal] means O1 c= $1 implies fa = (f, $1)-.a;
A3: now
    let O2;
    assume that
A4: O2 <> {} & O2 is limit_ordinal and
A5: for O3 st O3 in O2 holds S[O3];
    thus S[O2]
    proof
      assume O1 c= O2;
      then
A6:   (f, O2)-.a [= fa by A1,Th25;
      deffunc F(Ordinal)=(f, $1)-.a;
      consider L1 being T-Sequence such that
A7:   dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3) from
      ORDINAL2:sch 2;
A8:   fa is_less_than rng L1
      proof
        let q be Element of L;
        assume q in rng L1;
        then consider O3 being set such that
A9:     O3 in dom L1 and
A10:    q = L1.O3 by FUNCT_1:def 3;
        reconsider O3 as Ordinal by A9;
        per cases;
        suppose
          O1 c= O3;
          then fa [= (f, O3)-.a by A5,A7,A9;
          hence fa [= q by A7,A9,A10;
        end;
        suppose
          O3 c= O1;
          then fa [= (f, O3)-.a by A1,Th25;
          hence fa [= q by A7,A9,A10;
        end;
      end;
      (f, O2)-.a = "/\"(rng L1, L) by A4,A7,Th18;
      then fa [= (f, O2)-.a by A8,LATTICE3:39;
      hence thesis by A6,LATTICES:8;
    end;
  end;
A11: now
    let O2;
    assume
A12: S[O2];
    thus S[succ O2]
    proof
      assume
A13:  O1 c= succ O2;
      per cases;
      suppose
        O1 = succ O2;
        hence thesis;
      end;
      suppose
        O1 <> succ O2;
        then O1 c< succ O2 by A13,XBOOLE_0:def 8;
        then O1 in succ O2 by ORDINAL1:11;
        hence fa = f.(f, O2)-.a by A2,A12,ABIAN:def 3,ORDINAL1:22
          .= (f, succ O2)-.a by Th16;
      end;
    end;
  end;
A14: S[{}];
  thus for O2 holds S[O2] from ORDINAL2:sch 1(A14, A11, A3);
end;

Lm1: O1 c< O2 or O1 = O2 or O2 c< O1
proof
  assume that
A1: ( not O1 c< O2)& not O1 = O2 and
A2: not O2 c< O1;
  not O1 c= O2 by A1,XBOOLE_0:def 8;
  hence contradiction by A2,XBOOLE_0:def 8;
end;

theorem Th30:
  for a st a [= f.a ex O st card O c= card the carrier of L & (f,
  O)+.a is_a_fixpoint_of f
proof
  let a;
  set cL = the carrier of L;
  set ccL = card cL;
  set nccL = nextcard ccL;
  deffunc F(Ordinal)=(f, $1)+.a;
  consider Ls being T-Sequence such that
A1: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(
  O2) from ORDINAL2:sch 2;
  assume
A2: a [= f.a;
  now
    assume
A3: for O st O in nccL holds not (f, O)+.a is_a_fixpoint_of f;
A4: Ls is one-to-one
    proof
      let x1,x2 be set;
      assume that
A5:   x1 in dom Ls and
A6:   x2 in dom Ls and
A7:   Ls.x1 = Ls.x2;
      reconsider x1, x2 as Ordinal by A5,A6;
A8:   Ls.x1 = (f, x1)+.a by A1,A5;
A9:   Ls.x2 = (f, x2)+.a by A1,A6;
      per cases by Lm1;
      suppose
A10:    x1 c< x2;
        not (f, x2)+.a is_a_fixpoint_of f by A1,A3,A6;
        hence thesis by A2,A1,A6,A7,A8,A10,Th26;
      end;
      suppose
A11:    x2 c< x1;
        not (f, x1)+.a is_a_fixpoint_of f by A1,A3,A5;
        hence thesis by A2,A1,A5,A7,A9,A11,Th26;
      end;
      suppose
        x2 = x1;
        hence thesis;
      end;
    end;
    rng Ls c= cL
    proof
      let y be set;
      assume y in rng Ls;
      then consider x being set such that
A12:  x in dom Ls and
A13:  Ls.x = y by FUNCT_1:def 3;
      reconsider x as Ordinal by A12;
      Ls.x = (f, x)+.a by A1,A12;
      hence thesis by A13;
    end;
    then card nccL c= ccL by A1,A4,CARD_1:10;
    then
A14: nccL c= ccL by CARD_1:def 2;
    ccL in nccL by CARD_1:18;
    hence contradiction by A14,CARD_1:4;
  end;
  then consider O such that
A15: O in nccL and
A16: (f, O)+.a is_a_fixpoint_of f;
  take O;
  card O in nccL by A15,CARD_1:9;
  hence card O c= card cL by CARD_3:91;
  thus thesis by A16;
end;

theorem Th31:
  for a st f.a [= a ex O st card O c= card the carrier of L & (f,
  O)-.a is_a_fixpoint_of f
proof
  let a;
  set cL = the carrier of L;
  set ccL = card cL;
  set nccL = nextcard ccL;
  deffunc F(Ordinal)=(f, $1)-.a;
  consider Ls being T-Sequence such that
A1: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(
  O2) from ORDINAL2:sch 2;
  assume
A2: f.a [= a;
  now
    assume
A3: for O st O in nccL holds not (f, O)-.a is_a_fixpoint_of f;
A4: Ls is one-to-one
    proof
      let x1,x2 be set;
      assume that
A5:   x1 in dom Ls and
A6:   x2 in dom Ls and
A7:   Ls.x1 = Ls.x2;
      reconsider x1, x2 as Ordinal by A5,A6;
A8:   Ls.x1 = (f, x1)-.a by A1,A5;
A9:   Ls.x2 = (f, x2)-.a by A1,A6;
      per cases by Lm1;
      suppose
A10:    x1 c< x2;
        not (f, x2)-.a is_a_fixpoint_of f by A1,A3,A6;
        hence thesis by A2,A1,A6,A7,A8,A10,Th27;
      end;
      suppose
A11:    x2 c< x1;
        not (f, x1)-.a is_a_fixpoint_of f by A1,A3,A5;
        hence thesis by A2,A1,A5,A7,A9,A11,Th27;
      end;
      suppose
        x2 = x1;
        hence thesis;
      end;
    end;
    rng Ls c= cL
    proof
      let y be set;
      assume y in rng Ls;
      then consider x being set such that
A12:  x in dom Ls and
A13:  Ls.x = y by FUNCT_1:def 3;
      reconsider x as Ordinal by A12;
      Ls.x = (f, x)-.a by A1,A12;
      hence thesis by A13;
    end;
    then card nccL c= ccL by A1,A4,CARD_1:10;
    then
A14: nccL c= ccL by CARD_1:def 2;
    ccL in nccL by CARD_1:18;
    hence contradiction by A14,CARD_1:4;
  end;
  then consider O such that
A15: O in nccL and
A16: (f, O)-.a is_a_fixpoint_of f;
  take O;
  card O in nccL by A15,CARD_1:9;
  hence card O c= card cL by CARD_3:91;
  thus thesis by A16;
end;

theorem Th32:
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f ex O st
card O c= card the carrier of L & (f, O)+.(a"\/"b) is_a_fixpoint_of f & a [= (f
  , O)+.(a"\/"b) & b [= (f, O)+.(a"\/"b)
proof
  let a, b;
  reconsider ab = a"\/"b as Element of L;
A1: a [= ab by LATTICES:5;
  then
A2: f.a [= f.ab by QUANTAL1:def 12;
A3: b [= ab by LATTICES:5;
  then
A4: f.b [= f.ab by QUANTAL1:def 12;
  assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
  then
A5: a = f.a & b = f.b by ABIAN:def 3;
  then consider O such that
A6: card O c= card the carrier of L & (f, O)+.ab is_a_fixpoint_of f by A2,A4
,Th30,FILTER_0:6;
  take O;
  thus card O c= card the carrier of L & (f, O)+.(a"\/"b) is_a_fixpoint_of f
  by A6;
  ab [= f.ab by A5,A2,A4,FILTER_0:6;
  then
A7: ab [= (f, O)+.(a"\/"b) by Th22;
  hence a [= (f, O)+.(a"\/"b) by A1,LATTICES:7;
  thus thesis by A3,A7,LATTICES:7;
end;

theorem Th33:
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f ex O st
card O c= card the carrier of L & (f, O)-.(a"/\"b) is_a_fixpoint_of f & (f, O)
  -.(a"/\"b) [= a & (f, O)-.(a"/\"b) [= b
proof
  let a, b;
  reconsider ab = a"/\"b as Element of L;
A1: ab [= a by LATTICES:6;
  then
A2: f.ab [= f.a by QUANTAL1:def 12;
A3: ab [= b by LATTICES:6;
  then
A4: f.ab [= f.b by QUANTAL1:def 12;
  assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
  then
A5: a = f.a & b = f.b by ABIAN:def 3;
  then consider O such that
A6: card O c= card the carrier of L & (f, O)-.ab is_a_fixpoint_of f by A2,A4
,Th31,FILTER_0:7;
  take O;
  thus card O c= card the carrier of L & (f, O)-.(a"/\"b) is_a_fixpoint_of f
  by A6;
  f.ab [= ab by A5,A2,A4,FILTER_0:7;
  then
A7: (f, O)-.(a"/\"b) [= ab by Th23;
  hence (f, O)-.(a"/\"b) [= a by A1,LATTICES:7;
  thus thesis by A3,A7,LATTICES:7;
end;

theorem Th34:
  a [= b & b is_a_fixpoint_of f implies for O2 holds (f, O2)+.a [= b
proof
  assume that
A1: a [= b and
A2: b is_a_fixpoint_of f;
  defpred S[Ordinal] means (f, $1)+.a [= b;
A3: f.b = b by A2,ABIAN:def 3;
A4: now
    let O1;
    assume S[O1];
    then f.(f, O1)+.a [= f.b by QUANTAL1:def 12;
    hence S[succ O1] by A3,Th15;
  end;
A5: now
    deffunc F(Ordinal)=(f, $1)+.a;
    let O1;
    assume that
A6: O1 <> {} & O1 is limit_ordinal and
A7: for O2 st O2 in O1 holds S[O2];
    consider L1 being T-Sequence such that
A8: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
    ORDINAL2:sch 2;
A9: rng L1 is_less_than b
    proof
      let q be Element of L;
      assume q in rng L1;
      then consider O3 being set such that
A10:  O3 in dom L1 and
A11:  q = L1.O3 by FUNCT_1:def 3;
      reconsider O3 as Ordinal by A10;
      (f, O3)+.a [= b by A7,A8,A10;
      hence q [= b by A8,A10,A11;
    end;
    (f, O1)+.a = "\/"(rng L1, L) by A6,A8,Th17;
    hence S[O1] by A9,LATTICE3:def 21;
  end;
A12: S[{}] by A1,Th13;
  thus for O2 holds S[O2] from ORDINAL2:sch 1(A12, A4, A5);
end;

theorem Th35:
  b [= a & b is_a_fixpoint_of f implies for O2 holds b [= (f, O2) -.a
proof
  assume that
A1: b [= a and
A2: b is_a_fixpoint_of f;
  defpred S[Ordinal] means b [= (f, $1)-.a;
A3: f.b = b by A2,ABIAN:def 3;
A4: now
    let O1;
    assume S[O1];
    then f.b [= f.(f, O1)-.a by QUANTAL1:def 12;
    hence S[succ O1] by A3,Th16;
  end;
A5: now
    deffunc F(Ordinal)=(f, $1)-.a;
    let O1;
    assume that
A6: O1 <> {} & O1 is limit_ordinal and
A7: for O2 st O2 in O1 holds S[O2];
    consider L1 being T-Sequence such that
A8: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
    ORDINAL2:sch 2;
A9: b is_less_than rng L1
    proof
      let q be Element of L;
      assume q in rng L1;
      then consider O3 being set such that
A10:  O3 in dom L1 and
A11:  q = L1.O3 by FUNCT_1:def 3;
      reconsider O3 as Ordinal by A10;
      b [= (f, O3)-.a by A7,A8,A10;
      hence b [= q by A8,A10,A11;
    end;
    (f, O1)-.a = "/\"(rng L1, L) by A6,A8,Th18;
    hence S[O1] by A9,LATTICE3:39;
  end;
A12: S[{}] by A1,Th14;
  thus for O2 holds S[O2] from ORDINAL2:sch 1(A12, A4, A5);
end;

definition
  let L be complete Lattice, f be UnOp of L such that
B1: f is monotone;
  func FixPoints f -> strict Lattice means
  :Def9:
  ex P being non empty
  with_suprema with_infima Subset of L st P = {x where x is Element of L: x
  is_a_fixpoint_of f} & it = latt P;
  existence
  proof
    defpred P[set] means $1 is_a_fixpoint_of f;
    set P = {x where x is Element of L: P[x]};
A1: P is Subset of L from DOMAIN_1:sch 7;
    consider a being Element of L such that
A2: a is_a_fixpoint_of f by B1,Th21;
A3: a in P by A2;
    reconsider P as Subset of L by A1;
A4: P is with_suprema
    proof
      let x,y be Element of L;
      assume that
A5:   x in P and
A6:   y in P;
      consider a being Element of L such that
A7:   x = a and
A8:   a is_a_fixpoint_of f by A5;
      consider b being Element of L such that
A9:  y = b and
A10:  b is_a_fixpoint_of f by A6;
      reconsider a, b as Element of L;
      reconsider ab = a"\/"b as Element of L;
      consider O such that
      card O c= card the carrier of L and
A11:  (f, O)+.ab is_a_fixpoint_of f and
A12:  a [= (f, O)+.ab & b [= (f, O)+.ab by B1,A8,A10,Th32;
      set z = (f, O)+.ab;
      take z;
      thus z in P by A11;
      thus x [= z & y [= z by A7,A9,A12;
      let z9 be Element of L;
      assume that
A13:  z9 in P and
A14:  x [= z9 & y [= z9;
A15:  ex zz being Element of L st zz = z9 & zz is_a_fixpoint_of f by A13;
      ab [= z9 by A7,A9,A14,FILTER_0:6;
      hence z [= z9 by B1,A15,Th34;
    end;
    P is with_infima
    proof
      let x,y be Element of L;
      assume that
A16:  x in P and
A17:  y in P;
      consider a being Element of L such that
A18:  x = a and
A19:  a is_a_fixpoint_of f by A16;
      consider b being Element of L such that
A20:  y = b and
A21:  b is_a_fixpoint_of f by A17;
      reconsider a, b as Element of L;
      reconsider ab = a"/\"b as Element of L;
      consider O such that
      card O c= card the carrier of L and
A22:  (f, O)-.ab is_a_fixpoint_of f and
A23:  (f, O)-.ab [= a & (f, O)-.ab [= b by B1,A19,A21,Th33;
      set z = (f, O)-.ab;
      take z;
      thus z in P by A22;
      thus z [= x & z [= y by A18,A20,A23;
      let z9 be Element of L;
      assume that
A24:  z9 in P and
A25:  z9 [= x & z9 [= y;
A26:  ex zz being Element of L st zz = z9 & zz is_a_fixpoint_of f by A24;
      z9 [= ab by A18,A20,A25,FILTER_0:7;
      hence z9 [= z by B1,A26,Th35;
    end;
    then reconsider
    P as non empty with_suprema with_infima Subset of L by A3,A4;
    take latt P, P;
    thus P = {x where x is Element of L: x is_a_fixpoint_of f};
    thus thesis;
  end;
  uniqueness;
end;

theorem Th36:
  the carrier of FixPoints f = {x where x is Element of L: x
  is_a_fixpoint_of f}
proof
  ex P being non empty with_suprema with_infima Subset of L st P = {x
where x is Element of L: x is_a_fixpoint_of f} & FixPoints f = latt P by Def9;
  hence thesis by Def8;
end;

theorem Th37:
  the carrier of FixPoints f c= the carrier of L
proof
A1: the carrier of FixPoints f = {x where x is Element of L: x
  is_a_fixpoint_of f} by Th36;
  let x be set;
  assume x in the carrier of FixPoints f;
  then ex a st x = a & a is_a_fixpoint_of f by A1;
  hence thesis;
end;

theorem Th38:
  a in the carrier of FixPoints f iff a is_a_fixpoint_of f
proof
A1: the carrier of FixPoints f = {x where x is Element of L: x
  is_a_fixpoint_of f} by Th36;
  hereby
    assume a in the carrier of FixPoints f;
    then ex b st a = b & b is_a_fixpoint_of f by A1;
    hence a is_a_fixpoint_of f;
  end;
  assume a is_a_fixpoint_of f;
  hence thesis by A1;
end;

theorem Th39:
  for x, y being Element of FixPoints f, a, b st x = a & y = b
  holds (x [= y iff a [= b)
proof
A1: ex P being non empty with_suprema with_infima Subset of L st P = {x where
  x is Element of L: x is_a_fixpoint_of f} & FixPoints f = latt P by Def9;
  let x, y be Element of FixPoints f, a, b;
  assume
A2: x = a & y = b;
  ex a9, b9 being Element of L st x = a9 & y = b9 &( x [= y iff a9 [= b9)
  by A1,Def8;
  hence thesis by A2;
end;

theorem
  FixPoints f is complete
proof
  set F = FixPoints f;
  set cF = the carrier of F;
  set cL = the carrier of L;
  let X be set;
  set Y = X /\ cF;
  set s = "\/"(Y, L);
A1: Y c= cF by XBOOLE_1:17;
  Y is_less_than f.s
  proof
    let q be Element of cL;
    reconsider q9 = q as Element of L;
    assume
A2: q in Y;
    then q [= s by LATTICE3:38;
    then
A3: f.q [= f.s by QUANTAL1:def 12;
    q9 is_a_fixpoint_of f by A1,A2,Th38;
    hence q [= f.s by A3,ABIAN:def 3;
  end;
  then
A4: s [= f.s by LATTICE3:def 21;
  then consider O such that
  card O c= card cL and
A5: (f, O)+.s is_a_fixpoint_of f by Th30;
  reconsider p9 = (f, O)+.s as Element of L;
  reconsider p = p9 as Element of cF by A5,Th38;
  take p;
  thus X is_less_than p
  proof
    let q be Element of cF;
    q in cF & cF c= cL by Th37;
    then reconsider qL9 = q as Element of L;
    assume q in X;
    then q in Y by XBOOLE_0:def 4;
    then
A6: qL9 [= s by LATTICE3:38;
    s [= p9 by A4,Th22;
    then qL9 [= p9 by A6,LATTICES:7;
    hence q [= p by Th39;
  end;
  let r be Element of cF such that
A7: X is_less_than r;
  reconsider r99 = r as Element of F;
  cF = {x where x is Element of L: x is_a_fixpoint_of f} & r in the
  carrier of F by Th36;
  then consider r9 being Element of L such that
A8: r9 = r and
A9: r9 is_a_fixpoint_of f;
A10: Y c= X by XBOOLE_1:17;
  Y is_less_than r9
  proof
    let q be Element of cL;
    assume
A11: q in Y;
    then reconsider q99 = q as Element of F by A1;
    q99 [= r99 by A10,A7,A11,LATTICE3:def 17;
    hence q [= r9 by A8,Th39;
  end;
  then s [= r9 by LATTICE3:def 21;
  then p9 [= r9 by A9,Th34;
  hence p [= r by A8,Th39;
end;

definition
  let L, f;
  func lfp f -> Element of L equals
  (f, nextcard the carrier of L)+.Bottom L;
  coherence;
  func gfp f -> Element of L equals
  (f, nextcard the carrier of L)-.Top L;
  coherence;
end;

theorem Th41:
  lfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
  L & (f, O)+.Bottom L = lfp f
proof
  reconsider ze = Bottom L as Element of L;
A1: Bottom L [= f.ze by LATTICES:16;
  then consider O such that
A2: card O c= card the carrier of L and
A3: (f, O)+.Bottom L is_a_fixpoint_of f by Th30;
  card the carrier of L in nextcard the carrier of L by CARD_1:def 3;
  then card O in nextcard the carrier of L by A2,ORDINAL1:12;
  then O in nextcard the carrier of L by CARD_3:44;
  then
A4: O c= nextcard the carrier of L by ORDINAL1:def 2;
  hence lfp f is_a_fixpoint_of f by A1,A3,Th28;
  take O;
  thus card O c= card the carrier of L by A2;
  thus thesis by A1,A3,A4,Th28;
end;

theorem Th42:
  gfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
  L & (f, O)-.Top L = gfp f
proof
  reconsider je = Top L as Element of L;
A1: f.je [= Top L by LATTICES:19;
  then consider O such that
A2: card O c= card the carrier of L and
A3: (f, O)-.Top L is_a_fixpoint_of f by Th31;
  card the carrier of L in nextcard the carrier of L by CARD_1:def 3;
  then card O in nextcard the carrier of L by A2,ORDINAL1:12;
  then O in nextcard the carrier of L by CARD_3:44;
  then
A4: O c= nextcard the carrier of L by ORDINAL1:def 2;
  hence gfp f is_a_fixpoint_of f by A1,A3,Th29;
  take O;
  thus card O c= card the carrier of L by A2;
  thus thesis by A1,A3,A4,Th29;
end;

theorem Th43:
  a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f
proof
  defpred S[Ordinal] means (f, $1)+.Bottom L [= a;
A1: now
    deffunc F(Ordinal)=(f, $1)+.Bottom L;
    let O1;
    assume that
A2: O1 <> {} & O1 is limit_ordinal and
A3: for O2 st O2 in O1 holds S[O2];
    consider L1 being T-Sequence such that
A4: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
    ORDINAL2:sch 2;
A5: rng L1 is_less_than a
    proof
      let q be Element of L;
      assume q in rng L1;
      then consider C being set such that
A6:   C in dom L1 and
A7:   q = L1.C by FUNCT_1:def 3;
      reconsider C as Ordinal by A6;
      (f, C)+.Bottom L [= a by A3,A4,A6;
      hence q [= a by A4,A6,A7;
    end;
    (f, O1)+.Bottom L = "\/"(rng L1, L) by A2,A4,Th17;
    hence S[O1] by A5,LATTICE3:def 21;
  end;
  assume a is_a_fixpoint_of f;
  then
A8: f.a = a by ABIAN:def 3;
A9: now
    let O1;
    assume S[O1];
    then f.(f, O1)+.Bottom L [= f.a by QUANTAL1:def 12;
    hence S[succ O1] by A8,Th15;
  end;
  (f, {})+.Bottom L = Bottom L by Th13;
  then
A10: S[{}] by LATTICES:16;
  for O2 holds S[O2] from ORDINAL2:sch 1(A10, A9, A1);
  hence lfp f [= a;
  defpred S[Ordinal] means a [= (f, $1)-.Top L;
A11: now
    let O1;
    assume S[O1];
    then f.a [= f.(f, O1)-.Top L by QUANTAL1:def 12;
    hence S[succ O1] by A8,Th16;
  end;
A12: now
    deffunc F(Ordinal)=(f, $1)-.Top L;
    let O1;
    assume that
A13: O1 <> {} & O1 is limit_ordinal and
A14: for O2 st O2 in O1 holds S[O2];
    consider L1 being T-Sequence such that
A15: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3) from
    ORDINAL2:sch 2;
A16: a is_less_than rng L1
    proof
      let q be Element of L;
      assume q in rng L1;
      then consider C being set such that
A17:  C in dom L1 and
A18:  q = L1.C by FUNCT_1:def 3;
      reconsider C as Ordinal by A17;
      a [= (f, C)-.Top L by A14,A15,A17;
      hence a [= q by A15,A17,A18;
    end;
    (f, O1)-.Top L = "/\"(rng L1, L) by A13,A15,Th18;
    hence S[O1] by A16,LATTICE3:39;
  end;
  (f, {})-.Top L = Top L by Th14;
  then
A19: S[{}] by LATTICES:19;
  for O2 holds S[O2] from ORDINAL2:sch 1(A19, A11, A12);
  hence thesis;
end;

theorem
  f.a [= a implies lfp f [= a
proof
  assume
A1: f.a [= a;
  then consider O such that
  card O c= card the carrier of L and
A2: (f, O)-.a is_a_fixpoint_of f by Th31;
A3: lfp f [= (f, O)-.a by A2,Th43;
  (f, O)-.a [= a by A1,Th23;
  hence thesis by A3,LATTICES:7;
end;

theorem
  a [= f.a implies a [= gfp f
proof
  assume
A1: a [= f.a;
  then consider O such that
  card O c= card the carrier of L and
A2: (f, O)+.a is_a_fixpoint_of f by Th30;
A3: (f, O)+.a [= gfp f by A2,Th43;
  a [= (f, O)+.a by A1,Th22;
  hence thesis by A3,LATTICES:7;
end;

begin :: Boolean Lattices

reserve f for monotone UnOp of BooleLatt A;

theorem Th46:
  for f being UnOp of BooleLatt A holds f is monotone iff f is c=-monotone
proof
  let f be UnOp of BooleLatt A;
  thus f is monotone implies f is c=-monotone
  proof
    assume
A1: f is monotone;
    let x, y be Element of BooleLatt A;
    assume x c= y;
    then x [= y by LATTICE3:2;
    then f.x [= f.y by A1,QUANTAL1:def 12;
    hence thesis by LATTICE3:2;
  end;
  assume
A2: f is c=-monotone;
  let p, q be Element of BooleLatt A;
  assume p [= q;
  then p c= q by LATTICE3:2;
  then f.p c= f.q by A2,Def1;
  hence f.p [= f.q by LATTICE3:2;
end;

theorem
  ex g being c=-monotone Function of bool A, bool A st lfp (A, g) = lfp f
proof
  reconsider lf = lfp f as Subset of A by LATTICE3:def 1;
  the carrier of BooleLatt A = bool A by LATTICE3:def 1;
  then reconsider g = f as c=-monotone Function of bool A, bool A by Th46;
  reconsider lg = lfp(A, g) as Element of BooleLatt A by LATTICE3:def 1;
  take g;
  lg is_a_fixpoint_of f by Th4;
  then lfp f [= lg by Th43;
  then
A1: lf c= lg by LATTICE3:2;
  lfp f is_a_fixpoint_of f by Th41;
  then lfp (A, g) c= lf by Th8;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f
proof
  reconsider gf = gfp f as Subset of A by LATTICE3:def 1;
  the carrier of BooleLatt A = bool A by LATTICE3:def 1;
  then reconsider g = f as c=-monotone Function of bool A, bool A by Th46;
  reconsider gg = gfp(A, g) as Element of BooleLatt A by LATTICE3:def 1;
  take g;
  gg is_a_fixpoint_of f by Th5;
  then gg [= gfp f by Th43;
  then
A1: gg c= gf by LATTICE3:2;
  gfp f is_a_fixpoint_of f by Th42;
  then gf c= gfp (A, g) by Th8;
  hence thesis by A1,XBOOLE_0:def 10;
end;