The Mizar article:

The Equational Characterization of Continuous Lattices

by
Mariusz Zynel

Received October 25, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: WAYBEL_5
[ MML identifier index ]


environ

 vocabulary WAYBEL_0, ORDINAL2, WAYBEL_3, FILTER_2, QUANTAL1, YELLOW_0,
      LATTICE3, LATTICES, YELLOW_2, WAYBEL_1, YELLOW_1, PRE_TOPC, FUNCT_1,
      RELAT_1, BHSP_3, PBOOLE, PRALG_1, FUNCOP_1, ZF_REFLE, FUNCT_6, CARD_3,
      FINSEQ_4, BOOLE, ORDERS_1, TARSKI, YELLOW_6, CLASSES1, ZF_LANG, FUNCT_5,
      FUNCT_2, FINSUB_1, FINSET_1, REALSET1, RELAT_2, LATTICE2, CAT_1, SGRAPH1,
      MSUALG_3, SEQM_3, WAYBEL_5;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FINSET_1, FINSUB_1,
      FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCT_5, FUNCT_6, FUNCOP_1,
      STRUCT_0, ORDERS_1, LATTICE3, CARD_3, REALSET1, PBOOLE, PRALG_1, PRALG_2,
      MSUALG_1, MSUALG_3, PRE_TOPC, PRE_CIRC, BORSUK_1, CLASSES1, CLASSES2,
      GRCAT_1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3,
      YELLOW_6;
 constructors FINSUB_1, LATTICE3, TOPS_2, PRE_CIRC, BORSUK_1, PRALG_2,
      MSUALG_3, ORDERS_3, WAYBEL_1, WAYBEL_3, YELLOW_6, CLASSES1, GRCAT_1;
 clusters STRUCT_0, FINSET_1, LATTICE3, ORDERS_1, PBOOLE, MSUALG_1, CIRCCOMB,
      PRVECT_1, FRAENKEL, PRALG_1, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3,
      CLASSES2, YELLOW_6, CANTOR_1, FUNCT_2, FUNCOP_1, RELSET_1, SUBSET_1,
      FUNCT_4, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, LATTICE3;
 theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, CARD_3, ORDERS_1,
      LATTICE3, FUNCT_6, FUNCOP_1, FINSET_1, PBOOLE, PRALG_1, PRALG_2,
      MSUALG_1, MSUALG_3, EXTENS_1, AUTALG_1, RELAT_1, UNIALG_1, REALSET1,
      FINSUB_1, COMPTS_1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0,
      WAYBEL_3, CLASSES2, YELLOW_6, CLASSES1, GRCAT_1, RELSET_1, XBOOLE_0,
      XBOOLE_1, FUNCT_4;
 schemes FUNCT_1, FUNCT_2, MSSUBFAM, YELLOW_2, COMPTS_1;

begin  :: The Continuity of Lattices

reserve x, y, i for set,
        L for up-complete Semilattice;

Lm1:  ::Theorem 2.1 (1) implies (2)
  for L being continuous Semilattice
  for x being Element of L
    holds
   waybelow x is Ideal of L & x <= sup waybelow x &
     for I being Ideal of L st x <= sup I holds waybelow x c= I
proof
  let L be continuous Semilattice;
  let x be Element of L;

  thus waybelow x is Ideal of L;
  thus x <= sup waybelow x by WAYBEL_3:def 5;

  thus for I being Ideal of L st x <= sup I holds waybelow x c= I
  proof
    let I be Ideal of L;
    assume
  A1: x <= sup I;
      waybelow x c= I
    proof
      let y be set;
      assume y in waybelow x;
      then y in {y' where y' is Element of L: y' << x} by WAYBEL_3:def 3;
      then consider y' being Element of L such that
    A2:  y = y' & y' << x;
      thus y in I by A1,A2,WAYBEL_3:20;
   end;
   hence thesis;
 end;
end;

Lm2:  ::Theorem 2.1 (2) implies (1)
  (for x being Element of L holds
    waybelow x is Ideal of L & x <= sup waybelow x &
      for I being Ideal of L st x <= sup I holds waybelow x c= I)
        implies
       L is continuous
proof
  assume
A1: for x being Element of L holds
      waybelow x is Ideal of L & x <= sup waybelow x &
        for I being Ideal of L st x <= sup I holds waybelow x c= I;

    now
    let x be Element of L;
  A2:  x <= sup waybelow x by A1;
      waybelow x is non empty directed by A1;
  then A3:  ex_sup_of waybelow x,L by WAYBEL_0:75;
      waybelow x is_<=_than x by WAYBEL_3:9;
    then sup waybelow x <= x by A3,YELLOW_0:def 9;
    hence x = sup waybelow x by A2,YELLOW_0:def 3;
  end;
then A4: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;

    for x being Element of L holds waybelow x is non empty directed by A1;
  hence L is continuous by A4,WAYBEL_3:def 6;
end;

theorem  ::Theorem 2.1 (1) iff (2)
   L is continuous iff for x being Element of L holds
    waybelow x is Ideal of L & x <= sup waybelow x &
      for I being Ideal of L st x <= sup I holds waybelow x c= I
by Lm1,Lm2;

Lm3:  ::Theorem 2.1 (1) implies (3)
  L is continuous implies
    for x being Element of L ex I being Ideal of L st x <= sup I &
      for J being Ideal of L st x <= sup J holds I c= J
proof
  assume
A1: L is continuous;
  let x be Element of L;
  reconsider I = waybelow x as Ideal of L by A1,WAYBEL_3:def 6;
  take I;
  thus x <= sup I & for J being Ideal of L st x <= sup J holds
    I c= J by A1,Lm1;
end;

Lm4:  ::Theorem 2.1 (3) implies (1)
  (for x being Element of L ex I being Ideal of L st x <= sup I &
   for J being Ideal of L st x <= sup J holds I c= J)
     implies
    L is continuous
proof
  assume
A1: for x being Element of L ex I being Ideal of L st x <= sup I &
      for J being Ideal of L st x <= sup J holds I c= J;

    now
    let x be Element of L;
    consider I being Ideal of L such that
  A2: x <= sup I and
  A3: for J being Ideal of L st x <= sup J holds I c= J by A1;

      now
      let y be set;
      assume
    A4: y in I;
      then reconsider y'= y as Element of L;
        for J being Ideal of L st x <= sup J holds y in J
      proof
        let J be Ideal of L;
        assume x <= sup J;
        then I c= J by A3;
        hence y in J by A4;
      end;
      then y' << x by WAYBEL_3:21;
      hence y in waybelow x by WAYBEL_3:7;
    end;
  then A5: I c= waybelow x by TARSKI:def 3;

      now
      let y be set;
      assume
    A6: y in waybelow x;
      then reconsider y'= y as Element of L;
        y' << x by A6,WAYBEL_3:7;
      hence y in I by A2,WAYBEL_3:20;
    end;
    then waybelow x c= I by TARSKI:def 3;
    then waybelow x = I by A5,XBOOLE_0:def 10;
    hence waybelow x is Ideal of L & x <= sup waybelow x &
      for I being Ideal of L st x <= sup I holds waybelow x c= I by A2,A3;
  end;
  hence L is continuous by Lm2;
end;

theorem ::Theorem 2.1 (1) iff (3)
    L is continuous iff for x being Element of L
   ex I being Ideal of L st x <= sup I &
     for J being Ideal of L st x <= sup J holds I c= J
by Lm3,Lm4;

theorem ::Theorem 2.1 (1) implies (4)
    for L being continuous lower-bounded sup-Semilattice
    holds
   SupMap L has_a_lower_adjoint
proof
  let L be continuous lower-bounded sup-Semilattice;

  set P = InclPoset(Ids L);
  set r = SupMap L;
  deffunc F(Element of L) = inf(r"(uparrow {$1}));
    ex d being map of L, InclPoset(Ids L) st
    for t being Element of L holds d.t = F(t) from LambdaMD;
    then consider d being map of L, InclPoset(Ids L) such that
A1: for t being Element of L holds d.t = inf(r"(uparrow {t}));

    for t being Element of L holds d.t is_minimum_of r"(uparrow t)
  proof
    let t be Element of L;
    set I = inf(r"(uparrow t));

  A2: ex_inf_of r"(uparrow t),InclPoset(Ids L) by YELLOW_0:17;

  A3: d.t = inf(r"(uparrow {t})) by A1
         .= I by WAYBEL_0:def 18;

      I in the carrier of P;
    then I in Ids L by YELLOW_1:1;
  then A4: I in dom r by YELLOW_2:51;

    reconsider I'= I as Ideal of L by YELLOW_2:43;

    consider J being Ideal of L such that
  A5: t <= sup J and
  A6: for K being Ideal of L st t <= sup K holds J c= K by Lm3;

    reconsider J'= J as Element of P by YELLOW_2:43;

  A7: r"(uparrow t) is_>=_than J'
    proof
      let K be Element of P;
      reconsider K'= K as Ideal of L by YELLOW_2:43;
      assume K in r"(uparrow t);
      then K in dom r & r.K in uparrow t by FUNCT_1:def 13;
      then t <= r.K by WAYBEL_0:18;
      then t <= sup K' by YELLOW_2:def 3;
      then J' c= K' by A6;
      hence J' <= K by YELLOW_1:3;
    end;

      for K being Element of P st r"(uparrow t) is_>=_than K holds K <= J'
    proof
      let K be Element of P;
      assume
    A8: r"(uparrow t) is_>=_than K;
        J' in the carrier of P;
      then J' in Ids L by YELLOW_1:1;
    then A9: J in dom r by YELLOW_2:51;
        t <= r.J' by A5,YELLOW_2:def 3;
      then r.J in uparrow t by WAYBEL_0:18;
      then J in r"(uparrow t) by A9,FUNCT_1:def 13;
      hence K <= J' by A8,LATTICE3:def 8;
    end;
    then t <= sup I' by A5,A7,YELLOW_0:31;
    then t <= r.I by YELLOW_2:def 3;
    then r.I in uparrow t by WAYBEL_0:18;
    then I in r"(uparrow t) by A4,FUNCT_1:def 13;
    hence thesis by A2,A3,WAYBEL_1:def 6;
  end;
  then [r, d] is Galois by WAYBEL_1:11;
  hence r is upper_adjoint by WAYBEL_1:def 11;
end;

theorem ::Theorem 2.1 (4) implies (1)
    for L being up-complete lower-bounded LATTICE
    holds
   SupMap L is upper_adjoint implies L is continuous
proof
  let L be up-complete lower-bounded LATTICE;
  assume
A1: SupMap L is upper_adjoint;
  set P = InclPoset(Ids L);

    for x being Element of L ex I being Ideal of L st x <= sup I &
     for J being Ideal of L st x <= sup J holds I c= J
  proof
    let x be Element of L;
    set r = SupMap L;
    set I' = inf(r"(uparrow x));
    reconsider I = I' as Ideal of L by YELLOW_2:43;

    consider d being map of L, P such that
  A2: [r,d] is Galois by A1,WAYBEL_1:def 11;
      d.x is_minimum_of r"(uparrow x) by A2,WAYBEL_1:11;
    then ex_inf_of r"(uparrow x),P & d.x = I & I in r"(uparrow x)
      by WAYBEL_1:def 6;
    then r.I in uparrow x by FUNCT_1:def 13;
    then x <= r.I' by WAYBEL_0:18;
  then A3: x <= sup I by YELLOW_2:def 3;

      for J being Ideal of L st x <= sup J holds I c= J
    proof
      let J be Ideal of L;
      reconsider J'= J as Element of P by YELLOW_2:43;
    A4: J in dom r by YELLOW_2:52;
      assume x <= sup J;
      then x <= r.J' by YELLOW_2:def 3;
      then r.J' in uparrow x by WAYBEL_0:18;
      then J' in r"(uparrow x) by A4,FUNCT_1:def 13;
      then I' <= J' by YELLOW_2:24;
      hence I c= J by YELLOW_1:3;
    end;
    hence thesis by A3;
  end;
  hence L is continuous by Lm4;
end;

theorem  ::Theorem 2.1 (5) implies (4)
    for L being complete Semilattice
    holds
   SupMap L is infs-preserving sups-preserving implies
     SupMap L has_a_lower_adjoint
proof
  let L be complete Semilattice;
  set r = SupMap L;
  assume r is infs-preserving sups-preserving;
  then ex d being map of L, InclPoset(Ids L) st [r, d] is Galois &
    for t being Element of L holds d.t is_minimum_of r"(uparrow t)
      by WAYBEL_1:15;
  hence r is upper_adjoint by WAYBEL_1:def 11;
end;

:: Corollary 2.2 can be found in WAYBEL_4.

definition
  let J, D be set, K be ManySortedSet of J;
  mode DoubleIndexedSet of K, D is ManySortedFunction of K, (J --> D);
end;

definition
  let J be set, K be ManySortedSet of J, S be 1-sorted;
  mode DoubleIndexedSet of K, S is DoubleIndexedSet of K, the carrier of S;
end;

theorem Th6:
  for J, D being set, K being ManySortedSet of J
  for F being DoubleIndexedSet of K, D
  for j being set st j in J
    holds
   F.j is Function of K.j, D
proof
  let J, D be set, K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  let j be set;
  assume
A1: j in J;
   then (J --> D).j = D by FUNCOP_1:13;
  hence F.j is Function of K.j, D by A1,MSUALG_1:def 2;
end;

definition
  let J, D be non empty set, K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  let j be Element of J;
  redefine func F.j -> Function of K.j, D;
  coherence by Th6;
end;

definition
  let J, D be non empty set, K be non-empty ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  let j be Element of J;
  cluster rng(F.j) -> non empty;
  correctness
  proof
      dom(F.j) = K.j by FUNCT_2:def 1;
    hence rng(F.j) is non empty by RELAT_1:65;
  end;
end;

definition
  let J be set, D be non empty set;
  let K be non-empty ManySortedSet of J;
  cluster -> non-empty DoubleIndexedSet of K, D;
  correctness
  proof
    let F be DoubleIndexedSet of K, D;
      for j being set st j in dom F holds F.j is non empty
    proof
      let j be set;
      assume j in dom F;
    then A1: j in J by PBOOLE:def 3;
    then A2: K.j is non empty by PBOOLE:def 16;
      consider k being Element of K.j;
        F.j is Function of K.j, D by A1,Th6;
      then dom(F.j) = K.j by FUNCT_2:def 1;
      then [k, (F.j).k] in F.j by A2,FUNCT_1:def 4;
      hence thesis;
    end;
    hence thesis by UNIALG_1:def 6;
  end;
end;

theorem Th7:
  for F being Function-yielding Function
  for f being set
    holds
   f in dom(Frege F) implies f is Function
proof
  let F be Function-yielding Function;
  let f be set;
  assume f in dom(Frege F);
  then f in product doms F by PBOOLE:def 3;
  then ex g being Function st g = f & dom g = dom(doms F) &
    for x st x in dom(doms F) holds g.x in (doms F).x by CARD_3:def 5;
  hence thesis;
end;

theorem Th8:
  for F being Function-yielding Function
  for f being Function st f in dom Frege F
    holds
   dom f = dom F & dom F = dom((Frege F).f)
proof
  let F be Function-yielding Function;
  let f be Function;
  assume f in dom(Frege F);
then A1: f in product doms F by PBOOLE:def 3;
  then consider g being Function such that
A2: g = f and
A3: dom g = dom(doms F) and
      for x st x in dom(doms F) holds g.x in (doms F).x by CARD_3:def 5;
  thus dom f = dom F by A2,A3,EXTENS_1:3;

  thus dom ((Frege F).f) = dom(F..f) by A1,PRALG_2:def 8
             .= dom F by PRALG_1:def 18;
end;

theorem Th9:
  for F being Function-yielding Function
  for f being Function st f in dom Frege F
  for i being set st i in dom F
    holds
  f.i in dom(F.i) & ((Frege F).f).i = (F.i).(f.i) &
    (F.i).(f.i) in rng((Frege F).f)
proof
  let F be Function-yielding Function;
  let f be Function such that
A1: f in dom Frege F;
  set G = (Frege F).f;
  let i be set such that
A2: i in dom F;
A3: f in product doms F by A1,PBOOLE:def 3;
then A4: G = F..f by PRALG_2:def 8;
    i in dom(doms F) by A2,EXTENS_1:3;
  then f.i in (doms F).i by A3,CARD_3:18;
  hence f.i in dom(F.i) by A2,FUNCT_6:31;

  thus
A5: G.i = (F.i).(f.i) by A2,A4,PRALG_1:def 18;

    dom G = dom F by A1,Th8;
  hence (F.i).(f.i) in rng((Frege F).f) by A2,A5,FUNCT_1:def 5;
end;

theorem Th10:
  for J, D being set, K being ManySortedSet of J
  for F being DoubleIndexedSet of K, D
  for f being Function st f in dom(Frege F)
    holds
   (Frege F).f is Function of J, D
proof
  let J, D be set, K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  let f be Function such that
A1: f in dom(Frege F);

A2: dom F = J by PBOOLE:def 3;
  set G = (Frege F).f;
A3: dom G = dom F by A1,Th8;

    rng G c= D
  proof
    let y be set;
    assume y in rng G;
    then consider x such that
  A4: x in dom G and
  A5: y = G.x by FUNCT_1:def 5;
  A6: G.x = (F.x).(f.x) by A1,A3,A4,Th9;

      f.x in dom(F.x) by A1,A3,A4,Th9;
  then A7: y in rng(F.x) by A5,A6,FUNCT_1:def 5;
      F.x is Function of K.x, D by A2,A3,A4,Th6;
    then rng(F.x) c= D by RELSET_1:12;
    hence y in D by A7;
  end;
  hence G is Function of J, D by A2,A3,FUNCT_2:4;
end;


Lm5:
  for J, D being set, K being ManySortedSet of J
  for F being DoubleIndexedSet of K, D
  for f being Function st f in dom(Frege F)
  for j being set st j in J
    holds
   ((Frege F).f).j = (F.j).(f.j) & (F.j).(f.j) in rng((Frege F).f)
proof
  let J, D be set, K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  let f be Function such that
A1: f in dom(Frege F);
  let j be set; assume
   j in J;

then A2: j in dom F by PBOOLE:def 3;
  hence
  ((Frege F).f).j = (F.j).(f.j) by A1,Th9;
  thus (F.j).(f.j) in rng((Frege F).f) by A1,A2,Th9;
end;


Lm6:
  for J being set, K being ManySortedSet of J, D being non empty set
  for F being DoubleIndexedSet of K, D
  for f being Function st f in dom(Frege F)
  for j being set st j in J
    holds
   f.j in K.j
proof
  let J be set, K be ManySortedSet of J, D be non empty set;
  let F be DoubleIndexedSet of K, D;
  let f be Function such that
A1: f in dom(Frege F);
  let j be set such that
A2: j in J;

      dom F = J by PBOOLE:def 3;
then A3: f.j in dom(F.j) by A1,A2,Th9;
    F.j is Function of K.j, D by A2,Th6;
  hence f.j in K.j by A3,FUNCT_2:def 1;
end;

definition
  let f be non-empty Function;
  cluster doms f -> non-empty;
  correctness
  proof
      for j being set st j in dom doms f holds (doms f).j is non empty
    proof
      let j be set;
      assume that
    A1: j in dom doms f and
    A2: (doms f).j is empty;
      A3: j in f"SubFuncs rng f by A1,FUNCT_6:def 2;
    then A4: j in dom f & f.j is Function by FUNCT_6:28;
      reconsider fj = f.j as Function by A3,FUNCT_6:28;
        {} = dom fj by A2,A4,FUNCT_6:31;
      then f.j = {} by RELAT_1:64;
      hence contradiction by A4,UNIALG_1:def 6;
    end;
    hence thesis by UNIALG_1:def 6;
  end;
end;

definition
  let J, D be set, K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  redefine func Frege F -> DoubleIndexedSet of (product doms F --> J), D;
  coherence
  proof
    set PD = product doms F;
    set A = (PD --> J), B = (PD --> D);
    set G = Frege F;

      for i st i in PD holds G.i is Function of A.i, B.i
    proof
      let i;
      assume
    A1: i in PD;
    then A2: i in dom G by PBOOLE:def 3;
      then reconsider f = i as Function by Th7;
        A.i = J & B.i = D by A1,FUNCOP_1:13;
      then G.f is Function of A.i, B.i by A2,Th10;
      hence G.i is Function of A.i, B.i;
    end;
    hence thesis by MSUALG_1:def 2;
  end;
end;

definition
  let J, D be non empty set, K be non-empty ManySortedSet of J;
  let F be DoubleIndexedSet of K, D;
  let G be DoubleIndexedSet of (product doms F --> J), D;
  let f be Element of product doms F;
  redefine func G.f -> Function of J, D;
  coherence
  proof
       (product doms F --> J).f = J by FUNCOP_1:13;
    hence G.f is Function of J, D;
  end;
end;

definition
  let L be non empty RelStr;
  let F be Function-yielding Function;
  func \//(F, L) -> Function of dom F, the carrier of L means
:Def1:
  for x st x in dom F holds it.x = \\/(F.x, L);
  existence
  proof deffunc F(set) = \\/(F.$1, L);
      ex f being Function st dom f = dom F &
      for x st x in dom F holds f.x = F(x) from Lambda;
    then consider f being Function such that
  A1: dom f = dom F and
  A2: for x st x in dom F holds f.x = \\/(F.x, L);
      rng f c= the carrier of L
    proof
      let y;
      assume y in rng f;
      then consider x such that
    A3: x in dom f and
    A4: y = f.x by FUNCT_1:def 5;
        y = \\/(F.x, L) by A1,A2,A3,A4;
      hence y in the carrier of L;
    end;
    then reconsider f as Function of dom F, the carrier of L by A1,FUNCT_2:4;
    take f;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let f, g be Function of dom F, the carrier of L such that
  A5: for x st x in dom F holds f.x = \\/(F.x, L) and
  A6: for x st x in dom F holds g.x = \\/(F.x, L);
  A7: dom f = dom F & dom g = dom F by FUNCT_2:def 1;
      now
      let x;
      assume
    A8: x in dom F;
      hence f.x = \\/(F.x, L) by A5
               .= g.x by A6,A8;
    end;
    hence thesis by A7,FUNCT_1:9;
  end;

  func /\\(F, L) -> Function of dom F, the carrier of L means
:Def2:
  for x st x in dom F holds it.x = //\(F.x, L);
  existence
  proof deffunc F(set) = //\(F.$1, L);
      ex f being Function st dom f = dom F &
      for x st x in dom F holds f.x = F(x) from Lambda;
    then consider f being Function such that
  A9: dom f = dom F and
  A10: for x st x in dom F holds f.x = //\(F.x, L);
      rng f c= the carrier of L
    proof
      let y;
      assume y in rng f;
      then consider x such that
    A11: x in dom f and
    A12: y = f.x by FUNCT_1:def 5;
        y = //\(F.x, L) by A9,A10,A11,A12;
      hence y in the carrier of L;
    end;
    then reconsider f as Function of dom F, the carrier of L by A9,FUNCT_2:4;
    take f;
    thus thesis by A10;
  end;
  uniqueness
  proof
    let f, g be Function of dom F, the carrier of L such that
  A13: for x st x in dom F holds f.x = //\(F.x, L) and
  A14: for x st x in dom F holds g.x = //\(F.x, L);
  A15: dom f = dom F & dom g = dom F by FUNCT_2:def 1;
      now
      let x;
      assume
    A16: x in dom F;
      hence f.x = //\(F.x, L) by A13
               .= g.x by A14,A16;
    end;
    hence thesis by A15,FUNCT_1:9;
  end;
end;

definition
  let J be set, K be ManySortedSet of J, L be non empty RelStr;
  let F be DoubleIndexedSet of K, L;
  redefine func \//(F, L);
  synonym Sups F;

  redefine func /\\(F, L);
  synonym Infs F;
end;

definition
  let I, J be set, L be non empty RelStr;
  let F be DoubleIndexedSet of (I --> J), L;
  redefine func \//(F, L);
  synonym Sups F;

  redefine func /\\(F, L);
  synonym Infs F;
end;

theorem Th11:
  for L being non empty RelStr
  for F, G being Function-yielding Function st dom F = dom G &
    (for x st x in dom F holds \\/(F.x, L) = \\/(G.x, L))
      holds
     \//(F, L) = \//(G, L)
proof
  let L be non empty RelStr;
  let F, G be Function-yielding Function such that
A1: dom F = dom G and
A2: for x st x in dom F holds \\/(F.x, L) = \\/(G.x, L);
A3: dom \//(F, L) = dom F & dom \//(G, L) = dom G by FUNCT_2:def 1;

    for x st x in dom F holds \//(F, L).x = \//(G, L).x
  proof
    let x;
    assume
  A4: x in dom F;
    hence
      \//(F, L).x = \\/(F.x, L) by Def1
               .= \\/(G.x, L) by A2,A4
               .= \//(G, L).x by A1,A4,Def1;
  end;
  hence thesis by A1,A3,FUNCT_1:9;
end;

theorem Th12:
  for L being non empty RelStr
  for F, G being Function-yielding Function st dom F = dom G &
    (for x st x in dom F holds //\(F.x, L) = //\(G.x, L))
      holds
     /\\(F, L) = /\\(G, L)
proof
  let L be non empty RelStr;
  let F, G be Function-yielding Function such that
A1: dom F = dom G and
A2: for x st x in dom F holds //\(F.x, L) = //\(G.x, L);
A3: dom /\\(F, L) = dom F & dom /\\(G, L) = dom G by FUNCT_2:def 1;

    for x st x in dom F holds /\\(F, L).x = /\\(G, L).x
  proof
    let x;
    assume
  A4: x in dom F;
    hence
      /\\(F, L).x = //\(F.x, L) by Def2
               .= //\(G.x, L) by A2,A4
               .= /\\(G, L).x by A1,A4,Def2;
  end;
  hence thesis by A1,A3,FUNCT_1:9;
end;

theorem Th13:
  for L being non empty RelStr
  for F being Function-yielding Function
    holds
   (y in rng \//(F, L) iff ex x st x in dom F & y = \\/(F.x, L)) &
   (y in rng /\\(F, L) iff ex x st x in dom F & y = //\(F.x, L))
proof
  let L be non empty RelStr;
  let F be Function-yielding Function;

  thus y in rng \//(F, L) iff ex x st x in dom F & y = \\/(F.x, L)
  proof
    hereby
      assume y in rng \//(F, L);
      then consider x such that
    A1: x in dom \//(F, L) and
    A2: y = \//(F, L).x by FUNCT_1:def 5;
      take x;
          x in dom F by A1,FUNCT_2:def 1;
      hence x in dom F & y = \\/(F.x, L) by A2,Def1;
    end;
    given x such that
  A3: x in dom F and
  A4: y = \\/(F.x, L);
      x in dom \//(F, L) & y = \//(F, L).x by A3,A4,Def1,FUNCT_2:def 1;
    hence y in rng \//(F, L) by FUNCT_1:def 5;
  end;

  thus y in rng /\\(F, L) iff ex x st x in dom F & y = //\(F.x, L)
  proof
    hereby
      assume y in rng /\\(F, L);
      then consider x such that
    A5: x in dom /\\(F, L) and
    A6: y = /\\(F, L).x by FUNCT_1:def 5;
      take x;
          x in dom F by A5,FUNCT_2:def 1;
      hence x in dom F & y = //\(F.x, L) by A6,Def2;
    end;
    given x such that
  A7: x in dom F and
  A8: y = //\(F.x, L);
      x in dom /\\(F, L) & y = /\\(F, L).x by A7,A8,Def2,FUNCT_2:def 1;
    hence y in rng /\\(F, L) by FUNCT_1:def 5;
  end;
end;

theorem Th14:
  for L being non empty RelStr
  for J being non empty set, K being ManySortedSet of J
  for F being DoubleIndexedSet of K, L
    holds
   (x in rng Sups F iff ex j being Element of J st x = Sup(F.j)) &
   (x in rng Infs F iff ex j being Element of J st x = Inf(F.j))
proof
  let L be non empty RelStr;
  let J be non empty set, K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, L;
A1: dom F = J by PBOOLE:def 3;

  thus x in rng Sups F iff ex j being Element of J st x = Sup(F.j)
  proof
    hereby
      assume x in rng Sups F;
      then consider j being set such that
    A2: j in dom F and
    A3: x = \\/(F.j, L) by Th13;
      reconsider j as Element of J by A2,PBOOLE:def 3;
      take j;
      thus x = Sup(F.j) by A3;
    end;
    thus thesis by A1,Th13;
  end;

    hereby
      assume x in rng Infs F;
      then consider j being set such that
    A4: j in dom F and
    A5: x = //\(F.j, L) by Th13;
      reconsider j as Element of J by A4,PBOOLE:def 3;
      take j;
      thus x = Inf(F.j) by A5;
    end;
    thus thesis by A1,Th13;
end;

definition
  let J be non empty set, K be ManySortedSet of J, L be non empty RelStr;
  let F be DoubleIndexedSet of K, L;
  cluster rng Sups F -> non empty;
  correctness
  proof
    consider j being Element of J;
      Sup(F.j) in rng Sups F by Th14;
    hence thesis;
  end;

  cluster rng Infs F -> non empty;
  correctness
  proof
    consider j being Element of J;
      Inf(F.j) in rng Infs F by Th14;
    hence thesis;
  end;
end;

reserve L for complete LATTICE,
        a, b, c for Element of L,
        J for non empty set,

        K for non-empty ManySortedSet of J;

Lm7:
  for F being DoubleIndexedSet of K, L
  for f being set
    holds
   f is Element of product doms F iff f in dom(Frege F)
proof
  let F be DoubleIndexedSet of K, L;
  let f be set;
  hereby
    assume f is Element of product doms F;
    then f in product doms F;
    hence f in dom(Frege F) by PBOOLE:def 3;
  end;
  thus thesis by PBOOLE:def 3;
end;

theorem Th15:
  for F being Function-yielding Function
    holds
   ((for f being Function st f in dom Frege F holds //\((Frege F).f, L) <= a))
     implies Sup /\\(Frege F, L) <= a
proof
  let F be Function-yielding Function;
  assume
A1: for f being Function st f in dom(Frege F) holds //\((Frege F).f, L) <= a;

    rng /\\(Frege F, L) is_<=_than a
  proof
    let c;
    assume c in rng /\\(Frege F, L);
    then consider f being set such that
  A2: f in dom(Frege F) and
  A3: c = //\((Frege F).f, L) by Th13;
    reconsider f as Function by A2,Th7;
      f in dom(Frege F) by A2;
    hence c <= a by A1,A3;
  end;
  then sup rng /\\(Frege F, L) <= a by YELLOW_0:32;
  hence Sup /\\(Frege F, L) <= a by YELLOW_2:def 5;
end;

theorem Th16:
  for F being DoubleIndexedSet of K, L
    holds
   Inf Sups F >= Sup Infs Frege F
proof
  let F be DoubleIndexedSet of K, L;

A1:
  for j being Element of J
  for f being Element of product doms F
    holds
   Sup(F.j) >= Inf((Frege F).f)
  proof
    let j be Element of J;
    let f be Element of product doms F;
  A2: f in dom(Frege F) by Lm7;
    then reconsider k = f.j as Element of K.j by Lm6;
      (F.j).k = ((Frege F).f).j by A2,Lm5;
  then A3: Inf((Frege F).f) <= (F.j).k by YELLOW_2:55;
      (F.j).k <= Sup(F.j) by YELLOW_2:55;
    hence Sup(F.j) >= Inf((Frege F).f) by A3,ORDERS_1:26;
  end;

  set a = Sup Infs Frege F;

    a is_<=_than rng Sups F
  proof
    let c;
    assume c in rng Sups F;
    then consider j being Element of J such that
  A4: c = Sup(F.j) by Th14;
      for f being Function st f in dom(Frege F) holds //\((Frege F).f, L) <= c
    proof
      let f be Function;
      assume f in dom(Frege F);
      then reconsider f'= f as Element of product doms F by Lm7;
        Sup(F.j) >= Inf((Frege F).f') by A1;
      hence //\((Frege F).f, L) <= c by A4;
    end;
    hence a <= c by Th15;
  end;
  then a <= inf rng Sups F by YELLOW_0:33;
  hence Inf Sups F >= Sup Infs Frege F by YELLOW_2:def 6;
end;

theorem Th17:
  (L is continuous & for c st c << a holds c <= b) implies a <= b
proof
  assume that
A1: L is continuous and
A2: for c st c << a holds c <= b;
A3: L is complete satisfying_axiom_of_approximation by A1,WAYBEL_3:def 6;
    now
    let c;
    assume c in waybelow a;
    then c << a by WAYBEL_3:7;
    hence c <= b by A2;
  end;
  then waybelow a is_<=_than b by LATTICE3:def 9;
  then sup waybelow a <= b by YELLOW_0:32;
  hence a <= b by A3,WAYBEL_3:def 5;
end;


Lm8:    ::Theorem 2.3 (1) implies (2)
  L is continuous implies
    for J, K for F being DoubleIndexedSet of K, L st
      for j being Element of J holds rng(F.j) is directed
        holds
       Inf Sups F = Sup Infs Frege F
proof
  assume
A1: L is continuous;
  let J, K;
  let F be DoubleIndexedSet of K, L such that
A2: for j being Element of J holds rng(F.j) is directed;

    now
    let c;
    assume
  A3: c << Inf Sups F;

  A4:
    for j being Element of J holds c << Sup(F.j)
    proof
      let j be Element of J;
        Sup(F.j) in rng Sups F by Th14;
      then inf rng Sups F <= Sup(F.j) by YELLOW_2:24;
      then Inf Sups F <= Sup(F.j) by YELLOW_2:def 6;
      hence c << Sup(F.j) by A3,WAYBEL_3:2;
    end;


     ex f being Function st f in dom(Frege F) &
      for j being Element of J ex b st b = (F.j).(f.j) & c <= b
    proof

    A5:
      for j being Element of J ex k being Element of K.j st c <= (F.j).k
      proof
        let j be Element of J;
      A6: rng(F.j) is non empty directed Subset of L by A2;
      A7: c << Sup(F.j) by A4;
          Sup(F.j) <= sup(rng(F.j)) by YELLOW_2:def 5;
        then consider d being Element of L such that
      A8: d in rng(F.j) and
      A9: c <= d by A6,A7,WAYBEL_3:def 1;
        consider k being set such that
      A10: k in dom(F.j) and
      A11: d = (F.j).k by A8,FUNCT_1:def 5;
        reconsider k as Element of K.j by A10,FUNCT_2:def 1;
        take k;
        thus thesis by A9,A11;
      end;

      defpred P[set, set] means
        $1 in J & $2 in K.$1 & ex b st b = (F.$1).$2 & c <= b;

    A12:
      for j being set st j in J ex k being set st k in union rng K & P[j, k]
      proof
        let j be set;
        assume j in J;
        then reconsider j'= j as Element of J;
        consider k being Element of K.j' such that
      A13: c <= (F.j').k by A5;
        take k;
          j' in J;
        then j' in dom K by PBOOLE:def 3;
        then k in K.j' & K.j' in rng K by FUNCT_1:def 5;
        hence k in union rng K by TARSKI:def 4;

        thus P[j, k] by A13;
      end;

      consider f being Function such that
    A14: dom f = J and rng f c= union rng K and
    A15: for j being set st j in J holds P[j, f.j]
     from NonUniqBoundFuncEx(A12);

    A16: for j being Element of J holds
           f.j in K.j & ex b st b = (F.j).(f.j) & c <= b by A15;

    A17: dom f = dom F by A14,PBOOLE:def 3
             .= dom doms F by EXTENS_1:3;
        now
        let x be set;
        assume x in dom doms F;
      then A18: x in dom F by EXTENS_1:3;
        then reconsider j = x as Element of J by PBOOLE:def 3;

          (doms F).x = dom(F.j) by A18,FUNCT_6:31
                    .= K.j by FUNCT_2:def 1;
        hence f.x in (doms F).x by A15;
      end;
      then f in product doms F by A17,CARD_3:18;
      then f in dom(Frege F) by PBOOLE:def 3;
      hence thesis by A16;
    end;

    then consider f being Function such that
  A19: f in dom(Frege F) and
  A20: for j being Element of J ex b st b = (F.j).(f.j) & c <= b;
    reconsider f as Element of product doms F by A19,Lm7;
    reconsider G = (Frege F).f as Function of J, the carrier of L;

      now
      let j be Element of J;
        j in J;
    then A21: j in dom F by PBOOLE:def 3;
        ex b st b = (F.j).(f.j) & c <= b by A20;
     hence c <= G.j by A19,A21,Th9;
    end;
  then A22: c <= Inf((Frege F).f) by YELLOW_2:57;

    set a = Inf((Frege F).f);
      a in rng Infs Frege F by Th14;
    then a <= sup rng Infs Frege F by YELLOW_2:24;
    then a <= Sup Infs Frege F by YELLOW_2:def 5;
    hence c <= Sup Infs Frege F by A22,YELLOW_0:def 2;
  end;
then A23: Inf Sups F <= Sup Infs Frege F by A1,Th17;

    Inf Sups F >= Sup Infs Frege F by Th16;
  hence thesis by A23,YELLOW_0:def 3;
end;


theorem Th18:    ::Theorem 2.3 (2) implies (1)
  (for J being non empty set st J in the_universe_of the carrier of L
   for K being non-empty ManySortedSet of J st
    for j being Element of J holds K.j in the_universe_of the carrier of L
   for F being DoubleIndexedSet of K, L st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs Frege F)
    implies
   L is continuous
proof
  assume
A1: for J being non empty set st J in the_universe_of the carrier of L
    for K being non-empty ManySortedSet of J st
     for j being Element of J holds K.j in the_universe_of the carrier of L
    for F being DoubleIndexedSet of K, L st
      (for j being Element of J holds rng(F.j) is directed)
        holds
      Inf Sups F = Sup Infs Frege F;

    now
    let x be Element of L;
    set J = {j where j is directed non empty Subset of L : x <= sup j};
    set UN = the_universe_of the carrier of L;
A2: UN = Tarski-Class the_transitive-closure_of the carrier of L by YELLOW_6:
def 3;
    reconsider UN as universal set;
A3:the carrier of L c= the_transitive-closure_of the carrier of L
     by CLASSES1:59;
      the_transitive-closure_of the carrier of L in UN by A2,CLASSES1:5;
then A4: the carrier of L in UN by A3,CLASSES1:def 1;
then A5: bool the carrier of L in UN by CLASSES2:65;
A6: J c= bool the carrier of L
      proof let u be set;
       assume u in J;
        then ex j being directed non empty Subset of L st u = j & x <= sup j;
       hence u in bool the carrier of L;
      end;
then A7: J in UN by A5,CLASSES1:def 1;
  A8: {x} is directed non empty Subset of L by WAYBEL_0:5;
      x <= sup {x} by YELLOW_0:39;
  then A9: {x} in J by A8;
    then reconsider J as non empty set;

  A10:
    for j being Element of J holds j is directed non empty Subset of L
    proof
      let j be Element of J;
        j in J;
      then consider j' being directed non empty Subset of L such that
    A11: j'= j and
          x <= sup j';
      thus thesis by A11;
    end;

    set K = id J;
      dom K = J by FUNCT_1:34;
    then reconsider K as ManySortedSet of J by PBOOLE:def 3;
A12: for j being Element of J holds K.j in UN
     proof let j be Element of J;
         K.j = j by FUNCT_1:35;
       then K.j in J;
       hence K.j in UN by A4,A6,CLASSES1:def 1;
     end;
      for i st i in J holds K.i is non empty
    proof
      let i;
      assume i in J;
      then reconsider i'= i as Element of J;
        K.i = i' by FUNCT_1:35;
      hence K.i is non empty by A10;
    end;
    then reconsider K as non-empty ManySortedSet of J by PBOOLE:def 16;
    deffunc F(set) = id(K.$1);
      ex F being Function st dom F = J &
      for j being set st j in J holds F.j = F(j) from Lambda;
    then consider F being Function such that
  A13: dom F = J and
  A14: for j being set st j in J holds F.j = id(K.j);

    reconsider F as ManySortedSet of J by A13,PBOOLE:def 3;

      for j being set st j in dom F holds F.j is Function
    proof
      let j be set;
      assume j in dom F;
      then F.j = id(K.j) by A13,A14;
      hence F.j is Function;
    end;
    then reconsider F as ManySortedFunction of J by PRALG_1:def 15;

      for j being set st j in J holds
      F.j is Function of K.j, (J --> the carrier of L).j
    proof
      let j be set;
      assume j in J;
      then reconsider j as Element of J;
    A15:  F.j = id(K.j) by A14;
    then A16: dom(F.j) = K.j by FUNCT_2:def 1;
    A17: rng(F.j) c= K.j by A15,RELSET_1:12;
        K.j = j by FUNCT_1:35;
      then K.j is Subset of L by A10;
      then rng(F.j) c= the carrier of L by A17,XBOOLE_1:1;
      then rng(F.j) c= (J --> the carrier of L).j by FUNCOP_1:13;
      hence thesis by A16,FUNCT_2:4;
    end;
    then reconsider F as DoubleIndexedSet of K, L by MSUALG_1:def 2;

  A18: for j being Element of J, k being Element of K.j holds (F.j).k = k
    proof
      let j be Element of J;
      let k be Element of K.j;
        F.j = id(K.j) by A14;
      hence thesis by FUNCT_1:35;
    end;

  A19:
    for j being Element of J holds rng(F.j) = j
    proof
      let j be Element of J;
        now
        let y;
        assume y in rng(F.j);
        then consider x such that
      A20: x in dom(F.j) and
      A21: y = (F.j).x by FUNCT_1:def 5;
      A22: x in K.j by A20,FUNCT_2:def 1;
        then x in j by FUNCT_1:35;
        hence y in j by A18,A21,A22;
      end;
    then A23: rng(F.j) c= j by TARSKI:def 3;

        now
        let x;
        assume x in j;
      then A24: x in K.j by FUNCT_1:35;
      then A25: (F.j).x = x by A18;
          x in dom(F.j) by A24,FUNCT_2:def 1;
        hence x in rng(F.j) by A25,FUNCT_1:def 5;
      end;
      then j c= rng(F.j) by TARSKI:def 3;
      hence rng(F.j) = j by A23,XBOOLE_0:def 10;
    end;

  A26:
    for j being Element of J holds rng(F.j) is directed
    proof
      let j be Element of J;
        rng(F.j) = j by A19;
      hence thesis by A10;
    end;

      for f being Function st f in dom(Frege F)
      holds
     //\((Frege F).f, L) <= sup waybelow x
    proof
      let f be Function such that
    A27: f in dom(Frege F);
      set a = //\((Frege F).f, L);

        for D being non empty directed Subset of L st x <= sup D
        ex d being Element of L st d in D & a <= d
      proof
        let D be non empty directed Subset of L;
        assume x <= sup D;
        then D in J;
        then reconsider D'= D as Element of J;

      A28: for j being Element of J holds f.j in K.j
        proof
          let j be Element of J;
            j in J;
          then j in dom F by PBOOLE:def 3;
          then f.j in dom(F.j) by A27,Th9;
          hence thesis by FUNCT_2:def 1;
        end;

      A29: dom f = dom F by A27,Th8
               .= J by PBOOLE:def 3;

          now
          let y be set;
          assume y in rng f;
          then consider j being set such that
        A30: j in dom f and
        A31: y = f.j by FUNCT_1:def 5;
          reconsider j as Element of J by A29,A30;
            y in K.j by A28,A31;
        then A32: y in j by FUNCT_1:35;
            j is Subset of L by A10;
          hence y in the carrier of L by A32;
        end;
        then rng f c= the carrier of L by TARSKI:def 3;
        then reconsider f as Function of J, the carrier of L by A29,FUNCT_2:4;

      A33: Inf f <= f.D' by YELLOW_2:55;

      A34: dom f = dom F by A27,Th8
               .= dom((Frege F).f) by A27,Th8;

          now
          let j be set;
          assume j in dom f;
        then A35: j in dom F by A27,Th8;
          then reconsider j'= j as Element of J by PBOOLE:def 3;
        A36: f.j' is Element of K.j' by A28;
          thus ((Frege F).f).j = (F.j').(f.j') by A27,A35,Th9
                              .= f.j by A18,A36;
        end;
      then A37: a <= f.D' by A33,A34,FUNCT_1:9;

          f.D' in K.D' by A28;
        then f.D' in D' by FUNCT_1:35;
        hence ex d being Element of L st d in D & a <= d by A37;
      end;
      then a << x by WAYBEL_3:def 1;
      then a in waybelow x by WAYBEL_3:7;
      hence //\((Frege F).f, L) <= sup waybelow x by YELLOW_2:24;
    end;
  then A38: Sup Infs Frege F <= sup waybelow x by Th15;

      x is_<=_than rng Sups F
    proof
      let b be Element of L;
      assume b in rng Sups F;
      then consider j being Element of J such that
    A39: b = Sup(F.j) by Th14;
        j in J;
      then consider j' being directed non empty Subset of L such that
    A40: j'= j and
    A41: x <= sup j';
        b = sup rng(F.j) by A39,YELLOW_2:def 5
       .= sup j' by A19,A40;
      hence x <= b by A41;
    end;
    then x <= inf rng Sups F by YELLOW_0:33;
  then A42: x <= Inf Sups F by YELLOW_2:def 6;

    reconsider j = {x} as Element of J by A9;
      Sup(F.j) = sup rng(F.j) by YELLOW_2:def 5
            .= sup {x} by A19
            .= x by YELLOW_0:39;
    then x in rng Sups F by Th14;
    then inf rng Sups F <= x by YELLOW_2:24;
    then Inf Sups F <= x by YELLOW_2:def 6;
  then A43:  x = Inf Sups F by A42,ORDERS_1:25
     .= Sup Infs Frege F by A1,A7,A12,A26;
      x is_>=_than waybelow x by WAYBEL_3:9;
    then x >= sup waybelow x by YELLOW_0:32;
    hence x = sup waybelow x by A38,A43,ORDERS_1:25;
  end;
then A44: L is up-complete satisfying_axiom_of_approximation by WAYBEL_3:def 5;
    for x being Element of L holds waybelow x is non empty directed;
  hence L is continuous by A44,WAYBEL_3:def 6;
end;

Lm9:    ::Theorem 2.3 (2) implies (1)
  (for J, K for F being DoubleIndexedSet of K, L st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs Frege F)
    implies
   L is continuous
proof assume
   for J, K for F being DoubleIndexedSet of K, L st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs Frege F;
 then for J being non empty set st J in the_universe_of the carrier of L
    for K being non-empty ManySortedSet of J st
     for j being Element of J holds K.j in the_universe_of the carrier of L
    for F being DoubleIndexedSet of K, L st
      (for j being Element of J holds rng(F.j) is directed)
        holds
      Inf Sups F = Sup Infs Frege F;
 hence thesis by Th18;
end;

theorem ::Theorem 2.3 (1) iff (2)
    L is continuous iff for J, K for F being DoubleIndexedSet of K, L st
      for j being Element of J holds rng(F.j) is directed
        holds
       Inf Sups F = Sup Infs Frege F
by Lm8,Lm9;

definition
  let J, K, D be non empty set;
  let F be Function of [:J, K:], D;
  redefine func curry F -> DoubleIndexedSet of (J --> K), D;
  coherence
  proof
  A1: dom F = [:J, K:] by FUNCT_2:def 1;
    then reconsider F'= F as ManySortedSet of [:J, K:] by PBOOLE:def 3;

      for j being set st j in J holds
     (curry F').j is Function of (J --> K).j, (J --> D).j
    proof
      let j be set;
      assume
    A2: j in J;
    then A3: (J --> K).j = K & (J --> D).j = D by FUNCOP_1:13;
        J = dom curry F by A1,FUNCT_5:31;
      then reconsider G = (curry F').j as Function by A2,FUNCT_5:37;

      consider g being Function such that
    A4: (curry F').j = g and
    A5: dom g = K and
    A6: rng g c= rng F' and
          for k being set st k in K holds g.k = F'.[j, k]
        by A1,A2,FUNCT_5:36;

        rng F c= D by RELSET_1:12;
      then rng g c= D by A6,XBOOLE_1:1;
      then reconsider g as Function of K, D by A5,FUNCT_2:def 1,RELSET_1:11;
        G = g by A4;
      hence (curry F').j is Function of (J --> K).j, (J --> D).j by A3;
    end;
    hence thesis by MSUALG_1:def 2;
  end;
end;

reserve J, K, D for non empty set,
        j for Element of J,
        k for Element of K;

theorem Th20:
  for F being Function of [:J, K:], D
    holds
   dom curry F = J & dom((curry F).j) = K & F.[j, k] = ((curry F).j).k
proof
  let F be Function of [:J, K:], D;

  thus dom curry F = proj1 dom F by FUNCT_5:def 3
                  .= proj1 [:J, K:] by FUNCT_2:def 1
                  .= J by FUNCT_5:11;

    [:J, K:] <> {} & dom F = [:J, K:] & j in J by FUNCT_2:def 1;
  then ex g being Function st (curry F).j = g & dom g = K &
    rng g c= rng F & for i being set st i in K holds g.i = F.[j, i]
      by FUNCT_5:36;
  hence dom((curry F).j) = K;

    [j, k] in [:J, K:] by ZFMISC_1:106;
  then [j, k] in dom F by FUNCT_2:def 1;
  hence F.[j, k] = ((curry F).j).k by FUNCT_5:27;
end;

Lm10:    ::Theorem 2.3 (2') implies (1)
  (for J, K for F being Function of [:J, K:], the carrier of L st
    for j being Element of J holds rng((curry F).j) is directed
      holds Inf Sups curry F = Sup Infs Frege curry F)
    implies
   L is continuous
proof
  assume
A1: for J, K for F being Function of [:J, K:], the carrier of L st
       for j being Element of J holds rng((curry F).j) is directed
         holds
        Inf Sups (curry F) = Sup Infs (Frege curry F);

    for J for K being non-empty ManySortedSet of J
  for F being DoubleIndexedSet of K, L st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs(Frege F)
  proof
    let J;
    let K be non-empty ManySortedSet of J;
    let F be DoubleIndexedSet of K, L;
    assume
  A2: for j being Element of J holds rng(F.j) is directed;

    consider j being Element of J;
    consider k being Element of K.j;
      j in J;
    then j in dom K by PBOOLE:def 3;
    then k in K.j & K.j in rng K by FUNCT_1:def 5;
    then reconsider K'= union rng K as non empty set by TARSKI:def 4;

    defpred P[set, set, set] means
      $1 in J & (($2 in K.$1 & $3 = (F.$1).$2) or (not $2 in K.$1 & $3 =
Bottom L));

  A3:
    for j being Element of J for k' being Element of K'
      ex z being Element of L st P[j, k', z]
    proof
      let j be Element of J;
      let k' be Element of K';
      per cases;
      suppose k' in K.j;
      then reconsider k = k' as Element of K.j;
      take (F.j).k;
      thus thesis;

      suppose
    A4: not k' in K.j;
      take Bottom L;
      thus thesis by A4;
    end;

      ex G being Function of [:J, K':], the carrier of L st
      for j being Element of J
      for k being Element of K' holds P[j, k, G.[j, k]] from FuncEx2D(A3);
    then consider G being Function of [:J, K':], the carrier of L such that
  A5: for j being Element of J for k being Element of K' holds
      P[j, k, G.[j, k]];
  A6: for j being Element of J holds K.j c= K'
    proof
      let j be Element of J;
      hereby
        let k be set;
        assume
      A7: k in K.j;
          j in J;
       then j in dom K by PBOOLE:def 3;
        then K.j in rng K by FUNCT_1:def 5;
        hence k in K' by A7,TARSKI:def 4;
      end;
      thus thesis;
    end;

  A8: for j being Element of J holds rng(F.j) c= rng((curry G).j)
    proof
      let j be Element of J;
      hereby
        let y be set;
        assume y in rng(F.j);
        then consider k being set such that
      A9: k in dom(F.j) and
      A10: y = (F.j).k by FUNCT_1:def 5;
      A11: k in K.j & K.j c= K' by A6,A9,FUNCT_2:def 1;
        then reconsider k as Element of K';
          [j, k] in [:J, K':] by ZFMISC_1:106;
      then A12: [j, k] in dom G by FUNCT_2:def 1;
          k in K' & dom((curry G).j) = (J --> K').j by FUNCT_2:def 1;
      then A13: k in dom((curry G).j) by FUNCOP_1:13;
          y = G.[j, k] by A5,A10,A11
         .= ((curry G).j).k by A12,FUNCT_5:27;
        hence y in rng((curry G).j) by A13,FUNCT_1:def 5;
      end;
      thus thesis;
    end;

  A14: for j being Element of J holds rng((curry G).j) is directed
    proof
      let j be Element of J;
      set X = rng((curry G).j);

        for x, y being Element of L st x in X & y in X
        ex z being Element of L st z in X & x <= z & y <= z
      proof
        let x, y be Element of L;
      A15: rng(F.j) is directed by A2;

        assume
      A16: x in X & y in X;
        then consider a being set such that
      A17: a in dom((curry G).j) and
      A18: ((curry G).j).a = x by FUNCT_1:def 5;
        consider b being set such that
      A19: b in dom((curry G).j) and
      A20: ((curry G).j).b = y by A16,FUNCT_1:def 5;
        reconsider a'= a, b'= b as Element of K' by A17,A19,Th20;

      A21: x = G.[j, a'] & y = G.[j, b'] by A18,A20,Th20;

        per cases;
        suppose
      A22: a in K.j & b in K.j;
      then A23: a in dom(F.j) & b in dom(F.j) by FUNCT_2:def 1;
          x = (F.j).a' & y = (F.j).b' by A5,A21,A22;
        then x in rng(F.j) & y in rng(F.j) by A23,FUNCT_1:def 5;
        then consider z being Element of L such that
      A24: z in rng(F.j) and
      A25: x <= z & y <= z by A15,WAYBEL_0:def 1;
        take z;
          rng(F.j) c= X by A8;
        hence thesis by A24,A25;

        suppose a in K.j & not b in K.j;
      then A26: y = Bottom L by A5,A21;
        take x;
        thus thesis by A16,A26,YELLOW_0:44;

        suppose not a in K.j & b in K.j;
      then A27: x = Bottom L by A5,A21;
        take y;
        thus thesis by A16,A27,YELLOW_0:44;

        suppose not a in K.j & not b in K.j;
      then A28: x = Bottom L & y = Bottom L by A5,A21;
        take x;
        thus thesis by A16,A28;
      end;
      hence rng((curry G).j) is directed by WAYBEL_0:def 1;
    end;

  A29: dom doms F = dom F by EXTENS_1:3;
  A30: dom F = J by PBOOLE:def 3;
  A31: dom doms curry G = dom curry G by EXTENS_1:3;
  A32: dom curry G = J by Th20;

      product doms F c= product doms curry G
    proof
      let x be set;
      assume x in product doms F;
      then consider g being Function such that
    A33: x = g and
    A34: dom g = dom doms F and
    A35: for j being set st j in dom doms F holds g.j in (doms F).j
        by CARD_3:def 5;

    A36: dom g = dom doms curry G by A29,A30,A31,A34,Th20;
        for j being set st j in dom doms curry G holds g.j in (doms curry G).j
      proof
        let j be set;
        assume A37: j in dom doms curry G;
      then A38: j in J by A31,Th20;
        reconsider j' = j as Element of J by A31,A37,Th20;
      A39: g.j in (doms F).j by A29,A30,A35,A38;

      A40: (doms F).j = dom(F.j') by A30,FUNCT_6:31
                    .= K.j' by FUNCT_2:def 1;

      A41: K.j' c= K' by A6;

          (doms curry G).j = dom((curry G).j') by A32,FUNCT_6:31
                        .= K' by Th20;
        hence g.j in (doms curry G).j by A39,A40,A41;
      end;
      hence x in product doms curry G by A33,A36,CARD_3:def 5;
    end;
    then dom(Frege F) c= product doms curry G by PBOOLE:def 3;
  then A42: dom(Frege F) c= dom(Frege curry G) by PBOOLE:def 3;

  A43:
    for f being set st f in dom(Frege F)
      holds //\((Frege F).f, L) = //\((Frege curry G).f, L)
    proof
      let f' be set;
      assume
    A44: f' in dom(Frege F);
      then reconsider f= f' as Element of product doms F by PBOOLE:def 3;

    A45: dom((Frege F).f) = dom F by A44,Th8
                        .= J by PBOOLE:def 3;

    A46: dom((Frege curry G).f) = dom(curry G) by A42,A44,Th8
                              .= proj1 dom G by FUNCT_5:def 3
                              .= proj1 [:J, K':] by FUNCT_2:def 1
                              .= J by FUNCT_5:11;

        for j being set st j in J holds ((Frege F).f).j = ((Frege curry G).f).j
      proof
        let j' be set;
        assume j' in J;
        then reconsider j = j' as Element of J;

      A47: f.j in K.j & K.j c= K' by A6,A44,Lm6;
        then reconsider fj = f.j as Element of K';

          ((Frege F).f).j = (F.j).fj by A44,Lm5
                       .= G.[j, fj] by A5,A47
                       .= ((curry G).j).(f.j) by Th20
                       .= ((Frege curry G).f).j by A42,A44,Lm5;
        hence thesis;
      end;
      hence //\((Frege F).f', L) = //\((Frege curry G).f', L)
                    by A45,A46,FUNCT_1:9;
    end;

:: Unfortunately there are two cases: K = J --> K' or not.

  A48: Sup Infs(Frege curry G) = Sup Infs(Frege F)
    proof
      per cases;
:: case I
      suppose
    A49: for j being Element of J holds K.j = K';

        for j being set st j in J holds (doms F).j = (doms curry G).j
      proof
        let j be set;
        assume j in J;
        then reconsider j' = j as Element of J;
      A50: (doms F).j = dom(F.j') by A30,FUNCT_6:31
                    .= K.j' by FUNCT_2:def 1;
          (doms curry G).j = dom((curry G).j') by A32,FUNCT_6:31
                        .= K' by Th20;
        hence (doms F).j = (doms curry G).j by A49,A50;
      end;
      then doms F = doms curry G by A29,A30,A31,A32,FUNCT_1:9;
      then dom(Frege F) = product doms curry G by PBOOLE:def 3;
      then dom(Frege F) = dom(Frege curry G) by PBOOLE:def 3;
      hence thesis by A43,Th12;

:: case II
      suppose ex j being Element of J st K.j <> K';
      then consider j being Element of J such that
    A51: K.j <> K';
        K.j c= K' by A6;
      then not K' c= K.j by A51,XBOOLE_0:def 10;
      then consider k being set such that
    A52: k in K' & not k in K.j by TARSKI:def 3;
      reconsider k as Element of K' by A52;

    A53: rng Infs(Frege curry G) c= rng Infs(Frege F) \/ {Bottom L}
      proof
        let x be set;
        assume x in rng Infs(Frege curry G);
        then consider f being set such that
      A54: f in dom Frege curry G and
      A55: x = //\((Frege curry G).f, L) by Th13;
        reconsider f as Function by A54,Th7;

        per cases;
        suppose
      A56: for j being Element of J holds f.j in K.j;

      A57: dom f = dom curry G by A54,Th8
               .= dom doms F by A29,A30,Th20;

          for x st x in dom doms F holds f.x in (doms F).x
        proof
          let x;
          assume x in dom doms F;
          then reconsider j = x as Element of J by A30,EXTENS_1:3;
            (doms F).j = dom(F.j) by A30,FUNCT_6:31
                    .= K.j by FUNCT_2:def 1;
          hence thesis by A56;
        end;
        then f in product doms F by A57,CARD_3:18;
      then A58: f in dom Frege F by PBOOLE:def 3;
        then x = //\((Frege F).f, L) by A43,A55;
        then x in rng Infs(Frege F) by A58,Th13;
        hence thesis by XBOOLE_0:def 2;

        suppose ex j being Element of J st not f.j in K.j;
        then consider j being Element of J such that
      A59: not f.j in K.j;
          j in J;
        then j in dom curry G by Th20;
        then f.j in dom((curry G).j) by A54,Th9;
        then reconsider k = f.j as Element of K' by Th20;

          Bottom L = G.[j, k] by A5,A59
          .= ((curry G).j).(f.j) by Th20;
        then Bottom L in rng((Frege curry G).f) by A54,Lm5;
        then Bottom L >= "/\"(rng((Frege curry G).f), L) by YELLOW_2:24;
      then A60: Bottom L >= //\((Frege curry G).f, L) by YELLOW_2:def 6;
          Bottom L <= //\((Frege curry G).f, L) by YELLOW_0:44;
        then x = Bottom L by A55,A60,ORDERS_1:25;
        then x in {Bottom L} by TARSKI:def 1;
        hence thesis by XBOOLE_0:def 2;
      end;

A61:   rng Infs(Frege F) \/ {Bottom L} c= rng Infs(Frege curry G)
      proof
        let x be set;
        assume
      A62: x in rng Infs(Frege F) \/ {Bottom L};
        per cases by A62,XBOOLE_0:def 2;
        suppose x in rng Infs(Frege F);
        then consider f being set such that
      A63: f in dom Frege F and
      A64: x = //\((Frege F).f, L) by Th13;
          x = //\((Frege curry G).f, L) by A43,A63,A64;
        hence x in rng Infs(Frege curry G) by A42,A63,Th13;

        suppose A65: x in {Bottom L};
      then A66: x = Bottom L by TARSKI:def 1;
        reconsider x' = x as Element of L by A65;
        set f = J --> k;

      A67: dom f = J by FUNCOP_1:19
               .= dom doms curry G by A31,Th20;

          for x st x in dom doms curry G holds f.x in (doms curry G).x
        proof
          let x;
          assume x in dom doms curry G;
          then reconsider j = x as Element of J by A31,Th20;
        A68: f.j = k by FUNCOP_1:13;
            (doms curry G).j = dom((curry G).j) by A32,FUNCT_6:31
                          .= K' by Th20;
          hence thesis by A68;
        end;
        then f in product doms curry G by A67,CARD_3:18;
      then A69: f in dom Frege curry G by PBOOLE:def 3;
         x = G.[j, k] by A5,A52,A66
            .= ((curry G).j).k by Th20
            .= ((curry G).j).(f.j) by FUNCOP_1:13;
        then x in rng((Frege curry G).f) by A69,Lm5;
        then x' >= "/\"(rng((Frege curry G).f), L) by YELLOW_2:24;
      then A70: x' >= //\((Frege curry G).f, L) by YELLOW_2:def 6;
          x' <= //\((Frege curry G).f, L) by A66,YELLOW_0:44;
        then x' = //\((Frege curry G).f, L) by A70,ORDERS_1:25;
        hence x in rng Infs(Frege curry G) by A69,Th13;
      end;
    A71: ex_sup_of rng Infs(Frege F), L & ex_sup_of {Bottom
L}, L by YELLOW_0:17;
    A72: Bottom L <= Sup Infs(Frege F) by YELLOW_0:44;

        Sup Infs Frege curry G = sup rng Infs Frege curry G by YELLOW_2:def 5
              .= sup(rng Infs(Frege F) \/ {Bottom L}) by A53,A61,XBOOLE_0:def
10
              .= sup rng Infs(Frege F) "\/" sup{Bottom L} by A71,YELLOW_2:3
              .= sup rng Infs(Frege F) "\/" Bottom L by YELLOW_0:39
              .= Sup Infs(Frege F) "\/" Bottom L by YELLOW_2:def 5
              .= Sup Infs(Frege F) by A72,YELLOW_0:24;
      hence thesis;
    end;


  A73: dom F = J by PBOOLE:def 3
           .= dom curry G by PBOOLE:def 3;

      for j being set st j in dom F holds \\/(F.j, L) = \\/((curry G).j, L)
    proof
      let j' be set;
      assume
       j' in dom F;
      then reconsider j = j' as Element of J by PBOOLE:def 3;
      reconsider H = (curry G).j as Function of (J --> K').j, the carrier of L;
        (J --> K').j = K' by FUNCOP_1:13;
      then reconsider H as Function of K', the carrier of L;

    A74: ex_sup_of rng(F.j),L & ex_sup_of rng((curry G).j), L by YELLOW_0:17;
        rng(F.j) c= rng((curry G).j) by A8;
      then sup rng(F.j) <= sup rng((curry G).j) by A74,YELLOW_0:34;
      then Sup(F.j) <= sup(rng H) by YELLOW_2:def 5;
    then A75: Sup(F.j) <= Sup H by YELLOW_2:def 5;

        for k being Element of K' holds H.k <= Sup(F.j)
      proof
        let k be Element of K';
        per cases;
        suppose
      A76: k in K.j;
      then A77: (F.j).k = G.[j, k] by A5
                 .= H.k by Th20;
          k in dom(F.j) by A76,FUNCT_2:def 1;
        then H.k in rng(F.j) by A77,FUNCT_1:def 5;
        then H.k <= sup rng(F.j) by YELLOW_2:24;
        hence H.k <= Sup(F.j) by YELLOW_2:def 5;

        suppose not k in K.j;
        then Bottom L = G.[j, k] by A5
          .= H.k by Th20;
        hence H.k <= Sup(F.j) by YELLOW_0:44;
      end;
      then Sup H <= Sup(F.j) by YELLOW_2:56;
      hence \\/(F.j', L) = \\/((curry G).j', L) by A75,ORDERS_1:25;
    end;
    hence Inf Sups F = Inf Sups(curry G) by A73,Th11
                   .= Sup Infs(Frege F) by A1,A14,A48;
  end;
  hence thesis by Lm9;
end;

theorem ::Theorem 2.3 (1) iff (2')
    L is continuous iff
    for J, K being non empty set
    for F being Function of [:J, K:], the carrier of L st
      for j being Element of J holds rng((curry F).j) is directed
        holds
       Inf Sups curry F = Sup Infs Frege curry F
by Lm8,Lm10;


Lm11:
  for f being Function st f in Funcs(J, Fin K)
    holds
   for j holds f.j is finite Subset of K
proof
  let f be Function;
  assume f in Funcs(J, Fin K);
  then consider f' being Function such that
A1: f' = f and
A2: dom f' = J and
A3: rng f' c= Fin K by FUNCT_2:def 2;

    for j holds f.j is finite Subset of K
  proof
    let j;
      f.j in rng f by A1,A2,FUNCT_1:def 5;
    hence f.j is finite Subset of K by A1,A3,FINSUB_1:def 5;
  end;
  hence thesis;
end;


Lm12:
  for F being Function of [:J, K:], D
  for f being non-empty ManySortedSet of J st f in Funcs(J, Fin K)
  for G being DoubleIndexedSet of f, L st
    for j, x st x in f.j holds (G.j).x = F.[j, x]
    holds
   rng(G.j) is finite Subset of rng((curry F).j)
proof
  let F be Function of [:J, K:], D;
  let f be non-empty ManySortedSet of J such that
A1: f in Funcs(J, Fin K);
  let G be DoubleIndexedSet of f, L such that
A2: for j, x st x in f.j holds (G.j).x = F.[j, x];
A3: f.j is finite Subset of K by A1,Lm11;
A4:
  rng(G.j) c= rng((curry F).j)
  proof
    let y be set;
    assume y in rng(G.j);
    then consider k being set such that
  A5: k in dom(G.j) and
  A6: y = (G.j).k by FUNCT_1:def 5;
  A7: k in f.j by A5,FUNCT_2:def 1;
  then A8: k in K by A3;
    reconsider k as Element of K by A3,A7;
  A9: k in dom((curry F).j) by A8,Th20;
      y = F.[j, k] by A2,A6,A7
     .= ((curry F).j).k by Th20;
    hence y in rng((curry F).j) by A9,FUNCT_1:def 5;
  end;

    dom(G.j) is finite by A3,FUNCT_2:def 1;
then A10: (G.j).:(dom(G.j)) is finite by FINSET_1:17;

    rng(G.j) c= (G.j).:(dom(G.j))
  proof
    let y be set;
    assume y in rng(G.j);
    then consider k being set such that
  A11: k in dom(G.j) and
  A12: y = (G.j).k by FUNCT_1:def 5;
    thus y in (G.j).:(dom(G.j)) by A11,A12,FUNCT_1:def 12;
  end;
  hence thesis by A4,A10,FINSET_1:13;
end;

theorem Th22:
  for F being Function of [:J, K:], the carrier of L
  for X being Subset of L st X = {a where a is Element of L:
    ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
    ex G being DoubleIndexedSet of f, L st
      (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G}
    holds
   Inf Sups curry F >= sup X
proof
  let F be Function of [:J, K:], the carrier of L;
  let X be Subset of L;
  assume
A1: X = {a where a is Element of L:
    ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
    ex G being DoubleIndexedSet of f, L st
      (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G};

A2:
  for f being non-empty ManySortedSet of J st f in Funcs(J, Fin K)
  for G being DoubleIndexedSet of f, L st
    for j, x st x in f.j holds (G.j).x = F.[j, x]
  for j
    holds
   Sup((curry F).j) >= Sup(G.j)
  proof
    let f be non-empty ManySortedSet of J such that
  A3: f in Funcs(J, Fin K);
    let G be DoubleIndexedSet of f, L such that
  A4: for j, x st x in f.j holds (G.j).x = F.[j, x];
    let j;
  A5: ex_sup_of rng((curry F).j), L & ex_sup_of rng(G.j),L by YELLOW_0:17;

      rng(G.j) is Subset of rng((curry F).j) by A3,A4,Lm12;
    then sup rng((curry F).j) >= sup rng(G.j) by A5,YELLOW_0:34;
    then Sup((curry F).j) >= sup rng(G.j) by YELLOW_2:def 5;
    hence Sup((curry F).j) >= Sup(G.j) by YELLOW_2:def 5;
  end;

A6:
  for f being non-empty ManySortedSet of J st f in Funcs(J, Fin K)
  for G being DoubleIndexedSet of f, L st
    for j, x st x in f.j holds (G.j).x = F.[j, x]
    holds
   Inf Sups curry F >= Inf Sups G
  proof
    let f be non-empty ManySortedSet of J such that
  A7: f in Funcs(J, Fin K);
    let G be DoubleIndexedSet of f, L such that
  A8: for j, x st x in f.j holds (G.j).x = F.[j, x];

      rng Sups curry F is_>=_than Inf Sups G
    proof
      let a;
      assume a in rng Sups curry F;
      then consider j being Element of J such that
    A9: a = Sup((curry F).j) by Th14;

    A10: Sup((curry F).j) >= Sup(G.j) by A2,A7,A8;
        Sup(G.j) in rng Sups G by Th14;
      then Sup(G.j) >= inf rng Sups G by YELLOW_2:24;
      then Sup(G.j) >= Inf Sups G by YELLOW_2:def 6;
      hence a >= Inf Sups G by A9,A10,ORDERS_1:26;
    end;
    then inf rng Sups curry F >= Inf Sups G by YELLOW_0:33;
    hence Inf Sups curry F >= Inf Sups G by YELLOW_2:def 6;
  end;

    Inf Sups curry F is_>=_than X
  proof
    let a;
    assume a in X;
    then consider a' being Element of L such that
  A11: a' = a and
  A12: ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
      ex G being DoubleIndexedSet of f, L st
        (for j, x st x in
 f.j holds (G.j).x = F.[j, x]) & a' = Inf Sups G by A1;
    consider f being non-empty ManySortedSet of J such that
  A13: f in Funcs(J, Fin K) and
  A14: ex G being DoubleIndexedSet of f, L st
      (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a' = Inf Sups G by A12;
    consider G being DoubleIndexedSet of f, L such that
  A15: for j, x st x in f.j holds (G.j).x = F.[j, x] and
  A16: a' = Inf Sups G by A14;
    thus Inf Sups curry F >= a by A6,A11,A13,A15,A16;
  end;
  hence thesis by YELLOW_0:32;
end;


Lm13:   ::Theorem 2.3 (1) implies (3)
  L is continuous implies
    for J, K for F being Function of [:J, K:], the carrier of L
    for X being Subset of L st X = {a where a is Element of L:
      ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
      ex G being DoubleIndexedSet of f, L st
        (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G}
      holds
     Inf Sups curry F = sup X
proof
  assume
A1: L is continuous;

  hereby
    let J, K;
    let F be Function of [:J, K:], the carrier of L;
    let X be Subset of L;
    assume
  A2: X = {a where a is Element of L:
    ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
    ex G being DoubleIndexedSet of f, L st
      (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G};

    set FIK = {A where A is Subset of K: A is finite & A <> {}};
    consider k being Element of K;
      {k} c= K & {k} <> {} by ZFMISC_1:37;
    then {k} in FIK;
    then reconsider FIK as non empty set;

  A3: FIK c= Fin K
    proof
      let x be set;
      assume x in FIK;
      then consider A being Subset of K such that
    A4: x = A & A is finite & A <> {};
      thus x in Fin K by A4,FINSUB_1:def 5;
    end;

    set N = Funcs(J, FIK);
    deffunc F(Element of J, Element of N) = sup(((curry F).$1).:($2.$1));
      ex H being Function of [:J, N:], the carrier of L st
      for j being Element of J for g being Element of N holds
      H.[j, g] = F(j,g) from Lambda2D;
    then consider H being Function of [:J, N:], the carrier of L such that
  A5: for j for g being Element of N holds
      H.[j, g] = sup(((curry F).j).:(g.j));

     set cF = curry F, cH = curry H;

  A6: for j holds
    (for Y being finite Subset of rng(cF.j) st Y <> {} holds ex_sup_of Y,L) &
    (for x being Element of L st x in rng(cH.j)
      ex Y being finite Subset of rng(cF.j) st ex_sup_of Y,L & x = "\/"(Y,L)) &
    for Y being finite Subset of rng(cF.j) st Y <> {} holds "\/"(Y,L) in
 rng(cH.j)
    proof
      let j;
      set D = rng((curry H).j), R = rng((curry F).j);
      set Hj = (curry H).j, Fj = (curry F).j;

      thus for Y being finite Subset of R st Y <> {} holds ex_sup_of Y,L
        by YELLOW_0:17;
      thus for x being Element of L st x in D
        ex Y being finite Subset of R st ex_sup_of Y,L & x = "\/"(Y,L)
      proof
        let x be Element of L;
        assume x in D;
        then consider g being set such that
      A7: g in dom Hj and
      A8: Hj.g = x by FUNCT_1:def 5;
        reconsider g as Element of N by A7,Th20;
      A9: x = H.[j, g] by A8,Th20
           .= sup(Fj.:(g.j)) by A5;
        consider g' being Function such that
      A10: g' = g and
      A11: dom g' = J and
      A12: rng g' c= FIK by FUNCT_2:def 2;
          g.j in rng g by A10,A11,FUNCT_1:def 5;
        then g.j in FIK by A10,A12;
        then consider A being Subset of K such that
      A13: A = g.j & A is finite & A <> {};
        reconsider Y = Fj.:(g.j) as finite Subset of R
           by A13,FINSET_1:17,RELAT_1:144;
        take Y;
        thus thesis by A9,YELLOW_0:17;
      end;

      thus for Y being finite Subset of R st Y <> {} holds "\/"(Y,L) in D
      proof
        let Y be finite Subset of R;
        assume
      A14: Y <> {};
        consider Z being set such that
      A15: Z c= dom Fj and
      A16: Z is finite and
      A17: Fj.:Z = Y by COMPTS_1:1;
      A18: Z <> {} by A14,A17,RELAT_1:149;
          Z c= K by A15,Th20;
        then Z in FIK by A16,A18;
      then A19: {Z} c= FIK by ZFMISC_1:37;
      A20: dom(J --> Z) = J by FUNCOP_1:19;
          rng(J --> Z) = {Z} by FUNCOP_1:14;
        then reconsider g = J --> Z as Element of N by A19,A20,FUNCT_2:def 2;
          g in N;
      then A21: g in dom Hj by Th20;
      A22: g.j = Z by FUNCOP_1:13;
          Hj.g = H.[j, g] by Th20
            .= "\/"(Y, L) by A5,A17,A22;
        hence "\/"(Y, L) in D by A21,FUNCT_1:def 5;
      end;
    end;


      for j holds rng((curry H).j) is directed
    proof
      let j;
        (for Y being finite Subset of rng(cF.j) st
        Y <> {} holds ex_sup_of Y,L) &
      (for x being Element of L st x in rng(cH.j)
        ex Y being finite Subset of rng(cF.j) st
          ex_sup_of Y,L & x = "\/"(Y,L)) &
      for Y being finite Subset of rng(cF.j) st
        Y <> {} holds "\/"(Y,L) in rng(cH.j) by A6;
      hence rng(cH.j) is directed by WAYBEL_0:51;
    end;
  then A23: Inf Sups curry H = Sup Infs Frege curry H by A1,Lm8;

  A24: dom curry F = J by Th20
                 .= dom curry H by Th20;

      for j being set st j in dom curry F holds
      \\/((curry F).j, L) = \\/((curry H).j, L)
    proof
      let j' be set;
      assume j' in dom curry F;
      then reconsider j = j' as Element of J by Th20;
    A25: ex_sup_of rng(cF.j),L by YELLOW_0:17;
        (for Y being finite Subset of rng(cF.j) st
        Y <> {} holds ex_sup_of Y,L) &
      (for x being Element of L st x in rng(cH.j)
        ex Y being finite Subset of rng(cF.j) st
          ex_sup_of Y,L & x = "\/"(Y,L)) &
      for Y being finite Subset of rng(cF.j) st
        Y <> {} holds "\/"(Y,L) in rng(cH.j) by A6;
      then sup(rng(cF.j)) = sup(rng(cH.j)) by A25,WAYBEL_0:54;
      then Sup(cF.j) = sup(rng(cH.j)) by YELLOW_2:def 5;
      hence thesis by YELLOW_2:def 5;
    end;
  then A26: Inf Sups curry F = Inf Sups curry H by A24,Th11;


  A27: for h being Function-yielding Function st h in product doms curry H
    holds
      (for j holds ((Frege h).(id J)).j = (h.j).j & h.j in N &
        ((Frege h).(id J)).j is finite non empty Subset of K) &
      (Frege h).(id J) is non-empty ManySortedSet of J &
      (Frege h).(id J) in Funcs(J, FIK) & (Frege h).(id J) in Funcs(J, Fin K)
    proof
      let h be Function-yielding Function;
      set f = (Frege h).(id J);
      assume h in product doms curry H;
    then A28: h in dom Frege curry H by PBOOLE:def 3;

    A29: dom id J = J by FUNCT_1:34;
    A30: dom doms h = dom h by EXTENS_1:3;
    A31: dom h = dom curry H by A28,Th8
             .= J by Th20;

        for x st x in dom doms h holds (id J).x in (doms h).x
      proof
        let x;
        assume x in dom doms h;
        then reconsider j = x as Element of J by A31,EXTENS_1:3;
      A32: (id J).j = j by FUNCT_1:35;
          h.j in (J --> N).j by A28,Lm6;
        then h.j in N by FUNCOP_1:13;
        then consider g being Function such that
      A33: g = h.j and
      A34: dom g = J and
             rng g c= FIK by FUNCT_2:def 2;
          (doms h).j = J by A31,A33,A34,FUNCT_6:31;
        hence thesis by A32;
      end;
      then id J in product doms h by A29,A30,A31,CARD_3:18;
    then A35: id J in dom Frege h by PBOOLE:def 3;

      thus
    A36: for j holds ((Frege h).(id J)).j = (h.j).j & h.j in N &
        ((Frege h).(id J)).j is finite non empty Subset of K
      proof
        let j;
        thus
      A37: ((Frege h).(id J)).j = (h.j).((id J).j) by A31,A35,Th9
                              .= (h.j).j by FUNCT_1:35;

          h.j in (J --> N).j by A28,Lm6;
        hence
          h.j in N by FUNCOP_1:13;
        then consider g being Function such that
      A38: g = h.j and
      A39: dom g = J and
      A40: rng g c= FIK by FUNCT_2:def 2;
          f.j in rng g by A37,A38,A39,FUNCT_1:def 5;
        then f.j in FIK by A40;
        then consider A being Subset of K such that
      A41: f.j = A & A is finite & A <> {};
        thus f.j is finite non empty Subset of K by A41;
      end;

    A42: dom f = J by A31,A35,Th8;
      then reconsider f'= f as ManySortedSet of J by PBOOLE:def 3;

        for j being set st j in J holds f'.j is non empty by A36;
      hence f is non-empty ManySortedSet of J by PBOOLE:def 16;

    A43: rng f c= FIK
      proof
        let y be set;
        assume y in rng f;
        then consider j being set such that
      A44: j in dom f and
      A45: y = f.j by FUNCT_1:def 5;
          f.j is finite non empty Subset of K by A36,A42,A44;
        hence y in FIK by A45;
      end;
      hence f in Funcs(J, FIK) by A42,FUNCT_2:def 2;
        rng f c= Fin K by A3,A43,XBOOLE_1:1;
      hence f in Funcs(J, Fin K) by A42,FUNCT_2:def 2;
    end;

  A46: for h being Element of product doms curry H holds
        Inf((Frege curry H).h) <= sup X
    proof
      let h be Element of product doms curry H;
        h in product doms curry H;
    then A47: h in dom Frege curry H by PBOOLE:def 3;
        for x st x in dom h holds h.x is Function
      proof
        let x;
        assume
      A48: x in dom h;
          dom h = dom curry H by A47,Th8
             .= J by Th20;
        then reconsider j = x as Element of J by A48;
          h.j in (J --> N).j by A47,Lm6;
        then h.j in N by FUNCOP_1:13;
        then ex f being Function st h.j = f & dom f = J & rng f c= FIK
          by FUNCT_2:def 2;
        hence thesis;
      end;
      then reconsider h'= h as Function-yielding Function by PRALG_1:def 15;
      reconsider f = (Frege h').(id J) as non-empty ManySortedSet of J by A27;
    A49: f in Funcs(J, Fin K) by A27;

      defpred P[set,set,set] means $1 = F.[$3, $2];
    A50: for j being set st j in J holds
      for x st x in f.j ex y st y in (J --> the carrier of L).j & P[y,x,j]
      proof
        let i;
        assume i in J;
        then reconsider j = i as Element of J;
        let x;
        assume
      A51: x in f.i;
          f.j is Subset of K by A27;
        then reconsider k = x as Element of K by A51;
        take y = F.[j, k];
          [j, k] in [:J, K:] by ZFMISC_1:106;
        then y in the carrier of L by FUNCT_2:7;
        hence thesis by FUNCOP_1:13;
      end;

        ex G being ManySortedFunction of f, (J --> the carrier of L) st
        for j being set st j in J holds
          ex g being Function of f.j, (J --> the carrier of L).j st g = G.j &
          for x st x in f.j holds P[g.x,x,j] from MSFExFunc(A50);
      then consider G being ManySortedFunction of f, (J --> the carrier of L)
        such that
    A52: for j being set st j in J holds
          ex g being Function of f.j, (J --> the carrier of L).j st g = G.j &
          for x st x in f.j holds g.x = F.[j, x];
      reconsider G as DoubleIndexedSet of f, L;

    A53: for j, x st x in f.j holds (G.j).x = F.[j, x]
      proof
        let j, x;
        assume
      A54: x in f.j;
        consider g being Function of f.j, (J --> the carrier of L).j such that
       A55: g = G.j and
       A56: for x st x in f.j holds g.x = F.[j, x] by A52;
        thus thesis by A54,A55,A56;
      end;

        Inf((Frege curry H).h) is_<=_than rng Sups G
      proof
        let y be Element of L;
        assume y in rng Sups G;
        then consider j such that
      A57: y = Sup(G.j) by Th14;

      A58: ex_sup_of ((curry F.j).:(f.j)),L & ex_sup_of rng(G.j),L
          by YELLOW_0:17;

          (curry F.j).:(f.j) c= rng(G.j)
        proof
          let y be set;
          assume y in (curry F.j).:(f.j);
          then consider x being set such that
        A59: x in dom((curry F).j) and
        A60: x in f.j and
        A61: y = ((curry F).j).x by FUNCT_1:def 12;
          reconsider k = x as Element of K by A59,Th20;
        A62: y = F.[j, k] by A61,Th20
              .= (G.j).k by A53,A60;
            k in dom(G.j) by A60,FUNCT_2:def 1;
          hence y in rng(G.j) by A62,FUNCT_1:def 5;
        end;
        then sup((curry F.j).:(f.j)) <= sup rng(G.j) by A58,YELLOW_0:34;
      then A63: sup((curry F.j).:(f.j)) <= Sup(G.j) by YELLOW_2:def 5;

          j in J;
      then A64: j in dom curry H by Th20;
          h.j in (J --> N).j by A47,Lm6;
        then reconsider hj = h.j as Element of N by FUNCOP_1:13;

        A65: sup((curry F.j).:(f.j)) = sup((curry F.j).:(hj.j)) by A27
                              .= H.[j, hj] by A5
                              .= ((curry H).j).(h.j) by Th20
                              .= ((Frege curry H).h).j by A47,A64,Th9;
          Inf((Frege curry H).h) <= ((Frege curry H).h).j by YELLOW_2:55;
        hence Inf((Frege curry H).h) <= y by A57,A63,A65,ORDERS_1:26;
      end;
      then Inf((Frege curry H).h) <= inf rng Sups G by YELLOW_0:33;
    then A66: Inf((Frege curry H).h) <= Inf Sups G by YELLOW_2:def 6;

        Inf Sups G in X by A2,A49,A53;
      then Inf Sups G <= sup X by YELLOW_2:24;
      hence Inf((Frege curry H).h) <= sup X by A66,ORDERS_1:26;
    end;

      rng Infs Frege curry H is_<=_than sup X
    proof
      let x be Element of L;
      assume x in rng Infs Frege curry H;
      then consider h being set such that
    A67: h in dom Frege curry H and
    A68: x = //\((Frege curry H).h, L) by Th13;
      reconsider h as Element of product doms curry H by A67,PBOOLE:def 3;
        Inf((Frege curry H).h) <= sup X by A46;
      hence thesis by A68;
    end;
    then sup rng Infs Frege curry H <= sup X by YELLOW_0:32;
  then A69: Inf Sups curry F <= sup X by A23,A26,YELLOW_2:def 5;
      Inf Sups curry F >= sup X by A2,Th22;
    hence Inf Sups curry F = sup X by A69,ORDERS_1:25;
  end;
  thus thesis;
end;


Lm14:    ::Theorem 2.3 (3) implies (1)
  (for J, K for F being Function of [:J, K:], the carrier of L
  for X being Subset of L st X = {a where a is Element of L:
    ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
    ex G being DoubleIndexedSet of f, L st
      (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G}
    holds Inf Sups curry F = sup X)
      implies
     L is continuous
proof
  assume
A1:
  for J, K for F being Function of [:J, K:], the carrier of L
  for X being Subset of L st X = {a where a is Element of L:
    ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
    ex G being DoubleIndexedSet of f, L st
      (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G}
    holds Inf Sups curry F = sup X;

    for J, K for F being Function of [:J, K:], the carrier of L st
    for j being Element of J holds rng((curry F).j) is directed
      holds Inf Sups curry F = Sup Infs Frege curry F
  proof
    let J, K;
    let F be Function of [:J, K:], the carrier of L such that
  A2: for j being Element of J holds rng((curry F).j) is directed;

    defpred P[Element of L] means
      ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
      ex G being DoubleIndexedSet of f, L st
        (for j, x st x in f.j holds (G.j).x = F.[j, x]) & $1 = Inf Sups G;
    reconsider X = {a where a is Element of L: P[a]}
     as Subset of L from RelStrSubset;

      X is_<=_than Sup Infs Frege curry F
    proof
      let a' be Element of L;
      assume a' in X;
      then consider a being Element of L such that
    A3: a' = a and
    A4: ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
        ex G being DoubleIndexedSet of f, L st
         (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G;
      consider f being non-empty ManySortedSet of J such that
    A5: f in Funcs(J, Fin K) and
    A6: ex G being DoubleIndexedSet of f, L st
        (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G by A4;
      consider G being DoubleIndexedSet of f, L such that
    A7: for j, x st x in f.j holds (G.j).x = F.[j, x] and
    A8: a = Inf Sups G by A6;

      defpred P[set, set] means
        $1 in J & $2 in K & ex b st b = ((curry F).$1).$2 & a <= b;

    A9: for x st x in J ex y st y in K & P[x, y]
      proof
        let x;
        assume
            x in J;
        then reconsider j = x as Element of J;
      A10: rng((curry F).j) is non empty directed by A2;
          rng(G.j) is finite Subset of rng((curry F).j) by A5,A7,Lm12;
        then consider y being Element of L such that
      A11: y in rng((curry F).j) and
      A12: rng(G.j) is_<=_than y by A10,WAYBEL_0:1;
        consider k being set such that
      A13: k in dom((curry F).j) and
      A14: y = ((curry F).j).k by A11,FUNCT_1:def 5;
        reconsider k as Element of K by A13,Th20;
        take k;
          sup rng(G.j) <= y by A12,YELLOW_0:32;
      then A15: Sup(G.j) <= y by YELLOW_2:def 5;
          Sup(G.j) in rng Sups G by Th14;
        then inf rng Sups G <= Sup(G.j) by YELLOW_2:24;
        then Inf Sups G <= Sup(G.j) by YELLOW_2:def 6;
        then a <= y by A8,A15,ORDERS_1:26;
        hence thesis by A14;
      end;

      consider g being Function such that
    A16: dom g = J and rng g c= K and
    A17: for x st x in J holds P[x, g.x] from NonUniqBoundFuncEx(A9);

    A18: dom doms curry F = dom curry F by EXTENS_1:3;
    then A19: dom g = dom doms curry F by A16,Th20;

        for x st x in dom doms curry F holds g.x in (doms curry F).x
      proof
        let x;
        assume x in dom doms curry F;
        then reconsider j = x as Element of J by A18,Th20;
          dom curry F = J by Th20;
        then (doms curry F).j = dom((curry F).j) by FUNCT_6:31
                        .= K by Th20;
        hence thesis by A17;
      end;
      then reconsider g as Element of product doms curry F by A19,CARD_3:18;
        for j holds a <= ((Frege curry F).g).j
      proof
        let j;
      A20: dom Frege curry F = product doms curry F by PBOOLE:def 3;
        A21: J = dom curry F by Th20;
        consider b such that
      A22: b = ((curry F).j).(g.j) & a <= b by A17;
        thus thesis by A20,A21,A22,Th9;
      end;
    then A23: a <= Inf((Frege curry F).g) by YELLOW_2:57;
        Inf((Frege curry F).g) in rng Infs Frege curry F by Th14;
      then Inf((Frege curry F).g) <= sup rng Infs Frege curry F by YELLOW_2:24
;
      then Inf((Frege curry F).g) <= Sup Infs Frege curry F by YELLOW_2:def 5;
      hence a' <= Sup Infs Frege curry F by A3,A23,ORDERS_1:26;
    end;
    then sup X <= Sup Infs Frege curry F by YELLOW_0:32;
  then A24: Inf Sups curry F <= Sup Infs Frege curry F by A1;
      Inf Sups curry F >= Sup Infs Frege curry F by Th16;
    hence Inf Sups curry F = Sup Infs Frege curry F by A24,ORDERS_1:25;
  end;
  hence L is continuous by Lm10;
end;

theorem ::Theorem 2.3 (1) iff (3)
    L is continuous iff
   (for J, K for F being Function of [:J, K:], the carrier of L
   for X being Subset of L st X = {a where a is Element of L:
     ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) &
     ex G being DoubleIndexedSet of f, L st
       (for j, x st x in f.j holds (G.j).x = F.[j, x]) & a = Inf Sups G}
     holds Inf Sups curry F = sup X)
by Lm13,Lm14;


begin  :: Completely-Distributive Lattices

definition ::Definition 2.4
  let L be non empty RelStr;
  attr L is completely-distributive means
:Def3:
  L is complete &
    for J being non empty set, K being non-empty ManySortedSet of J
    for F being DoubleIndexedSet of K, L
      holds
     Inf Sups F = Sup Infs Frege F;
end;

reserve J for non empty set,

        K for non-empty ManySortedSet of J;


definition
  cluster trivial -> completely-distributive (non empty Poset);
  coherence
  proof
    let L be non empty Poset;
    assume
  A1: L is trivial;
    consider x being Element of L;

    thus L is complete
    proof
      let X be set;
      take x;
      thus X is_<=_than x
      proof
        let y be Element of L;
        thus y in X implies y <= x by A1,REALSET1:def 20;
      end;
      let y be Element of L;
        y = x by A1,REALSET1:def 20;
      hence thesis by ORDERS_1:24;
    end;
    then L is complete (non empty Poset);
    then reconsider L'= L as complete LATTICE;

      for x being Element of L' holds x = sup waybelow x
       by A1,REALSET1:def 20;
  then A2: L' is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
      for x being Element of L' holds waybelow x is non empty directed;
    then reconsider L' as continuous LATTICE by A2,WAYBEL_3:def 6;

      for J being non empty set, K being non-empty ManySortedSet of J
    for F being DoubleIndexedSet of K, L'
      holds
     Inf Sups F = Sup Infs(Frege F)
    proof
      let J be non empty set, K be non-empty ManySortedSet of J;
      let F be DoubleIndexedSet of K, L';

        for j being Element of J holds rng(F.j) is directed
      proof
        let j be Element of J;
          for x, y being Element of L st x in rng(F.j) & y in rng(F.j)
          ex z being Element of L st z in rng(F.j) & x <= z & y <= z
        proof
          let x, y be Element of L;
          assume x in rng(F.j) & y in rng(F.j);
          consider z being Element of rng(F.j);
          reconsider z as Element of L;
          take z;
          thus thesis by A1,REALSET1:def 20;
        end;
        hence rng(F.j) is directed by WAYBEL_0:def 1;
      end;
      hence Inf Sups F = Sup Infs(Frege F) by Lm8;
    end;
    hence thesis;
  end;
end;

definition
  cluster completely-distributive LATTICE;
  existence
  proof
    consider x being set, R be Order of {x};
      RelStr(#{x},R#) is trivial non empty RelStr;
    hence thesis;
  end;
end;

theorem Th24: ::Corollary 2.5
  for L being completely-distributive LATTICE holds L is continuous
proof
  let L be completely-distributive LATTICE;
    L is complete & (for F being DoubleIndexedSet of K, L st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs Frege F) by Def3;
  hence L is continuous by Lm9;
end;

definition
  cluster completely-distributive -> complete continuous LATTICE;
  correctness by Def3,Th24;
end;

theorem Th25:
  for L being non empty antisymmetric transitive with_infima RelStr
  for x being Element of L
  for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L &
    Y = {x"/\"y where y is Element of L: y in X}
    holds
   x "/\" sup X >= sup Y
proof
  let L be non empty antisymmetric transitive with_infima RelStr;
  let x be Element of L;
  let X, Y be Subset of L such that
A1: ex_sup_of X,L and
A2: ex_sup_of Y,L and
A3: Y = {x"/\"y where y is Element of L: y in X};

    Y is_<=_than (x "/\" sup X)
  proof
    let y be Element of L;
    assume y in Y;
    then consider z being Element of L such that
  A4:  y = x "/\" z and
  A5:  z in X by A3;
      X is_<=_than sup X by A1,YELLOW_0:30;
    then y <= z & z <= sup X by A4,A5,LATTICE3:def 9,YELLOW_0:23;
    then y <= x & y <= sup X by A4,YELLOW_0:23,def 2;
    hence y <= x "/\" sup X by YELLOW_0:23;
  end;
  hence sup Y <= x "/\" sup X by A2,YELLOW_0:30;
end;

Lm15:
  for L being completely-distributive LATTICE
  for X being non empty Subset of L
  for x being Element of L
    holds
   x "/\" sup X = "\/"({x"/\"y where y is Element of L: y in X}, L)
proof
  let L be completely-distributive LATTICE;
  let X be non empty Subset of L;
  let x be Element of L;
  set A = {x"/\"y where y is Element of L: y in X};
  set J = {1, 2}, K = (1, 2) --> ({1}, X);
  set F = (1, 2) --> ({1} --> x, id X);
A1: F.1 = {1} --> x & F.2 = id X by FUNCT_4:66;
A2: K.1 = {1} & K.2 = X by FUNCT_4:66;

  reconsider j1 = 1, j2 = 2 as Element of J by TARSKI:def 2;

    dom K = J by FUNCT_4:65;
  then reconsider K as ManySortedSet of J by PBOOLE:def 3;

    i in J implies K.i is non empty by A2,TARSKI:def 2;
  then reconsider K as non-empty ManySortedSet of J by PBOOLE:def 16;

      dom F = J by FUNCT_4:65;
  then reconsider F as ManySortedSet of J by PBOOLE:def 3;

    for j being set st j in J holds F.j is
    Function of K.j, (J --> the carrier of L).j
  proof
    let j be set;
    assume
  A3: j in J;
  then A4: (J --> the carrier of L).j = the carrier of L by FUNCOP_1:13;
    per cases by A3,TARSKI:def 2;
    suppose j = 1;
hence F.j is Function of K.j, (J --> the carrier of L).j
         by A2,A4,FUNCT_4:66;

    suppose j = 2;
    hence F.j is Function of K.j, (J --> the carrier of L).j
       by A1,A2,A4,FUNCT_2:9;
  end;
  then reconsider F as DoubleIndexedSet of K, L by MSUALG_1:def 2;

    x "/\" sup X is_<=_than rng Sups F
  proof
    let y be Element of L;
    assume y in rng Sups F;
    then consider j being Element of J such that
  A5: y = Sup(F.j) by Th14;
    per cases by TARSKI:def 2;
    suppose j = 1;
    then rng(F.j) = {x} by A1,FUNCOP_1:14;
    then Sup(F.j) = sup{x} by YELLOW_2:def 5;
    then y = x by A5,YELLOW_0:39;
    hence x "/\" sup X <= y by YELLOW_0:23;

    suppose j = 2;
    then rng(F.j) = X by A1,RELAT_1:71;
    then y = sup X by A5,YELLOW_2:def 5;
    hence x "/\" sup X <= y by YELLOW_0:23;
  end;
  then x "/\" sup X <= inf rng Sups F by YELLOW_0:33;
  then x "/\" sup X <= Inf Sups F by YELLOW_2:def 6;
then A6: x "/\" sup X <= Sup Infs Frege F by Def3;

    rng Infs Frege F is_<=_than "\/"({x"/\"y where y is Element of L: y in X},
L
)
  proof
    let y be Element of L;
    assume y in rng Infs Frege F;
    then consider f being set such that
  A7: f in dom Frege F and
  A8: y = //\(((Frege F).f), L) by Th13;
    reconsider f as Function by A7,Th7;
  A9: f.j1 in K.j1 & f.j2 in K.j2 by A7,Lm6;
    then reconsider f2 = f.2 as Element of X by FUNCT_4:66;
  A10: y = "/\"(rng((Frege F).f), L) by A8,YELLOW_2:def 6;
  A11: ex_inf_of rng((Frege F).f),L & ex_inf_of {x, f.2},L by YELLOW_0:17;

      {x, f2} c= rng((Frege F).f)
    proof
      let z be set;
      assume z in {x, f2};
      then z = x or z = f.2 by TARSKI:def 2;
      then z = (F.j1).(f.j1) or z = (F.j2).(f.j2)
          by A1,A2,A9,FUNCOP_1:13,FUNCT_1:35;
      hence z in rng((Frege F).f) by A7,Lm5;
    end;
    then y <= inf{x, f2} by A10,A11,YELLOW_0:35;
  then A12: y <= x"/\"f2 by YELLOW_0:40;
      x"/\"f2 in A;
    then x"/\"f2 <= "\/"(A, L) by YELLOW_2:24;
    hence thesis by A12,YELLOW_0:def 2;
  end;
  then sup rng Infs Frege F <= "\/"({x"/\"y where y is Element of L: y in X},
L) by YELLOW_0:32;
  then Sup Infs Frege F <= "\/"({x"/\"y where y is Element of L: y in X}, L)
by YELLOW_2:def 5;
then A13: x "/\" sup X <= "\/"({x"/\"y where y is Element of L: y in X}, L) by
A6,YELLOW_0:def 2;

    (x "/\").:X = A by WAYBEL_1:64;
  then reconsider A'= A as Subset of L;
    ex_sup_of X,L & ex_sup_of A',L by YELLOW_0:17;
  then x "/\" sup X >= sup A' by Th25;
  hence thesis by A13,YELLOW_0:def 3;
end;

theorem Th26:
  for L being completely-distributive LATTICE
  for X being Subset of L
  for x being Element of L
    holds
   x "/\" sup X = "\/"({x"/\"y where y is Element of L: y in X}, L)
proof
  let L be completely-distributive LATTICE;
  let X be Subset of L;
  let x be Element of L;
  set A = {x"/\"y where y is Element of L: y in X};
  per cases;
  suppose
A1: X is empty;
    now
    assume
  A2: A <> {};
    consider z being Element of A;
      z in A by A2;
    then consider y being Element of L such that
  A3: z = x"/\"y & y in X;
    thus contradiction by A1,A3;
  end;
  then sup X = Bottom L & "\/"(A, L) = Bottom
L by A1,YELLOW_0:def 11; hence thesis by WAYBEL_1:4;

  suppose X is non empty;
  hence thesis by Lm15;
end;

definition
  cluster completely-distributive -> Heyting LATTICE;
  correctness
  proof
    let L be LATTICE;
    assume L is completely-distributive;
    then reconsider L as completely-distributive LATTICE;
      for X being Subset of L
    for x being Element of L
      holds
     x"/\" sup X = "\/"({x"/\"
y where y is Element of L: y in X}, L) by Th26;
     then for x being Element of L holds x "/\" has_an_upper_adjoint by
WAYBEL_1:67;
     hence thesis by WAYBEL_1:def 19;
  end;
end;

:: For distributivity confer WAYBEL_1.


begin  :: SubFrames of Continuous Lattices

definition ::Definition 2.6
  let L be non empty RelStr;
  mode CLSubFrame of L is infs-inheriting directed-sups-inheriting
    (non empty full SubRelStr of L);
end;

theorem Th27:
  for F being DoubleIndexedSet of K, L st
    for j being Element of J holds rng(F.j) is directed
      holds
     rng Infs Frege F is directed
proof
  let F be DoubleIndexedSet of K, L;
  assume
A1: for j being Element of J holds rng(F.j) is directed;

  set X = rng Infs Frege F;

    for x, y being Element of L st x in X & y in X
    ex z being Element of L st z in X & x <= z & y <= z
  proof
    let x, y be Element of L;
    assume that
  A2: x in X and
  A3: y in X;
    consider g being set such that
  A4: g in dom(Frege F) and
  A5: x = //\((Frege F).g, L) by A2,Th13;
    reconsider g as Function by A4,Th7;
    reconsider G = (Frege F).g as Function of J, the carrier of L
      by A4,Th10;
  A6: x = "/\"(rng((Frege F).g), L) by A5,YELLOW_2:def 6;
  A7: ex_inf_of rng((Frege F).g),L by YELLOW_0:17;

    consider h being set such that
  A8: h in dom(Frege F) and
  A9: y = //\((Frege F).h, L) by A3,Th13;
    reconsider h as Function by A8,Th7;
    reconsider H = (Frege F).h as Function of J, the carrier of L
      by A8,Th10;
  A10: y = "/\"(rng((Frege F).h), L) by A9,YELLOW_2:def 6;
  A11: ex_inf_of rng((Frege F).h),L by YELLOW_0:17;

  A12:
    for j being Element of J
      ex k being Element of K.j st G.j <= (F.j).k & H.j <= (F.j).k
    proof
      let j be Element of J;
        j in J;
      then j in dom F by PBOOLE:def 3;
    then A13: G.j = (F.j).(g.j) & H.j = (F.j).(h.j) by A4,A8,Th9;
    A14: rng(F.j) is directed Subset of L by A1;
        j in J;
      then j in dom F by PBOOLE:def 3;
      then g.j in dom(F.j) & h.j in dom(F.j) by A4,A8,Th9;
      then G.j in rng(F.j) & H.j in rng(F.j) by A13,FUNCT_1:def 5;
      then consider c being Element of L such that
    A15: c in rng(F.j) and
    A16: G.j <= c & H.j <= c by A14,WAYBEL_0:def 1;
      consider k being set such that
    A17: k in dom(F.j) and
    A18: c = (F.j).k by A15,FUNCT_1:def 5;
      reconsider k as Element of K.j by A17,FUNCT_2:def 1;
      take k;
      thus G.j <= (F.j).k & H.j <= (F.j).k by A16,A18;
    end;

    defpred P[set, set] means
      $1 in J & $2 in K.$1 & for c being Element of L st c = (F.$1).$2
        holds
       (for a being Element of L st a = G.$1 holds a <= c) &
       (for b being Element of L st b = H.$1 holds b <= c);

   A19:
    for j being set st j in J ex k being set st k in union rng K & P[j, k]
    proof
      let j' be set;
      assume j' in J;
      then reconsider j = j' as Element of J;
      consider k being Element of K.j such that
    A20: G.j <= (F.j).k and
    A21: H.j <= (F.j).k by A12;
      take k;
        j in J;
      then j in dom K by PBOOLE:def 3;
      then k in K.j & K.j in rng K by FUNCT_1:def 5;
      hence k in union rng K by TARSKI:def 4;

      thus P[j', k] by A20,A21;
    end;

    consider f being Function such that
  A22: dom f = J and rng f c= union rng K and
  A23: for j being set st j in J holds P[j, f.j] from NonUniqBoundFuncEx(A19);
  A24: dom f = dom F by A22,PBOOLE:def 3
           .= dom doms F by EXTENS_1:3;
      now
      let x be set;
      assume x in dom doms F;
    then A25: x in dom F by EXTENS_1:3;
      then reconsider j = x as Element of J by PBOOLE:def 3;

        (doms F).x = dom(F.j) by A25,FUNCT_6:31
                  .= K.j by FUNCT_2:def 1;
      hence f.x in (doms F).x by A23;
    end;
    then f in product doms F by A24,CARD_3:18;
  then A26: f in dom(Frege F) by PBOOLE:def 3;

    then reconsider Ff = (Frege F).f as Function of J, the carrier of L
      by Th10;
    take z = Inf Ff;

    thus z in X by A26,Th13;

      now
      let j be Element of J;
    A27: j in J;
      then j in dom G by FUNCT_2:def 1;
    then A28: G.j in rng G by FUNCT_1:def 5;

        x is_<=_than rng G by A6,A7,YELLOW_0:def 10;
    then A29: x <= G.j by A28,LATTICE3:def 8;
        j in dom F by A27,PBOOLE:def 3;
      then (F.j).(f.j) = ((Frege F).f).j by A26,Th9;
      then G.j <= Ff.j by A23;
      hence x <= Ff.j by A29,ORDERS_1:26;
    end;
    hence x <= z by YELLOW_2:57;

      now
      let j be Element of J;
    A30: j in J;
      then j in dom H by FUNCT_2:def 1;
    then A31: H.j in rng H by FUNCT_1:def 5;

        y is_<=_than rng H by A10,A11,YELLOW_0:def 10;
    then A32: y <= H.j by A31,LATTICE3:def 8;
        j in dom F by A30,PBOOLE:def 3;
      then (F.j).(f.j) = ((Frege F).f).j by A26,Th9;
      then H.j <= Ff.j by A23;
      hence y <= Ff.j by A32,ORDERS_1:26;
    end;
    hence y <= z by YELLOW_2:57;
  end;
  hence X is directed by WAYBEL_0:def 1;
end;

theorem ::Theorem 2.7 (ii)
    L is continuous implies
    for S being CLSubFrame of L holds S is continuous LATTICE
proof
  assume
A1: L is continuous;
  reconsider L'= L as complete LATTICE;

  let S be CLSubFrame of L;
A2: S is complete LATTICE by YELLOW_2:32;

    for J, K for F being DoubleIndexedSet of K, S st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs Frege F
  proof
    let J, K;
    let F be DoubleIndexedSet of K, S such that
  A3: for j being Element of J holds rng(F.j) is directed;

      now
      let j be set;
      assume
    A4: j in J;
      then reconsider j'= j as Element of J;
    A5: F.j' is Function of K.j', the carrier of S;
      A6: the carrier of S c= the carrier of L by YELLOW_0:def 13;
         (J --> the carrier of L).j = the carrier of L by A4,FUNCOP_1:13;
      hence F.j is Function of K.j, (J --> the carrier of L).j by A5,A6,FUNCT_2
:9;
    end;
    then reconsider F'= F as DoubleIndexedSet of K, L by MSUALG_1:def 2;

      for j being Element of J holds rng(F'.j) is directed
    proof
      let j be Element of J;
        rng(F.j) is directed by A3;
      hence rng(F'.j) is directed by YELLOW_2:7;
    end;
  then A7: Inf Sups F' = Sup Infs Frege F' by A1,Lm8;

  A8: ex_inf_of (rng Sups F'),L' by YELLOW_0:17;

      now
      let x;
      assume x in rng Sups F;
      then consider j being Element of J such that
    A9: x = Sup(F.j) by Th14;
    A10: ex_sup_of rng(F.j),L' by YELLOW_0:17;
    A11: rng(F.j) is directed Subset of S by A3;
        x = sup rng(F.j) by A9,YELLOW_2:def 5
       .= sup rng(F'.j) by A10,A11,WAYBEL_0:7
       .= Sup(F'.j) by YELLOW_2:def 5;
      hence x in rng Sups F' by Th14;
    end;
  then A12: rng Sups F c= rng Sups F' by TARSKI:def 3;

      now
      let x;
      assume x in rng Sups F';
      then consider j being Element of J such that
    A13: x = Sup(F'.j) by Th14;
    A14: ex_sup_of rng(F.j),L' by YELLOW_0:17;
    A15: rng(F.j) is directed Subset of S by A3;
        x = sup rng(F'.j) by A13,YELLOW_2:def 5
       .= sup rng(F.j) by A14,A15,WAYBEL_0:7
       .= Sup(F.j) by YELLOW_2:def 5;
      hence x in rng Sups F by Th14;
    end;
    then rng Sups F' c= rng Sups F by TARSKI:def 3;
then A16: rng Sups F' = rng Sups F by A12,XBOOLE_0:def 10;
      ex_inf_of rng Sups F,L by YELLOW_0:17;
    then "/\"(rng Sups F,L) in the carrier of S by YELLOW_0:def 18;
    then inf rng Sups F' = inf rng Sups F by A8,A16,YELLOW_0:64;
  then A17: Inf Sups F' = inf rng Sups F by YELLOW_2:def 6;
  A18: ex_sup_of rng /\\(Frege F', L),L' by YELLOW_0:17;

  A19: rng Infs Frege F is non empty directed Subset of S by A2,A3,Th27;

      now
      let x;
      assume x in rng /\\(Frege F', L);
      then consider f being set such that
    A20: f in dom(Frege F') and
    A21: x = //\((Frege F').f, L) by Th13;
      reconsider f as Element of product doms F' by A20,Lm7;
        (Frege F).f is Function of J, the carrier of S by A20,Th10;
      then rng((Frege F).f) c= the carrier of S by RELSET_1:12;
    then A22: rng((Frege F).f) is Subset of S;
    A23: ex_inf_of rng((Frege F).f),L' by YELLOW_0:17;
then A24: "/\"(rng((Frege F).f), L) in the carrier of S by A22,YELLOW_0:def 18;
        x = "/\"(rng((Frege F').f), L) by A21,YELLOW_2:def 6
       .= "/\"(rng((Frege F).f), S) by A22,A23,A24,YELLOW_0:64
       .= //\((Frege F).f, S) by YELLOW_2:def 6;
      hence x in rng Infs Frege F by A20,Th13;
    end;
  then A25: rng /\\(Frege F', L) c= rng /\\(Frege F, S) by TARSKI:def 3;

      now
      let x;
      assume x in rng Infs Frege F;
      then consider f being set such that
    A26: f in dom(Frege F) and
    A27: x = //\((Frege F).f, S) by Th13;
      reconsider f as Function by A26,Th7;
        (Frege F).f is Function of J, the carrier of S by A26,Th10;
      then rng((Frege F).f) c= the carrier of S by RELSET_1:12;
    then A28: rng((Frege F).f) is Subset of S;
    A29: ex_inf_of rng((Frege F).f),L' by YELLOW_0:17;
then A30: "/\"(rng((Frege F).f), L) in the carrier of S by A28,YELLOW_0:def 18;
        x = "/\"(rng((Frege F).f), S) by A27,YELLOW_2:def 6
       .= "/\"(rng((Frege F').f), L) by A28,A29,A30,YELLOW_0:64
       .= //\((Frege F').f, L) by YELLOW_2:def 6;
      hence x in rng Infs Frege F' by A26,Th13;
    end;
    then rng Infs Frege F c= rng Infs Frege F' by TARSKI:def 3;
    then rng Infs Frege F' = rng Infs Frege F by A25,XBOOLE_0:def 10;
    then sup rng Infs Frege F' = sup rng Infs Frege F by A18,A19,WAYBEL_0:7;
    then Sup Infs Frege F' = sup rng Infs Frege F by YELLOW_2:def 5
                     .= Sup Infs Frege F by YELLOW_2:def 5;
    hence Inf Sups F = Sup Infs Frege F by A7,A17,YELLOW_2:def 6;
  end;
  hence S is continuous LATTICE by A2,Lm9;
end;

theorem Th29:
  for S being non empty Poset st ex g being map of L, S st
    g is infs-preserving onto
      holds
     S is complete LATTICE
proof
  let S be non empty Poset;
  given g being map of L, S such that
A1: g is infs-preserving and
A2: g is onto;

    for A being Subset of S holds ex_inf_of A,S
  proof
    let A be Subset of S;
    set Y = g"A;
      rng g = the carrier of S by A2,FUNCT_2:def 3;
  then A3: A = g.:Y by FUNCT_1:147;
  A4: ex_inf_of Y,L by YELLOW_0:17;
      g preserves_inf_of Y by A1,WAYBEL_0:def 32;
    hence thesis by A3,A4,WAYBEL_0:def 30;
  end;
  then S is complete (non empty Poset) by YELLOW_2:30;
  hence S is complete LATTICE;
end;

definition
  let J be set, y be set;
  redefine func J --> y;
  synonym J => y;
end;

definition
  let J be set, y be set;
  redefine func J --> y -> ManySortedSet of J;
  coherence
  proof
      dom (J --> y) = J by FUNCOP_1:19;
    hence thesis by PBOOLE:def 3;
  end;

  synonym J => y;
end;

definition
  let A, B, J be set, f be Function of A, B;
  redefine func J => f -> ManySortedFunction of (J --> A), (J --> B);
  coherence
  proof
    set JA = J --> A, JB = J --> B;

      for j being set st j in J holds (J => f).j is Function of JA.j, JB.j
    proof
      let j be set;
      assume j in J;
      then (J => f).j = f & JA.j = A & JB.j = B by FUNCOP_1:13;
      hence (J => f).j is Function of JA.j, JB.j;
    end;
    hence thesis by MSUALG_1:def 2;
  end;
end;

theorem Th30:
  for A, B being set
  for f being Function of A, B, g being Function of B, A st g*f = id A
    holds
   (J => g)**(J => f) = id (J --> A)
proof
  let A, B be set;
  let f be Function of A, B;
  let g be Function of B, A;
  assume
A1: g*f = id A;
  set F = (J => g)**(J => f);
    dom F = J by MSUALG_3:2;
  then reconsider F as ManySortedSet of J by PBOOLE:def 3;

A2:
  for j being set st j in J holds F.j = id ((J --> A).j)
  proof
    let j be set;
    assume
  A3: j in J;
      then (J => g).j = g & (J => f).j = f & (J --> A).j = A by FUNCOP_1:13;
    hence F.j = id ((J --> A).j) by A1,A3,MSUALG_3:2;
  end;

    now
    let j be set;
    assume j in J;
    then F.j = id ((J --> A).j) by A2;
    hence F.j is Function of (J --> A).j, (J --> A).j;
  end;
  then reconsider F as ManySortedFunction of (J --> A), (J --> A) by MSUALG_1:
def 2;

    for j being set st j in J holds F.j = id ((J --> A).j) by A2;
  hence (J => g)**(J => f) = id (J --> A) by MSUALG_3:def 1;
end;

theorem Th31:
  for J, A being non empty set, B being set, K being ManySortedSet of J
  for F being DoubleIndexedSet of K, A
  for f being Function of A, B
    holds
   (J => f)**F is DoubleIndexedSet of K, B
proof
  let J, A be non empty set;
  let B be set;
  let K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, A;
  let f be Function of A, B;
  set fF = (J => f)**F;

    dom fF = J by MSUALG_3:2;
  then reconsider fF as ManySortedSet of J by PBOOLE:def 3;

    for j being set st j in J holds fF.j is Function of K.j, (J --> B).j
  proof
    let j be set;
    assume
  A1: j in J;
    then reconsider j'= j as Element of J;
    reconsider Fj = F.j' as Function of K.j, A;
A2: (J --> B).j = B by A1,FUNCOP_1:13;
      fF.j = ((J => f).j)*(F.j) by A1,MSUALG_3:2
        .= f*Fj by FUNCOP_1:13;
    hence fF.j is Function of K.j, (J --> B).j by A2;
  end;
  hence (J --> f)**F is DoubleIndexedSet of K, B by MSUALG_1:def 2;
end;

theorem Th32:
  for J, A, B being non empty set, K being ManySortedSet of J
  for F being DoubleIndexedSet of K, A
  for f being Function of A, B
    holds
   doms((J => f)**F) = doms F
proof
  let J, A, B be non empty set;
  let K be ManySortedSet of J;
  let F be DoubleIndexedSet of K, A;
  let f be Function of A, B;

A1:
  dom doms((J => f)**F) = dom((J => f)**F) by EXTENS_1:3
                        .= J by MSUALG_3:2;
A2:
  dom doms F = dom F by EXTENS_1:3
            .= J by PBOOLE:def 3;

    now
    let x be set;
    assume
  A3: x in J;
    then reconsider j = x as Element of J;

  A4: rng(F.j) c= A & dom f = A by FUNCT_2:def 1,RELSET_1:12;
  A5: j in dom F by A3,PBOOLE:def 3;
      j in dom((J => f)**F) by A1,A3,EXTENS_1:3;
    then (doms((J => f)**F)).j = dom(((J => f)**F).j) by FUNCT_6:31
                          .= dom(((J => f).j)*(F.j)) by MSUALG_3:2
                          .= dom(f*(F.j)) by FUNCOP_1:13
                          .= dom(F.j) by A4,RELAT_1:46
                          .= (doms F).j by A5,FUNCT_6:31;
    hence (doms((J => f)**F)).x = (doms F).x;
  end;
  hence thesis by A1,A2,FUNCT_1:9;
end;

theorem ::Theorem 2.7 (iii)
    L is continuous implies
    for S being non empty Poset st ex g being map of L, S st
      g is infs-preserving directed-sups-preserving & g is onto
        holds
       S is continuous LATTICE
proof
  assume
A1: L is continuous;
  let S be non empty Poset;
  given g being map of L, S such that
A2: g is infs-preserving directed-sups-preserving and
A3: g is onto;

  reconsider S'= S as complete LATTICE by A2,A3,Th29;

    for J, K for F being DoubleIndexedSet of K, S' st
    for j being Element of J holds rng(F.j) is directed
      holds Inf Sups F = Sup Infs(Frege F)
  proof
    let J, K;
    let F be DoubleIndexedSet of K, S' such that
  A4: for j being Element of J holds rng(F.j) is directed;

    consider d being map of S, L such that
  A5: [g, d] is Galois and
        for t being Element of S holds d.t is_minimum_of g"(uparrow t)
      by A2,WAYBEL_1:15;

      for t being Element of S holds d.t is_minimum_of g"{t}
      by A3,A5,WAYBEL_1:23;
    then g*d = id S by WAYBEL_1:24;
  then A6: g*d = id the carrier of S by GRCAT_1:def 11;
  A7: d is monotone by A5,WAYBEL_1:9;
    reconsider dF = (J => d)**F as DoubleIndexedSet of K, L by Th31;
  A8: for j being Element of J holds rng(dF.j) is directed
    proof
      let j be Element of J;
        (J => d).j = d by FUNCOP_1:13;
    then A9: rng(dF.j) = rng(d*(F.j)) by MSUALG_3:2
                 .= d.:(rng(F.j)) by RELAT_1:160;

        rng(F.j) is directed by A4;
      hence rng(dF.j) is directed by A7,A9,YELLOW_2:17;
    end;
    reconsider gdF = (J => g)**dF as DoubleIndexedSet of K, S;

  A10:
    F = (id (J --> the carrier of S))**F by MSUALG_3:4
     .= ((J --> g)**(J --> d))**F by A6,Th30
     .= gdF by AUTALG_1:13;

  A11: rng Sups gdF c= g.:(rng Sups dF)
    proof
      let y be set;
      assume y in rng Sups gdF;
      then consider j being Element of J such that
    A12: y = Sup(gdF.j) by Th14;
        gdF.j = ((J => g).j)*(dF.j) by MSUALG_3:2
           .= g*(dF.j) by FUNCOP_1:13;
      then rng(gdF.j) = g.:(rng(dF.j)) by RELAT_1:160;
    then A13: y = sup(g.:(rng(dF.j))) by A12,YELLOW_2:def 5;

        rng(dF.j) is directed by A8;
    then A14: g preserves_sup_of rng(dF.j) by A2,WAYBEL_0:def 37;
        ex_sup_of rng(dF.j),L by YELLOW_0:17;
      then sup(g.:(rng(dF.j))) = g.sup(rng(dF.j)) by A14,WAYBEL_0:def 31;
    then A15: y = g.Sup(dF.j) by A13,YELLOW_2:def 5;

        Sup(dF.j) in the carrier of L & Sup(dF.j) in rng Sups dF by Th14;
      hence y in g.:(rng Sups dF) by A15,FUNCT_2:43;
    end;

  A16: g.:(rng Sups dF) c= rng Sups gdF
    proof
      let y be set;
      assume y in g.:(rng Sups dF);
      then consider x being set such that
          x in the carrier of L and
    A17: x in rng Sups dF and
    A18: y = g.x by FUNCT_2:115;
      consider j being Element of J such that
    A19: x = Sup(dF.j) by A17,Th14;
        rng(dF.j) is directed by A8;
    then A20: g preserves_sup_of rng(dF.j) by A2,WAYBEL_0:def 37;
        ex_sup_of rng(dF.j),L by YELLOW_0:17;
      then sup(g.:(rng(dF.j))) = g.sup(rng(dF.j)) by A20,WAYBEL_0:def 31;
    then A21: y = sup(g.:(rng(dF.j))) by A18,A19,YELLOW_2:def 5;
        gdF.j = ((J => g).j)*(dF.j) by MSUALG_3:2
           .= g*(dF.j) by FUNCOP_1:13;
      then rng(gdF.j) = g.:(rng(dF.j)) by RELAT_1:160;
      then y = Sup(gdF.j) by A21,YELLOW_2:def 5;
      hence y in rng Sups gdF by Th14;
    end;
  A22: ex_inf_of (rng Sups dF),L by YELLOW_0:17;
  A23: g preserves_inf_of (rng Sups dF) by A2,WAYBEL_0:def 32;

      rng Infs Frege dF is directed non empty by A8,Th27;
  then A24: g preserves_sup_of rng Infs Frege dF by A2,WAYBEL_0:def 37;
  A25: ex_sup_of rng Infs Frege dF,L by YELLOW_0:17;
  A26: for f being set st f in dom(Frege dF) holds
      rng((Frege F).f) = g.:(rng((Frege dF).f))
    proof
      let f be set;
      assume
    A27: f in dom(Frege dF);
      then reconsider f as Element of product doms dF by PBOOLE:def 3;
    A28: dom(Frege dF) = product(doms dF) by PBOOLE:def 3
                     .= product(doms F) by Th32
                     .= dom(Frege F) by PBOOLE:def 3;
    A29: dom((Frege dF).f) = dom dF by A27,Th8
                         .= J by PBOOLE:def 3;
    A30: dom((Frege F).f) = dom F by A27,A28,Th8
                        .= J by PBOOLE:def 3;
        dom g = the carrier of L by FUNCT_2:def 1;
      then rng((Frege dF).f) c= dom g;
    then A31: dom(g*((Frege dF).f)) = dom((Frege dF).f) by RELAT_1:46;

        now
        let i be set;
        assume
      A32: i in J;
        then reconsider j = i as Element of J;
      A33: j in dom dF by A32,PBOOLE:def 3;
        then f.j in dom(dF.j) by A27,Th9;
          then f.j in dom(((J => d).j)*(F.j)) by MSUALG_3:2;
      then A34: f.j in dom(d*(F.j)) by FUNCOP_1:13;
      A35: j in dom F by A32,PBOOLE:def 3;
          (g*((Frege dF).f)).j = g.(((Frege dF).f).j) by A29,FUNCT_1:23
                            .= g.((dF.j).(f.j)) by A27,A33,Th9
                            .= g.((((J => d).j)*(F.j)).(f.j)) by MSUALG_3:2
                            .= g.((d*(F.j)).(f.j)) by FUNCOP_1:13
                            .= (g*(d*(F.j))).(f.j) by A34,FUNCT_1:23
                            .= ((id the carrier of S)*(F.j)).(f.j) by A6,
RELAT_1:55
                            .= (F.j).(f.j) by FUNCT_2:23
                            .= ((Frege F).f).j by A27,A28,A35,Th9;
        hence (g*((Frege dF).f)).i = ((Frege F).f).i;
      end;
      then rng((Frege F).f) = rng(g*((Frege dF).f)) by A29,A30,A31,FUNCT_1:9
                .= g.:(rng((Frege dF).f)) by RELAT_1:160;
      hence thesis;
    end;


  A36: g.:(rng Infs Frege dF) c= rng Infs Frege F
    proof
      let y be set;
      assume y in g.:(rng Infs Frege dF);
      then consider x being set such that
          x in the carrier of L and
    A37: x in rng Infs Frege dF and
    A38: y = g.x by FUNCT_2:115;
      consider f being set such that
    A39: f in dom(Frege dF) and
    A40: x = //\((Frege dF).f, L) by A37,Th13;

      reconsider f as Element of product doms dF by A39,PBOOLE:def 3;
      reconsider f'= f as Element of product doms F by Th32;
      set X = rng((Frege dF).f);

    A41: g preserves_inf_of X by A2,WAYBEL_0:def 32;
        ex_inf_of X,L by YELLOW_0:17;
      then inf(g.:X) = g.inf X by A41,WAYBEL_0:def 30;
    then A42: y = inf(g.:X) by A38,A40,YELLOW_2:def 6;

    A43: dom(Frege dF) = product(doms dF) by PBOOLE:def 3
                     .= product(doms F) by Th32
                     .= dom(Frege F) by PBOOLE:def 3;

        rng((Frege F).f) = g.:(rng((Frege dF).f)) by A26,A39;
      then y = Inf((Frege F).f') by A42,YELLOW_2:def 6;
      hence y in rng Infs Frege F by A39,A43,Th13;
    end;

   A44: rng Infs Frege F c= g.:(rng Infs Frege dF)
    proof
      let y be set;
      assume y in rng Infs Frege F;
      then consider f being set such that
    A45: f in dom(Frege F) and
    A46: y = //\((Frege F).f, S) by Th13;

      reconsider f as Element of product doms F by A45,PBOOLE:def 3;
      reconsider f'= f as Element of product doms dF by Th32;


    A47: dom(Frege dF) = product(doms dF) by PBOOLE:def 3
                     .= product(doms F) by Th32
                     .= dom(Frege F) by PBOOLE:def 3;
      then rng((Frege F).f) = g.:(rng((Frege dF).f)) by A26,A45;
    then A48: y = "/\"(g.:(rng((Frege dF).f)), S) by A46,YELLOW_2:def 6;

      set X = rng((Frege dF).f');

    A49: g preserves_inf_of X by A2,WAYBEL_0:def 32;
        ex_inf_of X,L by YELLOW_0:17;
    then A50: y = g.inf X by A48,A49,WAYBEL_0:def 30
          .= g.Inf((Frege dF).f') by YELLOW_2:def 6;
        Inf((Frege dF).f') in rng Infs Frege dF by A45,A47,Th13;
      hence y in g.:(rng Infs Frege dF) by A50,FUNCT_2:43;
    end;
      Inf Sups F = inf rng Sups gdF by A10,YELLOW_2:def 6
              .= inf (g.:(rng Sups dF)) by A11,A16,XBOOLE_0:def 10
              .= g.(inf rng Sups dF) by A22,A23,WAYBEL_0:def 30
              .= g.(Inf Sups dF) by YELLOW_2:def 6
              .= g.(Sup Infs Frege dF) by A1,A8,Lm8
              .= g.(sup rng Infs Frege dF) by YELLOW_2:def 5
              .= sup(g.:(rng Infs Frege dF)) by A24,A25,WAYBEL_0:def 31
              .= sup rng Infs Frege F by A36,A44,XBOOLE_0:def 10
              .= Sup Infs Frege F by YELLOW_2:def 5;
    hence thesis;
  end;
  hence S is continuous LATTICE by Lm9;
end;


Back to top