:: Duality Based on Galois Connection. Part I
::  by Grzegorz Bancerek
::
:: Received August 8, 2001
:: Copyright (c) 2001-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies REWRITE1, WAYBEL_0, WAYBEL_1, FUNCT_1, XBOOLE_0, ORDERS_2,
      SEQM_3, SUBSET_1, XXREAL_0, RELAT_1, LATTICES, EQREL_1, ORDINAL2,
      STRUCT_0, ARYTM_0, ALTCAT_1, CAT_1, ZFMISC_1, YELLOW21, FILTER_0,
      WELLORD1, ORDERS_1, SETFAM_1, QC_LANG1, TARSKI, FUNCTOR0, FUNCT_2,
      WAYBEL11, YELLOW_9, RCOMP_1, CARD_FIL, YELLOW_0, RELAT_2, WAYBEL_3,
      LATTICE3, PRE_TOPC, GROUP_6, ALTCAT_2, FUNCOP_1, YELLOW20, YELLOW18,
      WAYBEL_8, FINSET_1, WAYBEL34;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, ORDERS_1, DOMAIN_1,
      FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, WELLORD1, ALTCAT_1, FUNCTOR0,
      ALTCAT_2, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, PRE_TOPC, T_0TOPSP,
      WAYBEL_3, WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18,
      YELLOW20, YELLOW21;
 constructors WELLORD1, BORSUK_1, T_0TOPSP, WAYBEL_8, WAYBEL11, YELLOW_9,
      WAYBEL18, YELLOW18, YELLOW20, YELLOW21, WAYBEL20;
 registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, FUNCT_2, FINSET_1,
      STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0,
      WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_8,
      WAYBEL10, WAYBEL11, FUNCTOR2, ALTCAT_4, LATTICE5, WAYBEL17, YELLOW_9,
      WAYBEL21, YELLOW18, YELLOW21, RELAT_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, PRE_TOPC, T_0TOPSP, LATTICE3, YELLOW_0, WAYBEL_0,
      WAYBEL_1, WAYBEL_3, WAYBEL11, FUNCTOR0, YELLOW21, XBOOLE_0;
 equalities SUBSET_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW21,
      BINOP_1, STRUCT_0, RELAT_1;
 expansions TARSKI, PRE_TOPC, T_0TOPSP, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3,
      WAYBEL11, XBOOLE_0;
 theorems ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, ORDERS_2, ORDERS_3,
      TSEP_1, TARSKI, FUNCOP_1, ALTCAT_1, ALTCAT_2, ALTCAT_4, FUNCTOR0,
      FUNCTOR1, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL_6,
      YELLOW_7, WAYBEL_8, YELLOW_3, WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL15,
      WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL21, YELLOW18, YELLOW20, YELLOW21,
      XBOOLE_0, XBOOLE_1, SETFAM_1, PARTFUN1;
 schemes FINSET_1, YELLOW18, YELLOW20, YELLOW21;

begin

::<section1>Infs-preserving and sups-preserving maps</section1>

registration
  let S,T be complete LATTICE;
  cluster Galois for Connection of S,T;
  existence
  proof set g = the infs-preserving Function of S,T;
    g is upper_adjoint by WAYBEL_1:16;
    then ex d being Function of T,S st [g,d] is Galois;
    hence thesis;
  end;
end;

theorem Th1:
  for S,T, S9,T9 being non empty RelStr
  st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9
  for c being Connection of S,T, c9 being Connection of S9,T9 st c = c9
  holds c is Galois implies c9 is Galois
proof
  let S,T, S9,T9 being non empty RelStr such that
A1: the RelStr of S = the RelStr of S9 and
A2: the RelStr of T = the RelStr of T9;
  let c be Connection of S,T, c9 be Connection of S9,T9 such that
A3: c = c9;
  given g being Function of S,T, d being Function of T,S such that
A4: c = [g,d] and
A5: g is monotone and
A6: d is monotone and
A7: for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s;
  reconsider g9 = g as Function of S9, T9 by A1,A2;
  reconsider d9 = d as Function of T9, S9 by A1,A2;
  take g9,d9;
  thus c9 = [g9,d9] by A3,A4;
  thus g9 is monotone & d9 is monotone by A1,A2,A5,A6,WAYBEL_9:1;
  let t9 be Element of T9, s9 be Element of S9;
  reconsider t = t9 as Element of T by A2;
  reconsider s = s9 as Element of S by A1;
A8: t9 <= g9.s9 iff t <= g.s by A2,YELLOW_0:1;
  d9.t9 <= s9 iff d.t <= s by A1,YELLOW_0:1;
  hence thesis by A7,A8;
end;

definition
  let S,T be LATTICE;
  let g be Function of S,T;
  assume that
A1: S is complete and
A2: g is infs-preserving;
A3: g is upper_adjoint by A1,A2,WAYBEL_1:16;
  func LowerAdj g -> Function of T,S means
  : Def1:
  [g, it] is Galois;
  uniqueness
  proof
    let d1,d2 be Function of T,S such that
A4: [g, d1] is Galois and
A5: [g, d2] is Galois;
    now
      let t be Element of T;
      reconsider t9 = t as Element of T;
A6:   d1.t9 is_minimum_of g"(uparrow t) by A4,WAYBEL_1:10;
A7:   d2.t9 is_minimum_of g"(uparrow t ) by A5,WAYBEL_1:10;
      d1.t = "/\"(g"(uparrow t), S) by A6;
      hence d1.t = d2.t by A7;
    end;
    hence thesis by FUNCT_2:63;
  end;
  existence by A3;
end;

definition
  let S,T be LATTICE;
  let d be Function of T,S;
  assume that
A1: T is complete and
A2: d is sups-preserving;
A3: d is lower_adjoint by A1,A2,WAYBEL_1:17;
  func UpperAdj d -> Function of S,T means
  : Def2:
  [it, d] is Galois;
  existence by A3;
  correctness
  proof
    let g1,g2 be Function of S,T such that
A4: [g1, d] is Galois and
A5: [g2, d] is Galois;
    now
      let t be Element of S;
      reconsider t9 = t as Element of S;
A6:   g1.t9 is_maximum_of d"(downarrow t) by A4,WAYBEL_1:11;
A7:   g2.t9 is_maximum_of d"(downarrow t) by A5,WAYBEL_1:11;
      g1.t = "\/"(d"(downarrow t), T) by A6;
      hence g1.t = g2.t by A7;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

Lm1: now
  let S,T be LATTICE;
  assume that
A1: S is complete and
A2: T is complete;
  reconsider S9 = S, T9 = T as complete LATTICE by A1,A2;
  let g be Function of S,T;
  assume g is infs-preserving;
  then reconsider g9 = g as infs-preserving Function of S9, T9;
  [g9, LowerAdj g9] is Galois by Def1;
  then LowerAdj g9 is lower_adjoint monotone by WAYBEL_1:8;
  hence LowerAdj g is monotone lower_adjoint sups-preserving;
end;

Lm2: now
  let S,T be LATTICE;
  assume that
A1: S is complete and
A2: T is complete;
  reconsider S9 = S, T9 = T as complete LATTICE by A1,A2;
  let g be Function of S,T;
  assume g is sups-preserving;
  then reconsider g9 = g as sups-preserving Function of S9, T9;
  [UpperAdj g9, g9] is Galois by Def2;
  then UpperAdj g9 is upper_adjoint monotone by WAYBEL_1:8;
  hence UpperAdj g is monotone upper_adjoint infs-preserving;
end;

registration
  let S,T be complete LATTICE;
  let g be infs-preserving Function of S,T;
  cluster LowerAdj g -> lower_adjoint;  :: sups-preserving
  coherence by Lm1;
end;

registration
  let S,T be complete LATTICE;
  let d be sups-preserving Function of T,S;
  cluster UpperAdj d -> upper_adjoint;  :: infs-preserving
  coherence by Lm2;
end;

theorem
  for S,T being complete LATTICE for g being infs-preserving Function of S,T
  for t being Element of T holds (LowerAdj g).t = inf (g"uparrow t)
proof
  let S,T be complete LATTICE;
  let g be infs-preserving Function of S,T;
  let t be Element of T;
  [g, LowerAdj g] is Galois by Def1;
  then (LowerAdj g).t is_minimum_of g"(uparrow t) by WAYBEL_1:10;
  hence thesis;
end;

theorem
  for S,T being complete LATTICE for d being sups-preserving Function of T,S
  for s being Element of S holds (UpperAdj d).s = sup (d"downarrow s)
proof
  let S,T be complete LATTICE;
  let d be sups-preserving Function of T,S;
  let s be Element of S;
  [UpperAdj d, d] is Galois by Def2;
  then (UpperAdj d).s is_maximum_of d"(downarrow s) by WAYBEL_1:11;
  hence thesis;
end;

definition
  let S,T be RelStr;
  let f be Function of the carrier of S, the carrier of T;
  func f opp -> Function of S opp, T opp equals
  f;
  coherence;
end;

registration
  let S,T be complete LATTICE;
  let g be infs-preserving Function of S,T;
  cluster g opp -> lower_adjoint;
  coherence
  proof
    [g, LowerAdj g] is Galois by Def1;
    then [(LowerAdj g) opp, g opp] is Galois by YELLOW_7:44;
    hence thesis;
  end;
end;

registration
  let S,T be complete LATTICE;
  let d be sups-preserving Function of S,T;
  cluster d opp -> upper_adjoint;
  coherence
  proof
    [UpperAdj d, d] is Galois by Def2;
    then [d opp, (UpperAdj d) opp] is Galois by YELLOW_7:44;
    hence thesis;
  end;
end;

theorem
  for S,T being complete LATTICE for g being infs-preserving Function of S, T
  holds LowerAdj g = UpperAdj (g opp)
proof
  let S,T be complete LATTICE;
  let g be infs-preserving Function of S, T;
  [g, LowerAdj g] is Galois by Def1;
  then [(LowerAdj g) opp, g opp] is Galois by YELLOW_7:44;
  hence thesis by Def2;
end;

theorem
  for S,T being complete LATTICE for d being sups-preserving Function of S, T
  holds LowerAdj (d opp) = UpperAdj d
proof
  let S,T be complete LATTICE;
  let d be sups-preserving Function of S, T;
  [UpperAdj d, d] is Galois by Def2;
  then [d opp, (UpperAdj d) opp] is Galois by YELLOW_7:44;
  hence thesis by Def1;
end;

theorem Th6:
  for L be non empty RelStr holds [id L, id L] is Galois
proof
  let L be non empty RelStr;
  take g = id L, d = id L;
  thus [id L, id L] = [g,d] & g is monotone & d is monotone;
  let t,s be Element of L;
  g.s = s by FUNCT_1:18;
  hence thesis by FUNCT_1:18;
end;

theorem Th7: :: 1.2.  LEMMA, p. 179
:: LowerAdj and UpperAdj preserve identities
  for L being complete LATTICE holds
  LowerAdj id L = id L & UpperAdj id L = id L
proof
  let L be complete LATTICE;
  [id L, id L] is Galois by Th6;
  hence thesis by Def1,Def2;
end;

theorem Th8: :: 1.2.  LEMMA, p. 179
:: LowerAdj preserves contravariantly composition
  for L1,L2,L3 being complete LATTICE
  for g1 being infs-preserving Function of L1,L2
  for g2 being infs-preserving Function of L2,L3 holds
  LowerAdj (g2*g1) = (LowerAdj g1)*(LowerAdj g2)
proof
  let L1,L2,L3 be complete LATTICE;
  let g1 be infs-preserving Function of L1,L2;
  let g2 be infs-preserving Function of L2,L3;
A1: [g1, LowerAdj g1] is Galois by Def1;
  [g2, LowerAdj g2] is Galois by Def1;
  then
A2: [g2*g1, (LowerAdj g1)*(LowerAdj g2)] is Galois by A1,WAYBEL15:5;
  g2*g1 is infs-preserving by WAYBEL20:25;
  hence thesis by A2,Def1;
end;

theorem Th9: :: 1.2.  LEMMA, p. 179
:: UpperAdj preserves contravariantly composition
  for L1,L2,L3 being complete LATTICE
  for d1 being sups-preserving Function of L1,L2
  for d2 being sups-preserving Function of L2,L3 holds
  UpperAdj (d2*d1) = (UpperAdj d1)*(UpperAdj d2)
proof
  let L1,L2,L3 be complete LATTICE;
  let d1 be sups-preserving Function of L1,L2;
  let d2 be sups-preserving Function of L2,L3;
A1: [UpperAdj d1, d1] is Galois by Def2;
  [UpperAdj d2, d2] is Galois by Def2;
  then
A2: [(UpperAdj d1)*(UpperAdj d2), d2*d1] is Galois by A1,WAYBEL15:5;
  d2*d1 is sups-preserving by WAYBEL20:27;
  hence thesis by A2,Def2;
end;

theorem Th10: :: 1.3. THEOREM, p. 179
  for S,T being complete LATTICE for g being infs-preserving Function of S,T
  holds UpperAdj LowerAdj g = g
proof
  let S,T be complete LATTICE;
  let g be infs-preserving Function of S,T;
  [g, LowerAdj g] is Galois by Def1;
  hence thesis by Def2;
end;

theorem Th11: :: 1.3. THEOREM, p. 179
  for S,T being complete LATTICE for d being sups-preserving Function of S,T
  holds LowerAdj UpperAdj d = d
proof
  let S,T be complete LATTICE;
  let d be sups-preserving Function of S,T;
  [UpperAdj d, d] is Galois by Def2;
  hence thesis by Def1;
end;

theorem Th12:
  for C being non empty AltCatStr
  for a,b,f being object st f in (the Arrows of C).(a,b)
  ex o1,o2 being Object of C
  st o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2
proof
  let C be non empty AltCatStr;
  let a,b,f be object;
  assume
A1: f in (the Arrows of C).(a,b);
  then [a,b] in dom the Arrows of C by FUNCT_1:def 2;
  then [a,b] in [:the carrier of C, the carrier of C:];
  then reconsider o1 = a, o2 = b as Object of C by ZFMISC_1:87;
  take o1, o2;
  thus thesis by A1,ALTCAT_1:def 1;
end;

definition :: 1.1 DEFINITION, p. 179
  let W be non empty set;
  defpred L[LATTICE] means $1 is complete;
  defpred P[LATTICE,LATTICE,Function of $1,$2] means $3 is infs-preserving;
  given w being Element of W such that
A1: w is non empty;
  func W-INF_category -> lattice-wise strict category means
  :
  Def4: (for x being LATTICE holds
  x is Object of it iff x is strict complete & the carrier of x in W) &
  for a,b being Object of it, f being monotone Function of latt a, latt b
  holds f in <^a,b^> iff f is infs-preserving;
  existence
  proof
    reconsider w as non empty set by A1;
    set r = the upper-bounded well-ordering Order of w;
    RelStr(#w,r#) is complete;
    then
A2: ex x being strict LATTICE st L[x] & the carrier of x in W;
A3: for a,b,c being LATTICE st L[a] & L[b] & L[c]
    for f being Function of a,b, g being Function
    of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by WAYBEL20:25;
A4: for a being LATTICE st L[a] holds P[a,a,id a];
    thus
    ex C being lattice-wise strict category st (for x being LATTICE holds
    x is Object of C iff x is strict & L[x] & the carrier of x in W) &
    for a,b being Object of C, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff P[latt a, latt b, f] from YELLOW21:sch 3(A2,A3,
    A4);
  end;
  uniqueness
  proof
    let C1, C2 be lattice-wise strict category such that
A5: for x being LATTICE holds
    x is Object of C1 iff x is strict & L[x] & the carrier of x in W and
A6: for a,b being Object of C1, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff f is infs-preserving and
A7: for x being LATTICE holds
    x is Object of C2 iff x is strict & L[x] & the carrier of x in W and
A8: for a,b being Object of C2, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff f is infs-preserving;
    defpred Q[set, set, set] means
    ex L1,L2 being LATTICE, f being Function of L1,L2
    st $1 = L1 & $2 = L2 & $3 = f & f is infs-preserving;
A9: now
      let a,b be Object of C1;
      let f be monotone Function of latt a, latt b;
      f in <^a,b^> iff f is infs-preserving by A6;
      hence f in <^a,b^> iff Q[a,b,f];
    end;
A10: now
      let a,b be Object of C2;
      let f be monotone Function of latt a, latt b;
      f in <^a,b^> iff f is infs-preserving by A8;
      hence f in <^a,b^> iff Q[a,b,f];
    end;
    for C1, C2 being lattice-wise category st (for x being LATTICE holds
    x is Object of C1 iff x is strict & L[x] & the carrier of x in W) &
    (for a,b being Object of C1, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff Q[a, b, f]) & (for x being LATTICE holds
    x is Object of C2 iff x is strict & L[x] & the carrier of x in W) &
    (for a,b being Object of C2, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff Q[a, b, f])
    holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW21:sch 5;
    hence thesis by A5,A7,A9,A10;
  end;
end;

Lm3: for W being with_non-empty_element set
for a,b being LATTICE, f being Function of a,b
holds f in (the Arrows of W-INF_category).(a,b) iff
a in the carrier of W-INF_category & b in the carrier of W-INF_category &
a is complete & b is complete & f is infs-preserving
proof
  let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
  let a,b be LATTICE, f be Function of a,b;
  set A = W-INF_category;
  hereby
    assume f in (the Arrows of A).(a,b);
    then consider o1, o2 being Object of A such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and f is Morphism of o1, o2 by Th12;
    reconsider g = f as Morphism of o1,o2 by A4;
    thus a in the carrier of A & b in the carrier of A by A2,A3;
    thus a is complete & b is complete by A1,A2,A3,Def4;
    @g = f by A4,YELLOW21:def 7;
    hence f is infs-preserving by A1,A2,A3,A4,Def4;
  end;
  assume that
A5: a in the carrier of W-INF_category and
A6: b in the carrier of W-INF_category;
  reconsider x = a, y = b as Object of A by A5,A6;
A7: latt x = a;
A8: latt y = b;
  assume that
  a is complete and b is complete and
A9: f is infs-preserving;
  f in <^x,y^> by A1,A7,A8,A9,Def4;
  hence thesis by ALTCAT_1:def 1;
end;

definition :: 1.1 DEFINITION, p. 179
  let W be non empty set;
  defpred L[LATTICE] means $1 is complete;
  defpred P[LATTICE,LATTICE,Function of $1,$2] means $3 is sups-preserving;
  given w being Element of W such that
A1: w is non empty;
  func W-SUP_category -> lattice-wise strict category means
  :
  Def5: (for x being LATTICE holds
  x is Object of it iff x is strict complete & the carrier of x in W) &
  for a,b being Object of it, f being monotone Function of latt a, latt b
  holds f in <^a,b^> iff f is sups-preserving;
  existence
  proof
    reconsider w as non empty set by A1;
    set r = the upper-bounded well-ordering Order of w;
    RelStr(#w,r#) is complete;
    then
A2: ex x being strict LATTICE st L[x] & the carrier of x in W;
A3: for a,b,c being LATTICE st L[a] & L[b] & L[c]
    for f being Function of a,b, g being Function
    of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by WAYBEL20:27;
A4: for a being LATTICE st L[a] holds P[a,a,id a];
    thus
    ex C being lattice-wise strict category st (for x being LATTICE holds
    x is Object of C iff x is strict & L[x] & the carrier of x in W) &
    for a,b being Object of C, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff P[latt a, latt b, f] from YELLOW21:sch 3
    (A2,A3,A4);
  end;
  uniqueness
  proof
    let C1, C2 be lattice-wise strict category such that
A5: for x being LATTICE holds
    x is Object of C1 iff x is strict & L[x] & the carrier of x in W and
A6: for a,b being Object of C1, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff f is sups-preserving and
A7: for x being LATTICE holds
    x is Object of C2 iff x is strict & L[x] & the carrier of x in W and
A8: for a,b being Object of C2, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff f is sups-preserving;
    defpred Q[set, set, set] means
    ex L1,L2 being LATTICE, f being Function of L1,L2
    st $1 = L1 & $2 = L2 & $3 = f & f is sups-preserving;
A9: now
      let a,b be Object of C1;
      let f be monotone Function of latt a, latt b;
      f in <^a,b^> iff f is sups-preserving by A6;
      hence f in <^a,b^> iff Q[a,b,f];
    end;
A10: now
      let a,b be Object of C2;
      let f be monotone Function of latt a, latt b;
      f in <^a,b^> iff f is sups-preserving by A8;
      hence f in <^a,b^> iff Q[a,b,f];
    end;
    for C1, C2 being lattice-wise category st (for x being LATTICE holds
    x is Object of C1 iff x is strict & L[x] & the carrier of x in W) &
    (for a,b being Object of C1, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff Q[a, b, f]) & (for x being LATTICE holds
    x is Object of C2 iff x is strict & L[x] & the carrier of x in W) &
    (for a,b being Object of C2, f being monotone Function of latt a, latt b
    holds f in <^a,b^> iff Q[a, b, f])
    holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW21:sch 5;
    hence thesis by A5,A7,A9,A10;
  end;
end;

Lm4: for W being with_non-empty_element set
for a,b being LATTICE, f being Function of a,b
holds f in (the Arrows of W-SUP_category).(a,b) iff
a in the carrier of W-SUP_category & b in the carrier of W-SUP_category &
a is complete & b is complete & f is sups-preserving
proof
  let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
  let a,b be LATTICE, f be Function of a,b;
  set A = W-SUP_category;
  hereby
    assume f in (the Arrows of A).(a,b);
    then consider o1, o2 being Object of A such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and f is Morphism of o1, o2 by Th12;
    reconsider g = f as Morphism of o1,o2 by A4;
    thus a in the carrier of A & b in the carrier of A by A2,A3;
    thus a is complete & b is complete by A1,A2,A3,Def5;
    @g = f by A4,YELLOW21:def 7;
    hence f is sups-preserving by A1,A2,A3,A4,Def5;
  end;
  assume that
A5: a in the carrier of W-SUP_category and
A6: b in the carrier of W-SUP_category;
  reconsider x = a, y = b as Object of A by A5,A6;
A7: latt x = a;
A8: latt y = b;
  assume that
  a is complete and b is complete and
A9: f is sups-preserving;
  f in <^x,y^> by A1,A7,A8,A9,Def5;
  hence thesis by ALTCAT_1:def 1;
end;

registration
  let W be with_non-empty_element set;
  cluster W-INF_category -> with_complete_lattices;
  coherence
  proof
    thus W-INF_category is lattice-wise;
    let a be Object of W-INF_category;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
    a = latt a;
    hence thesis by A1,Def4;
  end;
  cluster W-SUP_category -> with_complete_lattices;
  coherence
  proof
    thus W-SUP_category is lattice-wise;
    let a be Object of W-SUP_category;
A2: ex x being non empty set st x in W by SETFAM_1:def 10;
    a = latt a;
    hence thesis by A2,Def5;
  end;
end;

theorem Th13:
  for W being with_non-empty_element set for L being LATTICE holds
  L is Object of W-INF_category iff
  L is strict complete & the carrier of L in W
proof
  let W be with_non-empty_element set;
  ex a being non empty set st a in W by SETFAM_1:def 10;
  hence thesis by Def4;
end;

theorem Th14:
  for W being with_non-empty_element set
  for a, b being Object of W-INF_category for f being set
  holds f in <^a,b^> iff f is infs-preserving Function of latt a, latt b
proof
  let W be with_non-empty_element set;
  let a,b be Object of W-INF_category, f be set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
  hereby
    assume
A2: f in <^a,b^>;
    then reconsider g = f as Morphism of a,b;
    f = @g by A2,YELLOW21:def 7;
    hence f is infs-preserving Function of latt a, latt b by A1,A2,Def4;
  end;
  thus thesis by A1,Def4;
end;

theorem Th15:
  for W being with_non-empty_element set for L being LATTICE holds
  L is Object of W-SUP_category iff
  L is strict complete & the carrier of L in W
proof
  let W be with_non-empty_element set;
  ex a being non empty set st a in W by SETFAM_1:def 10;
  hence thesis by Def5;
end;

theorem Th16:
  for W being with_non-empty_element set
  for a, b being Object of W-SUP_category for f being set
  holds f in <^a,b^> iff f is sups-preserving Function of latt a, latt b
proof
  let W be with_non-empty_element set;
  let a,b be Object of W-SUP_category, f be set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
  hereby
    assume
A2: f in <^a,b^>;
    then reconsider g = f as Morphism of a,b;
    f = @g by A2,YELLOW21:def 7;
    hence f is sups-preserving Function of latt a, latt b by A1,A2,Def5;
  end;
  thus thesis by A1,Def5;
end;

theorem Th17:
  for W being with_non-empty_element set holds
  the carrier of W-INF_category = the carrier of W-SUP_category
proof
  let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
  thus the carrier of W-INF_category c= the carrier of W-SUP_category
  proof
    let x be object;
    assume
A2: x in the carrier of W-INF_category;
    then reconsider x as LATTICE by YELLOW21:def 4;
A3: x is strict complete by A1,A2,Def4;
    the carrier of x in W by A1,A2,Def4;
    then x is Object of W-SUP_category by A3,Def5;
    hence thesis;
  end;
  let x be object;
  assume
A4: x in the carrier of W-SUP_category;
  then reconsider x as LATTICE by YELLOW21:def 4;
A5: x is strict complete by A1,A4,Def5;
  the carrier of x in W by A1,A4,Def5;
  then x is Object of W-INF_category by A5,Def4;
  hence thesis;
end;

definition :: 1.2 LEMMA, p. 179
  let W be with_non-empty_element set;
  set A = W-INF_category, B = W-SUP_category;
  deffunc O(LATTICE) = $1;
  deffunc F(LATTICE,LATTICE, Function of $1,$2) = LowerAdj $3;
  defpred P[LATTICE,LATTICE, Function of $1,$2] means
  $1 is complete & $2 is complete & $3 is infs-preserving;
  defpred Q[LATTICE,LATTICE, Function of $1,$2] means
  $1 is complete & $2 is complete & $3 is sups-preserving;
A1: for a,b being LATTICE, f being Function of a,b
  holds f in (the Arrows of A).(a,b) iff
  a in the carrier of A & b in the carrier of A & P[a,b,f] by Lm3;
A2: for a,b being LATTICE, f being Function of a,b
  holds f in (the Arrows of B).(a,b) iff
  a in the carrier of B & b in the carrier of B & Q[a,b,f] by Lm4;
A3: for a being LATTICE st a in the carrier of A
  holds O(a) in the carrier of B by Th17;
A4: for a,b being LATTICE, f being Function of a,b st P[a,b,f]
  holds F(a,b,f) is Function of O(b),O(a) & Q[O(b), O(a), F(a,b,f)];
A5: now
    let a be LATTICE;
    assume a in the carrier of A;
    then a is complete by YELLOW21:def 5;
    hence F(a,a,id a) = id O(a) by Th7;
  end;
A6: for a,b,c being LATTICE, f being Function of a,b, g being Function of b,c
  st P[a,b,f] & P[b,c,g] holds F(a,c,g*f) = F(a,b,f)*F(b,c,g) by Th8;
  func W LowerAdj ->
  contravariant strict Functor of W-INF_category, W-SUP_category means
  :
  Def6: (for a being Object of W-INF_category holds it.a = latt a) &
  for a,b being Object of W-INF_category st <^a,b^> <> {}
  for f being Morphism of a,b holds it.f = LowerAdj @f;
  existence
  proof
    thus ex F being contravariant strict
    Functor of W-INF_category, W-SUP_category st
    (for a being Object of W-INF_category holds F.a = O(latt a)) &
    for a,b being Object of W-INF_category st <^a,b^> <> {}
    for f being Morphism of a,b holds F.f = F(latt a, latt b, @f)
    from YELLOW21:sch 7(A1,A2,A3,A4,A5,A6);
  end;
  uniqueness
  proof
    let F,G be contravariant strict Functor of A, B such that
A7: for a being Object of W-INF_category holds F.a = latt a and
A8: for a,b being Object of W-INF_category st <^a,b^> <> {}
    for f being Morphism of a,b holds F.f = LowerAdj @f and
A9: for a being Object of W-INF_category holds G.a = latt a and
A10: for a,b being Object of W-INF_category st <^a,b^> <> {}
    for f being Morphism of a,b holds G.f = LowerAdj @f;
A11: now
      let a be Object of A;
      thus F.a = latt a by A7
        .= G.a by A9;
    end;
    now
      let a,b be Object of A such that
A12:  <^a,b^> <> {};
      let f be Morphism of a,b;
      thus F.f = LowerAdj @f by A8,A12
        .= G.f by A10,A12;
    end;
    hence thesis by A11,YELLOW18:2;
  end;
  deffunc G(LATTICE,LATTICE, Function of $1,$2) = UpperAdj $3;
A13: for a being LATTICE st a in the carrier of B
  holds O(a) in the carrier of A by Th17;
A14: for a,b being LATTICE, f being Function of a,b st Q[a,b,f]
  holds G(a,b,f) is Function of O(b), O(a) & P[O(b), O(a), G(a,b,f)];
A15: now
    let a be LATTICE;
    assume a in the carrier of B;
    then a is complete by YELLOW21:def 5;
    hence G(a,a,id a) = id O(a) by Th7;
  end;
A16: for a,b,c being LATTICE, f being Function of a,b, g being Function of b,c
  st Q[a,b,f] & Q[b,c,g] holds G(a,c,g*f) = G(a,b,f)*G(b,c,g) by Th9;
  func W UpperAdj ->
  contravariant strict Functor of W-SUP_category, W-INF_category means
  :
  Def7: (for a being Object of W-SUP_category holds it.a = latt a) &
  for a,b being Object of W-SUP_category st <^a,b^> <> {}
  for f being Morphism of a,b holds it.f = UpperAdj @f;
  existence
  proof
    thus ex F being contravariant strict Functor of B,A st
    (for a being Object of B holds F.a = O(latt a)) &
    for a,b being Object of B st <^a,b^> <> {}
    for f being Morphism of a,b holds F.f = G(latt a, latt b, @f)
    from YELLOW21:sch 7(A2,A1,A13,A14,A15,A16);
  end;
  uniqueness
  proof
    let F,G be contravariant strict Functor of B,A such that
A17: for a being Object of B holds F.a = latt a and
A18: for a,b being Object of B st <^a,b^> <> {}
    for f being Morphism of a,b holds F.f = UpperAdj @f and
A19: for a being Object of B holds G.a = latt a and
A20: for a,b being Object of B st <^a,b^> <> {}
    for f being Morphism of a,b holds G.f = UpperAdj @f;
A21: now
      let a be Object of B;
      thus F.a = latt a by A17
        .= G.a by A19;
    end;
    now
      let a,b be Object of B such that
A22:  <^a,b^> <> {};
      let f be Morphism of a,b;
      thus F.f = UpperAdj @f by A18,A22
        .= G.f by A20,A22;
    end;
    hence thesis by A21,YELLOW18:2;
  end;
end;

registration
  let W be with_non-empty_element set;
  cluster W LowerAdj -> bijective;
  coherence
  proof
    set A = W-INF_category, B = W-SUP_category;
    set F = W LowerAdj;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
    deffunc O(Object of A) = latt $1;
    deffunc F(Object of A,Object of A,Morphism of $1,$2) = LowerAdj @$3;
A2: for a being Object of A holds F.a = O(a) by Def6;
A3: for a,b being Object of A st <^a,b^> <> {}
    for f being Morphism of a,b holds F.f = F(a,b,f) by Def6;
A4: for a,b be Object of A st O(a) = O(b) holds a = b;
A5: now
      let a,b be Object of A such that
A6:   <^a,b^> <> {};
      let f,g be Morphism of a,b;
A7:   @f = f by A6,YELLOW21:def 7;
A8:   @g = g by A6,YELLOW21:def 7;
A9:   latt a is complete;
A10:  latt b is complete;
A11:  @f is infs-preserving by A1,A6,A7,Def4;
A12:  @g is infs-preserving by A1,A6,A8,Def4;
      assume F(a,b,f) = F(a,b,g);
      hence f = UpperAdj LowerAdj @g by A7,A9,A10,A11,Th10
        .= g by A8,A9,A10,A12,Th10;
    end;
A13: now
      let a,b be Object of B such that
A14:  <^a,b^> <> {};
      let f be Morphism of a,b;
A15:  latt a is strict complete by A1,Def5;
A16:  the carrier of latt a in W by A1,Def5;
A17:  latt b is strict complete by A1,Def5;
      the carrier of latt b in W by A1,Def5;
      then reconsider c = latt b, d = latt a as Object of A by A15,A16,A17,Def4
;
      take c,d;
A18:  latt c = c;
A19:  latt d = d;
A20:  f = @f by A14,YELLOW21:def 7;
      then
A21:  @f is sups-preserving by A1,A14,Def5;
      then
A22:  UpperAdj @f is monotone infs-preserving by A18,A19;
A23:  UpperAdj @f in <^c,d^> by A1,A21,Def4;
      reconsider g = UpperAdj @f as Morphism of c,d by A1,A21,Def4;
      take g;
      thus b = O(c) & a = O(d) & <^c,d^> <> {} by A1,A22,Def4;
      g = @g by A23,YELLOW21:def 7;
      hence f = F(c,d,g) by A20,A21,Th11;
    end;
    thus thesis from YELLOW18:sch 12(A2,A3,A4,A5,A13);
  end;
  cluster W UpperAdj -> bijective;
  coherence
  proof
    set A = W-SUP_category, B = W-INF_category;
    set F = W UpperAdj;
A24: ex x being non empty set st x in W by SETFAM_1:def 10;
    deffunc O(Object of A) = latt $1;
    deffunc F(Object of A, Object of A, Morphism of $1,$2) = UpperAdj @$3;
A25: for a being Object of A holds F.a = O(a) by Def7;
A26: for a,b being Object of A st <^a,b^> <> {}
    for f being Morphism of a,b holds F.f = F(a,b,f) by Def7;
A27: for a,b be Object of A st O(a) = O(b) holds a = b;
A28: now
      let a,b be Object of A such that
A29:  <^a,b^> <> {};
      let f,g be Morphism of a,b;
A30:  @f = f by A29,YELLOW21:def 7;
A31:  @g = g by A29,YELLOW21:def 7;
A32:  latt a is complete;
A33:  latt b is complete;
A34:  @f is sups-preserving by A24,A29,A30,Def5;
A35:  @g is sups-preserving by A24,A29,A31,Def5;
      assume F(a,b,f) = F(a,b,g);
      hence f = LowerAdj UpperAdj @g by A30,A32,A33,A34,Th11
        .= g by A31,A32,A33,A35,Th11;
    end;
A36: now
      let a,b be Object of B such that
A37:  <^a,b^> <> {};
      let f be Morphism of a,b;
A38:  latt a is strict complete by A24,Def4;
A39:  the carrier of latt a in W by A24,Def4;
A40:  latt b is strict complete by A24,Def4;
      the carrier of latt b in W by A24,Def4;
      then reconsider c = latt b, d = latt a as Object of A by A38,A39,A40,Def5
;
      take c,d;
A41:  latt c = c;
A42:  latt d = d;
A43:  f = @f by A37,YELLOW21:def 7;
      then
A44:  @f is infs-preserving by A24,A37,Def4;
      then
A45:  LowerAdj @f is monotone sups-preserving by A41,A42;
A46:  LowerAdj @f in <^c,d^> by A24,A44,Def5;
      reconsider g = LowerAdj @f as Morphism of c,d by A24,A44,Def5;
      take g;
      thus b = O(c) & a = O(d) & <^c,d^> <> {} by A24,A45,Def5;
      g = @g by A46,YELLOW21:def 7;
      hence f = F(c,d,g) by A43,A44,Th10;
    end;
    thus thesis from YELLOW18:sch 12(A25,A26,A27,A28,A36);
  end;
end;

theorem Th18:
  for W being with_non-empty_element set
  holds W LowerAdj" = W UpperAdj & W UpperAdj" = W LowerAdj
proof
  let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
  set B = W-SUP_category;
  set F = W LowerAdj, G = W UpperAdj;
A2: now
    let a be Object of B;
    thus F.(G.a) = latt (G.a) by Def6
      .= latt a by Def7
      .= a;
  end;
  now
    let a,b be Object of B;
    assume
A3: <^a,b^> <> {};
    then
A4: <^G.b, G.a^> <> {} by FUNCTOR0:def 19;
    let f be Morphism of a,b;
A5: G.f = UpperAdj @f by A3,Def7;
A6: @f = f by A3,YELLOW21:def 7;
A7: @(G.f) = G.f by A4,YELLOW21:def 7;
A8: G.a = latt a by Def7;
A9: G.b = latt b by Def7;
A10: @f is sups-preserving by A1,A3,A6,Def5;
    thus F.(G.f) = LowerAdj @(G.f) by A4,Def6
      .= f by A5,A6,A7,A8,A9,A10,Th11;
  end;
  hence F" = G by A2,YELLOW20:7;
  set B = W-INF_category;
  set G = W LowerAdj, F = W UpperAdj;
A11: now
    let a be Object of B;
    thus F.(G.a) = latt (G.a) by Def7
      .= latt a by Def6
      .= a;
  end;
  now
    let a,b be Object of B;
    assume
A12: <^a,b^> <> {};
    then
A13: <^G.b, G.a^> <> {} by FUNCTOR0:def 19;
    let f be Morphism of a,b;
A14: G.f = LowerAdj @f by A12,Def6;
A15: @f = f by A12,YELLOW21:def 7;
A16: @(G.f) = G.f by A13,YELLOW21:def 7;
A17: G.a = latt a by Def6;
A18: G.b = latt b by Def6;
A19: @f is infs-preserving by A1,A12,A15,Def4;
    thus F.(G.f) = UpperAdj @(G.f) by A13,Def7
      .= f by A14,A15,A16,A17,A18,A19,Th10;
  end;
  hence thesis by A11,YELLOW20:7;
end;

theorem :: 1.3 THEOREM, p. 179
  for W being with_non-empty_element set holds
  (W LowerAdj)*(W UpperAdj) = id (W-SUP_category) &
  (W UpperAdj)*(W LowerAdj) = id (W-INF_category)
proof
  let W be with_non-empty_element set;
A1: W LowerAdj" = W UpperAdj by Th18;
  W UpperAdj" = W LowerAdj by Th18;
  hence thesis by A1,FUNCTOR1:18;
end;

theorem :: 1.3 THEOREM, p. 179
  for W being with_non-empty_element set holds
  W-INF_category, W-SUP_category are_anti-isomorphic
proof
  let W be with_non-empty_element set;
  take W LowerAdj;
  thus thesis;
end;

begin

::<section2>Scott continuous maps and continuous lattices</section2>

theorem Th21: :: 1.4. THEOREM, (1) <=> (2), p. 180
  for S,T being complete LATTICE, g being infs-preserving Function of S,T
  holds g is directed-sups-preserving iff
  for X being Scott TopAugmentation of T
  for Y being Scott TopAugmentation of S for V being open Subset of X holds
  uparrow ((LowerAdj g).:V) is open Subset of Y
proof
  let S,T be complete LATTICE, g be infs-preserving Function of S,T;
  hereby
    assume
A1: g is directed-sups-preserving;
    let X be Scott TopAugmentation of T;
    let Y be Scott TopAugmentation of S;
    let V be open Subset of X;
A2: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A3: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
    then reconsider g9 = g as Function of Y,X by A2;
    reconsider d = LowerAdj g as Function of X,Y by A2,A3;
    uparrow (d.:V) is inaccessible
    proof
      let D be non empty directed Subset of Y;
      assume sup D in uparrow (d.:V);
      then consider y being Element of Y such that
A4:   y <= sup D and
A5:   y in d.:V by WAYBEL_0:def 16;
      consider u being object such that
A6:   u in the carrier of X and
A7:   u in V and
A8:   y = d.u by A5,FUNCT_2:64;
      reconsider u as Element of X by A6;
      reconsider g = g9 as Function of Y,X;
      [g, d] is Galois Connection of S,T by Def1;
      then
A9:   [g, d] is Galois by A2,A3,Th1;
      then
A10:  d*g <= id Y by WAYBEL_1:18;
A11:  id X <= g*d by A9,WAYBEL_1:18;
A12:  (id X).u = u by FUNCT_1:18;
A13:  (g*d).u = g.(d.u) by FUNCT_2:15;
A14:  g is infs-preserving Function of Y,X by A2,A3,WAYBEL21:6;
A15:  u <= g.y by A8,A11,A12,A13,YELLOW_2:9;
      g.y <= g.sup D by A4,A14,ORDERS_3:def 5;
      then
A16:  u <= g.sup D by A15,ORDERS_2:3;
      V is upper by WAYBEL11:def 4;
      then
A17:  g.sup D in V by A7,A16;
      g is directed-sups-preserving by A1,A2,A3,WAYBEL21:6;
      then
A18:  g preserves_sup_of D;
      ex_sup_of D, Y by YELLOW_0:17;
      then
A19:  g.sup D = sup (g.:D) by A18;
A20:  g.:D is directed non empty by A14,YELLOW_2:15;
      V is inaccessible by WAYBEL11:def 4;
      then g.:D meets V by A17,A19,A20;
      then consider z being object such that
A21:  z in g.:D and
A22:  z in V by XBOOLE_0:3;
      consider x being object such that
A23:  x in the carrier of Y and
A24:  x in D and
A25:  z = g qua Function.x by A21,FUNCT_2:64;
      reconsider x as Element of Y by A23;
A26:  (d*g).x = d.(g.x) by FUNCT_2:15;
      (id Y).x = x by FUNCT_1:18;
      then
A27:  d.(g.x) <= x by A10,A26,YELLOW_2:9;
      d.z in d.:V by A22,FUNCT_2:35;
      then x in uparrow (d.:V) by A25,A27,WAYBEL_0:def 16;
      hence thesis by A24,XBOOLE_0:3;
    end;
    then uparrow (d.:V) is open Subset of Y by WAYBEL11:def 4;
    hence uparrow ((LowerAdj g).:V) is open Subset of Y by A3,WAYBEL_0:13;
  end;
  assume
A28: for X being Scott TopAugmentation of T
  for Y being Scott TopAugmentation of S for V being open Subset of X holds
  uparrow ((LowerAdj g).:V) is open Subset of Y;
  set X = the Scott TopAugmentation of T,Y = the Scott TopAugmentation of S;
A29: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A30: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
  then reconsider g9 = g as Function of Y,X by A29;
  reconsider g9 as infs-preserving Function of Y,X by A29,A30,WAYBEL21:6;
  set d = LowerAdj g;
  reconsider d9 = d as Function of X,Y by A29,A30;
  let D be Subset of S such that
A31: D is non empty directed;
  assume ex_sup_of D, S;
  thus ex_sup_of g.:D,T by YELLOW_0:17;
A32: sup (g.:D) <= g.sup D by WAYBEL17:15;
  reconsider D9 = D as Subset of Y by A30;
  reconsider D9 as non empty directed Subset of Y by A30,A31,WAYBEL_0:3;
  reconsider s = sup D as Element of Y by A30;
  set U9 = (downarrow sup (g9.:D9))`;
A33: U9 is open by WAYBEL11:12;
  then uparrow (d.:U9) is open Subset of Y by A28;
  then
A34: uparrow (d.:U9) is upper inaccessible Subset of Y by WAYBEL11:def 4;
  sup (g9.:D9) = sup (g.:D) by A29,YELLOW_0:17,26;
  then
A35: downarrow sup (g9.:D9) = downarrow sup (g.:D) by A29,WAYBEL_0:13;
A36: sup (g.:D) <= sup (g.:D);
A37: [g,d] is Galois by Def1;
  then
A38: d*g <= id S by WAYBEL_1:18;
A39: id T <= g*d by A37,WAYBEL_1:18;
A40: (id S).sup D = sup D by FUNCT_1:18;
  (d*g).sup D = d.(g.sup D) by FUNCT_2:15;
  then d.(g.sup D) <= sup D by A38,A40,YELLOW_2:9;
  then
A41: d9.(g9.s) <= s by A30,YELLOW_0:1;
A42: s = sup D9 by A30,YELLOW_0:17,26;
  g.sup D <= sup (g.:D)
  proof
    assume not thesis;
    then
A43: not g.sup D in downarrow sup (g.:D) by WAYBEL_0:17;
A44: sup (g.:D) in downarrow sup (g.:D) by A36,WAYBEL_0:17;
A45: g.sup D in U9 by A29,A35,A43,XBOOLE_0:def 5;
A46: not sup (g.:D) in U9 by A35,A44,XBOOLE_0:def 5;
A47: d9.(g9.s) in d9.:U9 by A45,FUNCT_2:35;
    d9.:U9 c= uparrow (d9.:U9) by WAYBEL_0:16;
    then
A48: s in uparrow (d9.:U9) by A41,A47,WAYBEL_0:def 20;
    uparrow (d9.:U9) = uparrow (d.:U9) by A30,WAYBEL_0:13;
    then D9 meets uparrow (d9.:U9) by A34,A42,A48,WAYBEL11:def 1;
    then consider x being object such that
A49: x in D9 and
A50: x in uparrow (d9.:U9) by XBOOLE_0:3;
    reconsider x as Element of Y by A49;
    consider u9 being Element of Y such that
A51: u9 <= x and
A52: u9 in d9.:U9 by A50,WAYBEL_0:def 16;
    consider u being object such that
A53: u in the carrier of X and
A54: u in U9 and
A55: u9 = d9.u by A52,FUNCT_2:64;
    reconsider u as Element of X by A53;
    reconsider a = u as Element of T by A29;
    (id T).a = u by FUNCT_1:18;
    then a <= (g*d).a by A39,YELLOW_2:9;
    then a <= g.(d.a) by FUNCT_2:15;
    then
A56: u <= g9.(d9.u) by A29,YELLOW_0:1;
    g9.(d9.u) <= g9.x by A51,A55,ORDERS_3:def 5;
    then
A57: u <= g9.x by A56,ORDERS_2:3;
    g9.x in g9.:D9 by A49,FUNCT_2:35;
    then g9.x <= sup (g9.:D9) by YELLOW_2:22;
    then
A58: u <= sup (g9.:D9) by A57,ORDERS_2:3;
    U9 is upper by A33,WAYBEL11:def 4;
    then sup (g9.:D9) in U9 by A54,A58;
    hence thesis by A29,A46,YELLOW_0:17,26;
  end;
  hence thesis by A32,ORDERS_2:2;
end;

definition
  let S,T be non empty reflexive RelStr;
  let f be Function of S,T;
  attr f is waybelow-preserving means
   for x,y being Element of S st x << y holds f.x << f.y;
end;

theorem Th22: :: 1.4. THEOREM, (1) => (3), p. 180
  for S,T being complete LATTICE, g being infs-preserving Function of S,T holds
  g is directed-sups-preserving implies LowerAdj g is waybelow-preserving
proof
  let S,T be complete LATTICE, g be infs-preserving Function of S,T such that
A1: g is directed-sups-preserving;
  set d = (LowerAdj g);
A2: [g,d] is Galois by Def1;
  let t,t9 be Element of T such that
A3: t << t9;
  let D be non empty directed Subset of S;
  assume d.t9 <= sup D;
  then
A4: t9 <= g.sup D by A2,WAYBEL_1:8;
A5: g preserves_sup_of D by A1;
  ex_sup_of D,S by YELLOW_0:17;
  then
A6: g.sup D = sup (g.:D) by A5;
  g.:D is directed non empty by YELLOW_2:15;
  then consider x being Element of T such that
A7: x in g.:D and
A8: t <= x by A3,A4,A6;
  consider s being object such that
A9: s in the carrier of S and
A10: s in D and
A11: x = g.s by A7,FUNCT_2:64;
  reconsider s as Element of S by A9;
  take s;
  thus thesis by A2,A8,A10,A11,WAYBEL_1:8;
end;

theorem Th23: :: 1.4. THEOREM, (3+) => (1), p. 180
  for S being complete LATTICE for T being complete continuous LATTICE
  for g being infs-preserving Function of S,T
  st LowerAdj g is waybelow-preserving holds g is directed-sups-preserving
proof
  let S be complete LATTICE;
  let T be complete continuous LATTICE;
  let g be infs-preserving Function of S,T such that
A1: for t,t9 being Element of T st t << t9
  holds (LowerAdj g).t << (LowerAdj g).t9;
  let D be Subset of S;
  assume
A2: D is non empty directed;
  assume ex_sup_of D,S;
  thus ex_sup_of g.:D, T by YELLOW_0:17;
A3: sup (g.:D) <= g.sup D by WAYBEL17:15;
A4: g.sup D = sup waybelow (g.sup D) by WAYBEL_3:def 5;
  waybelow (g.sup D) is_<=_than sup (g.:D)
  proof
    let t be Element of T;
    assume t in waybelow (g.sup D);
    then t << g.sup D by WAYBEL_3:7;
    then
A5: (LowerAdj g).t << (LowerAdj g).(g.sup D) by A1;
A6: [g, LowerAdj g] is Galois by Def1;
    then
A7: (LowerAdj g)*g <= id S by WAYBEL_1:18;
    (id S).sup D = sup D by FUNCT_1:18;
    then ((LowerAdj g)*g).sup D <= sup D by A7,YELLOW_2:9;
    then (LowerAdj g).(g.sup D) <= sup D by FUNCT_2:15;
    then consider x being Element of S such that
A8: x in D and
A9: (LowerAdj g).t <= x by A2,A5;
A10: g.x in g.:D by A8,FUNCT_2:35;
A11: t <= g.x by A6,A9,WAYBEL_1:8;
    g.x <= sup (g.:D) by A10,YELLOW_2:22;
    hence thesis by A11,ORDERS_2:3;
  end;
  then g.sup D <= sup (g.:D) by A4,YELLOW_0:32;
  hence thesis by A3,ORDERS_2:2;
end;

definition
  let S,T be TopSpace;
  let f be Function of S,T;
  attr f is relatively_open means
   for V being open Subset of S holds f.:V is open Subset of T|rng f;
end;

theorem
  for X,Y being non empty TopSpace for d being Function of X, Y holds
  d is relatively_open iff corestr d is open
proof
  let X,Y be non empty TopSpace;
  let d be Function of X, Y;
A1: corestr d = d by WAYBEL18:def 7;
A2: Image d = Y|rng d by WAYBEL18:def 6;
  thus d is relatively_open implies corestr d is open
  by A1,A2;
  assume
A3: for V being Subset of X st V is open holds (corestr d).:V is open;
  let V be open Subset of X;
  thus thesis by A1,A2,A3;
end;

theorem Th25: :: requirement of 1.5. REMARK, p. 181
  for S,T being complete LATTICE, g being infs-preserving Function of S,T
  for X being Scott TopAugmentation of T
  for Y being Scott TopAugmentation of S for V being open Subset of X holds
  (LowerAdj g).:V = (rng LowerAdj g) /\ uparrow ((LowerAdj g).:V)
proof
  let S,T be complete LATTICE, g be infs-preserving Function of S,T;
  let X be Scott TopAugmentation of T;
  let Y be Scott TopAugmentation of S;
A1: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A2: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
  then reconsider d = LowerAdj g as Function of X, Y by A1;
  let V be open Subset of X;
  reconsider A = uparrow ((LowerAdj g).:V) as Subset of Y by A2;
  d.:V = A /\ rng d
  proof
A3: d.:V c= A by WAYBEL_0:16;
    d.:V c= rng d by RELAT_1:111;
    hence d.:V c= A /\ rng d by A3,XBOOLE_1:19;
    let t be object;
    assume
A4: t in A /\ rng d;
    then
A5: t in A by XBOOLE_0:def 4;
A6: t in rng d by A4,XBOOLE_0:def 4;
    reconsider t as Element of S by A5;
    consider x being Element of S such that
A7: x <= t and
A8: x in (LowerAdj g).:V by A5,WAYBEL_0:def 16;
    consider u being object such that
A9: u in the carrier of T and
A10: u in V and
A11: x = (LowerAdj g).u by A8,FUNCT_2:64;
    dom d = the carrier of T by FUNCT_2:def 1;
    then consider v being object such that
A12: v in the carrier of T and
A13: t = d.v by A6,FUNCT_1:def 3;
    reconsider u,v as Element of T by A9,A12;
A14: (LowerAdj g).(u "\/" v) = x "\/" t by A11,A13,WAYBEL_6:2
      .= t by A7,YELLOW_0:24;
    reconsider V9 = V as Subset of T by A1;
    V is upper by WAYBEL11:def 4;
    then
A15: V9 is upper by A1,WAYBEL_0:25;
    u <= u "\/" v by YELLOW_0:22;
    then u "\/" v in V9 by A10,A15;
    hence thesis by A14,FUNCT_2:35;
  end;
  hence thesis;
end;

theorem Th26: :: 1.5. REMARK, (2) => (2'), p. 181
  for S,T being complete LATTICE, g being infs-preserving Function of S,T
  for X being Scott TopAugmentation of T
  for Y being Scott TopAugmentation of S st for V being open Subset of X holds
  uparrow ((LowerAdj g).:V) is open Subset of Y holds
  for d being Function of X, Y st d = LowerAdj g holds d is relatively_open
proof
  let S,T be complete LATTICE, g be infs-preserving Function of S,T;
  let X be Scott TopAugmentation of T;
  let Y be Scott TopAugmentation of S such that
A1: for V being open Subset of X holds
  uparrow ((LowerAdj g).:V) is open Subset of Y;
  let d be Function of X, Y such that
A2: d = LowerAdj g;
  let V be open Subset of X;
  reconsider A = uparrow ((LowerAdj g).:V) as open Subset of Y by A1;
  d.:V = A /\ rng d by A2,Th25;
  then
A3: d.:V = [#](Y|rng d) /\ A by PRE_TOPC:def 5;
A4: A in the topology of Y by PRE_TOPC:def 2;
  reconsider B = d.:V as Subset of Y|rng d by A3,XBOOLE_1:17;
  B in the topology of Y|rng d by A3,A4,PRE_TOPC:def 4;
  hence thesis by PRE_TOPC:def 2;
end;

registration
  let X,Y be complete LATTICE;
  let f be sups-preserving Function of X,Y;
  cluster Image f -> complete;
  coherence by YELLOW_2:34;
end;

theorem :: 1.5. REMARK, (2') => (2''), p. 181
  for S,T being complete LATTICE, g being infs-preserving Function of S,T
  for X being Scott TopAugmentation of T
  for Y being Scott TopAugmentation of S
  for Z being Scott TopAugmentation of Image LowerAdj g
  for d being Function of X, Y, d9 being Function
  of X, Z st d = LowerAdj g & d9 = d
  holds d is relatively_open implies d9 is open
proof
  let S,T be complete LATTICE, g be infs-preserving Function of S,T;
  let X be Scott TopAugmentation of T;
  let Y be Scott TopAugmentation of S;
  let Z be Scott TopAugmentation of Image LowerAdj g;
  let d be Function of X, Y, d9 be Function of X, Z such that
A1: d = LowerAdj g and
A2: d9 = d and
A3: for V being open Subset of X holds d.:V is open Subset of Y|rng d;
  let V be Subset of X;
  assume V is open;
  then reconsider A = d.:V as open Subset of Y|rng d by A3;
A4: Image LowerAdj g = subrelstr rng LowerAdj g by YELLOW_2:def 2;
  then
A5: the carrier of Image LowerAdj g = rng d by A1,YELLOW_0:def 15;
A6: [#](Y|rng d) = rng d by PRE_TOPC:def 5;
A7: the RelStr of Z = Image LowerAdj g by YELLOW_9:def 4;
A8: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
  reconsider B = A as Subset of Z by A1,A4,A6,A7,YELLOW_0:def 15;
  A in the topology of Y|rng d by PRE_TOPC:def 2;
  then consider C being Subset of Y such that
A9: C in the topology of Y and
A10: A = C /\ [#](Y|rng d) by PRE_TOPC:def 4;
  C is open by A9;
  then
A11: C is upper inaccessible by WAYBEL11:def 4;
A12: B is upper
  proof
    let x,y be Element of Z;
    reconsider x9 = x, y9 = y as Element of Image LowerAdj g by A7;
    reconsider a = x9, b = y9 as Element of S by YELLOW_0:58;
    reconsider a9 = a, b9 = b as Element of Y by A8;
    assume that
A13: x in B and
A14: x <= y;
A15: x9 <= y9 by A7,A14,YELLOW_0:1;
A16: a in C by A10,A13,XBOOLE_0:def 4;
    a <= b by A15,YELLOW_0:59;
    then a9 <= b9 by A8,YELLOW_0:1;
    then b9 in C by A11,A16;
    hence thesis by A5,A6,A10,XBOOLE_0:def 4;
  end;
  B is inaccessible
  proof
    let D be directed non empty Subset of Z such that
A17: sup D in B;
    reconsider D9 = D as non empty Subset of Image LowerAdj g by A7;
    reconsider E = D9 as non empty Subset of S by A5,A8,XBOOLE_1:1;
    reconsider E9 = E as non empty Subset of Y by A8;
    D9 is directed by A7,WAYBEL_0:3;
    then E is directed by YELLOW_2:7;
    then
A18: E9 is directed by A8,WAYBEL_0:3;
A19: ex_sup_of D9,S by YELLOW_0:17;
    Image LowerAdj g is sups-inheriting by YELLOW_2:32;
    then "\/"(D9,S) in the carrier of Image LowerAdj g by A19;
    then sup E = sup D9 by YELLOW_0:68
      .= sup D by A7,YELLOW_0:17,26;
    then sup E9 = sup D by A8,YELLOW_0:17,26;
    then sup E9 in C by A10,A17,XBOOLE_0:def 4;
    then C meets E by A11,A18;
    hence thesis by A5,A6,A10,XBOOLE_1:77;
  end;
  hence thesis by A2,A12,WAYBEL11:def 4;
end;

theorem Th28: :: 1.6. COROLLARY, p. 181
  for S,T being complete LATTICE, g being infs-preserving Function of S,T
  st g is one-to-one for X being Scott TopAugmentation of T
  for Y being Scott TopAugmentation of S
  for d being Function of X,Y st d = LowerAdj g holds
  g is directed-sups-preserving iff d is open
proof
  let S,T be complete LATTICE, g be infs-preserving Function of S,T such that
A1: g is one-to-one;
  let X be Scott TopAugmentation of T;
  let Y be Scott TopAugmentation of S;
  [g, LowerAdj g] is Galois by Def1;
  then LowerAdj g is onto by A1,WAYBEL_1:27;
  then
A2: rng LowerAdj g = the carrier of S by FUNCT_2:def 3;
A3: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
A4: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A5: [#]Y = the carrier of Y;
  let d be Function of X,Y such that
A6: d = LowerAdj g;
A7: Y|rng d = the TopStruct of Y by A2,A3,A5,A6,TSEP_1:93;
  thus g is directed-sups-preserving implies d is open
  proof
    assume g is directed-sups-preserving;
    then for V being open Subset of X holds
    uparrow ((LowerAdj g).:V) is open Subset of Y by Th21;
    then
A8: d is relatively_open by A6,Th26;
    let V be Subset of X;
    assume V is open;
    then d.:V is open Subset of Y|rng d by A8;
    hence d.:V in the topology of Y by A7,PRE_TOPC:def 2;
  end;
  assume
A9: for V being Subset of X st V is open holds d.:V is open;
  now
    let X9 be Scott TopAugmentation of T;
    let Y9 be Scott TopAugmentation of S;
    let V9 be open Subset of X9;
A10: the RelStr of X9 = the RelStr of T by YELLOW_9:def 4;
A11: the RelStr of Y9 = the RelStr of S by YELLOW_9:def 4;
    reconsider V = V9 as Subset of X by A4,A10;
    reconsider V as open Subset of X by A4,A10,YELLOW_9:50;
    reconsider d9 = d as Function of X9,Y9 by A3,A4,A10,A11;
    d.:V is open by A9;
    then
A12: d9.:V9 is open Subset of Y9 by A3,A11,YELLOW_9:50;
    then d9.:V9 is upper by WAYBEL11:def 4;
    then
A13: uparrow (d9.:V9) c= d9.:V9 by WAYBEL_0:24;
    d9.:V9 c= uparrow (d9.:V9) by WAYBEL_0:16;
    then uparrow (d9.:V9) = d9.:V9 by A13;
    hence uparrow ((LowerAdj g).:V9) is open Subset of Y9
    by A6,A11,A12,WAYBEL_0:13;
  end;
  hence thesis by Th21;
end;

registration
  let X be complete LATTICE;
  let f be projection Function of X,X;
  cluster Image f -> complete;
  coherence by WAYBEL_1:54;
end;

theorem Th29:
  for L being complete LATTICE, k being kernel Function of L,L holds
  corestr k is infs-preserving & inclusion k is sups-preserving &
  LowerAdj corestr k = inclusion k & UpperAdj inclusion k = corestr k
proof
  let L be complete LATTICE, k be kernel Function of L,L;
A1: [corestr k, inclusion k] is Galois by WAYBEL_1:39;
  then
A2: inclusion k is lower_adjoint;
A3: corestr k is upper_adjoint by A1;
  hence corestr k is infs-preserving & inclusion k is sups-preserving by A2;
  thus thesis by A1,A2,A3,Def1,Def2;
end;

theorem Th30:
  for L being complete LATTICE, k being kernel Function of L,L holds
  k is directed-sups-preserving iff corestr k is directed-sups-preserving
proof
  let L be complete LATTICE, k be kernel Function of L,L;
  set ck = corestr k;
  [ck, inclusion k] is Galois by WAYBEL_1:39;
  then
A1: inclusion k is lower_adjoint;
A2: k = (inclusion k)*ck by WAYBEL_1:32;
  hereby
    assume
A3: k is directed-sups-preserving;
    thus corestr k is directed-sups-preserving
    proof
      let D be Subset of L;
      assume D is non empty directed;
      then
A4:   k preserves_sup_of D by A3;
      assume ex_sup_of D, L;
      then
A5:   sup (k.:D) = k.sup D by A4
        .= (inclusion k).(ck.sup D) by A2,FUNCT_2:15
        .= ck.sup D by FUNCT_1:18;
      thus ex_sup_of ck.:D, Image k by YELLOW_0:17;
A6:   ex_sup_of (inclusion k).:(ck.:D), L by YELLOW_0:17;
A7:   Image k is sups-inheriting by WAYBEL_1:53;
      ex_sup_of ck.:D, L by YELLOW_0:17;
      then
A8:   "\/"((ck.:D), L) in the carrier of Image k by A7;
      ck.:D = (inclusion k).:(ck.:D) by WAYBEL15:12;
      hence sup (ck.:D) = sup ((inclusion k).:(ck.:D)) by A6,A8,YELLOW_0:64
        .= ck.sup D by A2,A5,RELAT_1:126;
    end;
  end;
  thus thesis by A1,A2,WAYBEL15:11;
end;

theorem :: 1.7. COROLLARY, (1) <=> (2), p. 181
  for L being complete LATTICE, k being kernel Function of L,L holds
  k is directed-sups-preserving iff
  for X being Scott TopAugmentation of Image k
  for Y being Scott TopAugmentation of L
  for V being Subset of L st V is open Subset of X
  holds uparrow V is open Subset of Y
proof
  let L be complete LATTICE, k be kernel Function of L,L;
A1: [corestr k, inclusion k] is Galois by WAYBEL_1:39;
  then
A2: corestr k is upper_adjoint;
  then
A3: inclusion k = LowerAdj corestr k by A1,Def1;
  hereby
    assume
A4: k is directed-sups-preserving;
    let X be Scott TopAugmentation of Image k;
    let Y be Scott TopAugmentation of L;
A5: the RelStr of X = Image k by YELLOW_9:def 4;
    let V be Subset of L;
    assume V is open Subset of X;
    then reconsider A = V as open Subset of X;
    reconsider B = A as Subset of Image k by A5;
A6: corestr k is directed-sups-preserving by A4,Th30;
    (inclusion k).:B = V by WAYBEL15:12;
    hence uparrow V is open Subset of Y by A2,A3,A6,Th21;
  end;
  assume
A7: for X being Scott TopAugmentation of Image k
  for Y being Scott TopAugmentation of L
  for V being Subset of L st V is open Subset of X
  holds uparrow V is open Subset of Y;
  now
    set g = corestr k;
    let X be Scott TopAugmentation of Image k;
    let Y be Scott TopAugmentation of L;
    let V be open Subset of X;
    the RelStr of X = Image k by YELLOW_9:def 4;
    then reconsider B = V as Subset of Image k;
    the carrier of Image k c= the carrier of L by YELLOW_0:def 13;
    then reconsider A = B as Subset of L by XBOOLE_1:1;
    uparrow A is open Subset of Y by A7;
    hence uparrow ((LowerAdj g).:V) is open Subset of Y by A3,WAYBEL15:12;
  end;
  then corestr k is directed-sups-preserving by A2,Th21;
  hence thesis by Th30;
end;

theorem Th32:
  for L being complete LATTICE
  for S being sups-inheriting non empty full SubRelStr of L
  for x,y being Element of L, a,b being Element of S st a = x & b = y
  holds x << y implies a << b
proof
  let L be complete LATTICE;
  let S be sups-inheriting non empty full SubRelStr of L;
  let x,y be Element of L, a,b be Element of S such that
A1: a = x and
A2: b = y and
A3: for D being non empty directed Subset of L st y <= sup D
  ex d being Element of L st d in D & x <= d;
  let D be non empty directed Subset of S such that
A4: b <= sup D;
  reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A5: ex_sup_of D, L by YELLOW_0:17;
  then "\/"(D,L) in the carrier of S by YELLOW_0:def 19;
  then sup E = sup D by A5,YELLOW_0:64;
  then y <= sup E by A2,A4,YELLOW_0:59;
  then consider e being Element of L such that
A6: e in E and
A7: x <= e by A3;
  reconsider d = e as Element of S by A6;
  take d;
  thus thesis by A1,A6,A7,YELLOW_0:60;
end;

theorem :: 1.7. COROLLARY, (1) => (3), p. 181
  for L being complete LATTICE, k being kernel Function of L,L
  st k is directed-sups-preserving
  for x,y being Element of L, a,b being Element of Image k st a = x & b = y
  holds x << y iff a << b
proof
  let L be complete LATTICE, k be kernel Function of L,L;
  set g = corestr k;
  assume k is directed-sups-preserving;
  then corestr k is directed-sups-preserving infs-preserving by Th29,Th30;
  then
A1: LowerAdj g is waybelow-preserving by Th22;
  let x,y be Element of L, a,b be Element of Image k;
A2: Image k is sups-inheriting by WAYBEL_1:53;
A3: inclusion k = LowerAdj g by Th29;
  then
A4: (LowerAdj g).a = a by FUNCT_1:18;
  (LowerAdj g).b = b by A3,FUNCT_1:18;
  hence thesis by A1,A2,A4,Th32;
end;

theorem :: 1.7. COROLLARY, (3) => (1), p. 181
  for L being complete LATTICE, k being kernel Function of L,L
  st Image k is continuous &
  for x,y being Element of L, a,b being Element of Image k st a = x & b = y
  holds x << y iff a << b holds k is directed-sups-preserving
proof
  let L be complete LATTICE, k be kernel Function of L,L such that
A1: Image k is continuous and
A2: for x,y being Element of L, a,b being Element of Image k st a = x & b = y
  holds x << y iff a << b;
  set g = corestr k;
A3: corestr k is infs-preserving by Th29;
  LowerAdj g is waybelow-preserving
  proof
    let t,t9 be Element of Image k;
A4: LowerAdj g = inclusion k by Th29;
    then
A5: (LowerAdj g).t = t by FUNCT_1:18;
    (LowerAdj g).t9 = t9 by A4,FUNCT_1:18;
    hence thesis by A2,A5;
  end;
  then corestr k is directed-sups-preserving by A1,A3,Th23;
  hence thesis by Th30;
end;

theorem Th35:
  for L being complete LATTICE, c being closure Function of L,L holds
  corestr c is sups-preserving & inclusion c is infs-preserving &
  UpperAdj corestr c = inclusion c & LowerAdj inclusion c = corestr c
proof
  let L be complete LATTICE, c be closure Function of L,L;
A1: [inclusion c, corestr c] is Galois by WAYBEL_1:36;
  then
A2: inclusion c is upper_adjoint;
A3: corestr c is lower_adjoint by A1;
  hence corestr c is sups-preserving & inclusion c is infs-preserving by A2;
  thus thesis by A1,A2,A3,Def1,Def2;
end;

theorem Th36:
  for L being complete LATTICE, c being closure Function of L,L holds
  Image c is directed-sups-inheriting iff
  inclusion c is directed-sups-preserving
proof
  let L be complete LATTICE, c be closure Function of L,L;
  set ic = inclusion c;
  thus Image c is directed-sups-inheriting implies
  inclusion c is directed-sups-preserving
  proof
    assume
A1: Image c is directed-sups-inheriting;
    let D be Subset of Image c;
    assume
A2: D is non empty directed;
    then reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A3: ic.:D = E by WAYBEL15:12;
    assume ex_sup_of D, Image c;
    thus ex_sup_of ic.:D, L by YELLOW_0:17;
    hence sup (ic.:D) = sup D by A1,A2,A3,WAYBEL_0:7
      .= ic.sup D by FUNCT_1:18;
  end;
  assume
A4: inclusion c is directed-sups-preserving;
  let X be directed Subset of Image c;
  assume
A5: X <> {};
  assume ex_sup_of X,L;
A6: ic preserves_sup_of X by A4,A5;
  ex_sup_of X, Image c by YELLOW_0:17;
  then sup (ic.:X) = ic.sup X by A6
    .= sup X by FUNCT_1:18;
  then sup (ic.:X) in the carrier of Image c;
  hence thesis by WAYBEL15:12;
end;

theorem :: 1.8. COROLLARY, (1) <=> (2), p. 182
  for L being complete LATTICE, c being closure Function of L,L holds
  Image c is directed-sups-inheriting iff
  for X being Scott TopAugmentation of Image c
  for Y being Scott TopAugmentation of L
  for f being Function of Y,X st f = c holds f is open
proof
  let L be complete LATTICE, c be closure Function of L,L;
A1: LowerAdj inclusion c = corestr c by Th35;
A2: corestr c = c by WAYBEL_1:30;
A3: inclusion c is infs-preserving Function of Image c, L by Th35;
A4: Image c is directed-sups-inheriting iff inclusion c is
  directed-sups-preserving by Th36;
  hence Image c is directed-sups-inheriting implies
  for X being Scott TopAugmentation of Image c
  for Y being Scott TopAugmentation of L
  for f being Function of Y,X st f = c holds f is open by A1,A2,A3,Th28;
  assume
A5: for X being Scott TopAugmentation of Image c
  for Y being Scott TopAugmentation of L
  for f being Function of Y,X st f = c holds f is open;

set X = the Scott TopAugmentation of Image c,Y = the Scott TopAugmentation of L
;
A6: the RelStr of X = the RelStr of Image c by YELLOW_9:def 4;
  the RelStr of Y = the RelStr of L by YELLOW_9:def 4;
  then reconsider f = c as Function of Y,X by A2,A6;
  f is open by A5;
  hence thesis by A1,A2,A3,A4,Th28;
end;

theorem :: 1.8. COROLLARY, (1) => (3), p. 182
  for L being complete LATTICE, c being closure Function of L,L holds
  Image c is directed-sups-inheriting implies corestr c is waybelow-preserving
proof
  let L be complete LATTICE, c be closure Function of L,L;
  assume Image c is directed-sups-inheriting;
  then inclusion c is directed-sups-preserving infs-preserving by Th35,Th36;
  then LowerAdj inclusion c is waybelow-preserving by Th22;
  hence thesis by Th35;
end;

theorem :: 1.8. COROLLARY, (3) => (1), p. 182
:: SHOULD BE:
:: for L being complete LATTICE, c being closure map of L,L
::  st
::    Image c is continuous & corestr c is waybelow-preserving
::  holds Image c is directed-sups-inheriting
:: ------------------------ a bug ???
  for L being continuous complete LATTICE, c being closure Function of L,L st
  corestr c is waybelow-preserving holds Image c is directed-sups-inheriting
proof
  let L be continuous complete LATTICE, c be closure Function of L,L;
  assume
A1: corestr c is waybelow-preserving;
A2: LowerAdj inclusion c = corestr c by Th35;
  inclusion c is infs-preserving by Th35;
  then inclusion c is directed-sups-preserving by A1,A2,Th23;
  hence thesis by Th36;
end;

begin

::<section3>Duality of subcategories of {\it INF} and {\it SUP}</section3>

definition :: 1.9. DEFINITION, p. 182
  let W be non empty set;
  set A = W-INF_category;
  defpred P[set] means not contradiction;
  defpred Q[Object of A, Object of A, Morphism of $1,$2] means
  @$3 is directed-sups-preserving;
A1: ex a being Object of A st P[a];
A2: for a,b,c being Object of A
  st P[a] & P[b] & P[c] & <^a,b^> <> {} & <^b,c^> <> {}
  for f being Morphism of a,b, g being Morphism of b,c
  st Q[a,b,f] & Q[b,c,g] holds Q[a,c,g*f]
  proof
    let a,b,c be Object of A such that
A3: <^a,b^> <> {} and
A4: <^b,c^> <> {};
    let f be Morphism of a,b, g be Morphism of b,c;
A5: <^a,c^> <> {} by A3,A4,ALTCAT_1:def 2;
A6: @f = f by A3,YELLOW21:def 7;
A7: @g = g by A4,YELLOW21:def 7;
    @(g*f) = g*f by A5,YELLOW21:def 7;
    then @(g*f) = (@g)*(@f) by A3,A4,A5,A6,A7,ALTCAT_1:def 12;
    hence thesis by WAYBEL20:28;
  end;
A8: for a being Object of A st P[a] holds Q[a,a,idm a]
  proof
    let a be Object of A;
    idm a = id latt a by YELLOW21:2;
    hence thesis by YELLOW21:def 7;
  end;
  func W-INF(SC)_category -> strict non empty subcategory of W-INF_category
  means
  :
  Def10: (for a being Object of W-INF_category holds a is Object of it) &
  for a,b being Object of W-INF_category
  for a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {}
  for f being Morphism of a,b holds
  f in <^a9,b9^> iff @f is directed-sups-preserving;
  existence
  proof
    ex B being strict non empty subcategory of A st
    (for a being Object of A holds a is Object of B iff P[a]) &
    for a,b being Object of A, a9,b9 being Object of B
    st a9 = a & b9 = b & <^a,b^> <> {}
    for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f]
    from YELLOW18:sch 7(A1,A2,A8);
    hence thesis;
  end;
  correctness
  proof
    let B1,B2 being strict non empty subcategory of A;
    assume for a being Object of W-INF_category holds a is Object of B1;
    then
    A9: for a being Object of W-INF_category holds a is Object of B1 iff P [a];
    assume
A10: for a,b being Object of W-INF_category
    for a9,b9 being Object of B1 st a9 = a & b9 = b & <^a,b^> <> {}
    for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
    assume for a being Object of W-INF_category holds a is Object of B2;
    then
    A11: for
 a being Object of W-INF_category holds a is Object of B2 iff P [ a];
    assume
A12: for a,b being Object of W-INF_category
    for a9,b9 being Object of B2 st a9 = a & b9 = b & <^a,b^> <> {}
    for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
    the AltCatStr of B1 = the AltCatStr of B2
    from YELLOW20:sch 1(A9,A10,A11,A12);
    hence thesis;
  end;
end;

definition :: 1.9. DEFINITION, p. 182
  let W be with_non-empty_element set;
A1: ex w being non empty set st w in W by SETFAM_1:def 10;
  set A = W-SUP_category;
  defpred P[set] means not contradiction;
  defpred Q[Object of A, Object of A, Morphism of $1,$2] means
  UpperAdj @$3 is directed-sups-preserving;
A2: ex a being Object of A st P[a];
A3: for a,b,c being Object of A
  st P[a] & P[b] & P[c] & <^a,b^> <> {} & <^b,c^> <> {}
  for f being Morphism of a,b, g being Morphism of b,c st Q[a,b,f] & Q[b,c,g]
  holds Q[a,c,g*f]
  proof
    let a,b,c be Object of A such that
A4: <^a,b^> <> {} and
A5: <^b,c^> <> {};
    let f be Morphism of a,b, g be Morphism of b,c;
A6: <^a,c^> <> {} by A4,A5,ALTCAT_1:def 2;
A7: @f = f by A4,YELLOW21:def 7;
A8: @g = g by A5,YELLOW21:def 7;
A9: @(g*f) = g*f by A6,YELLOW21:def 7;
A10: @g is sups-preserving Function of latt b, latt c by A1,A5,A8,Def5;
A11: @f is sups-preserving Function of latt a, latt b by A1,A4,A7,Def5;
    @(g*f) = (@g)*(@f) by A4,A5,A6,A7,A8,A9,ALTCAT_1:def 12;
    then UpperAdj @(g*f) = (UpperAdj @f)*(UpperAdj @g) by A10,A11,Th9;
    hence thesis by WAYBEL20:28;
  end;
A12: for a being Object of A st P[a] holds Q[a,a,idm a]
  proof
    let a be Object of A;
A13: idm a = id latt a by YELLOW21:2;
    UpperAdj id latt a = id latt a by Th7;
    hence thesis by A13,YELLOW21:def 7;
  end;
  func W-SUP(SO)_category -> strict non empty subcategory of W-SUP_category
  means
  :
  Def11: (for a being Object of W-SUP_category holds a is Object of it) &
  for a,b being Object of W-SUP_category
  for a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {}
  for f being Morphism of a,b holds
  f in <^a9,b9^> iff UpperAdj @f is directed-sups-preserving;
  existence
  proof
    ex B being strict non empty subcategory of A st
    (for a being Object of A holds a is Object of B iff P[a]) &
    for a,b being Object of A, a9,b9 being Object of B
    st a9 = a & b9 = b & <^a,b^> <> {}
    for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f]
    from YELLOW18:sch 7(A2,A3,A12);
    hence thesis;
  end;
  correctness
  proof
    let B1,B2 being strict non empty subcategory of A;
    assume for a being Object of W-SUP_category holds a is Object of B1;
    then
    A14: for
 a being Object of W-SUP_category holds a is Object of B1 iff P [ a];
    assume
A15: for a,b being Object of W-SUP_category
    for a9,b9 being Object of B1 st a9 = a & b9 = b & <^a,b^> <> {}
    for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
    assume for a being Object of W-SUP_category holds a is Object of B2;
    then
    A16: for
 a being Object of W-SUP_category holds a is Object of B2 iff P [ a];
    assume
A17: for a,b being Object of W-SUP_category
    for a9,b9 being Object of B2 st a9 = a & b9 = b & <^a,b^> <> {}
    for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
    the AltCatStr of B1 = the AltCatStr of B2
    from YELLOW20:sch 1(A14,A15,A16,A17);
    hence thesis;
  end;
end;

theorem Th40:
for S being non empty RelStr, T being non empty reflexive antisymmetric RelStr
  for t being Element of T for X being non empty Subset of S
  holds S --> t preserves_sup_of X & S --> t preserves_inf_of X
proof
  let S be non empty RelStr;
  let T be non empty reflexive antisymmetric RelStr;
  let t be Element of T;
  let X be non empty Subset of S;
  set f = S --> t;
A1: f.:X = {t}
  proof
    thus f.:X c= {t} by FUNCOP_1:81;
    set x = the Element of X;
    f.x = t by FUNCOP_1:7;
    then t in f.:X by FUNCT_2:35;
    hence thesis by ZFMISC_1:31;
  end;
A2: f.sup X = t by FUNCOP_1:7;
A3: f.inf X = t by FUNCOP_1:7;
A4: inf {t} = t by YELLOW_0:39;
A5: sup {t} = t by YELLOW_0:39;
A6: ex_sup_of {t}, T by YELLOW_0:38;
  ex_inf_of {t}, T by YELLOW_0:38;
  hence thesis by A1,A2,A3,A4,A5,A6;
end;

theorem Th41:
  for S being non empty RelStr
  for T being lower-bounded non empty reflexive antisymmetric RelStr
  holds S --> Bottom T is sups-preserving
proof
  let S be non empty RelStr;
  let T be lower-bounded non empty reflexive antisymmetric RelStr;
  let X be Subset of S such that ex_sup_of X,S;
  set f = (the carrier of S) --> Bottom T;
A1: f.sup X = Bottom T by FUNCOP_1:7;
  (S --> Bottom T).:X c= {Bottom T} by FUNCOP_1:81;
  then (S --> Bottom T).:X = {Bottom T} or (S --> Bottom T).:
  X = {} by ZFMISC_1:33;
  hence thesis by A1,YELLOW_0:38,39,42;
end;

theorem Th42:
  for S being non empty RelStr
  for T being upper-bounded non empty reflexive antisymmetric RelStr
  holds S --> Top T is infs-preserving
proof
  let S be non empty RelStr;
  let T be upper-bounded non empty reflexive antisymmetric RelStr;
  let X be Subset of S such that ex_inf_of X,S;
  set t = Top T, f = (the carrier of S) --> t;
A1: f.inf X = t by FUNCOP_1:7;
  (S --> t).:X c= {t} by FUNCOP_1:81;
  then (S --> t).:X = {t} or (S --> t).:X = {} by ZFMISC_1:33;
  hence thesis by A1,YELLOW_0:38,39,43;
end;

registration :: WAYBEL24
  let S be non empty RelStr;
  let T be upper-bounded non empty reflexive antisymmetric RelStr;
  cluster S --> Top T -> directed-sups-preserving infs-preserving;
  coherence
  by Th40,Th42;
end;

registration
  let S be non empty RelStr;
  let T be lower-bounded non empty reflexive antisymmetric RelStr;
  cluster S --> Bottom T -> filtered-infs-preserving sups-preserving;
  coherence
  by Th40,Th41;
end;

registration
  let S be non empty RelStr;
  let T be upper-bounded non empty reflexive antisymmetric RelStr;
  cluster directed-sups-preserving infs-preserving for Function of S, T;
  existence
  proof
    take S --> Top T;
    thus thesis;
  end;
end;

registration
  let S be non empty RelStr;
  let T be lower-bounded non empty reflexive antisymmetric RelStr;
  cluster filtered-infs-preserving sups-preserving for Function of S, T;
  existence
  proof
    take S --> Bottom T;
    thus thesis;
  end;
end;

theorem Th43:
  for W being with_non-empty_element set for L being LATTICE holds
  L is Object of W-INF(SC)_category iff
  L is strict complete & the carrier of L in W
proof
  let W be with_non-empty_element set;
  let L be LATTICE;
  the carrier of W-INF(SC)_category c= the carrier of W-INF_category
  by ALTCAT_2:def 11;
  then L in the carrier of W-INF(SC)_category implies
  L is Object of W-INF_category;
  then L is Object of W-INF(SC)_category iff L is Object of W-INF_category
  by Def10;
  hence thesis by Th13;
end;

theorem Th44:
  for W being with_non-empty_element set
  for a, b being Object of W-INF(SC)_category for f being set
  holds f in <^a,b^> iff
  f is directed-sups-preserving infs-preserving Function of latt a, latt b
proof
  let W be with_non-empty_element set;
  let a,b be Object of W-INF(SC)_category, f be set;
  the carrier of W-INF(SC)_category c= the carrier of W-INF_category by
ALTCAT_2:def 11;
  then reconsider a1 = a, b1 = b as Object of W-INF_category;
  hereby
    assume
A1: f in <^a,b^>;
A2: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
    then reconsider g = f as Morphism of a1,b1 by A1;
    f = @g by A1,A2,YELLOW21:def 7;
    hence f is directed-sups-preserving infs-preserving Function
    of latt a, latt b by A1,A2,Def10,Th14;
  end;
  assume f is directed-sups-preserving infs-preserving Function
  of latt a, latt b;
  then reconsider f as
  directed-sups-preserving infs-preserving Function of latt a, latt b;
A3: f in <^a1,b1^> by Th14;
  reconsider g = f as Morphism of a1,b1 by Th14;
  f = @g by A3,YELLOW21:def 7;
  hence thesis by A3,Def10;
end;

theorem
  for W being with_non-empty_element set for L being LATTICE holds
  L is Object of W-SUP(SO)_category iff
  L is strict complete & the carrier of L in W
proof
  let W be with_non-empty_element set;
  let L be LATTICE;
  the carrier of W-SUP(SO)_category c= the carrier of W-SUP_category
  by ALTCAT_2:def 11;
  then L in the carrier of W-SUP(SO)_category implies
  L is Object of W-SUP_category;
  then L is Object of W-SUP(SO)_category iff L is Object of W-SUP_category
  by Def11;
  hence thesis by Th15;
end;

theorem Th46:
  for W being with_non-empty_element set
  for a, b being Object of W-SUP(SO)_category for f being set
  holds f in <^a,b^> iff
  ex g being sups-preserving Function of latt a, latt b st g = f &
  UpperAdj g is directed-sups-preserving
proof
  let W be with_non-empty_element set;
  let a,b be Object of W-SUP(SO)_category, f be set;
  the carrier of W-SUP(SO)_category c= the carrier of W-SUP_category by
ALTCAT_2:def 11;
  then reconsider a1 = a, b1 = b as Object of W-SUP_category;
  hereby
    assume
A1: f in <^a,b^>;
A2: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
    then reconsider g = f as Morphism of a1,b1 by A1;
A3: f = @g by A1,A2,YELLOW21:def 7;
A4: UpperAdj @g is directed-sups-preserving by A1,A2,Def11;
    f is sups-preserving Function of latt a1, latt b1 by A1,A2,Th16;
    hence ex g being sups-preserving Function of latt a, latt b st g = f &
    UpperAdj g is directed-sups-preserving by A3,A4;
  end;
  given g being sups-preserving Function of latt a, latt b such that
A5: g = f and
A6: UpperAdj g is directed-sups-preserving;
A7: f in <^a1,b1^> by A5,Th16;
  reconsider g = f as Morphism of a1,b1 by A5,Th16;
  f = @g by A7,YELLOW21:def 7;
  hence thesis by A5,A6,A7,Def11;
end;

theorem :: Remark after 1.9. DEFINITION, p. 182
  for W being with_non-empty_element set
  holds W-INF(SC)_category = Intersect(W-INF_category, W-UPS_category)
proof
  let W be with_non-empty_element set;
  consider w being non empty set such that
A1: w in W by SETFAM_1:def 10;
  set r = the upper-bounded well-ordering Order of w;
A2: now
    let a be Object of W-INF_category, b be Object of W-UPS_category;
    idm a = id latt a by YELLOW21:2;
    hence a = b implies idm a = idm b by YELLOW21:2;
  end;
  set B = Intersect(W-INF_category, W-UPS_category);
A3: W-INF_category, W-UPS_category have_the_same_composition by YELLOW20:12;
  then
A4: the carrier of B = (the carrier of W-INF_category) /\
  (the carrier of W-UPS_category) by YELLOW20:def 3;
A5: RelStr(#w,r#) is Object of W-INF_category by A1,Th13;
  RelStr(#w,r#) is Object of W-UPS_category by A1,YELLOW21:14;
  then Intersect(W-INF_category, W-UPS_category) is non empty by A4,A5,
XBOOLE_0:def 4;
  then reconsider I = Intersect(W-INF_category, W-UPS_category) as
  non empty subcategory of W-INF_category by A2,YELLOW20:12,25;
  set A = W-INF(SC)_category;
  deffunc B(set,set) = (the Arrows of A).($1,$2);
A6: for C1, C2 being para-functional semi-functional category
  st the carrier of C1 = the carrier of A &
  (for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
  the carrier of C2 = the carrier of A &
  (for a,b being Object of C2 holds <^a,b^> = B(a,b))
  holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW18:sch 19;
A7: the carrier of I = the carrier of A
  proof
    thus the carrier of I c= the carrier of A
    proof
      let x be object;
      assume x in the carrier of I;
      then reconsider x as Object of I;
      reconsider L = x as LATTICE by YELLOW21:def 4;
A8:   x in the carrier of W-UPS_category by A4,XBOOLE_0:def 4;
      then
A9:   L is strict complete by A1,YELLOW21:def 10;
      the carrier of L in W by A1,A8,YELLOW21:def 10;
      then L is Object of A by A9,Th43;
      hence thesis;
    end;
    let x be object;
    assume x in the carrier of A;
    then reconsider x as Object of A;
    reconsider L = x as LATTICE by YELLOW21:def 4;
A10: L is complete strict by Th43;
A11: the carrier of L in W by Th43;
    then
A12: x is Object of W-INF_category by A10,Th13;
    x is Object of W-UPS_category by A10,A11,YELLOW21:def 10;
    hence thesis by A4,A12,XBOOLE_0:def 4;
  end;
A13: for a,b being Object of A holds <^a,b^> = B(a,b) by ALTCAT_1:def 1;
  now
    let a,b be Object of I;
    reconsider a9 = a, b9 = b as Object of A by A7;
    reconsider a1 = a, b1 = b as Object of W-INF_category by A4,XBOOLE_0:def 4;
    reconsider a2 = a, b2 = b as Object of W-UPS_category by A4,XBOOLE_0:def 4;
A14: dom the Arrows of W-INF_category = [:the carrier of W-INF_category, the
    carrier of W-INF_category:] by PARTFUN1:def 2;
    dom the Arrows of W-UPS_category = [:the carrier of W-UPS_category, the
    carrier of W-UPS_category:] by PARTFUN1:def 2;
    then
A15: (dom the Arrows of W-INF_category) /\ (dom the Arrows of W
    -UPS_category) = [:(the carrier of W-INF_category)/\ the carrier of W
-UPS_category, (the carrier of W-INF_category)/\ the carrier of W-UPS_category
    :] by A14,ZFMISC_1:100;
A16: <^a,b^> = (the Arrows of I).(a,b) by ALTCAT_1:def 1
      .= Intersect(the Arrows of W-INF_category, the Arrows of W-UPS_category)
    . [a,b] by A3,YELLOW20:def 3
      .= ((the Arrows of W-INF_category).(a,b)) /\
    ((the Arrows of W-UPS_category). [a,b]) by A4,A15,YELLOW20:def 2
      .= <^a1,b1^> /\ ((the Arrows of W-UPS_category).(a,b)) by ALTCAT_1:def 1
      .= <^a1,b1^> /\ <^a2,b2^> by ALTCAT_1:def 1;
    now
      let f be object;
      f in <^a,b^> iff f in <^a1,b1^> & f in <^a2,b2^> by A16,XBOOLE_0:def 4;
      then f in <^a,b^> iff f is directed-sups-preserving Function of latt a2,
      latt b2 & f is infs-preserving Function of latt a1, latt b1
      by Th14,YELLOW21:15;
      then f in <^a,b^> iff f in <^a9,b9^> by Th44;
      hence f in <^a,b^> iff f in B(a,b) by ALTCAT_1:def 1;
    end;
    hence <^a,b^> = B(a,b) by TARSKI:2;
  end;
  hence thesis by A6,A7,A13;
end;

definition :: 1.9. DEFINITION, p. 182
  let W be with_non-empty_element set;
  defpred P[Object of W-INF(SC)_category] means latt $1 is continuous;
  consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
  set r = the upper-bounded well-ordering Order of a;
  set b = RelStr(#a,r#);
  func W-CL_category -> strict full non empty subcategory of W-INF(SC)_category
  means
  : Def12:
  for a being Object of W-INF(SC)_category holds
  a is Object of it iff latt a is continuous;
  existence
  proof
    b is Object of W-INF_category by A1,Def4;
    then reconsider b as Object of W-INF(SC)_category by Def10;
    b = latt b;
    then
A2: ex b being Object of W-INF(SC)_category st P[b];
    thus
    ex B being strict full non empty subcategory of W-INF(SC)_category st
    for a being Object of W-INF(SC)_category holds a is Object of B iff P[a]
    from YELLOW20:sch 2(A2);
  end;
  correctness
  proof
    let B1,B2 be strict full non empty subcategory of W-INF(SC)_category
    such that
A3: for a being Object of W-INF(SC)_category holds a is Object of B1 iff P[a]
    and
    A4: for
 a being Object of W-INF(SC)_category holds a is Object of B2 iff P[a];
    the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3(A3,
    A4);
    hence thesis;
  end;
end;

registration
  let W be with_non-empty_element set;
  cluster W-CL_category -> with_complete_lattices;
  coherence;
end;

theorem Th48:
  for W being with_non-empty_element set
  for L being LATTICE st the carrier of L in W
  holds L is Object of W-CL_category iff L is strict complete continuous
proof
  let W be with_non-empty_element set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: the carrier of W-INF(SC)_category c= the carrier of W-INF_category
  by ALTCAT_2:def 11;
A3: the carrier of W-CL_category c= the carrier of W-INF(SC)_category
  by ALTCAT_2:def 11;
  let L be LATTICE;
  assume
A4: the carrier of L in W;
  hereby
    assume
A5: L is Object of W-CL_category;
    then L in the carrier of W-CL_category;
    then reconsider a = L as Object of W-INF(SC)_category by A3;
A6: a in the carrier of W-INF(SC)_category;
    latt a is continuous by A5,Def12;
    hence L is strict complete continuous by A1,A2,A6,Def4;
  end;
  assume
A7: L is strict complete continuous;
  then L is Object of W-INF_category by A4,Def4;
  then reconsider a = L as Object of W-INF(SC)_category by Def10;
  latt a = L;
  hence thesis by A7,Def12;
end;

theorem Th49:
  for W being with_non-empty_element set for a,b being Object of W-CL_category
  for f being set holds f in <^a,b^> iff
  f is infs-preserving directed-sups-preserving Function of latt a, latt b
proof
  let W be with_non-empty_element set;
  let a,b be Object of W-CL_category, f be set;
  the carrier of W-CL_category c= the carrier of W-INF(SC)_category by
ALTCAT_2:def 11;
  then reconsider a1 = a, b1 = b as Object of W-INF(SC)_category;
  <^a,b^> = <^a1,b1^> by ALTCAT_2:28;
  hence thesis by Th44;
end;

definition :: 1.9. DEFINITION, p. 182
  let W be with_non-empty_element set;
  defpred P[Object of W-SUP(SO)_category] means latt $1 is continuous;
  consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
  set r = the upper-bounded well-ordering Order of a;
  set b = RelStr(#a,r#);
  func W-CL-opp_category ->
  strict full non empty subcategory of W-SUP(SO)_category means
  :
  Def13: for a being Object of W-SUP(SO)_category holds
  a is Object of it iff latt a is continuous;
  existence
  proof
    b is Object of W-SUP_category by A1,Def5;
    then reconsider b as Object of W-SUP(SO)_category by Def11;
    b = latt b;
    then
A2: ex b being Object of W-SUP(SO)_category st P[b];
    thus
    ex B being strict full non empty subcategory of W-SUP(SO)_category st
    for a being Object of W-SUP(SO)_category holds a is Object of B iff P[a]
    from YELLOW20:sch 2(A2);
  end;
  correctness
  proof
    let B1,B2 be strict full non empty subcategory of W-SUP(SO)_category
    such that
A3: for a being Object of W-SUP(SO)_category holds a is Object of B1 iff P[a]
    and
    A4: for
 a being Object of W-SUP(SO)_category holds a is Object of B2 iff P[a];
    the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3(A3,
    A4);
    hence thesis;
  end;
end;

theorem Th50:
  for W being with_non-empty_element set
  for L being LATTICE st the carrier of L in W
  holds L is Object of W-CL-opp_category iff L is strict complete continuous
proof
  let W be with_non-empty_element set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: the carrier of W-SUP(SO)_category c= the carrier of W-SUP_category
  by ALTCAT_2:def 11;
A3: the carrier of W-CL-opp_category c= the carrier of W-SUP(SO)_category
  by ALTCAT_2:def 11;
  let L be LATTICE;
  assume
A4: the carrier of L in W;
  hereby
    assume
A5: L is Object of W-CL-opp_category;
    then L in the carrier of W-CL-opp_category;
    then reconsider a = L as Object of W-SUP(SO)_category by A3;
A6: a in the carrier of W-SUP(SO)_category;
    latt a is continuous by A5,Def13;
    hence L is strict complete continuous by A1,A2,A6,Def5;
  end;
  assume
A7: L is strict complete continuous;
  then L is Object of W-SUP_category by A4,Def5;
  then reconsider a = L as Object of W-SUP(SO)_category by Def11;
  latt a = L;
  hence thesis by A7,Def13;
end;

theorem Th51:
  for W being with_non-empty_element set
  for a, b being Object of W-CL-opp_category for f being set
  holds f in <^a,b^> iff
  ex g being sups-preserving Function of latt a, latt b st g = f &
  UpperAdj g is directed-sups-preserving
proof
  let W be with_non-empty_element set;
  let a,b be Object of W-CL-opp_category, f be set;
  the carrier of W-CL-opp_category c= the carrier of W-SUP(SO)_category
  by ALTCAT_2:def 11;
  then reconsider a1 = a, b1 = b as Object of W-SUP(SO)_category;
  <^a,b^> = <^a1,b1^> by ALTCAT_2:28;
  hence thesis by Th46;
end;

:: 1.10. THEOREM, p. 182

theorem Th52:
  for W being with_non-empty_element set holds
  W-INF(SC)_category, W-SUP(SO)_category are_anti-isomorphic_under W LowerAdj
proof
  let W be with_non-empty_element set;
  set A1 = W-INF_category;
  set B1 = W-INF(SC)_category, B2 = W-SUP(SO)_category;
  set F = W LowerAdj;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: for a being Object of A1 holds
  a is Object of B1 iff F.a is Object of B2 by Def10,Def11;
A3: now
    let a,b be Object of A1 such that
A4: <^a,b^> <> {};
    let a1,b1 be Object of B1 such that
A5: a1 = a and
A6: b1 = b;
    let a2,b2 be Object of B2 such that
A7: a2 = F.a and
A8: b2 = F.b;
    let f be Morphism of a,b;
A9: <^F.b,F.a^> <> {} by A4,FUNCTOR0:def 19;
A10: @f = f by A4,YELLOW21:def 7;
A11: @(F.f) = F.f by A9,YELLOW21:def 7;
A12: F.a = latt a by Def6;
A13: F.b = latt b by Def6;
A14: F.f = LowerAdj @f by A4,Def6;
    reconsider g = f as infs-preserving Function
    of latt a1, latt b1 by A1,A4,A5,A6,A10,Def4;
    UpperAdj LowerAdj g = g by Th10;
    then f in <^a1,b1^> iff UpperAdj LowerAdj g is directed-sups-preserving
    by A4,A5,A6,A10,Def10;
    hence f in <^a1,b1^> iff F.f in <^b2,a2^> by A5,A6,A7,A8,A9,A10,A11,A12,A13
,A14,Def11;
  end;
  thus thesis by A2,A3,YELLOW20:57;
end;

theorem
  for W being with_non-empty_element set holds
  W-SUP(SO)_category, W-INF(SC)_category are_anti-isomorphic_under W UpperAdj
proof
  let W be with_non-empty_element set;
  W-SUP(SO)_category, W-INF(SC)_category
  are_anti-isomorphic_under (W LowerAdj)" by Th52,YELLOW20:51;
  hence thesis by Th18;
end;

theorem Th54:
  for W being with_non-empty_element set holds
  W-CL_category, W-CL-opp_category are_anti-isomorphic_under W LowerAdj
proof
  let W be with_non-empty_element set;
  set A1 = W-INF_category, A2 = W-SUP_category;
  reconsider B1 = W-CL_category as non empty subcategory of A1 by ALTCAT_4:36;
  reconsider B2 = W-CL-opp_category as non empty subcategory of A2
  by ALTCAT_4:36;
  set F = W LowerAdj;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: for a being Object of A1 holds a is Object of B1 iff F.a is Object of B2
  proof
    let a be Object of A1;
A3: F.a = latt a by Def6;
A4: the carrier of latt a in W by A1,Def4;
    then a is Object of B1 iff latt a is strict complete continuous by Th48;
    hence thesis by A3,A4,Th50;
  end;
A5: now
    let a,b be Object of A1 such that
A6: <^a,b^> <> {};
    let a1,b1 be Object of B1 such that
A7: a1 = a and
A8: b1 = b;
    let a2,b2 be Object of B2 such that
A9: a2 = F.a and
A10: b2 = F.b;
    let f be Morphism of a,b;
A11: @f = f by A6,YELLOW21:def 7;
A12: F.a = latt a by Def6;
A13: F.b = latt b by Def6;
A14: F.f = LowerAdj @f by A6,Def6;
    reconsider g = f as infs-preserving Function
    of latt a1, latt b1 by A1,A6,A7,A8,A11,Def4;
A15: UpperAdj LowerAdj g = g by Th10;
    then f in <^a1,b1^> iff UpperAdj LowerAdj g is directed-sups-preserving
    by Th49;
    hence f in <^a1,b1^> implies F.f in <^b2,a2^> by A7,A8,A9,A10,A11,A12,A13
,A14,Th51;
    assume F.f in <^b2,a2^>;
    then ex g being sups-preserving Function of latt b2, latt a2 st F.f = g &
    UpperAdj g is directed-sups-preserving by Th51;
    hence f in <^a1,b1^> by A7,A8,A9,A10,A11,A12,A13,A14,A15,Th49;
  end;
  B1,B2 are_anti-isomorphic_under F by A2,A5,YELLOW20:57;
  hence thesis;
end;

theorem
  for W being with_non-empty_element set holds
  W-CL-opp_category, W-CL_category are_anti-isomorphic_under W UpperAdj
proof
  let W be with_non-empty_element set;
  set A1 = W-INF_category, A2 = W-SUP_category;
  reconsider B1 = W-CL_category as non empty subcategory of A1 by ALTCAT_4:36;
  reconsider B2 = W-CL-opp_category as non empty subcategory of A2
  by ALTCAT_4:36;
  B2, B1 are_anti-isomorphic_under (W LowerAdj)" by Th54,YELLOW20:51;
  hence thesis by Th18;
end;

begin

::<section4>Compact preserving maps and sup-semilattices morphisms</section4>

definition
  let S,T be non empty reflexive RelStr;
  let f be Function of S,T;
  attr f is compact-preserving means
  for s being Element of S st s is compact holds f.s is compact;
end;

theorem Th56: :: 1.11. PROPOSITION, (1) => (2) p.183
  for S,T being complete LATTICE, d being sups-preserving Function of T,S
  st d is waybelow-preserving holds d is compact-preserving
proof
  let S,T be complete LATTICE, d be sups-preserving Function of T,S such that
A1: for t,t9 being Element of T st t << t9 holds d.t << d.t9;
  let t be Element of T;
  assume t << t;
  hence d.t << d.t by A1;
end;

theorem Th57: :: 1.11. PROPOSITION, (2) => (1) p.183
  for S,T being complete LATTICE, d being sups-preserving Function of T,S
  st T is algebraic & d is compact-preserving holds d is waybelow-preserving
proof
  let S,T be complete LATTICE, d be sups-preserving Function of T,S such that
A1: T is algebraic and
A2: for t being Element of T st t is compact holds d.t is compact;
  let t,t9 be Element of T;
  assume t << t9;
  then consider k being Element of T such that
A3: k in the carrier of CompactSublatt T and
A4: t <= k and
A5: k <= t9 by A1,WAYBEL_8:7;
  k is compact by A3,WAYBEL_8:def 1;
  then d.k is compact by A2;
  then
A6: d.k << d.k;
A7: d.t <= d.k by A4,WAYBEL_1:def 2;
  d.k <= d.t9 by A5,WAYBEL_1:def 2;
  hence thesis by A6,A7,WAYBEL_3:2;
end;

theorem Th58:
  for R,S,T being non empty RelStr, X being Subset of R
  for f being Function of R,S for g being Function of S,T
  st f preserves_sup_of X & g preserves_sup_of f.:X
  holds g*f preserves_sup_of X
proof
  let R,S,T be non empty RelStr, X be Subset of R;
  let f be Function of R,S;
  let g be Function of S,T such that
A1: ex_sup_of X, R implies ex_sup_of f.:X, S & sup (f.:X) = f.sup X and
A2: ex_sup_of f.:X, S implies
  ex_sup_of g.:(f.:X), T & sup (g.:(f.:X)) = g.sup (f.:X);
A3: g.:(f.:X) = (g*f).:X by RELAT_1:126;
  assume ex_sup_of X, R;
  hence thesis by A1,A2,A3,FUNCT_2:15;
end;

definition
  let S,T be non empty RelStr;
  let f be Function of S,T;
  attr f is finite-sups-preserving means
  for X being finite Subset of S holds f preserves_sup_of X;
  attr f is bottom-preserving means

  f preserves_sup_of {}S;
end;

theorem
  for R,S,T being non empty RelStr
  for f being Function of R,S for g being Function of S,T
  st f is finite-sups-preserving & g is finite-sups-preserving
  holds g*f is finite-sups-preserving
proof
  let R,S,T be non empty RelStr;
  let f be Function of R,S;
  let g be Function of S,T such that
A1: for X being finite Subset of R holds f preserves_sup_of X and
A2: for X being finite Subset of S holds g preserves_sup_of X;
  let X be finite Subset of R;
  g preserves_sup_of f.:X by A2;
  hence thesis by A1,Th58;
end;

definition
  let S,T be non empty antisymmetric lower-bounded RelStr;
  let f be Function of S,T;
  redefine attr f is bottom-preserving means
  : Def17:
  f.Bottom S = Bottom T;
  compatibility
  proof
    thus f is bottom-preserving implies f.Bottom S = Bottom T
    proof
      assume f preserves_sup_of {}S;
      then ex_sup_of {}S, S implies sup (f.:{}S) = f.sup {}S;
      hence thesis by YELLOW_0:42;
    end;
    assume that
A1: f.Bottom S = Bottom T and ex_sup_of {}S, S;
    thus ex_sup_of f.:{}S, T by YELLOW_0:42;
    thus thesis by A1;
  end;
end;

definition
  let L be non empty RelStr;
  let S be SubRelStr of L;
  attr S is finite-sups-inheriting means
   for X being finite Subset of S st ex_sup_of X,L
  holds "\/"(X,L) in the carrier of S;
  attr S is bottom-inheriting means
  : Def19:
  Bottom L in the carrier of S;
end;

registration
  let S,T be non empty RelStr;
  cluster sups-preserving -> bottom-preserving for Function of S,T;
  coherence;
end;

registration
  let L be lower-bounded antisymmetric non empty RelStr;
  cluster finite-sups-inheriting ->
    bottom-inheriting join-inheriting for SubRelStr of L;
  coherence
  proof
    let S be SubRelStr of L;
    assume
A1: S is finite-sups-inheriting;
    then ex_sup_of {}, L implies "\/" ({}S, L) in the carrier of S;
    hence Bottom L in the carrier of S by YELLOW_0:42;
    let x,y be Element of L;
    assume that
A2: x in the carrier of S and
A3: y in the carrier of S;
    reconsider X = {x,y} as finite Subset of S by A2,A3,ZFMISC_1:32;
    ex_sup_of X,L implies "\/"(X,L) in the carrier of S by A1;
    hence thesis;
  end;
end;

registration
  let L be non empty RelStr;
  cluster sups-inheriting -> finite-sups-inheriting for SubRelStr of L;
  coherence;
end;

registration
  let S,T be lower-bounded non empty Poset;
  cluster sups-preserving for Function of S,T;
  existence
  proof set f = the sups-preserving Function of S,T;
    take f;
    thus thesis;
  end;
end;

registration
  let L be lower-bounded antisymmetric non empty RelStr;
  cluster bottom-inheriting -> non empty lower-bounded for
full SubRelStr of L;
  coherence
  proof
    let S be full SubRelStr of L;
    assume
A1: Bottom L in the carrier of S;
    hence
A2: S is non empty;
    reconsider x = Bottom L as Element of S by A1;
    take x;
    let y be Element of S;
    assume
A3: y in the carrier of S;
    reconsider a = y as Element of L by A2,YELLOW_0:58;
    Bottom L <= a by YELLOW_0:44;
    hence thesis by A3,YELLOW_0:60;
  end;
end;

registration
  let L be lower-bounded antisymmetric non empty RelStr;
  cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting
    full for SubRelStr of L;
  existence
  proof set S = the non empty sups-inheriting full SubRelStr of L;
    take S;
    thus thesis;
  end;
end;

theorem Th60:
  for L being lower-bounded antisymmetric non empty RelStr
  for S being non empty bottom-inheriting full SubRelStr of L
  holds Bottom S = Bottom L
proof
  let L be lower-bounded antisymmetric non empty RelStr;
  let S be non empty bottom-inheriting full SubRelStr of L;
  reconsider s = Bottom L as Element of S by Def19;
  reconsider l = Bottom S as Element of L by YELLOW_0:58;
A1: Bottom L <= l by YELLOW_0:44;
A2: Bottom S <= s by YELLOW_0:44;
  Bottom S >= s by A1,YELLOW_0:60;
  hence thesis by A2,ORDERS_2:2;
end;

registration
  let L be with_suprema lower-bounded non empty Poset;
  cluster bottom-inheriting join-inheriting -> finite-sups-inheriting
    for full SubRelStr of L;
  coherence
  proof
    let S be full SubRelStr of L;
    assume S is bottom-inheriting join-inheriting;
    then reconsider S9 = S as join-inheriting bottom-inheriting full SubRelStr
    of L;
    let X be finite Subset of S;
    reconsider X9 = X as Subset of S9;
A1: X is finite;
    defpred P[set] means for Y being finite Subset of S9 st Y = $1
    holds ex_sup_of Y,L & "\/"(Y, L) = sup Y;
A2: Bottom L = "\/"({}, L);
    Bottom S9 = "\/"({}, S9);
    then
A3: P[{}] by A2,Th60,YELLOW_0:42;
A4: for x,B being set st x in X & B c= X & P[B] holds P[B \/ {x}]
    proof
      let x,B be set such that x in X and B c= X and
A5:   for Y being finite Subset of S9 st Y = B
      holds ex_sup_of Y,L & "\/"(Y, L) = sup Y;
      let Y be finite Subset of S9 such that
A6:   Y = B \/ {x};
A7:   B c= Y by A6,XBOOLE_1:7;
A8:   {x} c= Y by A6,XBOOLE_1:7;
      reconsider Z = B as finite Subset of S9 by A7,XBOOLE_1:1;
A9:   ex_sup_of Z,L by A5;
A10:  "\/"(Z, L) = sup Z by A5;
      x in Y by A8,ZFMISC_1:31;
      then reconsider x as Element of S9;
      reconsider a = x as Element of L by YELLOW_0:58;
A11:  ex_sup_of {a}, L by YELLOW_0:38;
      hence ex_sup_of Y,L by A6,A9,YELLOW_2:3;
A12:  Z = {} or Z <> {} & S9 is with_suprema;
A13:  ex_sup_of {x}, S9 by YELLOW_0:54;
A14:  ex_sup_of Z, S9 by A12,YELLOW_0:42,54;
      thus "\/"(Y, L) = "\/"(Z, L) "\/" sup {a} by A6,A9,A11,YELLOW_2:3
        .= "\/"(Z, L) "\/" a by YELLOW_0:39
        .= (sup Z) "\/" x by A10,YELLOW_0:70
        .= (sup Z) "\/" sup {x} by YELLOW_0:39
        .= sup Y by A6,A13,A14,YELLOW_2:3;
    end;
    P[X] from FINSET_1:sch 2(A1,A3,A4);
    then "\/"(X, L) = sup X9;
    hence thesis;
  end;
end;

theorem
  for S,T being non empty RelStr, f being Function of S,T
  st f is finite-sups-preserving holds f is join-preserving bottom-preserving;

theorem Th62:
  for S,T being lower-bounded with_suprema Poset, f being Function of S,T
  st f is join-preserving bottom-preserving holds f is finite-sups-preserving
proof
  let S,T be lower-bounded with_suprema Poset, f be Function of S,T;
  assume
A1: f is join-preserving bottom-preserving;
  let X be finite Subset of S;
A2: X is finite;
  defpred P[set] means
  for Y being finite Subset of S st Y = $1 holds f preserves_sup_of Y;
  f preserves_sup_of {}S by A1;
  then
A3: P[{}];
A4: for x,B being set st x in X & B c= X & P[B] holds P[B \/ {x}]
  proof
    let x,B be set such that x in X and B c= X and
A5: for Y being finite Subset of S st Y = B holds f preserves_sup_of Y;
    let Y be finite Subset of S such that
A6: Y = B \/ {x};
A7: B c= Y by A6,XBOOLE_1:7;
A8: {x} c= Y by A6,XBOOLE_1:7;
    reconsider Z = B as finite Subset of S by A7,XBOOLE_1:1;
A9: x in Y by A8,ZFMISC_1:31;
    then reconsider x as Element of S;
A10: f preserves_sup_of Z by A5;
    f.:Z = {} or f.:Z <> {} & f.:Z is finite;
    then
A11: ex_sup_of f.:Z,T by YELLOW_0:42,54;
A12: ex_sup_of {f.x},T by YELLOW_0:54;
    Z = {} or Z <> {};
    then
A13: ex_sup_of Z,S by YELLOW_0:42,54;
A14: f preserves_sup_of {sup Z, x} by A1;
A15: sup {x} = x by YELLOW_0:39;
A16: ex_sup_of {x}, S by YELLOW_0:38;
A17: ex_sup_of Y,S by A9,YELLOW_0:54;
    assume ex_sup_of Y,S;
    thus ex_sup_of f.:Y,T by A9,YELLOW_0:54;
    dom f = the carrier of S by FUNCT_2:def 1;
    then Im(f,x) = {f.x} by FUNCT_1:59;
    then
A18: f.:Y = (f.:Z) \/ {f.x} by A6,RELAT_1:120;
    sup {f.x} = f.x by YELLOW_0:39;
    hence sup (f.:Y) = (sup (f.:Z)) "\/" (f.x) by A11,A12,A18,YELLOW_2:3
      .= (f.(sup Z)) "\/" (f.x) by A10,A13
      .= f.((sup Z) "\/" x) by A14,YELLOW_3:9
      .= f.sup Y by A6,A13,A15,A16,A17,YELLOW_0:36;
  end;
  P[X] from FINSET_1:sch 2(A2,A3,A4);
  hence thesis;
end;

registration
  let S,T be non empty RelStr;
  cluster sups-preserving -> finite-sups-preserving for Function of S,T;
  coherence;
  cluster finite-sups-preserving ->
    join-preserving bottom-preserving for Function of S,T;
  coherence;
end;

registration
  let S be non empty RelStr;
  let T be lower-bounded non empty reflexive antisymmetric RelStr;
  cluster sups-preserving finite-sups-preserving for Function of S,T;
  existence
  proof set f = the sups-preserving Function of S,T;
    take f;
    thus thesis;
  end;
end;

registration :: WAYBEL13:15
  let L be lower-bounded non empty Poset;
  cluster CompactSublatt L -> lower-bounded;
  coherence
  proof Bottom L is compact by WAYBEL_3:15;
    then reconsider c = Bottom L as Element of CompactSublatt L by
WAYBEL_8:def 1;
    take c;
    let b be Element of CompactSublatt L such that
    b in the carrier of CompactSublatt L;
    reconsider x = b as Element of L by YELLOW_0:58;
    Bottom L <= x by YELLOW_0:44;
    hence c <= b by YELLOW_0:60;
  end;
end;

theorem Th63:
  for S being RelStr, T being non empty RelStr, f being Function of S,T
  for S9 being SubRelStr of S for T9 being SubRelStr of T
  st f.:the carrier of S9 c= the carrier of T9
  holds f|the carrier of S9 is Function of S9, T9
proof
  let S be RelStr, T be non empty RelStr, f be Function of S,T;
  let S9 be SubRelStr of S, T9 be SubRelStr of T such that
A1: f.:the carrier of S9 c= the carrier of T9;
  set g = f|the carrier of S9;
A2: dom f = the carrier of S by FUNCT_2:def 1;
  the carrier of S9 c= the carrier of S by YELLOW_0:def 13;
  then
A3: dom g = the carrier of S9 by A2,RELAT_1:62;
  rng g = f.:the carrier of S9 by RELAT_1:115;
  hence thesis by A1,A3,FUNCT_2:2;
end;

theorem Th64:
  for S,T being LATTICE, f being join-preserving Function of S,T
  for S9 being non empty join-inheriting full SubRelStr of S
  for T9 being non empty join-inheriting full SubRelStr of T
  for g being Function of S9, T9 st g = f|the carrier of S9
  holds g is join-preserving
proof
  let S,T be LATTICE, f be join-preserving Function of S,T;
  let S9 be non empty join-inheriting full SubRelStr of S;
  let T9 be non empty join-inheriting full SubRelStr of T;
  let g be Function of S9, T9 such that
A1: g = f|the carrier of S9;
  now
    let x,y be Element of S9;
    reconsider a = x, b = y as Element of S by YELLOW_0:58;
    x"\/"y = a"\/"b by YELLOW_0:70;
    then
A2: g.(x"\/"y) = f.(a"\/"b) by A1,FUNCT_1:49;
A3: g.x = f.a by A1,FUNCT_1:49;
A4: g.y = f.b by A1,FUNCT_1:49;
    thus g.(x"\/"y) = (f.a)"\/"(f.b) by A2,WAYBEL_6:2
      .= (g.x)"\/"(g.y) by A3,A4,YELLOW_0:70;
  end;
  hence thesis by WAYBEL_6:2;
end;

theorem Th65:
  for S,T being lower-bounded LATTICE
  for f being finite-sups-preserving Function of S,T
  for S9 being non empty finite-sups-inheriting full SubRelStr of S
  for T9 being non empty finite-sups-inheriting full SubRelStr of T
  for g being Function of S9, T9 st g = f|the carrier of S9
  holds g is finite-sups-preserving
proof
  let S,T be lower-bounded LATTICE;
  let f be finite-sups-preserving Function of S,T;
  let S9 be non empty finite-sups-inheriting full SubRelStr of S;
  let T9 be non empty finite-sups-inheriting full SubRelStr of T;
  let g be Function of S9, T9 such that
A1: g = f|the carrier of S9;
  Bottom S9 = Bottom S by Th60;
  then g.Bottom S9 = f.Bottom S by A1,FUNCT_1:49
    .= Bottom T by Def17
    .=
  Bottom T9 by Th60;
  then g is bottom-preserving;
  hence thesis by A1,Th62,Th64;
end;

registration
  let L be complete LATTICE;
  cluster CompactSublatt L -> finite-sups-inheriting;
  coherence
  proof
    Bottom L in the carrier of CompactSublatt L by WAYBEL_8:3;
    then CompactSublatt L is bottom-inheriting join-inheriting non empty
    full SubRelStr of L by Def19;
    hence thesis;
  end;
end;

theorem Th66:
  for S,T being complete LATTICE
  for d being sups-preserving Function of T,S holds d is compact-preserving
  iff d|the carrier of CompactSublatt T is
  finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
proof
  let S,T be complete LATTICE, d be sups-preserving Function of T,S;
  thus
  d is compact-preserving implies d|the carrier of CompactSublatt T is
  finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
  proof
    assume
A1: for x being Element of T st x is compact holds d.x is compact;
    d.:the carrier of CompactSublatt T c= the carrier of CompactSublatt S
    proof
      let y be object;
      assume y in d.: the carrier of CompactSublatt T;
      then consider x being object such that
A2:   x in the carrier of T and
A3:   x in the carrier of CompactSublatt T and
A4:   y = d.x by FUNCT_2:64;
      reconsider x as Element of T by A2;
      x is compact by A3,WAYBEL_8:def 1;
      then d.x is compact by A1;
      hence thesis by A4,WAYBEL_8:def 1;
    end;
    hence thesis by Th63,Th65;
  end;
  assume
A5: d|the carrier of CompactSublatt T is
  finite-sups-preserving Function of CompactSublatt T, CompactSublatt S;
  let x be Element of T;
  assume x is compact;
  then
A6: x in the carrier of CompactSublatt T by WAYBEL_8:def 1;
  then d.x = (d|the carrier of CompactSublatt T).x by FUNCT_1:49;
  then d.x in the carrier of CompactSublatt S by A5,A6,FUNCT_2:5;
  hence thesis by WAYBEL_8:def 1;
end;

theorem :: 1.12. COROLLARY, p. 183
  for S,T being complete LATTICE st T is algebraic
  for g being infs-preserving Function of S,T holds
  g is directed-sups-preserving iff
  (LowerAdj g)|the carrier of CompactSublatt T is
  finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
proof
  let S,T be complete LATTICE such that
A1: T is algebraic;
  let g be infs-preserving Function of S,T;
  hereby
    assume g is directed-sups-preserving;
    then LowerAdj g is waybelow-preserving by Th22;
    then LowerAdj g is compact-preserving by Th56;
    hence (LowerAdj g)|the carrier of CompactSublatt T is
    finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
    by Th66;
  end;
  assume (LowerAdj g)|the carrier of CompactSublatt T is
  finite-sups-preserving Function of CompactSublatt T, CompactSublatt S;
  then LowerAdj g is compact-preserving by Th66;
  then LowerAdj g is waybelow-preserving by A1,Th57;
  hence thesis by A1,Th23;
end;