The Mizar article:

Fixpoints in Complete Lattices

by
Piotr Rudnicki, and
Andrzej Trybulec

Received September 16, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: KNASTER
[ MML identifier index ]


environ

 vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCT_4, COHSP_1, FUNCOP_1, SETFAM_1,
      TARSKI, SGRAPH1, CARD_1, LATTICES, BINOP_1, ORDINAL1, ORDINAL2, LATTICE3,
      FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1, BHSP_3, SEQM_3, KNASTER,
      PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, RELAT_2,
      RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1,
      SETFAM_1, FUNCT_4, WELLORD1, ORDINAL1, ORDINAL2, CARD_1, COHSP_1,
      LATTICES, LATTICE3, QUANTAL1, ORDERS_1, FUNCT_7;
 constructors NAT_1, BINOP_1, DOMAIN_1, WELLORD2, COHSP_1, BOOLEALG, QUANTAL1,
      PROB_1, FUNCT_7, WELLORD1;
 clusters SUBSET_1, STRUCT_0, FUNCT_1, LATTICES, CARD_1, LATTICE3, RELSET_1,
      ORDINAL1, QUANTAL1;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, FUNCT_1, COHSP_1, LATTICE3, QUANTAL1, XBOOLE_0;
 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_1, RELAT_2, ORDINAL1,
      CARD_3, CARD_4, PROB_1, XBOOLE_0, XBOOLE_1, FUNCT_7, PARTFUN1;
 schemes NAT_1, FUNCT_1, FUNCT_2, DOMAIN_1, ORDINAL2;

begin :: Preliminaries

reserve f, g, h for Function;

theorem Th1:
 f is one-to-one & g is one-to-one & rng f misses rng g
  implies f+*g is one-to-one
proof assume
A1: f is one-to-one & g is one-to-one & rng f misses rng g;
 set fg = f+*g;
 let x1,x2 be set; assume
A2: x1 in dom fg & x2 in dom fg & fg.x1 = fg.x2;
then A3: (x1 in dom f or x1 in dom g) & (x2 in dom f or x2 in dom g)
 by FUNCT_4:13;
 per cases;
 suppose A4: x1 in dom g & x2 in dom g;
   then fg.x1 = g.x1 & fg.x2 = g.x2 by FUNCT_4:14;
  hence x1 = x2 by A1,A2,A4,FUNCT_1:def 8;
 suppose A5: x1 in dom g & not x2 in dom g;
then A6: x2 in dom f by A2,FUNCT_4:13;
A7: fg.x1 = g.x1 & fg.x2 = f.x2 by A5,FUNCT_4:12,14;
       g.x1 in rng g & f.x2 in rng f by A5,A6,FUNCT_1:def 5;
  hence x1 = x2 by A1,A2,A7,XBOOLE_0:3;
 suppose A8: not x1 in dom g & x2 in dom g;
then A9: x1 in dom f by A2,FUNCT_4:13;
A10: fg.x1 = f.x1 & fg.x2 = g.x2 by A8,FUNCT_4:12,14;
       g.x2 in rng g & f.x1 in rng f by A8,A9,FUNCT_1:def 5;
  hence x1 = x2 by A1,A2,A10,XBOOLE_0:3;
 suppose A11: not x1 in dom g & not x2 in dom g;
    then fg.x1 = f.x1 & fg.x2 = f.x2 by FUNCT_4:12;
  hence x1 = x2 by A1,A2,A3,A11,FUNCT_1:def 8;
end;

canceled;

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
A1: h = f \/ g & dom f misses dom g;
then A2: dom h = dom f \/ dom g by RELAT_1:13;
 hereby assume
A3: 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
A4:  x1 in dom f & x2 in dom f & f.x1 = f.x2 & x1<>x2 by FUNCT_1:def 8;
      [x1, f.x1] in f & [x2, f.x2] in f by A4,FUNCT_1:def 4;
then A5:  [x1, f.x1] in h & [x2, f.x2] in h by A1,XBOOLE_0:def 2;
A6:  x1 in dom h & x2 in dom h by A2,A4,XBOOLE_0:def 2;
    then f.x1 = h.x1 & f.x2 = h.x2 by A5,FUNCT_1:def 4;
   hence contradiction by A3,A4,A6,FUNCT_1:def 8;
  end;
  thus g is one-to-one proof assume not g is one-to-one;
    then consider x1, x2 being set such that
A7:  x1 in dom g & x2 in dom g & g.x1 = g.x2 & x1<>x2 by FUNCT_1:def 8;
      [x1, g.x1] in g & [x2, g.x2] in g by A7,FUNCT_1:def 4;
then A8:  [x1, g.x1] in h & [x2, g.x2] in h by A1,XBOOLE_0:def 2;
A9:  x1 in dom h & x2 in dom h by A2,A7,XBOOLE_0:def 2;
    then g.x1 = h.x1 & g.x2 = h.x2 by A8,FUNCT_1:def 4;
   hence contradiction by A3,A7,A9,FUNCT_1:def 8;
  end;
  thus rng f misses rng g proof assume not thesis;
    then consider hx being set such that
A10:  hx in rng f & hx in rng g by XBOOLE_0:3;
    consider x1 being set such that
A11:  x1 in dom f & hx = f.x1 by A10,FUNCT_1:def 5;
    consider x2 being set such that
A12:  x2 in dom g & hx = g.x2 by A10,FUNCT_1:def 5;
A13:  x1 <> x2 by A1,A11,A12,XBOOLE_0:3;
      [x1, hx] in f & [x2, hx] in g by A11,A12,FUNCT_1:def 4;
then A14:  [x1, hx] in h & [x2, hx] in h by A1,XBOOLE_0:def 2;
A15:  x1 in dom h & x2 in dom h by A2,A11,A12,XBOOLE_0:def 2;
    then h.x1 = hx & h.x2 = hx by A14,FUNCT_1:def 4;
   hence contradiction by A3,A13,A15,FUNCT_1:def 8;
  end;
 end;
 assume
A16: f is one-to-one & g is one-to-one & rng f misses rng g;
     f \/ g = f+*g by A1,FUNCT_4:32;
 hence h is one-to-one by A1,A16,Th1;
end;

begin :: Fix points in general

definition
  let x be set, f be Function;
 pred x is_a_fixpoint_of f means
:Def1: x in dom f & x = f.x;
end;

definition
  let A be non empty set, a be Element of A, f be Function of A, A;
 redefine pred a is_a_fixpoint_of f means
:Def2: a = f.a;
 compatibility proof
  thus a is_a_fixpoint_of f implies a = f.a by Def1;
  assume
A1: a = f.a;
     a in A;
  hence a in dom f by FUNCT_2:67;
  thus a = f.a by A1;
 end;
end;

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

theorem Th4:
 x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f,n)
proof
 assume x is_a_fixpoint_of iter(f,n);
then A1: x in dom iter(f, n) & x = iter(f, n).x by Def1;
     iter(f, n) is Function of X, X by FUNCT_7:85;
then A2: dom f = X & rng f c= X & dom iter(f, n) = X by FUNCT_2:67;
   then f.x in rng f by A1,FUNCT_1:def 5;
 hence f.x in dom iter(f, n) by A2;
 thus f.x = (f*iter(f, n)).x by A1,FUNCT_1:23
         .= iter(f, n+1).x by FUNCT_7:73
         .= (iter(f, n)*f).x by FUNCT_7:71
         .= iter(f, n).(f.x) by A1,A2,FUNCT_1:23;
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;
     iter(f, n) is Function of X, X by FUNCT_7:85;
   then dom f = X & dom iter(f, n) = X by FUNCT_2:67;
 hence x in dom f by A1,Def1;
    f.x is_a_fixpoint_of iter(f, n) by A1,Th4;
 hence x = f.x by A2;
end;

definition let A, B be non empty set, f be Function of A, B;
 redefine attr f is c=-monotone means
:Def3: 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 12;
  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;

definition let A be set, B be non empty set;
 cluster c=-monotone Function of A, B;
 existence proof
  consider b being Element of B;
  reconsider f = A --> b as Function of A, B by FUNCOP_1:58;
  take f;
  let x, y be set; assume
A1:  x in dom f & y in dom f & x c= y;
  then f.x = b by FUNCOP_1:13 .= f.y by A1,FUNCOP_1:13;
  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
:Def4:  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 of bool X
     from SubsetD;
   reconsider H as Subset-Family of X by SETFAM_1:def 7;
     meet H is Subset of X;
  hence thesis;
 end;
 func gfp (X, f) -> Subset of X equals
:Def5:  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 of bool X
     from SubsetD;
     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 Th6:
 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 of bool X
    from SubsetD;
  reconsider H as Subset-Family of X by SETFAM_1:def 7;
 set A = meet H;
A1: lfp(X,f) = A by Def4;
   now X c= X;
  then reconsider X' = X as Element of bool X;
       f.X' c= X'; then X' in H;
  hence H <> {};
  let h be set; assume
A2: h in H; then consider x being Subset of X such that
A3: x = h & f.x c= x;
     A c= h by A2,SETFAM_1:4; then f.A c= f.x by A3,Def3;
  hence f.A c= h by A3,XBOOLE_1:1;
 end;
then A4: f.A c= A by SETFAM_1:6;
   then f.(f.A) c= f.A by Def3; then f.A in H; then A c= f.A by SETFAM_1:4;
 hence f.(lfp(X,f)) = lfp(X,f) by A1,A4,XBOOLE_0:def 10;
end;

theorem Th7:
  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 of bool X from SubsetD;
 set A = union H;
A1: gfp(X,f) = A by Def5;
   now let x be set; assume
A2: x in H; then consider h being Subset of X such that
A3: x = h & h c= f.h;
     h c= A by A2,A3,ZFMISC_1:92; then f.h c= f.A by Def3;
  hence x c= f.A by A3,XBOOLE_1:1;
 end;
then A4: A c= f.A by ZFMISC_1:94; then f.A c= f.(f.A) by Def3;
   then f.A in H; then f.A c= A by ZFMISC_1:92;
 hence f.(gfp (X,f)) = gfp(X,f) by A1,A4,XBOOLE_0:def 10;
end;

theorem Th8:
 f.S c= S implies lfp(X,f) c= S
proof
 set H = {h where h is Subset of X : f.h c= h };
A1: lfp(X,f) = meet H by Def4;
 assume f.S c= S; then S in H;
 hence lfp(X,f) c= S by A1,SETFAM_1:4;
end;

theorem Th9:
  S c= f.S implies S c= gfp(X,f)
proof
 set H = {h where h is Subset of X : h c= f.h };
A1: gfp(X,f) = union H by Def5;
 assume S c= f.S; then S in H;
 hence S c= gfp(X,f) by A1,ZFMISC_1:92;
end;

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

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
  deffunc G(set)=F($1);
 consider f being Function such that
A3: dom f = bool A() & for x being set st x in bool A() holds f.x = G(x)
         from Lambda;
    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 & x = f.y by FUNCT_1:def 5;
       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 x in bool A() by A4;
  end;
 then reconsider f as Function of bool A(), bool A()
 by A3,FUNCT_2:def 1,RELSET_1:11;
    now let a, b be set; assume
  A5: a in dom f & b in dom f & a c= b;
     then f.a = F(a) & f.b = F(b) by A3;
   hence f.a c= f.b by A1,A5;
  end;
 then reconsider f as c=-monotone Function of bool A(), bool A() by COHSP_1:def
12;
 take d = lfp(A(), f);
    d is_a_fixpoint_of f by Th6; then d = f.d by Def1;
 hence F(d) = d by A3;
 thus d c= A();
end;

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

theorem Th11: :: Banach decomposition
  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: now let x be set; assume x in bool X; X\g.:(Y\f.:x) c= X by XBOOLE_1:36;
    hence F(x) in bool X;
   end;
   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 Lambda1(A1);
    now let x, y be set; assume
A3: x in dom h & y in dom h & x c= y;
    then f.:x c= f.:y by RELAT_1:156;
    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:156;
    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,A3;
  end;
  then reconsider h as c=-monotone Function of bool X, bool X by COHSP_1:def 12
;
  take Xa = lfp (X, h); take Xb = X \ Xa; take Ya = f.:Xa; take Yb = Y \ Ya;
  thus Xa misses Xb by PROB_1:13; thus Ya misses Yb by PROB_1:13;
  thus Xa \/ Xb = X by XBOOLE_1:45; thus Ya \/ Yb = Y by XBOOLE_1:45;
  thus f.:Xa = Ya;
A4: Xa is_a_fixpoint_of h by Th6;
  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 A4,Def1;
end;

theorem Th12: :: Schroeder-Bernstein
 f is one-to-one & g is one-to-one implies
   ex h being Function of X,Y st h is bijective
proof assume
A1: f is one-to-one & g is one-to-one;
  consider Xa, Xb, Ya, Yb being set such that
A2: Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y &
   f.:Xa = Ya & g.:Yb = Xb by Th11;
   set fXa = f|Xa; set gYb = g|Yb; set h = fXa+*gYb";
A3: dom f = X by FUNCT_2:def 1; Xa c= X by A2,XBOOLE_1:7;
then A4: dom fXa = Xa by A3,RELAT_1:91;
A5: rng fXa = Ya by A2,RELAT_1:148;
A6: fXa is one-to-one by A1,FUNCT_1:84;
A7: dom g = Y by FUNCT_2:def 1; Yb c= Y by A2,XBOOLE_1:7;
then A8: dom gYb = Yb by A7,RELAT_1:91;
A9: gYb is one-to-one by A1,FUNCT_1:84; rng gYb = Xb by A2,RELAT_1:148;
then A10: dom (gYb") = Xb by A9,FUNCT_1:54;
then A11: X = dom h by A2,A4,FUNCT_4:def 1;
A12: rng (gYb") = Yb by A8,A9,FUNCT_1:55;
     fXa \/ gYb" = h by A2,A4,A10,FUNCT_4:32;
then A13: rng h = Y by A2,A5,A12,RELAT_1:26;
  then reconsider h as Function of X, Y by A11,FUNCT_2:def 1,RELSET_1:11;
  take h;
    gYb" is one-to-one by A9,FUNCT_1:62;
then A14: h is one-to-one by A2,A5,A6,A12,Th1;
   h is onto by A13,FUNCT_2:def 3;
 hence h is bijective by A14,FUNCT_2:def 4;
end;

theorem Th13:
 (ex f st f is bijective) implies X,Y are_equipotent
proof given h being Function of X, Y such that
A1: h is bijective;
A2: h is one-to-one onto by A1,FUNCT_2:def 4;
then A3: rng h = Y by FUNCT_2:def 3;
   take h;
   hereby let x; assume
A4: x in X;
then A5: x in dom h by FUNCT_2:def 1;
    take y = h.x;
    thus y in Y by A3,A4,FUNCT_2:6;
    thus [x,y] in h by A5,FUNCT_1:8;
   end;
   hereby let y; assume y in Y;
    then consider x such that
A6:  x in dom h & y = h.x by A3,FUNCT_1:def 5;
    take x;
    thus x in X & [x,y] in h by A6,FUNCT_1:8;
   end;
   let x,y,z,u; assume
      [x,y] in h & [z,u] in h;
    then x in dom h & y = h.x & z in dom h & u = h.z by FUNCT_1:8;
   hence x = z iff y = u by A2,FUNCT_1:def 8;
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 Th12;
  hence thesis by Th13;
end;

begin :: The lattice of a lattice subset

definition
  let L be non empty LattStr, f be UnOp of L, x be Element of L;
 redefine func f.x -> Element of L;
 coherence proof
     f.x is Element of L;
  hence thesis;
 end;
end;

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
:Def6: 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 C(Ordinal,set)=f.$2;
   deffunc D(Ordinal,T-Sequence)="\/"(rng $2, L);

   (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 TS_Def;
hence thesis;
end;
 func (f, O)-.x means
:Def7: 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 C(Ordinal,set)=f.$2;
   deffunc D(Ordinal,T-Sequence)="/\"(rng $2, L);

   (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 TS_Def;
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;

canceled;

theorem Th16:
 (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 Def6;
 thus F({}) = x from TS_Result0(A1);
end;

theorem Th17:
 (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 Def7;
 thus F({}) = x from TS_Result0(A1);
end;

theorem Th18:
 (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 Def6;
    for O being Ordinal holds F(succ O) = C(O,F(O))
                            from TS_ResultS(A1);
 hence thesis;
end;

theorem Th19:
 (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 Def7;
    for O being Ordinal holds F(succ O) = C(O,F(O))
                            from TS_ResultS(A1);
 hence thesis;
end;

theorem Th20:
  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 Def6;
 thus F(O) = D(O,T) from TS_ResultL(A4, A1, A2, A3);
end;

theorem Th21:
  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 Def7;
 thus F(O) = D(O,T) from TS_ResultL(A4, A1, A2, A3);
end;

theorem
    iter(f, n).x = (f, n)+.x
proof
A1: dom f = the carrier of L by FUNCT_2:def 1;
then A2: x in dom f \/ rng f by XBOOLE_0:def 2;
defpred P[Nat] means iter(f, $1).x = (f, $1)+.x;
 iter(f, 0).x = id(dom f \/ rng f).x by FUNCT_7:70
    .= x by A2,FUNCT_1:35
    .= (f, 0)+.x by Th16; then A3: P[0];
A4: now let n be Nat; assume
     A5: P[n];
           rng f c= the carrier of L by RELSET_1:12;
then A6:  dom iter(f, n) = dom f by A1,FUNCT_7:76;
     iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:73
         .= f.(f, n)+.x by A1,A5,A6,FUNCT_1:23
         .= (f, succ n)+.x by Th18
         .= (f, n+1)+.x by CARD_1:52;
         hence P[n+1];
    end;
    for n being Nat holds P[n] from Ind(A3, A4);
 hence iter(f, n).x = (f, n)+.x;
end;

theorem
   iter(f, n).x = (f, n)-.x
proof
A1: dom f = the carrier of L by FUNCT_2:def 1;
then A2: x in dom f \/ rng f by XBOOLE_0:def 2;
defpred P[Nat] means iter(f, $1).x = (f, $1)-.x;
 iter(f, 0).x = id(dom f \/ rng f).x by FUNCT_7:70
    .= x by A2,FUNCT_1:35
    .= (f, 0)-.x by Th17; then A3: P[0];
A4: now let n be Nat; assume
     A5: P[n];
           rng f c= the carrier of L by RELSET_1:12;
then A6:   dom iter(f, n) = dom f by A1,FUNCT_7:76;
     iter(f, n+1).x = (f*iter(f, n)).x by FUNCT_7:73
         .= f.(f, n)-.x by A1,A5,A6,FUNCT_1:23
         .= (f, succ n)-.x by Th19
         .= (f, n+1)-.x by CARD_1:52;
         hence P[n+1];
    end;
    for n being Nat holds P[n] from Ind(A3, A4);
 hence iter(f, n).x = (f, n)-.x;
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
 defpred P[Ordinal] means (f, $1)+.a is Element of L;
      (f, {})+.a = a by Th16;
then A1: P[{}];
A2: now let O1; assume P[O1];
      then reconsider fa = (f, O1)+.a as Element of L;
        f.fa = (f, succ O1)+.a by Th18;
     hence P[succ O1];
    end;
    deffunc F(Ordinal)=(f, $1)+.a;
A3: now let O1; assume
    A4: O1 <> {} & O1 is_limit_ordinal &
       for O2 st O2 in O1 holds P[O2];
       consider Ls being T-Sequence such that
    A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2)
                           from TS_Lambda;
         (f, O1)+.a = "\/"(rng Ls, L) by A4,A5,Th20;
     hence P[O1];
    end;
     for O holds P[O] from Ordinal_Ind(A1, A2, A3);
  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
 defpred P[Ordinal] means (f, $1)-.a is Element of L;
      (f, {})-.a = a by Th17;
then A1: P[{}];
A2: now let O1; assume P[O1];
      then reconsider fa = (f, O1)-.a as Element of L;
        f.fa = (f, succ O1)-.a by Th19;
     hence P[succ O1];
    end;
    deffunc F(Ordinal)=(f, $1)-.a;
A3: now let O1; assume
    A4: O1 <> {} & O1 is_limit_ordinal &
       for O2 st O2 in O1 holds P[O2];
       consider Ls being T-Sequence such that
    A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 =F(O2)
                           from TS_Lambda;
         (f, O1)-.a = "/\"(rng Ls, L) by A4,A5,Th21;
     hence P[O1];
    end;
     for O holds P[O] from Ordinal_Ind(A1, A2, A3);
  hence thesis;
 end;
end;

definition
 let L be non empty LattStr, P be Subset of L;
 attr P is with_suprema means
:Def8:
  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 z' being Element of L st z' in P & x [= z' & y [= z' holds z [= z';
 attr P is with_infima means
:Def9:
  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 z' being Element of L st z' in P & z' [= x & z' [= y holds z' [= z;
end;

definition
 let L be Lattice;
 cluster non empty with_suprema with_infima 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 & y in P;
    take z = x"\/"y;
    thus z in P;
    thus x [= z & y [= z by LATTICES:22;
    let z' be Element of L; assume z' in P & x [= z' & y [= z';
    hence z [= z' by BOOLEALG:11;
   end;
  let x,y be Element of L such that x in P & y in P;
  take z = x"/\"y;
  thus z in P;
  thus z [= x & z [= y by LATTICES:23;
  let z' be Element of L; assume z' in P & z' [= x & z' [= y;
  hence z' [= z by BOOLEALG:12;
 end;
end;

definition
 let L be Lattice,
     P be non empty with_suprema with_infima Subset of L;
func latt P -> strict Lattice means
:Def10:
  the carrier of it = P &
  for x, y being Element of it ex x', y' being Element of L st x = x' & y = y'
          & (x [= y iff x' [= y');
existence proof
  set LL = LattRel L;
  set cL = the carrier of L;
  set LR = LL|_2 P;
     LR c= [:P, P:] by WELLORD1:15;
  then reconsider LR as Relation of P by RELSET_1:def 1;
 field LL = cL by FILTER_1:33;
   then
A1: LL is_reflexive_in cL & LL is_antisymmetric_in cL &
     LL is_transitive_in cL by RELAT_2:def 9,def 12,def 16;
A2: field LR = P proof
      thus field LR c= P by WELLORD1:20;
      let x be set;
       assume A3: x in P;
     then A4: [x,x] in [:P, P:] by ZFMISC_1:106;
     A5: [x,x] in LL by A1,A3,RELAT_2:def 1;
          LR = LL /\ [:P, P:] by WELLORD1:def 6;
        then [x, x] in LR by A4,A5,XBOOLE_0:def 3;
       hence x in field LR by RELAT_1:30;
     end;
     LR is reflexive by WELLORD1:22;
then A6: LR is_reflexive_in P by A2,RELAT_2:def 9;
     LR is antisymmetric by WELLORD1:25;
then A7: LR is_antisymmetric_in P by A2,RELAT_2:def 12;
     LR is transitive by WELLORD1:24;
then A8: LR is_transitive_in P by A2,RELAT_2:def 16;
  dom LR = P by A6,ORDERS_1:98;
  then LR is total by PARTFUN1:def 4;
  then reconsider LR as Order of P
         by A2,A6,A7,A8,RELAT_2:def 9,def 12,def 16;
 set RS = RelStr(#P, LR#);
A9: 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
    A10: zL in P & xL [= zL & yL [= zL &
        for z' being Element of L st z' in P & xL [= z' & yL [= z'
          holds zL [= z' by Def8;
      reconsider z = zL as Element of RS by A10;
     take z;
        [xL,zL] in [:P,P:] & [yL,zL] in [:P,P:] &
      [xL,zL] in LL & [yL,zL] in LL by A10,FILTER_1:32,ZFMISC_1:106;
      then [xL,zL] in LR & [yL,zL] in LR by WELLORD1:16;
     hence x <= z & y <= z by ORDERS_1:def 9;
     let z' be Element of RS; assume
    A11: x <= z' & y <= z';
       z' in P; then reconsider z'L = z' as Element of L;
          [x,z'] in LR & [y,z'] in LR by A11,ORDERS_1:def 9;
        then [x,z'] in LL & [y,z'] in LL by WELLORD1:16;
        then xL [= z'L & yL [= z'L by FILTER_1:32;
        then zL [= z'L by A10;
        then [zL,z'L] in [:P, P:] & [zL,z'L] in LL
                   by A10,FILTER_1:32,ZFMISC_1:106;
        then [zL,z'L] in LR by WELLORD1:16;
     hence z <= z' by ORDERS_1:def 9;
    end;
A12: 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
    A13: zL in P & zL [= xL & zL [= yL &
        for z' being Element of L st z' in P & z' [= xL & z' [= yL
          holds z' [= zL by Def9;
      reconsider z = zL as Element of RS by A13;
     take z;
        [zL,xL] in [:P,P:] & [zL,yL] in [:P,P:] &
      [zL,xL] in LL & [zL,yL] in LL by A13,FILTER_1:32,ZFMISC_1:106;
      then [zL,xL] in LR & [zL,yL] in LR by WELLORD1:16;
     hence z <= x & z <= y by ORDERS_1:def 9;
     let z' be Element of RS; assume
    A14: z' <= x & z' <= y;
       z' in P; then reconsider z'L = z' as Element of L;
          [z',x] in LR & [z',y] in LR by A14,ORDERS_1:def 9;
        then [z',x] in LL & [z',y] in LL by WELLORD1:16;
        then z'L [= xL & z'L [= yL by FILTER_1:32;
        then z'L [= zL by A13;
        then [z'L,zL] in [:P, P:] & [z'L,zL] in LL
                   by A13,FILTER_1:32,ZFMISC_1:106;
        then [z'L,zL] in LR by WELLORD1:16;
     hence z' <= z by ORDERS_1:def 9;
    end;
A15: RS is Poset by A6,A7,A8,ORDERS_1:def 4,def 5,def 6;
 take IT = latt RS;
A16: LattPOSet IT = RelStr(#the carrier of IT, LattRel IT#) by LATTICE3:def 2;
A17: RS = LattPOSet IT by A9,A12,A15,LATTICE3:def 15;
 thus
  the carrier of IT = P by A9,A12,A15,A16,LATTICE3:def 15;
 let x, y be Element of IT;
     x in P & y in P by A16,A17;
  then reconsider x' = x, y' = y as Element of L;
 take x', y';
 thus x = x' & y = y';
 hereby assume x [= y;
    then [x, y] in LR by A16,A17,FILTER_1:32;
    then [x, y] in LattRel L by WELLORD1:16;
  hence x' [= y' by FILTER_1:32;
 end;
A18: [x, y] in [:P, P:] by A16,A17,ZFMISC_1:106;
 assume x' [= y';
   then [x, y] in LattRel L by FILTER_1:32;
   then [x, y] in LattRel IT by A16,A17,A18,WELLORD1:16;
 hence x [= y by FILTER_1:32;
end;
uniqueness proof
 let it1, it2 be strict Lattice such that
A19: the carrier of it1 = P &
 for x, y being Element of it1 ex x', y' being Element of L st x = x' & y = y'
          & (x [= y iff x' [= y') and
A20: the carrier of it2 = P &
 for x, y being Element of it2 ex x', y' being Element of L st x = x' & y = y'
          & (x [= y iff x' [= y');
A21: LattPOSet it1 = RelStr(#the carrier of it1,LattRel it1#)
          by LATTICE3:def 2;
A22: LattPOSet it2 = RelStr(#the carrier of it2,LattRel it2#)
          by LATTICE3:def 2;
A23: LattRel it1 = { [p,q] where p is Element of it1,
              q is Element of it1: p [= q }
                         by FILTER_1:def 8;
A24: LattRel it2 = { [p,q] where p is Element of it2,
              q is Element of it2: 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
     A25: a = [p1, q1] & p1 [= q1 by A23;
       reconsider p1, q1 as Element of it1;
       consider pl1, ql1 being Element of L such that
     A26: p1 = pl1 & q1 = ql1 & (p1 [= q1 iff pl1 [= ql1) by A19;
       reconsider p2 = p1, q2 = q1 as Element of it2 by A19,A20;
       consider pl2, ql2 being Element of L such that
     A27: p2 = pl2 & q2 = ql2 & (p2 [= q2 iff pl2 [= ql2) by A20;
      thus a in LattRel it2 by A24,A25,A26,A27;
     end;
     assume a in LattRel it2;
       then consider p1, q1 being Element of it2 such that
     A28: a = [p1, q1] & p1 [= q1 by A24;
       reconsider p1, q1 as Element of it2;
       consider pl1, ql1 being Element of L such that
     A29: p1 = pl1 & q1 = ql1 & (p1 [= q1 iff pl1 [= ql1) by A20;
       reconsider p2 = p1, q2 = q1 as Element of it1 by A19,A20;
       consider pl2, ql2 being Element of L such that
     A30: p2 = pl2 & q2 = ql2 & (p2 [= q2 iff pl2 [= ql2) by A19;
      thus a in LattRel it1 by A23,A28,A29,A30;
    end;
   then LattRel it1 = LattRel it2 by TARSKI:2;
 hence it1 = it2 by A19,A20,A21,A22,LATTICE3:6;
end;
end;

begin :: Complete lattices ::::::::::::::::::::::::::::::::::::::::::::::::

definition
cluster complete -> bounded Lattice;
 coherence proof let L be Lattice; assume L is complete;
   then L is 0_Lattice & L is 1_Lattice by LATTICE3:50,51;
  hence L is bounded by LATTICES:def 15;
 end;
end;

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

theorem Th24:
 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 a be Element of L; assume a in H;
      then consider h being Element of L such that
   A1: a = h & h [= f.h;
      reconsider fh = f.h as Element of L;
      take fh;
      thus a [= fh & fh in fH by A1;
   end;
then A2: uH [= fuH by LATTICE3:48;
     now let fh be Element of L; assume fh in fH;
     then consider h being Element of L such that
   A3: fh = f.h & h [= f.h;
        h in H by A3;
      then h [= uH by LATTICE3:38;
    hence fh [= f.uH by A3,QUANTAL1:def 12;
   end;
   then fH is_less_than f.uH by LATTICE3:def 17;
   then fuH [= f.uH by LATTICE3:def 21;
then A4: uH [= f.uH by A2,LATTICES:25;
   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 A4,LATTICES:26;
end;

theorem Th25:
 for a st a [= f.a for O holds a [= (f, O)+.a
proof
 let a; assume
A1: a [= f.a;
 defpred S[Ordinal] means a [= (f, $1)+.a;
A2: S[{}] by Th16;
A3: now let O1; assume S[O1];
      then f.a [= f.((f, O1)+.a) by QUANTAL1:def 12;
      then a [= f.((f, O1)+.a) by A1,LATTICES:25;
     hence S[succ O1] by Th18;
    end;
    deffunc F(Ordinal)=(f, $1)+.a;
A4: now let O1; assume
    A5: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
      consider Ls being T-Sequence such that
    A6: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2)
                           from TS_Lambda;
      consider O2 being set such that
    A7: O2 in O1 by A5,XBOOLE_0:def 1;
      reconsider O2 as Ordinal by A7,ORDINAL1:23;
    A8: Ls.O2 = (f, O2)+.a by A6,A7;
        Ls.O2 in rng Ls by A6,A7,FUNCT_1:def 5;
    then A9: (f, O2)+.a [= "\/"(rng Ls, L) by A8,LATTICE3:38;
        S[O2] by A5,A7;
      then a [= "\/"(rng Ls, L) by A9,LATTICES:25;
     hence S[O1] by A5,A6,Th20;
    end;
 thus for O holds S[O] from Ordinal_Ind(A2, A3, A4);
end;

theorem Th26:
 for a st f.a [= a for O holds (f, O)-.a [= a
proof
 let a; assume
A1: f.a [= a;
 defpred S[Ordinal] means (f, $1)-.a [= a;
A2: S[{}] by Th17;
A3: now let O1; assume S[O1];
      then f.((f, O1)-.a) [= f.a by QUANTAL1:def 12;
      then f.((f, O1)-.a) [= a by A1,LATTICES:25;
     hence S[succ O1] by Th19;
    end;
    deffunc F(Ordinal)=(f, $1)-.a;
A4: now let O1; assume
    A5: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
      consider Ls being T-Sequence such that
    A6: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = F(O2)
                           from TS_Lambda;
      consider O2 being set such that
    A7: O2 in O1 by A5,XBOOLE_0:def 1;
      reconsider O2 as Ordinal by A7,ORDINAL1:23;
    A8: Ls.O2 = (f, O2)-.a by A6,A7;
        Ls.O2 in rng Ls by A6,A7,FUNCT_1:def 5;
    then A9:  "/\"(rng Ls, L) [= (f, O2)-.a by A8,LATTICE3:38;
        S[O2] by A5,A7;
      then "/\"(rng Ls, L) [= a by A9,LATTICES:25;
     hence S[O1] by A5,A6,Th21;
    end;
 thus for O holds S[O] from Ordinal_Ind(A2, A3, A4);
end;

theorem Th27:
  for a st a [= f.a
   for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a
proof let a; assume
A1: a [= f.a;
 defpred S[Ordinal] means
              for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O1)+.a [= (f, O2)+.a;
A2: S[{}]
   proof
     let O1, O2; assume A3: O1 c= O2 & O2 c= {};
      then O2 = {} by XBOOLE_1:3;
     hence (f, O1)+.a [= (f, O2)+.a by A3,XBOOLE_1:3;
    end;
A4: now let O4; assume A5: S[O4];
     thus S[succ O4]
     proof
     let O1, O2; assume
    A6: O1 c= O2 & O2 c= succ O4;
    per cases;
    suppose O1 = O2 & O2 <> succ O4;
     hence (f, O1)+.a [= (f, O2)+.a;
    suppose O1 <> O2 & O2 <> succ O4;
      then O2 c< succ O4 by A6,XBOOLE_0:def 8;
      then O2 in succ O4 by ORDINAL1:21;
      then O2 c= O4 by ORDINAL1:34;
     hence (f, O1)+.a [= (f, O2)+.a by A5,A6;
    suppose O1 = O2 & O2 = succ O4;
     hence (f, O1)+.a [= (f, O2)+.a;
    suppose A7: O1 <> O2 & O2 = succ O4;
        then O1 c< O2 by A6,XBOOLE_0:def 8;
    then A8: O1 in O2 by ORDINAL1:21;
    A9: (f, O4)+.a [= (f, succ O4)+.a proof
     per cases by ORDINAL1:42;
     suppose A10: O4 is_limit_ordinal;
      thus thesis proof
      per cases;
      suppose O4 = {};
       then (f, O4)+.a = a by Th16;
       hence thesis by A1,Th18;
      suppose A11: O4 <> {};
      deffunc F(Ordinal)=(f, $1)+.a;
          consider L1 being T-Sequence such that
      A12: dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
                                            from TS_Lambda;
      A13: (f, O4)+.a = "\/"(rng L1, L) by A10,A11,A12,Th20;
            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
          A14: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
            reconsider O3 as Ordinal by A14,ORDINAL1:23;
               O3 c= O4 by A12,A14,ORDINAL1:def 2;
             then (f, O3)+.a [= (f, O4)+.a by A5;
             then f.(f, O3)+.a [= f.(f, O4)+.a by QUANTAL1:def 12;
             then (f, succ O3)+.a [= f.(f, O4)+.a by Th18;
           then A15: (f, succ O3)+.a [= (f, succ O4)+.a by Th18;
           A16: succ O3 c= O4 by A12,A14,ORDINAL1:33;
                 O3 in succ O3 by ORDINAL1:10;
               then O3 c= succ O3 by ORDINAL1:def 2;
           then A17: (f, O3)+.a [= (f, succ O3)+.a by A5,A16;
                 q = (f, O3)+.a by A12,A14;
           hence q [= (f, succ O4)+.a by A15,A17,LATTICES:25;
          end;
       hence thesis by A13,LATTICE3:def 21;
      end;
     suppose ex O3 st O4 = succ O3; then consider O3 such that
      A18: O4 = succ O3;
            succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
          then O3 c= O4 by A18,XBOOLE_1:7;
          then (f, O3)+.a [= (f, O4)+.a by A5;
          then f.((f, O3)+.a) [= f.((f, O4)+.a) by QUANTAL1:def 12;
          then (f, O4)+.a [= f.((f, O4)+.a) by A18,Th18;
      hence thesis by Th18;
     end;
        O1 c= O4 by A7,A8,ORDINAL1:34;
      then (f, O1)+.a [= (f, O4)+.a by A5;
     hence (f, O1)+.a [= (f, O2)+.a by A7,A9,LATTICES:25;
     end;
    end;
A19: now let O4; assume
    A20: O4 <> {} & O4 is_limit_ordinal & for O3 st O3 in O4 holds S[O3];
    thus S[O4]
    proof
     let O1, O2; assume
    A21: O1 c= O2 & O2 c= O4;
A22:   O2 c< O4 iff O2 c= O4 & O2 <> O4 by XBOOLE_0:def 8;
A23:   O1 c< O2 iff O1 c= O2 & O1 <> O2 by XBOOLE_0:def 8;
     per cases by A21,A22,ORDINAL1:21;
     suppose A24: O2 = O4;
      thus (f, O1)+.a [= (f, O2)+.a proof
       per cases by A21,A23,ORDINAL1:21;
       suppose O1 = O2;
        hence thesis;
       suppose A25: O1 in O2;
       deffunc F(Ordinal)=(f, $1)+.a;
           consider L1 being T-Sequence such that
      A26: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
                      from TS_Lambda;
      A27: (f, O2)+.a = "\/"(rng L1, L) by A20,A24,A26,Th20;
          L1.O1 = (f, O1)+.a & L1.O1 in rng L1 by A25,A26,FUNCT_1:def 5;
       hence thesis by A27,LATTICE3:38;
      end;
     suppose O2 in O4;
      hence (f, O1)+.a [= (f, O2)+.a by A20,A21;
    end;
    end;
A28: for O4 holds S[O4] from Ordinal_Ind(A2, A4, A19);
 let O1, O2; assume O1 c= O2;
 hence (f, O1)+.a [= (f, O2)+.a by A28;
end;

theorem Th28:
  for a st f.a [= a
   for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a
proof let a; assume
A1: f.a [= a;
 defpred S[Ordinal] means
              for O1, O2 st O1 c= O2 & O2 c= $1 holds (f, O2)-.a [= (f, O1)-.a;
A2: S[{}]
    proof
     let O1, O2; assume A3: O1 c= O2 & O2 c= {};
      then O2 = {} by XBOOLE_1:3;
     hence (f, O2)-.a [= (f, O1)-.a by A3,XBOOLE_1:3;
    end;
A4: now let O4; assume
    A5: S[O4];
    thus S[succ O4]
    proof
     let O1, O2; assume
    A6: O1 c= O2 & O2 c= succ O4;
    per cases;
    suppose O1 = O2 & O2 <> succ O4;
     hence (f, O2)-.a [= (f, O1)-.a;
    suppose O1 <> O2 & O2 <> succ O4;
      then O2 c< succ O4 by A6,XBOOLE_0:def 8;
      then O2 in succ O4 by ORDINAL1:21;
      then O2 c= O4 by ORDINAL1:34;
     hence (f, O2)-.a [= (f, O1)-.a by A5,A6;
    suppose O1 = O2 & O2 = succ O4;
     hence (f, O2)-.a [= (f, O1)-.a;
    suppose A7: O1 <> O2 & O2 = succ O4;
        then O1 c< O2 by A6,XBOOLE_0:def 8;
    then A8: O1 in O2 by ORDINAL1:21;
    A9: (f, succ O4)-.a [= (f, O4)-.a proof
     per cases by ORDINAL1:42;
     suppose A10: O4 is_limit_ordinal;
      thus thesis proof
      per cases;
      suppose O4 = {};
       then (f, O4)-.a = a by Th17;
       hence thesis by A1,Th19;
      suppose A11: O4 <> {};
      deffunc F(Ordinal)=(f, $1)-.a;
          consider L1 being T-Sequence such that
      A12: dom L1 = O4 & for O3 st O3 in O4 holds L1.O3 = F(O3)
                    from TS_Lambda;
      A13: (f, O4)-.a = "/\"(rng L1, L) by A10,A11,A12,Th21;
            (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
          A14: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
            reconsider O3 as Ordinal by A14,ORDINAL1:23;
               O3 c= O4 by A12,A14,ORDINAL1:def 2;
             then (f, O4)-.a [= (f, O3)-.a by A5;
             then f.(f, O4)-.a [= f.(f, O3)-.a by QUANTAL1:def 12;
             then (f, succ O4)-.a [= f.(f, O3)-.a by Th19;
           then A15: (f, succ O4)-.a [= (f, succ O3)-.a by Th19;
           A16: succ O3 c= O4 by A12,A14,ORDINAL1:33;
                 O3 in succ O3 by ORDINAL1:10;
               then O3 c= succ O3 by ORDINAL1:def 2;
           then A17: (f, succ O3)-.a [= (f, O3)-.a by A5,A16;
                 q = (f, O3)-.a by A12,A14;
           hence (f, succ O4)-.a [= q by A15,A17,LATTICES:25;
          end;
       hence thesis by A13,LATTICE3:34;
      end;
     suppose ex O3 st O4 = succ O3; then consider O3 such that
      A18: O4 = succ O3;
            succ O3 = O3 \/ {O3} by ORDINAL1:def 1;
          then O3 c= O4 by A18,XBOOLE_1:7;
          then (f, O4)-.a [= (f, O3)-.a by A5;
          then f.((f, O4)-.a) [= f.((f, O3)-.a) by QUANTAL1:def 12;
          then f.((f, O4)-.a) [= (f, O4)-.a by A18,Th19;
      hence thesis by Th19;
     end;
        O1 c= O4 by A7,A8,ORDINAL1:34;
      then (f, O4)-.a [= (f, O1)-.a by A5;
     hence (f, O2)-.a [= (f, O1)-.a by A7,A9,LATTICES:25;
     end;
    end;
A19: now let O4; assume
    A20: O4 <> {} & O4 is_limit_ordinal & for O3 st O3 in O4 holds S[O3];
    thus S[O4]
    proof
     let O1, O2; assume
    A21: O1 c= O2 & O2 c= O4;
A22:   O2 c< O4 iff O2 c= O4 & O2 <> O4 by XBOOLE_0:def 8;
A23:   O1 c< O2 iff O1 c= O2 & O1 <> O2 by XBOOLE_0:def 8;
     per cases by A21,A22,ORDINAL1:21;
     suppose A24: O2 = O4;
      thus (f, O2)-.a [= (f, O1)-.a proof
       per cases by A21,A23,ORDINAL1:21;
       suppose O1 = O2;
        hence thesis;
       suppose A25: O1 in O2;
       deffunc F(Ordinal)=(f, $1)-.a;
           consider L1 being T-Sequence such that
      A26: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
                from TS_Lambda;
      A27: (f, O2)-.a = "/\"(rng L1, L) by A20,A24,A26,Th21;
          L1.O1 = (f, O1)-.a & L1.O1 in rng L1 by A25,A26,FUNCT_1:def 5;
       hence thesis by A27,LATTICE3:38;
      end;
     suppose O2 in O4;
      hence (f, O2)-.a [= (f, O1)-.a by A20,A21;
    end;
    end;
A28: for O4 holds S[O4] from Ordinal_Ind(A2, A4, A19);
 let O1, O2; assume O1 c= O2;
 hence (f, O2)-.a [= (f, O1)-.a by A28;
end;

theorem Th29:
  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; assume
A2: O1 c< O2 & not (f, O2)+.a is_a_fixpoint_of f &
   (f, O1)+.a = (f, O2)+.a;
   then O1 in O2 by ORDINAL1:21;
   then succ O1 c= O2 by ORDINAL1:33;
then A3: (f, succ O1)+.a [= (f, O2)+.a by A1,Th27;
     succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
   then O1 c= succ O1 by XBOOLE_1:7;
  then (f, O1)+.a [= (f, succ O1)+.a by A1,Th27;
  then (f, O1)+.a = (f, succ O1)+.a by A2,A3,LATTICES:26;
  then (f, O1)+.a = f.(f, O1)+.a by Th18;
 hence contradiction by A2,Def2;
end;

theorem Th30:
  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; assume
A2: O1 c< O2 & not (f, O2)-.a is_a_fixpoint_of f &
   (f, O1)-.a = (f, O2)-.a;
   then O1 in O2 by ORDINAL1:21;
   then succ O1 c= O2 by ORDINAL1:33;
then A3: (f, O2)-.a [= (f, succ O1)-.a by A1,Th28;
     succ O1 = O1 \/ {O1} by ORDINAL1:def 1;
   then O1 c= succ O1 by XBOOLE_1:7;
  then (f, succ O1)-.a [= (f, O1)-.a by A1,Th28;
  then (f, O1)-.a = (f, succ O1)-.a by A2,A3,LATTICES:26;
  then (f, O1)-.a = f.(f, O1)-.a by Th19;
 hence contradiction by A2,Def2;
end;

theorem Th31:
 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
A1: a [= f.a & (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;
A2: S[{}] by XBOOLE_1:3;
A3: now let O2; assume
    A4: S[O2];
    thus S[succ O2]
    proof
     assume
A5:   O1 c= succ O2;
     per cases;
     suppose O1 = succ O2;
      hence fa = (f, succ O2)+.a;
     suppose O1 <> succ O2;
      then O1 c< succ O2 by A5,XBOOLE_0:def 8;
then O1 in succ O2 by ORDINAL1:21;
     hence fa = f.(f, O2)+.a by A1,A4,Def1,ORDINAL1:34
            .= (f, succ O2)+.a by Th18;
    end;
    end;
A6: now let O2; assume
    A7: O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds S[O3];
     thus S[O2]
     proof
       deffunc F(Ordinal)=(f, $1)+.a;
        consider L1 being T-Sequence such that
    A8: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
            from TS_Lambda;
    A9: (f, O2)+.a = "\/"(rng L1, L) by A7,A8,Th20;
          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
        A10: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
            reconsider O3 as Ordinal by A10,ORDINAL1:23;
            per cases;
            suppose O1 c= O3;
              then (f, O3)+.a [= fa by A7,A8,A10;
             hence q [= fa by A8,A10;
            suppose O3 c= O1;
              then (f, O3)+.a [= fa by A1,Th27;
             hence q [= fa by A8,A10;
        end;
     then A11: (f, O2)+.a [= fa by A9,LATTICE3:def 21;
        assume O1 c= O2; then fa [= (f, O2)+.a by A1,Th27;
     hence fa = (f, O2)+.a by A11,LATTICES:26;
     end;
    end;
 thus for O2 holds S[O2] from Ordinal_Ind(A2, A3, A6);
end;

theorem Th32:
 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
A1: f.a [= a & (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;
A2: S[{}] by XBOOLE_1:3;
A3: now let O2; assume
    A4: S[O2];
    thus S[succ O2]
    proof
     assume
A5:  O1 c= succ O2;
     per cases;
     suppose O1 = succ O2;
      hence fa = (f, succ O2)-.a;
     suppose O1 <> succ O2;
      then O1 c< succ O2 by A5,XBOOLE_0:def 8;
then O1 in succ O2 by ORDINAL1:21;
    hence fa = f.(f, O2)-.a by A1,A4,Def1,ORDINAL1:34
            .= (f, succ O2)-.a by Th19;
    end;
    end;
A6: now let O2; assume
    A7: O2 <> {} & O2 is_limit_ordinal & for O3 st O3 in O2 holds S[O3];
     thus S[O2]
     proof
       deffunc F(Ordinal)=(f, $1)-.a;
        consider L1 being T-Sequence such that
    A8: dom L1 = O2 & for O3 st O3 in O2 holds L1.O3 = F(O3)
             from TS_Lambda;
    A9: (f, O2)-.a = "/\"(rng L1, L) by A7,A8,Th21;
          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
        A10: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
            reconsider O3 as Ordinal by A10,ORDINAL1:23;
            per cases;
            suppose O1 c= O3;
             then fa [= (f, O3)-.a by A7,A8,A10;
             hence fa [= q by A8,A10;
            suppose O3 c= O1;
             then fa [= (f, O3)-.a by A1,Th28;
             hence fa [= q by A8,A10;
        end;
     then A11: fa [= (f, O2)-.a by A9,LATTICE3:40;
        assume O1 c= O2; then (f, O2)-.a [= fa by A1,Th28;
     hence fa = (f, O2)-.a by A11,LATTICES:26;
     end;
    end;
 thus for O2 holds S[O2] from Ordinal_Ind(A2, A3, A6);
end;

Lm1: :: trzeba przenisc do ORDINAL1
 O1 c< O2 or O1 = O2 or O2 c< O1
proof assume not(O1 c< O2 or O1 = O2 or O2 c< O1);
  then not(O1 c= O2 or O2 c= O1) by XBOOLE_0:def 8;
 hence contradiction;
end;

theorem Th33:
  for a st a [= f.a
   ex O st Card O <=` Card the carrier of L & (f, O)+.a is_a_fixpoint_of f
proof let a; assume
A1: a [= f.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
A2: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(O2)
                         from TS_Lambda;
     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
   A5: x1 in dom Ls & x2 in dom Ls & Ls.x1 = Ls.x2;
       then reconsider x1, x2 as Ordinal by ORDINAL1:23;
   A6: Ls.x1 = (f, x1)+.a & Ls.x2 = (f, x2)+.a by A2,A5;
      per cases by Lm1;
      suppose A7: x1 c< x2;
         not (f, x2)+.a is_a_fixpoint_of f by A2,A3,A5;
       hence thesis by A1,A5,A6,A7,Th29;
      suppose A8: x2 c< x1;
         not (f, x1)+.a is_a_fixpoint_of f by A2,A3,A5;
       hence thesis by A1,A5,A6,A8,Th29;
      suppose x2 = x1;
       hence thesis;
     end;
       rng Ls c= cL proof let y be set; assume y in rng Ls;
       then consider x being set such that
     A9: x in dom Ls & Ls.x = y by FUNCT_1:def 5;
        reconsider x as Ordinal by A9,ORDINAL1:23;
          Ls.x = (f, x)+.a by A2,A9;
      hence y in cL by A9;
     end;
     then Card nccL <=` ccL by A2,A4,CARD_1:26;
     then nccL <=` ccL & ccL <` nccL by CARD_1:32,def 5;
    hence contradiction by CARD_1:14;
   end;
   then consider O such that
A10: O in nccL & (f, O)+.a is_a_fixpoint_of f;
 take O;
    Card O <` nccL by A10,CARD_1:25;
 hence Card O <=` Card cL by CARD_4:23;
 thus (f, O)+.a is_a_fixpoint_of f by A10;
end;

theorem Th34:
  for a st f.a [= a
   ex O st Card O <=` Card the carrier of L & (f, O)-.a is_a_fixpoint_of f
proof let a; assume
A1: f.a [= 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
A2: dom Ls = nccL & for O2 being Ordinal st O2 in nccL holds Ls.O2 = F(O2)
                         from TS_Lambda;
     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
   A5: x1 in dom Ls & x2 in dom Ls & Ls.x1 = Ls.x2;
       then reconsider x1, x2 as Ordinal by ORDINAL1:23;
   A6: Ls.x1 = (f, x1)-.a & Ls.x2 = (f, x2)-.a by A2,A5;
      per cases by Lm1;
      suppose A7: x1 c< x2;
         not (f, x2)-.a is_a_fixpoint_of f by A2,A3,A5;
       hence thesis by A1,A5,A6,A7,Th30;
      suppose A8: x2 c< x1;
         not (f, x1)-.a is_a_fixpoint_of f by A2,A3,A5;
       hence thesis by A1,A5,A6,A8,Th30;
      suppose x2 = x1;
       hence thesis;
     end;
       rng Ls c= cL proof let y be set; assume y in rng Ls;
       then consider x being set such that
     A9: x in dom Ls & Ls.x = y by FUNCT_1:def 5;
        reconsider x as Ordinal by A9,ORDINAL1:23;
          Ls.x = (f, x)-.a by A2,A9;
      hence y in cL by A9;
     end;
     then Card nccL <=` ccL by A2,A4,CARD_1:26;
     then nccL <=` ccL & ccL <` nccL by CARD_1:32,def 5;
    hence contradiction by CARD_1:14;
   end;
   then consider O such that
A10: O in nccL & (f, O)-.a is_a_fixpoint_of f;
 take O;
    Card O <` nccL by A10,CARD_1:25;
 hence Card O <=` Card cL by CARD_4:23;
 thus (f, O)-.a is_a_fixpoint_of f by A10;
end;

theorem Th35:
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f
   ex O st Card O <=` 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; assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
then A1: a = f.a & b = f.b by Def1;
   reconsider ab = a"\/"b as Element of L;
A2: a [= ab & b [= ab by LATTICES:22;
   then f.a [= f.ab & f.b [= f.ab by QUANTAL1:def 12;
then A3: ab [= f.ab by A1,FILTER_0:6;
   then consider O such that
A4: Card O <=` Card the carrier of L &
      (f, O)+.ab is_a_fixpoint_of f by Th33;
 take O;
 thus Card O <=` Card the carrier of L &
      (f, O)+.(a"\/"b) is_a_fixpoint_of f by A4;
A5: ab [= (f, O)+.(a"\/"b) by A3,Th25;
 hence a [= (f, O)+.(a"\/"b) by A2,LATTICES:25;
 thus b [= (f, O)+.(a"\/"b) by A2,A5,LATTICES:25;
end;

theorem Th36:
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f
   ex O st Card O <=` 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; assume a is_a_fixpoint_of f & b is_a_fixpoint_of f;
then A1: a = f.a & b = f.b by Def1;
   reconsider ab = a"/\"b as Element of L;
A2: ab [= a & ab [= b by LATTICES:23;
   then f.ab [= f.a & f.ab [= f.b by QUANTAL1:def 12;
then A3: f.ab [= ab by A1,FILTER_0:7;
   then consider O such that
A4: Card O <=` Card the carrier of L &
      (f, O)-.ab is_a_fixpoint_of f by Th34;
 take O;
 thus Card O <=` Card the carrier of L &
      (f, O)-.(a"/\"b) is_a_fixpoint_of f by A4;
A5: (f, O)-.(a"/\"b) [= ab by A3,Th26;
 hence (f, O)-.(a"/\"b) [= a by A2,LATTICES:25;
 thus (f, O)-.(a"/\"b) [= b by A2,A5,LATTICES:25;
end;

theorem Th37:
 a [= f.a & a [= b & b is_a_fixpoint_of f
  implies for O2 holds (f, O2)+.a [= b
proof assume
A1: a [= f.a & a [= b & b is_a_fixpoint_of f;
then A2: f.b = b by Def1;
 defpred S[Ordinal] means (f, $1)+.a [= b;
A3: S[{}] by A1,Th16;
A4: now let O1; assume S[O1];
      then f.(f, O1)+.a [= f.b by QUANTAL1:def 12;
     hence S[succ O1] by A2,Th18;
    end;
A5: now let O1; assume
    A6: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
    deffunc F(Ordinal)=(f, $1)+.a;
        consider L1 being T-Sequence such that
    A7: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
            from TS_Lambda;
    A8: (f, O1)+.a = "\/"(rng L1, L) by A6,A7,Th20;
          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
        A9: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
            reconsider O3 as Ordinal by A9,ORDINAL1:23;
           (f, O3)+.a [= b by A6,A7,A9;
           hence q [= b by A7,A9;
        end;
     hence S[O1] by A8,LATTICE3:def 21;
    end;
  thus for O2 holds S[O2] from Ordinal_Ind(A3, A4, A5);
end;

theorem Th38:
 f.a [= a & b [= a & b is_a_fixpoint_of f
  implies for O2 holds b [= (f, O2)-.a
proof
 assume
A1: f.a [= a & b [= a & b is_a_fixpoint_of f;
then A2: f.b = b by Def1;
 defpred S[Ordinal] means b [= (f, $1)-.a;
A3: S[{}] by A1,Th17;
A4: now let O1; assume S[O1];
     then f.b [= f.(f, O1)-.a by QUANTAL1:def 12;
     hence S[succ O1] by A2,Th19;
    end;
A5: now let O1; assume
    A6: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
    deffunc F(Ordinal)=(f, $1)-.a;
        consider L1 being T-Sequence such that
    A7: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
             from TS_Lambda;
    A8: (f, O1)-.a = "/\"(rng L1, L) by A6,A7,Th21;
          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
        A9: O3 in dom L1 & q = L1.O3 by FUNCT_1:def 5;
            reconsider O3 as Ordinal by A9,ORDINAL1:23;
              b [= (f, O3)-.a by A6,A7,A9;
           hence b [= q by A7,A9;
        end;
     hence S[O1] by A8,LATTICE3:40;
    end;
  thus for O2 holds S[O2] from Ordinal_Ind(A3, A4, A5);
end;

definition
 let L be complete Lattice, f be UnOp of L such that
A1: f is monotone;
 func FixPoints f -> strict Lattice means
:Def11:
 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]};
  consider a being Element of L such that
A2: a is_a_fixpoint_of f by A1,Th24;
A3: a in P by A2;
      P is Subset of L from SubsetD;
    then reconsider P as Subset of L;
A4: P is with_suprema proof
     let x,y be Element of L;assume A5: x in P & y in P;
      then consider a being Element of L such that
    A6: x = a & a is_a_fixpoint_of f;
      consider b being Element of L such that
    A7: y = b & b is_a_fixpoint_of f by A5;
     reconsider a, b as Element of L;
     reconsider ab = a"\/"b as Element of L;
      consider O such that
    A8: Card O <=` Card the carrier of L &
        (f, O)+.ab is_a_fixpoint_of f &
        a [= (f, O)+.ab & b [= (f, O)+.ab by A1,A6,A7,Th35;
     set z = (f, O)+.ab;
     take z;
     thus z in P by A8;
     thus x [= z & y [= z by A6,A7,A8;
     let z' be Element of L; assume
    A9: z' in P & x [= z' & y [= z';
      then consider zz being Element of L such that
    A10: zz = z' & zz is_a_fixpoint_of f;
    A11: a = f.a & b = f.b by A6,A7,Def1;
          a [= ab & b [= ab by LATTICES:22;
        then f.a [= f.ab & f.b [= f.ab by A1,QUANTAL1:def 12;
    then A12: ab [= f.ab by A11,FILTER_0:6;
          ab [= z' by A6,A7,A9,FILTER_0:6;
     hence z [= z' by A1,A10,A12,Th37;
    end;
  P is with_infima proof
     let x,y be Element of L; assume A13: x in P & y in P;
      then consider a being Element of L such that
    A14: x = a & a is_a_fixpoint_of f;
      consider b being Element of L such that
    A15: y = b & b is_a_fixpoint_of f by A13;
     reconsider a, b as Element of L;
     reconsider ab = a"/\"b as Element of L;
      consider O such that
    A16: Card O <=` Card the carrier of L &
        (f, O)-.ab is_a_fixpoint_of f &
        (f, O)-.ab [= a & (f, O)-.ab [= b by A1,A14,A15,Th36;
     set z = (f, O)-.ab;
     take z;
     thus z in P by A16;
     thus z [= x & z [= y by A14,A15,A16;
     let z' be Element of L; assume
    A17: z' in P & z' [= x & z' [= y;
      then consider zz being Element of L such that
    A18: zz = z' & zz is_a_fixpoint_of f;
    A19: a = f.a & b = f.b by A14,A15,Def1;
          ab [= a & ab [= b by LATTICES:23;
        then f.ab [= f.a & f.ab [= f.b by A1,QUANTAL1:def 12;
    then A20: f.ab [= ab by A19,FILTER_0:7;
          z' [= ab by A14,A15,A17,FILTER_0:7;
     hence z' [= z by A1,A18,A20,Th38;
    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 Th39:
 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 Def11;
 hence thesis by Def10;
end;

theorem Th40:
  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 Th39;
 let x be set; assume x in the carrier of FixPoints f;
  then consider a such that
A2: x = a & a is_a_fixpoint_of f by A1;
 thus x in the carrier of L by A2;
end;

theorem Th41:
  (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 Th39;
 hereby assume a in the carrier of FixPoints f; then consider b such that
 A2: a = b & b is_a_fixpoint_of f by A1;
  thus a is_a_fixpoint_of f by A2;
 end;
 assume a is_a_fixpoint_of f;
 hence thesis by A1;
end;

theorem Th42:
  for x, y being Element of FixPoints f, a, b
     st x = a & y = b holds (x [= y iff a [= b)
proof
   consider P being non empty with_suprema with_infima Subset of L such that
A1: P = {x where x is Element of L: x is_a_fixpoint_of f} &
   FixPoints f = latt P by Def11;
 let x, y be Element of FixPoints f, a, b; assume
A2: x = a & y = b;
  consider a', b' being Element of L such that
A3: x = a' & y = b' & (x [= y iff a' [= b') by A1,Def10;
 thus x [= y iff a [= b by A2,A3;
end;

theorem
    FixPoints f is complete
proof
   set F = FixPoints f;
   set cF = the carrier of F;
   set cL = the carrier of L;
A1: cF = {x where x is Element of L: x is_a_fixpoint_of f} by Th39;
  let X be set;
  set Y = X /\ cF;
A2: Y c= X & Y c= cF by XBOOLE_1:17;
  set s = "\/"(Y, L);
     Y is_less_than f.s proof
    let q be Element of cL; assume
   A3: q in Y;
       then q [= s by LATTICE3:38;
   then A4: f.q [= f.s by QUANTAL1:def 12;
       reconsider q' = q as Element of L;
         q' is_a_fixpoint_of f by A2,A3,Th41;
    hence q [= f.s by A4,Def1;
   end;
then A5: s [= f.s by LATTICE3:def 21;
   then consider O such that
A6: Card O <=` Card cL & (f, O)+.s is_a_fixpoint_of f by Th33;
  reconsider p' = (f, O)+.s as Element of L;
  reconsider p = p' as Element of cF by A6,Th41;
  reconsider p'' = p as Element of F;
  take p;
  thus X is_less_than p proof
   let q be Element of cF; assume
  A7: q in X;
      reconsider q' = q as Element of F;
        q in cF & cF c= cL by Th40;
      then reconsider qL' = q as Element of L;
        q in Y by A7,XBOOLE_0:def 3;
  then A8: qL' [= s by LATTICE3:38;
        s [= p' by A5,Th25;
      then qL' [= p' by A8,LATTICES:25;
      then q' [= p'' by Th42;
    hence q [= p;
  end;
  let r be Element of cF such that
A9: X is_less_than r;
     r in the carrier of F;
    then consider r' being Element of L such that
A10: r' = r & r' is_a_fixpoint_of f by A1;
   reconsider r'' = r as Element of F;
      Y is_less_than r' proof
     let q be Element of cL; assume
    A11: q in Y;
        then reconsider q'' = q as Element of F by A2;
        reconsider q' = q as Element of L;
          q'' [= r'' by A2,A9,A11,LATTICE3:def 17;
        then q' [= r' by A10,Th42;
     hence q [= r';
    end;
 then s [= r' by LATTICE3:def 21;
    then p' [= r' by A5,A10,Th37;
    then p'' [= r'' by A10,Th42;
  hence p [= r;
end;

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

theorem Th44:
 (lfp f is_a_fixpoint_of f) &
 (ex O st Card O <=` 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:41;
   then consider O such that
A2: Card O <=` Card the carrier of L and
A3: (f, O)+.Bottom L is_a_fixpoint_of f by Th33;
     Card the carrier of L in nextcard the carrier of L by CARD_1:def 6;
   then Card O in nextcard the carrier of L by A2,ORDINAL1:22;
   then O in nextcard the carrier of L by CARD_3:60;
   then O c= nextcard the carrier of L by ORDINAL1:def 2;
then A4: (f, O)+.Bottom L = (f, nextcard the carrier of L)+.Bottom
L by A1,A3,Th31;
 hence lfp f is_a_fixpoint_of f by A3,Def12;
 take O;
 thus Card O <=` Card the carrier of L by A2;
 thus thesis by A4,Def12;
end;

theorem Th45:
 (gfp f is_a_fixpoint_of f) &
 (ex O st Card O <=` 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:45;
   then consider O such that
A2: Card O <=` Card the carrier of L and
A3: (f, O)-.Top L is_a_fixpoint_of f by Th34;
     Card the carrier of L in nextcard the carrier of L by CARD_1:def 6;
   then Card O in nextcard the carrier of L by A2,ORDINAL1:22;
   then O in nextcard the carrier of L by CARD_3:60;
   then O c= nextcard the carrier of L by ORDINAL1:def 2;
then A4: (f, O)-.Top L = (f, nextcard the carrier of L)-.Top L by A1,A3,Th32;
 hence gfp f is_a_fixpoint_of f by A3,Def13;
 take O;
 thus Card O <=` Card the carrier of L by A2;
 thus thesis by A4,Def13;
end;

theorem Th46:
  a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f
proof assume
   a is_a_fixpoint_of f;
then A1: f.a = a by Def1;
 defpred S[Ordinal] means (f, $1)+.Bottom L [= a;
      (f, {})+.Bottom L = Bottom L by Th16;
then A2: S[{}] by LATTICES:41;
A3: now let O1; assume S[O1];
      then f.(f, O1)+.Bottom L [= f.a by QUANTAL1:def 12;
     hence S[succ O1] by A1,Th18;
    end;
A4: now let O1; assume
    A5: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
    deffunc F(Ordinal)=(f, $1)+.Bottom L;
        consider L1 being T-Sequence such that
    A6: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
           from TS_Lambda;
    A7: (f, O1)+.Bottom L = "\/"(rng L1, L) by A5,A6,Th20;
          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
        A8: C in dom L1 & q = L1.C by FUNCT_1:def 5;
            reconsider C as Ordinal by A8,ORDINAL1:23;
           (f, C)+.Bottom L [= a by A5,A6,A8;
           hence q [= a by A6,A8;
        end;
     hence S[O1] by A7,LATTICE3:def 21;
    end;
A9: for O2 holds S[O2] from Ordinal_Ind(A2, A3, A4);
     lfp f = (f, nextcard the carrier of L)+.Bottom L by Def12;
 hence lfp f [= a by A9;
 defpred S[Ordinal] means a [= (f, $1)-.Top L;
      (f, {})-.Top L = Top L by Th17;
then A10: S[{}] by LATTICES:45;
A11: now let O1; assume S[O1];
     then f.a [= f.(f, O1)-.Top L by QUANTAL1:def 12;
     hence S[succ O1] by A1,Th19;
    end;
A12: now let O1; assume
    A13: O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds S[O2];
    deffunc F(Ordinal)=(f, $1)-.Top L;
        consider L1 being T-Sequence such that
    A14: dom L1 = O1 & for O3 st O3 in O1 holds L1.O3 = F(O3)
             from TS_Lambda;
    A15: (f, O1)-.Top L = "/\"(rng L1, L) by A13,A14,Th21;
          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
        A16: C in dom L1 & q = L1.C by FUNCT_1:def 5;
            reconsider C as Ordinal by A16,ORDINAL1:23;
           a [= (f, C)-.Top L by A13,A14,A16;
           hence a [= q by A14,A16;
        end;
     hence S[O1] by A15,LATTICE3:40;
    end;
A17: for O2 holds S[O2] from Ordinal_Ind(A10, A11, A12);
     gfp f = (f, nextcard the carrier of L)-.Top L by Def13;
 hence a [= gfp f by A17;
end;


theorem
   f.a [= a implies lfp f [= a
proof assume
A1: f.a [= a;
   then consider O such that
     Card O <=` Card the carrier of L and
A2: (f, O)-.a is_a_fixpoint_of f by Th34;
A3: (f, O)-.a [= a by A1,Th26;
     lfp f [= (f, O)-.a by A2,Th46;
 hence lfp f [= a by A3,LATTICES:25;
end;

theorem
   a [= f.a implies a [= gfp f
proof assume
A1:  a [= f.a;
   then consider O such that
     Card O <=` Card the carrier of L and
A2: (f, O)+.a is_a_fixpoint_of f by Th33;
A3: a [= (f, O)+.a by A1,Th25;
     (f, O)+.a [= gfp f by A2,Th46;
 hence a [= gfp f by A3,LATTICES:25;
end;

begin :: Boolean Lattices

reserve f for (monotone UnOp of BooleLatt A);

definition
 let A be set;
 cluster BooleLatt A -> complete;
 coherence by LATTICE3:25;
end;

theorem Th49:
 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 f.x c= f.y 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,Def3;
 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
A1: 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 Th49;
  take g;
   reconsider lf = lfp f as Subset of A by LATTICE3:def 1;
     lfp f is_a_fixpoint_of f by Th44;
then A2: lfp (A, g) c= lf by Th10;
   reconsider lg = lfp(A, g) as Element of BooleLatt A by A1;
     lg is_a_fixpoint_of f by Th6;
   then lfp f [= lg by Th46;
   then lf c= lg by LATTICE3:2;
 hence lfp (A, g) = lfp f by A2,XBOOLE_0:def 10;
end;

theorem
    ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f
proof
A1: 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 Th49;
  take g;
   reconsider gf = gfp f as Subset of A by LATTICE3:def 1;
     gfp f is_a_fixpoint_of f by Th45;
then A2: gf c= gfp (A, g) by Th10;
   reconsider gg = gfp(A, g) as Element of BooleLatt A by A1;
     gg is_a_fixpoint_of f by Th7;
   then gg [= gfp f by Th46;
   then gg c= gf by LATTICE3:2;
 hence gfp (A, g) = gfp f by A2,XBOOLE_0:def 10;
end;

Back to top