The Mizar article:

Galois Connections

by
Czeslaw Bylinski

Received September 25, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: WAYBEL_1
[ MML identifier index ]


environ

 vocabulary FUNCT_1, RELAT_1, PRE_TOPC, ORDERS_1, SEQM_3, RELAT_2, LATTICE3,
      LATTICES, WAYBEL_0, YELLOW_1, BOOLE, YELLOW_0, CAT_1, WELLORD1, ORDINAL2,
      BHSP_3, FILTER_0, FILTER_2, BINOP_1, SGRAPH1, GROUP_6, QUANTAL1,
      YELLOW_2, LATTICE2, ZF_LANG, FILTER_1, WAYBEL_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      PRE_TOPC, STRUCT_0, WELLORD1, ORDERS_1, LATTICE3, QUANTAL1, ORDERS_3,
      YELLOW_0, GRCAT_1, YELLOW_1, WAYBEL_0, YELLOW_2;
 constructors TOPS_2, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, GRCAT_1;
 clusters STRUCT_0, RELSET_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0,
      RELAT_1, FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, WAYBEL_0,
      XBOOLE_0;
 theorems STRUCT_0, ZFMISC_1, ORDERS_1, FUNCT_1, FUNCT_2, LATTICE3, RELAT_1,
      TARSKI, WELLORD1, TMAP_1, ORDERS_3, YELLOW_0, YELLOW_1, YELLOW_2,
      WAYBEL_0, GRCAT_1, RELSET_1, XBOOLE_0, XBOOLE_1;
 schemes FUNCT_2, YELLOW_2;

begin :: Preliminaries

definition let L1,L2 be non empty 1-sorted, f be map of L1,L2;
 redefine attr f is one-to-one means
     for x,y being Element of L1 st f.x = f.y holds x=y;
  compatibility
 proof
  thus f is one-to-one implies
   for x,y being Element of L1 st f.x = f.y holds x=y
    by FUNCT_2:25;
  assume
A1: for x,y being Element of L1 st f.x = f.y holds x=y;
     for x,y be set st x in the carrier of L1 & y in the carrier of L1
     holds f.x = f.y implies x=y by A1;
   hence thesis by FUNCT_2:25;
 end;
end;

theorem Th1:
  for L being non empty 1-sorted, f being map of L,L
    st for x being Element of L holds f.x = x
   holds f = id L by TMAP_1:92;

definition let L1,L2 be non empty RelStr, f be map of L1,L2;
 redefine attr f is monotone means
:Def2: for x,y being Element of L1 st x <= y holds f.x <= f.y;
  compatibility
 proof
  thus f is monotone implies
    for x,y being Element of L1 st x <= y holds f.x <= f.y by ORDERS_3:def 5;
  assume for x,y being Element of L1 st x <= y holds f.x <= f.y;
  hence for x,y being Element of L1 st x <= y
   for a,b being Element of L2 st a = f.x & b = f.y holds a <= b;
 end;
end;

theorem Th2:
   for L being antisymmetric transitive with_infima RelStr,
       x,y,z being Element of L
     st x <= y holds x "/\" z <= y "/\" z
 proof let L be antisymmetric transitive with_infima RelStr;
  let x,y,z be Element of L;
  assume
A1:  x <= y;
    x"/\"z <= x by YELLOW_0:23;
  then x"/\"z <= y & x"/\"z <= z by A1,ORDERS_1:26,YELLOW_0:23;
  hence x"/\"z <= y"/\"z by YELLOW_0:23;
 end;

theorem Th3:
   for L being antisymmetric transitive with_suprema RelStr,
       x,y,z being Element of L
     st x <= y holds x "\/" z <= y "\/" z
 proof let L be antisymmetric transitive with_suprema RelStr;
  let x,y,z be Element of L;
  assume
A1:  x <= y;
    y <= y"\/"z by YELLOW_0:22;
  then x <= y"\/"z & z <= y"\/"z by A1,ORDERS_1:26,YELLOW_0:22;
  hence x"\/"z <= y"\/"z by YELLOW_0:22;
 end;

theorem Th4:
 for L being non empty lower-bounded antisymmetric RelStr
  for x being Element of L holds
 (L is with_infima implies Bottom L "/\" x = Bottom L) &
 (L is with_suprema reflexive transitive implies Bottom L "\/" x = x)
 proof let L be non empty lower-bounded antisymmetric RelStr;
       let x be Element of L;
 thus L is with_infima implies Bottom L "/\" x = Bottom L
  proof
   assume L is with_infima;
   then Bottom L <= Bottom L "/\" x & Bottom L "/\" x <= Bottom L by YELLOW_0:
23,44;
   hence Bottom L "/\" x = Bottom L by ORDERS_1:25;
  end;
  assume
A1:  L is with_suprema;
  assume
   L is reflexive transitive;
then A2:  x <= x by ORDERS_1:24;
    Bottom L <= x by YELLOW_0:44;
  then x <= Bottom L "\/" x & Bottom L "\/" x <= x by A1,A2,YELLOW_0:22;
  hence Bottom L "\/" x = x by ORDERS_1:25;
 end;

theorem Th5:
 for L being non empty upper-bounded antisymmetric RelStr
  for x being Element of L holds
 (L is with_infima transitive reflexive implies Top L "/\" x = x) &
 (L is with_suprema implies Top L "\/" x = Top L)
 proof let L be non empty upper-bounded antisymmetric RelStr,
           x be Element of L;
  thus L is with_infima transitive reflexive implies Top L "/\" x = x
  proof assume
A1: L is with_infima transitive reflexive;
     x <= Top L by YELLOW_0:45;
   then x "/\" x <= Top L "/\" x by A1,Th2;
   then Top L "/\" x <= x & x <= Top L "/\" x by A1,YELLOW_0:23,25;
   hence Top L "/\" x = x by ORDERS_1:25;
  end;
  assume L is with_suprema;
  then Top L "\/" x <= Top L & Top L <= Top L "\/" x by YELLOW_0:22,45;
  hence Top L "\/" x = Top L by ORDERS_1:25;
 end;

definition let L be non empty RelStr;
 attr L is distributive means
:Def3: for x,y,z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/"
 (x "/\" z);
end;

theorem Th6:
   for L being LATTICE
    holds L is distributive iff
     for x,y,z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x
"\/" z)
 proof let L be LATTICE;
   hereby
    assume
A1:   L is distributive;
    let x,y,z be Element of L;
    thus x"\/"(y"/\"z) = (x"\/"(z"/\"x))"\/"(y"/\"z) by LATTICE3:17
                  .= x"\/"((z"/\"x)"\/"(z"/\"y)) by LATTICE3:14
                  .= x"\/"((x"\/"y)"/\"z) by A1,Def3
                  .= ((x"\/"y)"/\"x)"\/"((x"\/"y)"/\"z) by LATTICE3:18
                  .= (x"\/"y)"/\"(x"\/"z) by A1,Def3;

   end;
  assume
A2:  for x,y,z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x
"\/" z);
  let x,y,z be Element of L;
  thus x"/\"(y"\/"z) = (x"/\"(x"\/"z))"/\"(y"\/"z) by LATTICE3:18
                .= x"/\"((z"\/"x)"/\"(y"\/"z)) by LATTICE3:16
                .= x"/\"(z"\/"(x"/\"y)) by A2
                .= ((y"/\"x)"\/"x)"/\"((x"/\"y)"\/"z) by LATTICE3:17
                .= (x"/\"y)"\/"(x"/\"z) by A2;
 end;

definition let X be set;
 cluster BoolePoset X -> distributive;
  coherence
 proof
   let x,y,z be Element of BoolePoset X;
   thus x"/\"(y"\/"z) = x /\ (y"\/"z) by YELLOW_1:17
                 .= x /\ (y \/ z) by YELLOW_1:17
                 .= x/\y \/ x/\z by XBOOLE_1:23
                 .= (x"/\"y)\/(x/\z) by YELLOW_1:17
                 .= (x"/\"y)\/(x"/\"z) by YELLOW_1:17
                 .= (x"/\"y)"\/"(x"/\"z) by YELLOW_1:17;
 end;
end;


definition let S be non empty RelStr, X be set;
  pred ex_min_of X,S means
    ex_inf_of X,S & "/\"(X,S) in X;
   synonym X has_the_min_in S;
  pred ex_max_of X,S means
:Def5:  ex_sup_of X,S & "\/"(X,S) in X;
   synonym X has_the_max_in S;
end;

definition
 let S be non empty RelStr, s be Element of S, X be set;
  pred s is_minimum_of X means
:Def6:  ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S) in X;
  pred s is_maximum_of X means
:Def7:  ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S)in X;
end;

definition let L be RelStr;
 cluster id L -> isomorphic;
  coherence
 proof
  per cases;
  suppose
A1:  L is non empty;
A2:  id L = id the carrier of L by GRCAT_1:def 11;
then A3:  id L is one-to-one;
A4:  id L is monotone by A1,YELLOW_2:13;
A6: id L = (id L)" by A2,FUNCT_1:67;
   thus thesis by A1,A3,A4,A6,WAYBEL_0:def 38;
  suppose L is empty;
   hence thesis by WAYBEL_0:def 38;
 end;
end;

definition let L1,L2 be RelStr;
 pred L1,L2 are_isomorphic means
:Def8:  ex f being map of L1,L2 st f is isomorphic;
 reflexivity
  proof let L be RelStr;
   take id L;
   thus thesis;
  end;
end;

theorem
     for L1,L2 be non empty RelStr st L1,L2 are_isomorphic
    holds L2,L1 are_isomorphic
 proof let L1,L2 be non empty RelStr;
  given f being map of L1,L2 such that
A1:  f is isomorphic;
  consider g being map of L2,L1 such that
A2:  g = (f qua Function)" and
A3:  g is monotone by A1,WAYBEL_0:def 38;
A4:  f is one-to-one by A1,WAYBEL_0:def 38;
then A5:  g is one-to-one by A2,FUNCT_1:62;
A6:  f is monotone by A1,WAYBEL_0:def 38;
    f = (g qua Function)" by A2,A4,FUNCT_1:65;
  then g is isomorphic by A3,A5,A6,WAYBEL_0:def 38;
  hence thesis by Def8;
 end;

theorem
     for L1,L2,L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic
    holds L1,L3 are_isomorphic
 proof let L1,L2,L3 be RelStr;
  given f1 being map of L1,L2 such that
A1:  f1 is isomorphic;
  given f2 being map of L2,L3 such that
A2:  f2 is isomorphic;
A3: now assume L1 is empty;
     then the carrier of L1 is empty by STRUCT_0:def 1;
     then f2*f1 is Function of the carrier of L1,the carrier of L3
      by FUNCT_2:19;
     hence f2*f1 is map of L1,L3;
    end;
  per cases;
  suppose L1 is non empty & L2 is non empty & L3 is non empty;
   then reconsider L1,L2,L3 as non empty RelStr;
   reconsider f1 as map of L1,L2;
   reconsider f2 as map of L2,L3;
   consider g1 being map of L2,L1 such that
A4:  g1 = (f1 qua Function)" and
A5:  g1 is monotone by A1,WAYBEL_0:def 38;
A6:  f1 is one-to-one by A1,WAYBEL_0:def 38;
A7:  f1 is monotone by A1,WAYBEL_0:def 38;
   consider g2 being map of L3,L2 such that
A8:  g2 = (f2 qua Function)" and
A9:  g2 is monotone by A2,WAYBEL_0:def 38;
A10:  f2 is one-to-one by A2,WAYBEL_0:def 38;
A11:  f2 is monotone by A2,WAYBEL_0:def 38;
A12:  f2*f1 is one-to-one by A6,A10,FUNCT_1:46;
A13:  f2*f1 is monotone by A7,A11,YELLOW_2:14;
A14:  g1*g2 is monotone by A5,A9,YELLOW_2:14;
     g1*g2 = ((f2*f1) qua Function)" by A4,A6,A8,A10,FUNCT_1:66;
   then f2*f1 is isomorphic by A12,A13,A14,WAYBEL_0:def 38;
   hence thesis by Def8;
  suppose
A15:  L1 is empty;
   then L2 is empty by A1,WAYBEL_0:def 38;
then A16:  L3 is empty by A2,WAYBEL_0:def 38;
   reconsider f = f2*f1 as map of L1,L3 by A3,A15;
     f is isomorphic by A15,A16,WAYBEL_0:def 38;
   hence thesis by Def8;
  suppose A17: L2 is empty;
then A18:  L1 is empty & L3 is empty by A1,A2,WAYBEL_0:def 38;
   reconsider f = f2*f1 as map of L1,L3 by A1,A3,A17,WAYBEL_0:def 38;
     f is isomorphic by A18,WAYBEL_0:def 38;
   hence thesis by Def8;
  suppose
A19:  L3 is empty;
   then A20: L2 is empty by A2,WAYBEL_0:def 38;
then A21:  L1 is empty by A1,WAYBEL_0:def 38;
   reconsider f = f2*f1 as map of L1,L3 by A1,A3,A20,WAYBEL_0:def 38;
     f is isomorphic by A19,A21,WAYBEL_0:def 38;
   hence thesis by Def8;
 end;

begin :: Galois Connections

definition let S,T be RelStr;
   mode Connection of S,T -> set means
:Def9:  ex g being map of S,T, d being map of T,S st it = [g,d];
  existence
 proof consider g being map of S,T, d being map of T,S;
   take [g,d]; thus thesis;
 end;
end;

definition let S,T be RelStr, g be map of S,T, d be map of T,S;
 redefine func [g,d] -> Connection of S,T;
  coherence by Def9;
end;

:: Definition 3.1
definition let S,T be non empty RelStr, gc be Connection of S,T;
  attr gc is Galois means
:Def10: ex g being map of S,T, d being map of T,S
    st gc = [g,d] & g is monotone & d is monotone &
     for t being Element of T, s being Element of S
      holds t <= g.s iff d.t <= s;
end;

theorem Th9:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   holds [g,d] is Galois iff
     g is monotone & d is monotone &
      for t being Element of T, s being Element of S holds t <= g.s iff d.t <=
 s
proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
 hereby assume [g,d] is Galois;
   then consider g' being map of S,T, d' being map of T,S
    such that
A1:   [g,d] = [g',d'] and
A2:   g' is monotone & d' is monotone &
      for t being Element of T, s being Element of S
       holds t <= g'.s iff d'.t <= s by Def10;
     g = g' & d = d' by A1,ZFMISC_1:33;
  hence g is monotone & d is monotone &
   for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s
    by A2;
 end;
 thus thesis by Def10;
end;

:: Definition 3.1
definition let S,T be non empty RelStr, g be map of S,T;
 attr g is upper_adjoint means
:Def11:  ex d being map of T,S st [g,d] is Galois;
 synonym g has_a_lower_adjoint;
end;

:: Definition 3.1
definition let S,T be non empty RelStr, d be map of T,S;
 attr d is lower_adjoint means
:Def12:  ex g being map of S,T st [g,d] is Galois;
 synonym d has_an_upper_adjoint;
end;

theorem Th10:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   st [g,d] is Galois holds g is upper_adjoint & d is lower_adjoint
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume
A1: [g,d] is Galois;
  hence ex d being map of T,S st [g,d] is Galois;
  thus ex g being map of S,T st [g,d] is Galois by A1;
 end;

:: Theorem 3.2  (1) iff (2)
theorem Th11:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   holds [g,d] is Galois iff
    g is monotone &
     for t being Element of T holds d.t is_minimum_of g"(uparrow t)
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  hereby
   assume
A1:   [g,d] is Galois;
   hence g is monotone by Th9;
   let t be Element of T;
   thus d.t is_minimum_of g"(uparrow t)
    proof
     set X = g"(uparrow t);
A2:    d.t is_<=_than X
      proof let s be Element of S;
       assume s in X;
       then g.s in uparrow t by FUNCT_1:def 13;
       then t <= g.s by WAYBEL_0:18;
       hence d.t <= s by A1,Th9;
      end;
       t <= g.(d.t) by A1,Th9;
     then g.(d.t) in uparrow t by WAYBEL_0:18;
then A3:    d.t in X by FUNCT_2:46;
     then A4: for s being Element of S st s is_<=_than
 X holds d.t >= s by LATTICE3:def 8;
     hence ex_inf_of X,S & d.t = inf X by A2,YELLOW_0:31;
     thus inf X in X by A2,A3,A4,YELLOW_0:31;
    end;
  end;
  assume that
A5: g is monotone and
A6: for t being Element of T holds d.t is_minimum_of g"(uparrow t);
A7: d is monotone
   proof let t1,t2 be Element of T;
    assume
A8:   t1 <= t2;
A9:   d.t1 is_minimum_of g"(uparrow t1) by A6;
then A10:   ex_inf_of g"(uparrow t1),S by Def6;
A11:   d.t2 is_minimum_of g"(uparrow t2) by A6;
then A12:   ex_inf_of g"(uparrow t2),S by Def6;
      uparrow t2 c= uparrow t1 by A8,WAYBEL_0:22;
    then g"(uparrow t2) c= g"(uparrow t1) by RELAT_1:178;
    then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A10,A12,YELLOW_0:35;
    then d.t1 <= inf (g"(uparrow t2)) by A9,Def6;
    hence d.t1 <= d.t2 by A11,Def6;
   end;
    for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s
   proof let t be Element of T, s be Element of S;
    set X = g"(uparrow t);
A13:  d.t is_minimum_of X by A6;
    hereby
     assume t <= g.s;
     then g.s in uparrow t by WAYBEL_0:18;
then A14:    s in X by FUNCT_2:46;
A15:    d.t is_minimum_of g"(uparrow t) by A6;
      then ex_inf_of X,S by Def6;
      then X is_>=_than inf X by YELLOW_0:def 10;
      then s >= inf X by A14,LATTICE3:def 8;
     hence d.t <= s by A15,Def6;
    end;
    assume d.t <= s;
then A16:    g.(d.t) <= g.s by A5,Def2;
       inf X in X by A13,Def6;
     then g.(inf X) in uparrow t by FUNCT_1:def 13;
     then g.(inf X) >= t by WAYBEL_0:18;
     then g.(d.t) >= t by A13,Def6;
     hence t <= g.s by A16,ORDERS_1:26;
   end;
  hence thesis by A5,A7,Th9;
 end;

:: Theorem 3.2 (1) iff (3)
theorem Th12:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   holds [g,d] is Galois iff
     d is monotone &
      for s being Element of S holds g.s is_maximum_of d"(downarrow s)
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  hereby
   assume
A1:   [g,d] is Galois;
   hence d is monotone by Th9;
   let s be Element of S;
   thus g.s is_maximum_of d"(downarrow s)
    proof
     set X = d"(downarrow s);
A2:    g.s is_>=_than X
      proof let t be Element of T;
       assume t in X;
       then d.t in downarrow s by FUNCT_1:def 13;
       then s >= d.t by WAYBEL_0:17;
       hence g.s >= t by A1,Th9;
      end;
      s >= d.(g.s) by A1,Th9;
    then d.(g.s) in downarrow s by WAYBEL_0:17;
then A3:   g.s in X by FUNCT_2:46;
     then A4: for t being Element of T st t is_>=_than X holds g.s <= t
      by LATTICE3:def 9;
     hence ex_sup_of X,T & g.s = sup X by A2,YELLOW_0:30;
     thus sup X in X by A2,A3,A4,YELLOW_0:30;
    end;
  end;
  assume that
A5: d is monotone and
A6: for s being Element of S holds g.s is_maximum_of d"(downarrow s);
A7: g is monotone
   proof let s1,s2 be Element of S;
    assume
A8:   s1 <= s2;
A9:   g.s1 is_maximum_of d"(downarrow s1) by A6;
then A10:   ex_sup_of d"(downarrow s1),T by Def7;
A11:   g.s2 is_maximum_of d"(downarrow s2) by A6;
then A12:   ex_sup_of d"(downarrow s2),T by Def7;
      downarrow s1 c= downarrow s2 by A8,WAYBEL_0:21;
    then d"(downarrow s1) c= d"(downarrow s2) by RELAT_1:178;
    then sup (d"(downarrow s1)) <=
 sup (d"(downarrow s2)) by A10,A12,YELLOW_0:34;
    then g.s1 <= sup (d"(downarrow s2)) by A9,Def7;
    hence g.s1 <= g.s2 by A11,Def7;
   end;
    for t being Element of T, s being Element of S holds s >= d.t iff g.s >= t
   proof let t be Element of T, s be Element of S;
    set X = d"(downarrow s);
A13:  g.s is_maximum_of X by A6;
    hereby
     assume s >= d.t;
      then d.t in downarrow s by WAYBEL_0:17;
then A14:    t in X by FUNCT_2:46;
         ex_sup_of X,T by A13,Def7;
      then X is_<=_than sup X by YELLOW_0:def 9;
      then t <= sup X by A14,LATTICE3:def 9;
     hence g.s >= t by A13,Def7;
    end;
    assume g.s >= t;
then A15:    d.(g.s) >= d.t by A5,Def2;
       sup X in X by A13,Def7;
     then d.(sup X) in downarrow s by FUNCT_1:def 13;
     then d.(sup X) <= s by WAYBEL_0:17;
     then d.(g.s) <= s by A13,Def7;
     hence s >= d.t by A15,ORDERS_1:26;
   end;
  hence thesis by A5,A7,Th9;
 end;

:: Theorem 3.3 (first part)
theorem Th13:
  for S,T being non empty Poset,g being map of S,T st g is upper_adjoint
   holds g is infs-preserving
 proof let S,T be non empty Poset,g be map of S,T;
  given d being map of T,S such that
A1:  [g,d] is Galois;
  let X be Subset of S;
  assume
A2:  ex_inf_of X,S;
  set s = inf X;
A3:  g.s is_<=_than g.:X
   proof let t be Element of T;
A4:   g is monotone by A1,Th9;
A5:   s is_<=_than X by A2,YELLOW_0:31;
    assume t in g.:X;
     then consider si being Element of S such that
A6:   si in X and
A7:   t = g.si by FUNCT_2:116;
    reconsider si as Element of S;
      s <= si by A5,A6,LATTICE3:def 8;
    hence g.s <= t by A4,A7,Def2;
   end;
    for t being Element of T st t is_<=_than g.:X holds g.s >= t
   proof let t be Element of T; assume
A8:  t is_<=_than g.:X;
       d.t is_<=_than X
      proof let si be Element of S; assume
       si in X;
       then g.si in g.:X by FUNCT_2:43;
       then t <= g.si by A8,LATTICE3:def 8;
       hence d.t <= si by A1,Th9;
      end;
     then d.t <= s by A2,YELLOW_0:31;
     hence g.s >= t by A1,Th9;
   end;
  hence thesis by A3,YELLOW_0:31;
 end;

definition let S,T be non empty Poset;
 cluster upper_adjoint -> infs-preserving map of S,T;
  coherence by Th13;
end;

:: Theorem 3.3 (second part)
theorem Th14:
  for S,T being non empty Poset, d being map of T,S st d is lower_adjoint
   holds d is sups-preserving
 proof let S,T be non empty Poset, d be map of T,S;
  given g being map of S,T such that
A1:  [g,d] is Galois;
  let X be Subset of T;
  assume
A2:  ex_sup_of X,T;
  set t = sup X;
A3:  d.t is_>=_than d.:X
   proof let s be Element of S;
A4:   d is monotone by A1,Th9;
A5:   t is_>=_than X by A2,YELLOW_0:30;
    assume s in d.:X;
     then consider ti being Element of T such that
A6:   ti in X and
A7:   s = d.ti by FUNCT_2:116;
    reconsider ti as Element of T;
      t >= ti by A5,A6,LATTICE3:def 9;
    hence d.t >= s by A4,A7,Def2;
   end;
    for s being Element of S st s is_>=_than d.:X holds d.t <= s
   proof let s be Element of S; assume
A8:  s is_>=_than d.:X;
       g.s is_>=_than X
      proof let ti be Element of T; assume
       ti in X;
       then d.ti in d.:X by FUNCT_2:43;
       then s >= d.ti by A8,LATTICE3:def 9;
       hence g.s >= ti by A1,Th9;
      end;
     then g.s >= t by A2,YELLOW_0:30;
     hence d.t <= s by A1,Th9;
   end;
  hence thesis by A3,YELLOW_0:30;
 end;

definition let S,T be non empty Poset;
 cluster lower_adjoint -> sups-preserving map of S,T;
  coherence by Th14;
end;

:: Theorem 3.4
theorem Th15:
  for S,T being non empty Poset,g being map of S,T
    st S is complete & g is infs-preserving
   ex d being map of T,S st [g,d] is Galois &
    for t being Element of T holds d.t is_minimum_of g"(uparrow t)
  proof let S,T be non empty Poset,g be map of S,T;
   assume that
A1:  S is complete and
A2:  g is infs-preserving;
   defpred P[set,set] means
      ex t being Element of T st t = $1 & $2 = inf (g"(uparrow t));
A3: for e being set st e in the carrier of T
     ex u being set st u in the carrier of S & P[e,u]
     proof let e be set;
      assume e in the carrier of T;
      then reconsider t = e as Element of T;
      take inf (g"(uparrow t));
      thus thesis;
     end;
   consider d being Function of the carrier of T, the carrier of S such that
A4: for e being set st e in the carrier of T holds P[e,d.e]
       from FuncEx1(A3);
A5: for t being Element of T holds d.t = inf (g"(uparrow t))
     proof let t be Element of T;
        ex t1 being Element of T st t1 = t & d.t = inf (g"(uparrow t1))
       by A4;
      hence thesis;
     end;
    reconsider d as map of T,S;
    take d;
      for X being Filter of S holds g preserves_inf_of X by A2,WAYBEL_0:def 32;
     then A6:    g is monotone by WAYBEL_0:69;
A7:    d is monotone
      proof let t1,t2 be Element of T;
A8:     ex_inf_of g"(uparrow t1),S by A1,YELLOW_0:17;
A9:     ex_inf_of g"(uparrow t2),S by A1,YELLOW_0:17;
       assume t1 <= t2;
       then uparrow t2 c= uparrow t1 by WAYBEL_0:22;
       then g"(uparrow t2) c= g"(uparrow t1) by RELAT_1:178;
       then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A8,A9,YELLOW_0:35;
       then d.t1 <= inf (g"(uparrow t2)) by A5;
       hence d.t1 <= d.t2 by A5;
      end;
      for t being Element of T, s being Element of S holds t <= g.s iff d.t <=
s
      proof let t be Element of T, s be Element of S;
A10:     ex_inf_of g"(uparrow t),S by A1,YELLOW_0:17;
      then inf (g"(uparrow t)) is_<=_than g"(uparrow t) by YELLOW_0:31;
      then A11:     d.t is_<=_than g"(uparrow t) by A5;
       hereby
        assume t <= g.s;
        then g.s in uparrow t by WAYBEL_0:18;
        then s in g"(uparrow t) by FUNCT_2:46;
        hence d.t <= s by A11,LATTICE3:def 8;
       end;
       assume d.t <= s;
       then g.(d.t) <= g.s by A6,Def2;
then A12:       g.(inf (g"(uparrow t))) <= g.s by A5;
         g preserves_inf_of (g"(uparrow t)) by A2,WAYBEL_0:def 32;
then A13:     ex_inf_of g.:(g"(uparrow t)),T &
         g.(inf (g"(uparrow t))) = inf (g.:(g"(uparrow t)))
          by A10,WAYBEL_0:def 30;
A14:     ex_inf_of uparrow t,T by WAYBEL_0:39;
         g.:(g"(uparrow t)) c= uparrow t by FUNCT_1:145;
       then g.(inf (g"(uparrow t))) >= inf(uparrow t)
        by A13,A14,YELLOW_0:35;
       then g.(inf (g"(uparrow t))) >= t by WAYBEL_0:39;
       hence t <= g.s by A12,ORDERS_1:26;
      end;
    hence [g,d] is Galois by A6,A7,Th9;
    let t be Element of T;
    thus
A15:   ex_inf_of g"(uparrow t),S by A1,YELLOW_0:17;
    thus
A16:   d.t = inf (g"(uparrow t)) by A5;
      g preserves_inf_of (g"(uparrow t)) by A2,WAYBEL_0:def 32;
then A17:   ex_inf_of g.:(g"(uparrow t)),T &
       g.(inf (g"(uparrow t))) = inf (g.:(g"(uparrow t)))
         by A15,WAYBEL_0:def 30;
A18:   ex_inf_of uparrow t,T by WAYBEL_0:39;
       g.:(g"(uparrow t)) c= uparrow t by FUNCT_1:145;
    then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A17,A18,YELLOW_0:35;
    then g.(inf (g"(uparrow t))) >= t by WAYBEL_0:39;
    then g.(d.t) >= t by A5;
    then g.(d.t) in uparrow t by WAYBEL_0:18;
    hence inf (g"(uparrow t)) in g"(uparrow t) by A16,FUNCT_2:46;
  end;

:: Theorem 3.4 (dual)
theorem Th16:
  for S,T being non empty Poset, d being map of T,S
    st T is complete & d is sups-preserving
   ex g being map of S,T st [g,d] is Galois &
    for s being Element of S holds g.s is_maximum_of d"(downarrow s)
  proof let S,T be non empty Poset, d be map of T,S;
   assume that
A1:  T is complete and
A2:  d is sups-preserving;
   defpred P[set,set] means
      ex s being Element of S st s = $1 & $2 = sup (d"(downarrow s));
A3: for e being set st e in the carrier of S
     ex u being set st u in the carrier of T & P[e,u]
     proof let e be set;
      assume e in the carrier of S;
      then reconsider s = e as Element of S;
      take sup (d"(downarrow s));
      thus thesis;
     end;
   consider g being Function of the carrier of S, the carrier of T such that
A4: for e being set st e in the carrier of S holds P[e,g.e]
       from FuncEx1(A3);
A5:  for s being Element of S holds g.s = sup (d"(downarrow s))
     proof let s be Element of S;
        ex s1 being Element of S st s1 = s & g.s = sup (d"(downarrow s1)) by A4
;
      hence thesis;
     end;
    reconsider g as map of S,T;
    take g;
      for X being Ideal of T holds d preserves_sup_of X by A2,WAYBEL_0:def 33;
     then A6:    d is monotone by WAYBEL_0:72;
A7:    g is monotone
      proof let s1,s2 be Element of S;
A8:     ex_sup_of d"(downarrow s1),T by A1,YELLOW_0:17;
A9:     ex_sup_of d"(downarrow s2),T by A1,YELLOW_0:17;
       assume s1 <= s2;
       then downarrow s1 c= downarrow s2 by WAYBEL_0:21;
       then d"(downarrow s1) c= d"(downarrow s2) by RELAT_1:178;
       then sup (d"(downarrow s1)) <= sup (d"(downarrow s2))
        by A8,A9,YELLOW_0:34;
       then g.s1 <= sup (d"(downarrow s2)) by A5;
       hence g.s1 <= g.s2 by A5;
      end;
      for t being Element of T, s being Element of S holds s >= d.t iff g.s >=
t
      proof let t be Element of T, s be Element of S;
A10:    ex_sup_of d"(downarrow s),T by A1,YELLOW_0:17;
      then sup (d"(downarrow s)) is_>=_than d"(downarrow s) by YELLOW_0:30;
      then A11:     g.s is_>=_than d"(downarrow s) by A5;
       hereby
        assume s >= d.t;
        then d.t in downarrow s by WAYBEL_0:17;
        then t in d"(downarrow s) by FUNCT_2:46;
        hence g.s >= t by A11,LATTICE3:def 9;
       end;
       assume g.s >= t;
       then d.(g.s) >= d.t by A6,Def2;
then A12:     d.(sup (d"(downarrow s))) >= d.t by A5;
         d preserves_sup_of (d"(downarrow s)) by A2,WAYBEL_0:def 33;
then A13:     ex_sup_of d.:(d"(downarrow s)),S &
         d.(sup (d"(downarrow s))) = sup (d.:(d"(downarrow s)))
          by A10,WAYBEL_0:def 31;
A14:     ex_sup_of downarrow s,S by WAYBEL_0:34;
         d.:(d"(downarrow s)) c= downarrow s by FUNCT_1:145;
       then d.(sup (d"(downarrow s))) <= sup(downarrow s)
        by A13,A14,YELLOW_0:34;
       then d.(sup (d"(downarrow s))) <= s by WAYBEL_0:34;
       hence s >= d.t by A12,ORDERS_1:26;
      end;
    hence [g,d] is Galois by A6,A7,Th9;
    let s be Element of S;
    thus
A15:   ex_sup_of d"(downarrow s),T by A1,YELLOW_0:17;
    thus
A16:   g.s = sup (d"(downarrow s)) by A5;
      d preserves_sup_of (d"(downarrow s)) by A2,WAYBEL_0:def 33;
then A17:   ex_sup_of d.:(d"(downarrow s)),S &
       d.(sup (d"(downarrow s))) = sup (d.:(d"(downarrow s)))
         by A15,WAYBEL_0:def 31;
A18:   ex_sup_of downarrow s,S by WAYBEL_0:34;
       d.:(d"(downarrow s)) c= downarrow s by FUNCT_1:145;
     then d.(sup (d"(downarrow s))) <= sup(downarrow s)
      by A17,A18,YELLOW_0:34;
    then d.(sup (d"(downarrow s))) <= s by WAYBEL_0:34;
    then d.(g.s) <= s by A5;
    then d.(g.s) in downarrow s by WAYBEL_0:17;
    hence sup (d"(downarrow s)) in d"(downarrow s) by A16,FUNCT_2:46;
  end;

:: Corollary 3.5 (i)
theorem
    for S,T being non empty Poset, g being map of S,T
    st S is complete
   holds (g is infs-preserving iff g is monotone & g has_a_lower_adjoint)
 proof let S,T be non empty Poset,g be map of S,T;
  assume
A1:   S is complete;
  hereby assume g is infs-preserving;
   then ex d being map of T,S st[g,d] is Galois &
     for t being Element of T holds d.t is_minimum_of g"(uparrow t)
    by A1,Th15;
   hence g is monotone & g has_a_lower_adjoint by Def11,Th11;
  end;
  assume g is monotone;
  assume ex d being map of T,S st [g,d] is Galois;
  then g is upper_adjoint by Def11;
  hence g is infs-preserving by Th13;
 end;

:: Corollary 3.5 (ii)
theorem Th18:
  for S,T being non empty Poset, d being map of T,S
    st T is complete
   holds d is sups-preserving iff d is monotone & d has_an_upper_adjoint
 proof let S,T be non empty Poset, d be map of T,S;
  assume
A1:   T is complete;
  hereby assume d is sups-preserving;
   then ex g being map of S,T st [g,d] is Galois &
     for s being Element of S holds g.s is_maximum_of d"(downarrow s)
     by A1,Th16;
   hence d is monotone & d has_an_upper_adjoint by Def12,Th12;
  end;
  assume d is monotone;
  assume ex g being map of S,T st [g,d] is Galois;
  then d is lower_adjoint by Def12;
  hence d is sups-preserving by Th14;
 end;

:: Theorem 3.6 (1) iff (2)
theorem Th19:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   st [g,d] is Galois holds d*g <= id S & id T <= g*d
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume
A1:  [g,d] is Galois;
    for s being Element of S holds (d*g).s <= (id S).s
   proof let s be Element of S;
       d.(g.s) <= s by A1,Th9;
     then (d*g).s <= s by FUNCT_2:21;
     hence thesis by TMAP_1:91;
    end;
   hence d*g <= id S by YELLOW_2:10;
     for t being Element of T holds (id T).t <= (g*d).t
    proof let t be Element of T;
       t <= g.(d.t) by A1,Th9;
     then t <= (g*d).t by FUNCT_2:21;
     hence thesis by TMAP_1:91;
    end;
   hence id T <= g*d by YELLOW_2:10;
 end;

:: Theorem 3.6 (2) implies (1)
theorem Th20:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st g is monotone & d is monotone & d*g <= id S & id T <= g*d
   holds [g,d] is Galois
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume that
A1:  g is monotone and
A2:  d is monotone and
A3:  d*g <= id S and
A4:  id T <= g*d;
    for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s
   proof let t be Element of T, s be Element of S;
    hereby assume t <= g.s;
then A5:    d.t <= d.(g.s) by A2,Def2;
       (d*g).s <= (id S).s by A3,YELLOW_2:10;
     then d.(g.s) <= (id S).s by FUNCT_2:21;
     then d.(g.s) <= s by TMAP_1:91;
     hence d.t <= s by A5,ORDERS_1:26;
    end;
    assume d.t <= s;
then A6:   g.(d.t) <= g.s by A1,Def2;
      (id T).t <= (g*d).t by A4,YELLOW_2:10;
    then (id T).t <= g.(d.t) by FUNCT_2:21;
    then t <= g.(d.t) by TMAP_1:91;
    hence t <= g.s by A6,ORDERS_1:26;
   end;
  hence [g,d] is Galois by A1,A2,Th9;
 end;

:: Theorem 3.6 (2) implies (3)
theorem Th21:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st g is monotone & d is monotone & d*g <= id S & id T <= g*d
   holds d = d*g*d & g = g*d*g
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
   assume that
A1:  g is monotone and
A2:  d is monotone and
A3:  d*g <= id S and
A4:  id T <= g*d;
    for t being Element of T holds d.t = (d*g*d).t
   proof let t be Element of T;
      (id T).t <= (g*d).t by A4,YELLOW_2:10;
    then t <= (g*d).t by TMAP_1:91;
    then d.t <= d.((g*d).t) by A2,Def2;
    then d.t <= (d*(g*d)).t by FUNCT_2:21;
then A5:  d.t <= (d*g*d).t by RELAT_1:55;
      (d*g).(d.t) <= (id S).(d.t) by A3,YELLOW_2:10;
    then (d*g).(d.t) <= d.t by TMAP_1:91;
    then d.t >= (d*g*d).t by FUNCT_2:21;
    hence thesis by A5,ORDERS_1:25;
   end;
  hence d = d*g*d by YELLOW_2:9;
    for s being Element of S holds g.s = (g*d*g).s
   proof let s be Element of S;
      (id T).(g.s) <= (g*d).(g.s) by A4,YELLOW_2:10;
    then (g.s) <= (g*d).(g.s) by TMAP_1:91;
then A6:  g.s <= (g*d*g).s by FUNCT_2:21;
      (d*g).s <= (id S).s by A3,YELLOW_2:10;
    then (d*g).s <= s by TMAP_1:91;
    then g.((d*g).s) <= g.s by A1,Def2;
    then (g*(d*g)).s <= g.s by FUNCT_2:21;
    then g.s >= (g*d*g).s by RELAT_1:55;
    hence thesis by A6,ORDERS_1:25;
   end;
  hence g = g*d*g by YELLOW_2:9;
 end;

:: Theorem 3.6 (3) implies (4)
theorem Th22:
  for S,T being non empty RelStr, g being map of S,T, d being map of T,S
    st d = d*g*d & g = g*d*g
   holds g*d is idempotent & d*g is idempotent
 proof let S,T be non empty RelStr, g be map of S,T, d be map of T,S;
  assume
A1: d = d*g*d;
  assume g = g*d*g;
  hence (g*d)*(g*d) = g*d by RELAT_1:55;
  thus (d*g)*(d*g) = d*g by A1,RELAT_1:55;
 end;

:: Proposition 3.7 (1) implies (2)
theorem Th23:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois & g is onto
   for t being Element of T holds d.t is_minimum_of g"{t}
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume that
A1:  [g,d] is Galois and
A2:  g is onto;
 let t be Element of T;
A3:  d.t is_minimum_of g"(uparrow t) by A1,Th11;
then A4:  d.t = inf (g"(uparrow t)) by Def6;
A5:  rng g = the carrier of T by A2,FUNCT_2:def 3;
then A6:  g.:(g"(uparrow t)) = uparrow t by FUNCT_1:147;
   consider s being set such that
A7:  s in the carrier of S and
A8:  g.s = t by A5,FUNCT_2:17;
   reconsider s as Element of S by A7;
       ex_inf_of g"(uparrow t),S by A3,Def6;
then A9:  d.t is_<=_than g"(uparrow t) by A4,YELLOW_0:31;
A10:  g is monotone by A1,Th9;
     {t} c= uparrow {t} by WAYBEL_0:16;
then A11:  {t} c= uparrow t by WAYBEL_0:def 18;
then A12:  g"{t} c= g"(uparrow t) by RELAT_1:178;
A13:  t in {t} by TARSKI:def 1;
   then s in g"(uparrow t) by A8,A11,FUNCT_2:46;
   then d.t <= s by A9,LATTICE3:def 8;
then A14:  g.(d.t) <= t by A8,A10,Def2;
     d.t in g"(uparrow t) by A3,A4,Def6;
   then g.(d.t) in g.:(g"(uparrow t)) by FUNCT_2:43;
   then t <= g.(d.t) by A6,WAYBEL_0:18;
then A15:  g.(d.t) = t by A14,ORDERS_1:25;
A16:  ex_inf_of g"(uparrow t),S by A3,Def6;
A17:  d.t in g"{t} by A13,A15,FUNCT_2:46;
  thus
A18:  ex_inf_of g"{t},S
   proof
    take d.t;
    thus
A19:   g"{t} is_>=_than d.t by A9,A12,YELLOW_0:9;
    thus for b be Element of S st g"{t} is_>=_than b holds b <= d.t
     by A17,LATTICE3:def 8;
    let c be Element of S;
    assume g"{t} is_>=_than c;
then A20:   c <= d.t by A17,LATTICE3:def 8;
    assume for b being Element of S st g"{t} is_>=_than b holds b <= c;
    then d.t <= c by A19;
    hence c = d.t by A20,ORDERS_1:25;
   end;
then A21:  inf (g"{t}) >= d.t by A4,A12,A16,YELLOW_0:35;
     inf (g"{t}) is_<=_than g"{t} by A18,YELLOW_0:31;
  then inf (g"{t}) <= d.t by A17,LATTICE3:def 8;
  hence d.t = inf(g"{t}) by A21,ORDERS_1:25;
  hence inf(g"{t}) in g"{t} by A13,A15,FUNCT_2:46;
 end;

:: Proposition 3.7 (2) implies (3)
theorem Th24:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st for t being Element of T holds d.t is_minimum_of g"{t}
   holds g*d = id T
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume
A1:  for t being Element of T holds d.t is_minimum_of g"{t};
    for t being Element of T holds (g*d).t = t
   proof let t be Element of T;
      d.t is_minimum_of g"{t} by A1;
    then d.t = inf(g"{t}) & inf(g"{t}) in g"{t} by Def6;
    then g.(d.t) in {t} by FUNCT_2:46;
    then g.(d.t) = t by TARSKI:def 1;
    hence (g*d).t = t by FUNCT_2:21;
   end;
  hence g*d = id T by Th1;
 end;

:: Proposition 3.7 (3) implies (4)
theorem Th25:
   for L1,L2 being non empty 1-sorted,
       g1 being map of L1,L2, g2 being map of L2,L1
    st g2*g1 = id L1 holds g1 is one-to-one & g2 is onto
 proof let L1,L2 be non empty 1-sorted;
  let g1 be map of L1,L2, g2 be map of L2,L1;
  assume g2*g1 = id L1;
then A1:  g2*g1 = id the carrier of L1 by GRCAT_1:def 11;
  hence g1 is one-to-one by FUNCT_2:29;
    rng g2 = the carrier of L1 by A1,FUNCT_2:29;
  hence g2 is onto by FUNCT_2:def 3;
 end;

:: Proposition 3.7 (4) iff (1)
theorem
    for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois
   holds g is onto iff d is one-to-one
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume
A1:  [g,d] is Galois;
  hereby
   assume g is onto;
   then for t being Element of T holds d.t is_minimum_of g"{t} by A1,Th23;
   then g*d = id T by Th24;
   hence d is one-to-one by Th25;
  end;
  assume
A2:  d is one-to-one;
A3:  the carrier of T = dom d & the carrier of T = dom (g*d) &
      rng (g*d) c= the carrier of T by FUNCT_2:def 1;
A4:  g is monotone & d is monotone by A1,Th9;
    d*g <= id S & id T <= g*d by A1,Th19;
  then d = d*g*d by A4,Th21
        .= d*(g*d) by RELAT_1:55;
  then g*d = id (the carrier of T) by A2,A3,FUNCT_1:50
          .= id T by GRCAT_1:def 11;
  hence g is onto by Th25;
 end;

:: Proposition 3.7 (1*) implies (2*)
theorem Th27:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois & d is onto
   for s being Element of S holds g.s is_maximum_of d"{s}
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume that
A1:  [g,d] is Galois and
A2:  d is onto;
 let s be Element of S;
A3:  g.s is_maximum_of (d"(downarrow s)) by A1,Th12;
then A4:  g.s = sup (d"(downarrow s)) by Def7;
A5:  rng d = the carrier of S by A2,FUNCT_2:def 3;
then A6:  d.:(d"(downarrow s)) = downarrow s by FUNCT_1:147;
   consider t being set such that
A7:  t in the carrier of T and
A8:  d.t = s by A5,FUNCT_2:17;
   reconsider t as Element of T by A7;
       ex_sup_of d"(downarrow s),T by A3,Def7;
then A9:  g.s is_>=_than d"(downarrow s) by A4,YELLOW_0:30;
A10:  d is monotone by A1,Th9;
     {s} c= downarrow {s} by WAYBEL_0:16;
then A11:  {s} c= downarrow s by WAYBEL_0:def 17;
then A12:  d"{s} c= d"(downarrow s) by RELAT_1:178;
A13:  s in {s} by TARSKI:def 1;
   then t in d"(downarrow s) by A8,A11,FUNCT_2:46;
   then g.s >= t by A9,LATTICE3:def 9;
then A14:  d.(g.s) >= s by A8,A10,Def2;
     g.s in d"(downarrow s) by A3,A4,Def7;
   then d.(g.s) in d.:(d"(downarrow s)) by FUNCT_2:43;
   then s >= d.(g.s) by A6,WAYBEL_0:17;
then A15:  d.(g.s) = s by A14,ORDERS_1:25;
A16:  ex_sup_of d"(downarrow s),T by A3,Def7;
A17:  g.s in d"{s} by A13,A15,FUNCT_2:46;
  thus
A18:  ex_sup_of d"{s},T
   proof
    take g.s;
    thus
A19:   d"{s} is_<=_than g.s by A9,A12,YELLOW_0:9;
    thus for b be Element of T st d"{s} is_<=_than b holds b >= g.s
     by A17,LATTICE3:def 9;
    let c be Element of T;
    assume d"{s} is_<=_than c;
then A20:   c >= g.s by A17,LATTICE3:def 9;
    assume for b being Element of T st d"{s} is_<=_than b holds b >= c;
    then g.s >= c by A19;
    hence c = g.s by A20,ORDERS_1:25;
   end;
then A21:  sup (d"{s}) <= g.s by A4,A12,A16,YELLOW_0:34;
     sup (d"{s}) is_>=_than d"{s} by A18,YELLOW_0:30;
  then sup (d"{s}) >= g.s by A17,LATTICE3:def 9;
  hence g.s = sup(d"{s}) by A21,ORDERS_1:25;
  hence sup(d"{s}) in d"{s} by A13,A15,FUNCT_2:46;
 end;

:: Proposition 3.7 (2*) implies (3*)
theorem Th28:
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st for s being Element of S holds g.s is_maximum_of d"{s}
   holds d*g = id S
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume
A1:  for s being Element of S holds g.s is_maximum_of d"{s};
    for s being Element of S holds (d*g).s = s
   proof let s be Element of S;
      g.s is_maximum_of d"{s} by A1;
    then g.s = sup(d"{s}) & sup(d"{s}) in d"{s} by Def7;
    then d.(g.s) in {s} by FUNCT_2:46;
    then d.(g.s) = s by TARSKI:def 1;
    hence (d*g).s = s by FUNCT_2:21;
   end;
  hence d*g = id S by Th1;
 end;

:: Proposition 3.7 (1*) iff (4*)
theorem
    for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois
   holds g is one-to-one iff d is onto
 proof let S,T be non empty Poset,g be map of S,T, d be map of T,S;
  assume
A1:  [g,d] is Galois;
  hereby assume
A2:  g is one-to-one;
A3:  the carrier of S = dom g & the carrier of S = dom (d*g) &
      rng (d*g) c= the carrier of S by FUNCT_2:def 1;
A4:  g is monotone & d is monotone by A1,Th9;
     d*g <= id S & id T <= g*d by A1,Th19;
   then g = g*d*g by A4,Th21
         .= g*(d*g) by RELAT_1:55;
   then d*g = id (the carrier of S) by A2,A3,FUNCT_1:50
           .= id S by GRCAT_1:def 11;
   hence d is onto by Th25;
  end;
  assume d is onto;
  then for s being Element of S holds g.s is_maximum_of d"{s} by A1,Th27;
  then d*g = id S by Th28;
  hence g is one-to-one by Th25;
 end;

:: Definition 3.8 (i)
definition let L be non empty RelStr, p be map of L,L;
  attr p is projection means
:Def13: p is idempotent monotone;
  synonym p is_a_projection_operator;
end;

definition let L be non empty RelStr;
  cluster id L -> projection;
   coherence
 proof
  thus id L is idempotent by YELLOW_2:23;
  thus id L is monotone;
 end;
end;

definition let L be non empty RelStr;
 cluster projection map of L,L;
  existence
 proof take id L;
  thus thesis;
 end;
end;

:: Definition 3.8 (ii)
definition let L be non empty RelStr, c be map of L,L;
  attr c is closure means
:Def14: c is projection & id(L) <= c;
 synonym c is_a_closure_operator;
end;

definition let L be non empty RelStr;
 cluster closure -> projection map of L,L;
  coherence by Def14;
end;

Lm1:
  for L1,L2 being non empty RelStr, f being map of L1,L2
   st L2 is reflexive holds f <= f
 proof let L1,L2 be non empty RelStr, f be map of L1,L2;
  assume L2 is reflexive;
  then for x be Element of L1 holds f.x <= f.x by ORDERS_1:24;
  hence thesis by YELLOW_2:10;
 end;

definition let L be non empty reflexive RelStr;
 cluster closure map of L,L;
  existence
 proof take id L;
  thus id L is projection;
  thus thesis by Lm1;
 end;
end;

definition let L be non empty reflexive RelStr;
 cluster id L -> closure;
  coherence
 proof
  thus id L is projection;
  thus thesis by Lm1;
 end;
end;

:: Definition 3.8 (iii)
definition let L be non empty RelStr, k be map of L,L;
  attr k is kernel means
:Def15: k is projection & k <= id(L);
 synonym k is_a_kernel_operator;
end;

definition let L be non empty RelStr;
 cluster kernel -> projection map of L,L;
  coherence by Def15;
end;

definition let L be non empty reflexive RelStr;
 cluster kernel map of L,L;
  existence
 proof take id L;
  thus id L is projection;
  thus thesis by Lm1;
 end;
end;

definition let L be non empty reflexive RelStr;
 cluster id L -> kernel;
  coherence
 proof
  thus id L is projection;
  thus thesis by Lm1;
 end;
end;

Lm2:
  for L being non empty 1-sorted, p being map of L,L st p is idempotent
   for x being set st x in rng p holds p.x = x
 proof let L be non empty 1-sorted, p be map of L,L such that
A1:  p is idempotent;
  let x be set;
  assume x in rng p;
   then consider a being set such that
A2:  a in dom p and
A3:  x = p.a by FUNCT_1:def 5;
     a in the carrier of L by A2,FUNCT_2:def 1;
   then a is Element of L;
   hence p.x = x by A1,A3,YELLOW_2:20;
 end;

theorem Th30:
  for L being non empty Poset, c being map of L,L, X being Subset of L
    st c is_a_closure_operator & ex_inf_of X,L & X c= rng c
   holds inf X = c.(inf X)
 proof let L be non empty Poset, c be map of L,L, X be Subset of L such that
A1:  c is_a_projection_operator and
A2:  id(L) <= c and
A3:  ex_inf_of X,L and
A4:  X c= rng c;
A5:  c is idempotent by A1,Def13;
A6:  c is monotone by A1,Def13;
    id(L).(inf X) <= c.(inf X) by A2,YELLOW_2:10;
then A7:  inf X <= c.(inf X) by TMAP_1:91;
    c.(inf X) is_<=_than X
   proof let x be Element of L;
    assume
A8:   x in X;
      inf X is_<=_than X by A3,YELLOW_0:31;
    then inf X <= x by A8,LATTICE3:def 8;
then c.(inf X) <= c.x by A6,Def2;
    hence thesis by A4,A5,A8,Lm2;
   end;
  then c.(inf X) <= inf X by A3,YELLOW_0:31;
  hence thesis by A7,ORDERS_1:25;
 end;

theorem Th31:
  for L being non empty Poset, k being map of L,L, X being Subset of L
    st k is_a_kernel_operator & ex_sup_of X,L & X c= rng k
   holds sup X = k.(sup X)
 proof let L be non empty Poset, k be map of L,L, X be Subset of L such that
A1:  k is_a_projection_operator and
A2:  k <= id(L) and
A3:  ex_sup_of X,L and
A4:  X c= rng k;
A5:  k is idempotent by A1,Def13;
A6:  k is monotone by A1,Def13;
    id(L).(sup X) >= k.(sup X) by A2,YELLOW_2:10;
then A7:  sup X >= k.(sup X) by TMAP_1:91;
    k.(sup X) is_>=_than X
   proof let x be Element of L;
    assume
A8:   x in X;
      sup X is_>=_than X by A3,YELLOW_0:30;
    then sup X >= x by A8,LATTICE3:def 9;
then k.(sup X) >= k.x by A6,Def2;
   hence thesis by A4,A5,A8,Lm2;
   end;
  then k.(sup X) >= sup X by A3,YELLOW_0:30;
  hence thesis by A7,ORDERS_1:25;
 end;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 func corestr(g) -> map of L1,Image g equals
:Def16:  (the carrier of Image g)|g;
 coherence
  proof
A1:  the carrier of Image g = rng g by YELLOW_2:11;
   then (the carrier of Image g)|g = g & the carrier of L1 = dom g
    by FUNCT_2:def 1,RELAT_1:125;
   then (the carrier of Image g)|g
      is Function of the carrier of L1, the carrier of Image g by A1,FUNCT_2:3;
   hence thesis;
  end;
end;

theorem Th32:
  for L1, L2 being non empty RelStr,g being map of L1,L2 holds corestr g = g
 proof let L1, L2 be non empty RelStr, g be map of L1,L2;
    the carrier of Image g = rng g by YELLOW_2:11;
  then (the carrier of Image g)|g = g by RELAT_1:125;
  hence thesis by Def16;
 end;

Lm3:
  for L1, L2 being non empty RelStr, g being map of L1,L2
   holds corestr g is onto
 proof let L1, L2 be non empty RelStr, g be map of L1,L2;
     the carrier of Image g = rng g by YELLOW_2:11
                      .= rng corestr g by Th32;
   hence thesis by FUNCT_2:def 3;
 end;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 cluster corestr g -> onto;
  coherence by Lm3;
end;

theorem Th33:
  for L1, L2 being non empty RelStr, g being map of L1,L2 st g is monotone
   holds corestr g is monotone
 proof let L1, L2 be non empty RelStr, g be map of L1,L2 such that
A1: g is monotone;
  let s1,s2 be Element of L1;
  reconsider s1' = g.s1, s2' = g.s2 as Element of L2;
A2: s1' = (corestr g).s1 & s2' = (corestr g).s2 by Th32;
  assume s1 <= s2;
  then g.s1 <= g.s2 by A1,Def2;
  hence thesis by A2,YELLOW_0:61;
 end;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 func inclusion(g) -> map of Image g,L2 equals
:Def17:  id Image g;
 coherence
  proof
A1:   dom id Image g = dom id the carrier of Image g by GRCAT_1:def 11
                 .= the carrier of Image g by RELAT_1:71;
     rng id Image g = rng id the carrier of Image g by GRCAT_1:def 11
              .= the carrier of Image g by RELAT_1:71
              .= rng g by YELLOW_2:11;
   then id Image g is Function of the carrier of Image g, the carrier of L2
    by A1,FUNCT_2:def 1,RELSET_1:11;
   hence thesis;
  end;
end;

theorem Th34:
  for L1, L2 being non empty RelStr, g being map of L1,L2,
      s being Element of Image g
   holds (inclusion g).s = s
 proof
  let L1, L2 be non empty RelStr, g be map of L1,L2, s be Element of Image g;
  thus s = (id Image g).s by TMAP_1:91
        .= (inclusion g).s by Def17;
 end;

Lm4:
  for L1, L2 being non empty RelStr,g being map of L1,L2
   holds inclusion g is one-to-one
 proof let L1, L2 be non empty RelStr,g be map of L1,L2;
    inclusion g = id Image g by Def17
             .= id the carrier of Image g by GRCAT_1:def 11;
  hence thesis;
 end;

Lm5:
  for L1, L2 being non empty RelStr,g being map of L1,L2
   holds inclusion g is monotone
 proof let L1, L2 be non empty RelStr,g be map of L1,L2;
  let s1,s2 be Element of Image g;
  reconsider s1'=(id Image g).s1, s2' = (id Image g).s2 as Element of L2
   by YELLOW_0:59;
A1:  s1' = (inclusion g).s1 & s2' = (inclusion g).s2 by Def17;
  assume s1 <= s2;
  then (id Image g).s1 <= s2 by TMAP_1:91;
  then (id Image g).s1 <= (id Image g).s2 by TMAP_1:91;
  hence (inclusion g).s1 <= (inclusion g).s2 by A1,YELLOW_0:60;
 end;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 cluster inclusion g -> one-to-one monotone;
  coherence by Lm4,Lm5;
end;

theorem Th35:
  for L being non empty RelStr, f being map of L,L
   holds (inclusion f)*(corestr f) = f
 proof let L be non empty RelStr, f be map of L,L;
  thus (inclusion f)*(corestr f)
     = (inclusion f)*f by Th32
    .= (id Image f)*f by Def17
    .= (id the carrier of Image f)*f by GRCAT_1:def 11
    .= (id rng f)*f by YELLOW_2:11
    .= f by FUNCT_1:42;
 end;

::Theorem 3.10 (1) implies (2)
theorem Th36:
   for L being non empty Poset, f being map of L,L st f is idempotent
    holds (corestr f)*(inclusion f) = id(Image f)
 proof let L be non empty Poset, f be map of L,L;
  assume
A1:  f is idempotent;
     for s being Element of Image f holds ((corestr f)*(inclusion f)).s = s
    proof let s be Element of Image f;
       the carrier of Image f = rng corestr f by FUNCT_2:def 3;
     then consider l being set such that
A2:    l in the carrier of L and
A3:    (corestr f).l = s by FUNCT_2:17;
     reconsider l as Element of L by A2;
A4:    (corestr f).l = f.l by Th32;
     thus ((corestr f)*(inclusion f)).s
         = (corestr f).((inclusion f).s) by FUNCT_2:21
        .= (corestr f).s by Th34
        .= f.(f.l) by A3,A4,Th32
        .= s by A1,A3,A4,YELLOW_2:20;
    end;
   hence (corestr f)*(inclusion f) = id(Image f) by Th1;
 end;

::Theorem 3.10 (1) implies (3)
theorem
    for L being non empty Poset, f being map of L,L st f
is_a_projection_operator
    ex T being non empty Poset, q being map of L,T, i being map of T,L
      st q is monotone & q is onto & i is monotone & i is one-to-one &
         f = i*q & id(T) = q*i
 proof let L be non empty Poset, f be map of L,L;
  assume f is_a_projection_operator;
then A1:  f is monotone idempotent by Def13;
  reconsider T = Image f as non empty Poset;
  reconsider q = corestr f as map of L,T;
  reconsider i = inclusion f as map of T,L;
  take T,q,i;
  thus q is monotone by A1,Th33;
  thus q is onto;
  thus i is monotone one-to-one;
  thus f = i*q by Th35;
  thus id(T) = q*i by A1,Th36;
 end;

::Theorem 3.10 (3) implies (1)
theorem
     for L being non empty Poset, f being map of L,L
    st (ex T being non empty Poset, q being map of L,T, i being map of T,L
         st q is monotone & i is monotone & f = i*q & id(T) = q*i)
    holds f is_a_projection_operator
 proof let L be non empty Poset, f be map of L,L;
  given T being non empty Poset, q being map of L,T, i being map of T,L
   such that
A1:  q is monotone and
A2:  i is monotone and
A3:  f = i*q and
A4:  id(T) = q*i;
A5:  i*q*i = i*id(T) by A4,RELAT_1:55
          .= i*(id the carrier of T) by GRCAT_1:def 11
          .= i by FUNCT_2:23;
       q*i*q = (id the carrier of T)*q by A4,GRCAT_1:def 11
          .= q by FUNCT_2:23;
  hence f is idempotent by A3,A5,Th22;
  thus f is monotone by A1,A2,A3,YELLOW_2:14;
 end;

::Theorem 3.10 (1_1) implies (2_1)
theorem Th39:
   for L being non empty Poset, f being map of L,L st f is_a_closure_operator
    holds [inclusion f,corestr f] is Galois
 proof let L be non empty Poset, f be map of L,L;
  assume that
A1:  f is idempotent monotone and
A2:  id L <= f;
  set g = (corestr f), d = inclusion f;
A3: g is monotone by A1,Th33;
    g*d = id(Image f) by A1,Th36;
then A4:  g*d <= id(Image f) by Lm1;
    id L <= d*g by A2,Th35;
  hence thesis by A3,A4,Th20;
 end;

::Theorem 3.10 (2_1) implies (3_1)
theorem
     for L being non empty Poset, f being map of L,L st f is_a_closure_operator
    ex S being non empty Poset, g being map of S,L, d being map of L,S
      st [g,d] is Galois & f = g*d
 proof let L be non empty Poset, f be map of L,L;
  assume
A1:  f is_a_closure_operator;
  reconsider S = Image f as non empty Poset;
  reconsider g = inclusion f as map of S,L;
  reconsider d = corestr f as map of L,S;
  take S,g,d;
  thus [g,d] is Galois by A1,Th39;
  thus f = g*d by Th35;
 end;

::Theorem 3.10 (3_1) implies (1_1)
theorem Th41:
   for L being non empty Poset, f being map of L,L
      st f is monotone &
        ex S being non empty Poset, g being map of S,L, d being map of L,S
         st [g,d] is Galois & f = g*d
    holds f is_a_closure_operator
 proof let L be non empty Poset, f be map of L,L such that
A1:  f is monotone;
  given S being non empty Poset, g being map of S,L, d being map of L,S
   such that
A2: [g,d] is Galois and
A3: f = g*d;
A4:  d*g <= id S & id L <= g*d by A2,Th19;
    d is monotone & g is monotone by A2,Th9;
  then d = d*g*d & g = g*d*g by A4,Th21;
  hence f is idempotent monotone by A1,A3,Th22;
  thus id(L) <= f by A2,A3,Th19;
 end;

::Theorem 3.10 (1_2) implies (2_2)
theorem Th42:
   for L being non empty Poset, f being map of L,L st f is_a_kernel_operator
    holds [corestr f,inclusion f] is Galois
 proof let L be non empty Poset, f be map of L,L;
  assume that
A1:  f is idempotent monotone and
A2:  f <= id(L);
  set g = (corestr f), d = inclusion f;
A3: g is monotone by A1,Th33;
    g*d = id(Image f) by A1,Th36;
then A4: id(Image f) <= g*d by Lm1;
    d*g <= id L by A2,Th35;
  hence thesis by A3,A4,Th20;
 end;

::Theorem 3.10 (2_2) implies (3_2)
theorem
     for L being non empty Poset, f being map of L,L st f is_a_kernel_operator
     ex T being non empty Poset, g being map of L,T, d being map of T,L
      st [g,d] is Galois & f = d*g
 proof let L be non empty Poset, f be map of L,L;
  assume
A1:  f is_a_kernel_operator;
  reconsider T = Image f as non empty Poset;
  reconsider g = corestr f as map of L,T;
  reconsider d = inclusion f as map of T,L;
  take T,g,d;
  thus [g,d] is Galois by A1,Th42;
  thus f = d*g by Th35;
 end;

::Theorem 3.10 (3_2) implies (1_2)
theorem
     for L being non empty Poset, f being map of L,L
    st f is monotone &
      ex T being non empty Poset, g being map of L,T, d being map of T,L
       st [g,d] is Galois & f = d*g
    holds f is_a_kernel_operator
 proof let L be non empty Poset, f be map of L,L;
  assume
A1: f is monotone;
   given T being non empty Poset, g being map of L,T, d being map of T,L
    such that
A2:  [g,d] is Galois and
A3:  f = d*g;
A4:  d*g <= id L & id T <= g*d by A2,Th19;
    d is monotone & g is monotone by A2,Th9;
  then d = d*g*d & g = g*d*g by A4,Th21;
  hence f is idempotent monotone by A1,A3,Th22;
  thus f <= id L by A2,A3,Th19;
end;

:: Lemma 3.11 (i) (part I)
theorem Th45:
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  holds rng p = {c where c is Element of L: c <= p.c} /\
                {k where k is Element of L: p.k <= k}
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is idempotent and
       p is monotone;
  set Lc = {c where c is Element of L: c <= p.c};
  set Lk = {k where k is Element of L: p.k <= k};
A2:  dom p = the carrier of L by FUNCT_2:def 1;
   thus rng p c= Lc /\ Lk
    proof let x be set;
     assume
A3:    x in rng p;
     then reconsider x'=x as Element of L;
     consider l being set such that
A4:    l in dom p and
A5:    p.l = x by A3,FUNCT_1:def 5;
       l is Element of L by A2,A4;
     then x' <= p.x' & p.x' <= x' by A1,A5,YELLOW_2:20;
     then x in Lc & x in Lk;
     hence x in Lc /\ Lk by XBOOLE_0:def 3;
    end;
   let x be set;
   assume x in Lc /\ Lk;
then A6:  x in Lc & x in Lk by XBOOLE_0:def 3;
   then consider lc being Element of L such that
A7:  x = lc & lc <= p.lc;
   consider lk being Element of L such that
A8:  x = lk & p.lk <= lk by A6;
   x = p.x by A7,A8,ORDERS_1:25;
   hence x in rng p by A2,A7,FUNCT_1:def 5;
 end;

theorem Th46:
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  holds {c where c is Element of L: c <= p.c} is non empty Subset of L &
    {k where k is Element of L: p.k <= k} is non empty Subset of L
 proof let L be non empty Poset, p be map of L,L such that
A1: p is_a_projection_operator;
  defpred P[Element of L] means $1 <= p.$1;
  defpred Q[Element of L] means p.$1 <= $1;
  set Lc = {c where c is Element of L: P[c]};
  set Lk = {k where k is Element of L: Q[k]};
  A2: rng p = Lc /\ Lk by A1,Th45;
    Lc is Subset of L from RelStrSubset;
  hence Lc is non empty Subset of L by A2;
    Lk is Subset of L from RelStrSubset;
  hence Lk is non empty Subset of L by A2;
 end;

:: Lemma 3.11 (i) (part II)
theorem Th47:
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  holds rng(p|{c where c is Element of L: c <= p.c}) = rng p &
    rng(p|{k where k is Element of L: p.k <= k}) = rng p
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is_a_projection_operator;
  set Lc = {c where c is Element of L: c <= p.c};
  set Lk = {k where k is Element of L: p.k <= k};
A2:  rng p = Lc /\ Lk by A1,Th45;
A3:  dom p = the carrier of L by FUNCT_2:def 1;
  thus rng(p|Lc) = rng p
   proof
    thus rng(p|Lc) c= rng p by RELAT_1:99;
    let y be set;
    assume y in rng p;
then A4:   y in Lc & y in Lk by A2,XBOOLE_0:def 3;
    then consider lc being Element of L such that
A5:   y = lc & lc <= p.lc;
    consider lk being Element of L such that
A6:   y = lk & p.lk <= lk by A4;
    y = p.y by A5,A6,ORDERS_1:25;
    hence y in rng(p|Lc) by A3,A4,A5,FUNCT_1:73;
   end;
  thus rng(p|Lk) c= rng p by RELAT_1:99;
  let y be set;
  assume y in rng p;
then A7:  y in Lc & y in Lk by A2,XBOOLE_0:def 3;
  then consider lc being Element of L such that
A8:  y = lc & lc <= p.lc;
  consider lk being Element of L such that
A9:  y = lk & p.lk <= lk by A7;
   y = p.y by A8,A9,ORDERS_1:25;
  hence y in rng(p|Lk) by A3,A7,A8,FUNCT_1:73;
end;

theorem Th48:
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lc being non empty Subset of L, Lk being non empty Subset of L
   st Lc = {c where c is Element of L: c <= p.c}
  holds p|Lc is map of subrelstr Lc,subrelstr Lc
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is_a_projection_operator;
  let Lc be non empty Subset of L, Lk be non empty Subset of L such that
A2:  Lc = {c where c is Element of L: c <= p.c};
  set Lk = {k where k is Element of L: p.k <= k};
    rng p = Lc /\ Lk by A1,A2,Th45;
  then rng(p|Lc) = Lc /\ Lk by A1,A2,Th47;
then A3:  rng(p|Lc) c= Lc by XBOOLE_1:17;
A4:  Lc = the carrier of subrelstr Lc by YELLOW_0:def 15;
    p|Lc is Function of Lc,the carrier of L by FUNCT_2:38;
  then p|Lc is Function of Lc,Lc by A3,FUNCT_2:8;
  hence p|Lc is map of subrelstr Lc,subrelstr Lc by A4;
 end;

theorem
    for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lk being non empty Subset of L
   st Lk = {k where k is Element of L: p.k <= k}
  holds p|Lk is map of subrelstr Lk,subrelstr Lk
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is_a_projection_operator;
  let Lk be non empty Subset of L such that
A2:  Lk = {k where k is Element of L: p.k <= k};
  set Lc = {c where c is Element of L: c <= p.c};
    rng p = Lc /\ Lk by A1,A2,Th45;
  then rng(p|Lk) = Lc /\ Lk by A1,A2,Th47;
then A3:  rng(p|Lk) c= Lk by XBOOLE_1:17;
A4:  Lk = the carrier of subrelstr Lk by YELLOW_0:def 15;
    p|Lk is Function of Lk,the carrier of L by FUNCT_2:38;
  then p|Lk is Function of Lk,Lk by A3,FUNCT_2:8;
  hence p|Lk is map of subrelstr Lk,subrelstr Lk by A4;
 end;

:: Lemma 3.11 (i) (part IIIa)
theorem Th50:
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lc being non empty Subset of L
   st Lc = {c where c is Element of L: c <= p.c}
  for pc being map of subrelstr Lc,subrelstr Lc st pc = p|Lc
   holds pc is_a_closure_operator
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is idempotent and
A2:  p is monotone;
  let Lc be non empty Subset of L such that
A3:  Lc = {c where c is Element of L: c <= p.c};
  let pc be map of subrelstr Lc,subrelstr Lc such that
A4:  pc = p|Lc;
A5:   dom pc = the carrier of subrelstr Lc by FUNCT_2:def 1;
  hereby
     now let x be Element of subrelstr Lc;
A6:  pc.x = p.x by A4,A5,FUNCT_1:70;
A7:  x is Element of L by YELLOW_0:59;
      p.(p.x) = pc.(pc.x) by A4,A5,A6,FUNCT_1:70
                .= (pc*pc).x by A5,FUNCT_1:23;
    hence (pc*pc).x = pc.x by A1,A6,A7,YELLOW_2:20;
   end;
   hence pc*pc = pc by FUNCT_2:113;
   thus pc is monotone
    proof let x1,x2 be Element of subrelstr Lc;
     reconsider x1' = x1, x2' = x2 as Element of L by YELLOW_0:59;
A8:    pc.x1 = p.x1' & pc.x2 = p.x2' by A4,A5,FUNCT_1:70;
     assume x1 <= x2;
     then x1' <= x2' by YELLOW_0:60;
     then p.x1' <= p.x2' by A2,Def2;
     hence thesis by A8,YELLOW_0:61;
    end;
  end;
    now
   let x be Element of subrelstr Lc;
   reconsider x'=x as Element of L by YELLOW_0:59;
A9:  pc.x = p.x' by A4,A5,FUNCT_1:70;
       x in the carrier of subrelstr Lc;
   then x in Lc by YELLOW_0:def 15;
   then ex c being Element of L st x = c & c <= p.c by A3;
   then x <= pc.x by A9,YELLOW_0:61;
   hence (id subrelstr Lc).x <= pc.x by TMAP_1:91;
  end;
  hence id(subrelstr Lc) <= pc by YELLOW_2:10;
 end;

:: Lemma 3.11 (i) (part IIIb)
theorem
    for L being non empty Poset, p being map of L,L
    st p is_a_projection_operator
   for Lk being non empty Subset of L
    st Lk = {k where k is Element of L: p.k <= k}
   for pk being map of subrelstr Lk,subrelstr Lk st pk = p|Lk
    holds pk is_a_kernel_operator
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is idempotent and
A2:  p is monotone;
  let Lk be non empty Subset of L such that
A3:  Lk = {k where k is Element of L: p.k <= k};
  let pk be map of subrelstr Lk,subrelstr Lk such that
A4:  pk = p|Lk;
A5:   dom pk = the carrier of subrelstr Lk by FUNCT_2:def 1;
  hereby
     now let x be Element of subrelstr Lk;
A6:   pk.x = p.x by A4,A5,FUNCT_1:70;
A7:   x is Element of L by YELLOW_0:59;
       p.(p.x) = pk.(pk.x) by A4,A5,A6,FUNCT_1:70
                 .= (pk*pk).x by A5,FUNCT_1:23;
     hence (pk*pk).x = pk.x by A1,A6,A7,YELLOW_2:20;
    end;
   hence pk*pk = pk by FUNCT_2:113;
   thus pk is monotone
    proof let x1,x2 be Element of subrelstr Lk;
     reconsider x1' = x1, x2' = x2 as Element of L by YELLOW_0:59;
A8:   pk.x1 = p.x1' & pk.x2 = p.x2' by A4,A5,FUNCT_1:70;
     assume x1 <= x2;
     then x1' <= x2' by YELLOW_0:60;
     then p.x1' <= p.x2' by A2,Def2;
     hence thesis by A8,YELLOW_0:61;
    end;
  end;
    now
   let x be Element of subrelstr Lk;
   reconsider x'=x as Element of L by YELLOW_0:59;
A9:  pk.x = p.x' by A4,A5,FUNCT_1:70;
       x in the carrier of subrelstr Lk;
   then x in Lk by YELLOW_0:def 15;
   then ex c being Element of L st x = c & p.c <= c by A3;
   then pk.x <= x by A9,YELLOW_0:61;
   hence pk.x <= (id subrelstr Lk).x by TMAP_1:91;
  end;
  hence pk <= id(subrelstr Lk) by YELLOW_2:10;
 end;

:: Lemma 3.11 (ii) (part I)
theorem Th52:
  for L being non empty Poset, p being map of L,L st p is monotone
   for Lc being Subset of L st Lc = {c where c is Element of L: c <= p.c}
    holds subrelstr Lc is sups-inheriting
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is monotone;
  let Lc be Subset of L such that
A2:  Lc = {c where c is Element of L: c <= p.c};
   let X be Subset of subrelstr Lc;
   assume
A3:   ex_sup_of X,L;
     p.("\/"(X,L)) is_>=_than X
    proof let x be Element of L;
     assume
A4:    x in X;
     then x in the carrier of subrelstr Lc;
     then x in Lc by YELLOW_0:def 15;
     then consider l being Element of L such that
A5:    x = l & l <= p.l by A2;
       ("\/"(X,L)) is_>=_than X by A3,YELLOW_0:30;
     then x <= "\/"(X,L) by A4,LATTICE3:def 9;
     then p.x <= p.("\/"(X,L)) by A1,Def2;
     hence x <= p.("\/"(X,L)) by A5,ORDERS_1:26;
    end;
   then "\/"(X,L) <= p.("\/"(X,L)) by A3,YELLOW_0:30;
   then "\/"(X,L) in Lc by A2;
   hence "\/"(X,L) in the carrier of subrelstr Lc by YELLOW_0:def 15;
 end;

:: Lemma 3.11 (ii) (part II)
theorem Th53:
  for L being non empty Poset, p being map of L,L st p is monotone
   for Lk being Subset of L st Lk = {k where k is Element of L: p.k <= k}
    holds subrelstr Lk is infs-inheriting
 proof let L be non empty Poset, p be map of L,L such that
A1:  p is monotone;
  let Lk be Subset of L such that
A2:  Lk = {k where k is Element of L: p.k <= k};
  let X be Subset of subrelstr Lk;
  assume
A3:  ex_inf_of X,L;
     p.("/\"(X,L)) is_<=_than X
    proof let x be Element of L;
     assume
A4:    x in X;
     then x in the carrier of subrelstr Lk;
     then x in Lk by YELLOW_0:def 15;
     then consider l being Element of L such that
A5:    x = l & l >= p.l by A2;
       ("/\"(X,L)) is_<=_than X by A3,YELLOW_0:31;
     then x >= "/\"(X,L) by A4,LATTICE3:def 8;
     then p.x >= p.("/\"(X,L)) by A1,Def2;
     hence x >= p.("/\"(X,L)) by A5,ORDERS_1:26;
    end;
   then "/\"(X,L) >= p.("/\"(X,L)) by A3,YELLOW_0:31;
   then "/\"(X,L) in Lk by A2;
   hence "/\"(X,L) in the carrier of subrelstr Lk by YELLOW_0:def 15;
 end;

:: Lemma 3.11 (iii) (part I)
theorem
    for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lc being non empty Subset of L
    st Lc = {c where c is Element of L: c <= p.c}
   holds
    (p is infs-preserving
      implies subrelstr Lc is infs-inheriting & Image p is infs-inheriting) &
    (p is filtered-infs-preserving
      implies subrelstr Lc is filtered-infs-inheriting &
              Image p is filtered-infs-inheriting)
 proof let L be non empty Poset, p be map of L,L; assume
A1:  p is_a_projection_operator;
then A2:  p is monotone by Def13;
  let Lc be non empty Subset of L such that
A3:  Lc = {c where c is Element of L: c <= p.c};
  reconsider Lk = {k where k is Element of L: p.k <=
 k} as non empty Subset of L
   by A1,Th46;
A4:  the carrier of Image p = rng p by YELLOW_2:11
                           .= Lc /\ Lk by A1,A3,Th45;
then A5:  the carrier of Image p c= Lc & the carrier of Image p c= Lk by
XBOOLE_1:17
;
A6:  Lc = the carrier of subrelstr Lc & Lk = the carrier of subrelstr Lk
       by YELLOW_0:def 15;
A7:  the carrier of Image p c= the carrier of subrelstr Lc
       by A5,YELLOW_0:def 15;
  hereby assume A8: p is infs-preserving;
   thus
A9:  subrelstr Lc is infs-inheriting
    proof let X be Subset of subrelstr Lc;
       the carrier of subrelstr Lc is Subset of L by YELLOW_0:def 15;
     then X is Subset of L by XBOOLE_1:1;
     then reconsider X' = X as Subset of L;
     assume
A10:   ex_inf_of X,L;
       p preserves_inf_of X' by A8,WAYBEL_0:def 32;
then A11:    ex_inf_of p.:X,L & inf (p.:X') = p.(inf X') by A10,WAYBEL_0:def 30
;
        inf X' is_<=_than p.:X'
       proof let y be Element of L;
        assume y in p.:X';
        then consider x being Element of L such that
A12:        x in X' and
A13:        y = p.x by FUNCT_2:116;
        reconsider x as Element of L;
          x in Lc by A6,A12;
        then A14: ex x' being Element of L st x' = x & x' <= p.x' by A3;
          inf X' is_<=_than X' by A10,YELLOW_0:31;
        then inf X' <= x by A12,LATTICE3:def 8;
        hence inf X' <= y by A13,A14,ORDERS_1:26;
       end;
     then inf X' <= p.(inf X') by A11,YELLOW_0:31;
     hence "/\"(X,L) in the carrier of subrelstr Lc by A3,A6;
    end;
   thus Image p is infs-inheriting
    proof let X be Subset of Image p such that
A15:    ex_inf_of X,L;
       X c= Lc by A5,XBOOLE_1:1;
     then X is Subset of subrelstr Lc by A6;
then A16:     "/\"(X,L) in the carrier of subrelstr Lc by A9,A15,YELLOW_0:def
18;
A17:    subrelstr Lk is infs-inheriting by A2,Th53;
       X c= the carrier of subrelstr Lk by A5,A6,XBOOLE_1:1;
     then X is Subset of subrelstr Lk;
     then "/\"(X,L) in the carrier of subrelstr Lk by A15,A17,YELLOW_0:def 18;
     hence "/\"(X,L) in the carrier of Image p by A4,A6,A16,XBOOLE_0:def 3;
    end;
  end;
  assume A18: p is filtered-infs-preserving;
  thus
A19:  subrelstr Lc is filtered-infs-inheriting
   proof let X be filtered Subset of subrelstr Lc;
    assume X <> {};
    then reconsider X' = X as non empty filtered Subset of L by YELLOW_2:7;
    assume
A20:   ex_inf_of X,L;
      p preserves_inf_of X' by A18,WAYBEL_0:def 36;
then A21:    ex_inf_of p.:X,L & inf (p.:X') = p.(inf X') by A20,WAYBEL_0:def 30
;
      inf X' is_<=_than p.:X'
     proof let y be Element of L;
      assume y in p.:X';
      then consider x being Element of L such that
A22:     x in X' and
A23:     y = p.x by FUNCT_2:116;
        reconsider x as Element of L;
        x in Lc by A6,A22;
      then A24: ex x' being Element of L st x' = x & x' <= p.x' by A3;
        inf X' is_<=_than X' by A20,YELLOW_0:31;
      then inf X' <= x by A22,LATTICE3:def 8;
      hence inf X' <= y by A23,A24,ORDERS_1:26;
     end;
    then inf X' <= p.(inf X') by A21,YELLOW_0:31;
    hence "/\"(X,L) in the carrier of subrelstr Lc by A3,A6;
   end;
  let X be filtered Subset of Image p such that
A25:  X <> {} and
A26:  ex_inf_of X,L;
     X is filtered Subset of subrelstr Lc by A7,YELLOW_2:8;
   then A27:   "/\"(X,L) in the carrier of subrelstr Lc by A19,A25,A26,WAYBEL_0
:def 3;
A28:  subrelstr Lk is infs-inheriting by A2,Th53;
     X c= the carrier of subrelstr Lk by A5,A6,XBOOLE_1:1;
   then X is Subset of subrelstr Lk;
   then "/\"(X,L) in the carrier of subrelstr Lk by A26,A28,YELLOW_0:def 18;
   hence "/\"(X,L) in the carrier of Image p by A4,A6,A27,XBOOLE_0:def 3;
 end;

:: Lemma 3.11 (iii) (part II)
theorem
    for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lk being non empty Subset of L
    st Lk = {k where k is Element of L: p.k <= k}
   holds
    (p is sups-preserving
      implies subrelstr Lk is sups-inheriting & Image p is sups-inheriting) &
    (p is directed-sups-preserving
      implies subrelstr Lk is directed-sups-inheriting &
              Image p is directed-sups-inheriting)
 proof let L be non empty Poset, p be map of L,L; assume
A1:  p is_a_projection_operator;
then A2:  p is monotone by Def13;
  let Lk be non empty Subset of L such that
A3:  Lk = {k where k is Element of L: p.k <= k};
  reconsider Lc = {c where c is Element of L: c <=
 p.c} as non empty Subset of L
   by A1,Th46;
A4:  the carrier of Image p = rng p by YELLOW_2:11
                           .= Lc /\ Lk by A1,A3,Th45;
then A5:  the carrier of Image p c= Lc & the carrier of Image p c= Lk by
XBOOLE_1:17
;
A6:  Lc = the carrier of subrelstr Lc & Lk = the carrier of subrelstr Lk
       by YELLOW_0:def 15;
A7:  the carrier of Image p c= the carrier of subrelstr Lk
      by A5,YELLOW_0:def 15;
  hereby assume A8: p is sups-preserving;
   thus
A9:  subrelstr Lk is sups-inheriting
    proof let X be Subset of subrelstr Lk;
       the carrier of subrelstr Lk is Subset of L by YELLOW_0:def 15;
     then X is Subset of L by XBOOLE_1:1;
     then reconsider X' = X as Subset of L;
     assume
A10:   ex_sup_of X,L;
       p preserves_sup_of X' by A8,WAYBEL_0:def 33;
then A11:    ex_sup_of p.:X,L & sup (p.:X') = p.(sup X') by A10,WAYBEL_0:def 31
;
        sup X' is_>=_than p.:X'
       proof let y be Element of L;
        assume y in p.:X';
        then consider x being Element of L such that
A12:        x in X' and
A13:        y = p.x by FUNCT_2:116;
        reconsider x as Element of L;
          x in Lk by A6,A12;
        then A14: ex x' being Element of L st x' = x & x' >= p.x' by A3;
          sup X' is_>=_than X' by A10,YELLOW_0:30;
        then sup X' >= x by A12,LATTICE3:def 9;
        hence sup X' >= y by A13,A14,ORDERS_1:26;
       end;
     then sup X' >= p.(sup X') by A11,YELLOW_0:30;
     hence "\/"(X,L) in the carrier of subrelstr Lk by A3,A6;
    end;
   thus Image p is sups-inheriting
    proof let X be Subset of Image p such that
A15:    ex_sup_of X,L;
       X c= Lk by A5,XBOOLE_1:1;
     then X is Subset of subrelstr Lk by A6;
then A16:     "\/"(X,L) in the carrier of subrelstr Lk by A9,A15,YELLOW_0:def
19;
A17:    subrelstr Lc is sups-inheriting by A2,Th52;
       X c= the carrier of subrelstr Lc by A5,A6,XBOOLE_1:1;
     then X is Subset of subrelstr Lc;
     then "\/"(X,L) in the carrier of subrelstr Lc by A15,A17,YELLOW_0:def 19;
     hence "\/"(X,L) in the carrier of Image p by A4,A6,A16,XBOOLE_0:def 3;
    end;
  end;
  assume A18: p is directed-sups-preserving;
  thus
A19:  subrelstr Lk is directed-sups-inheriting
    proof let X be directed Subset of subrelstr Lk;
     assume X <> {};
     then reconsider X' = X as non empty directed Subset of L by YELLOW_2:7;
     assume
A20:   ex_sup_of X,L;
       p preserves_sup_of X' by A18,WAYBEL_0:def 37;
then A21:    ex_sup_of p.:X,L & sup (p.:X') = p.(sup X') by A20,WAYBEL_0:def 31
;
        sup X' is_>=_than p.:X'
       proof let y be Element of L;
        assume y in p.:X';
        then consider x being Element of L such that
A22:        x in X' and
A23:        y = p.x by FUNCT_2:116;
        reconsider x as Element of L;
          x in Lk by A6,A22;
        then A24: ex x' being Element of L st x' = x & x' >= p.x' by A3;
          sup X' is_>=_than X' by A20,YELLOW_0:30;
        then sup X' >= x by A22,LATTICE3:def 9;
        hence sup X' >= y by A23,A24,ORDERS_1:26;
       end;
     then sup X' >= p.(sup X') by A21,YELLOW_0:30;
     hence "\/"(X,L) in the carrier of subrelstr Lk by A3,A6;
    end;
  let X be directed Subset of Image p such that
A25:  X <> {} and
A26:  ex_sup_of X,L;
    X is directed Subset of subrelstr Lk by A7,YELLOW_2:8;
  then A27:  "\/"(X,L) in the carrier of subrelstr Lk by A19,A25,A26,WAYBEL_0:
def 4;
A28:  subrelstr Lc is sups-inheriting by A2,Th52;
    X c= the carrier of subrelstr Lc by A5,A6,XBOOLE_1:1;
  then X is Subset of subrelstr Lc;
  then "\/"(X,L) in the carrier of subrelstr Lc by A26,A28,YELLOW_0:def 19;
  hence "\/"(X,L) in the carrier of Image p by A4,A6,A27,XBOOLE_0:def 3;
 end;

:: Proposition 3.12 (i)
theorem Th56:
  for L being non empty Poset, p being map of L,L holds
   (p is_a_closure_operator implies Image p is infs-inheriting) &
   (p is_a_kernel_operator implies Image p is sups-inheriting)
 proof let L be non empty Poset, p be map of L,L;
  hereby assume
A1:  p is_a_closure_operator;
   thus Image p is infs-inheriting
    proof let X be Subset of Image p; assume
A2:    ex_inf_of X,L;
A3:    the carrier of Image p = rng p by YELLOW_2:11;
     then X c= the carrier of L by XBOOLE_1:1;
     then reconsider X'=X as Subset of L;
       p.("/\"(X',L)) = "/\"(X',L) by A1,A2,A3,Th30;
     hence "/\"(X,L) in the carrier of Image p by A3,FUNCT_2:6;
    end;
  end;
  assume
A4:  p is_a_kernel_operator;
  let X be Subset of Image p; assume
A5:  ex_sup_of X,L;
A6:  the carrier of Image p = rng p by YELLOW_2:11;
  then X c= the carrier of L by XBOOLE_1:1;
  then reconsider X'=X as Subset of L;
    p.("\/"(X',L)) = "\/"(X',L) by A4,A5,A6,Th31;
  hence "\/"(X,L) in the carrier of Image p by A6,FUNCT_2:6;
 end;

:: Proposition 3.12 (ii)
theorem
    for L being complete (non empty Poset), p being map of L,L
    st p is_a_projection_operator
   holds Image p is complete
 proof let L be complete (non empty Poset), p be map of L,L;
  assume
A1:  p is_a_projection_operator;
  then reconsider Lc = {c where c is Element of L: c <= p.c},
             Lk = {k where k is Element of L: p.k <= k}
    as non empty Subset of L by Th46;
A2:  p is monotone by A1,Def13;
  reconsider pc = p|Lc as map of subrelstr Lc,subrelstr Lc by A1,Th48;
    subrelstr Lc is sups-inheriting by A2,Th52;
then A3:  subrelstr Lc is complete LATTICE by YELLOW_2:33;
    pc is_a_closure_operator by A1,Th50;
  then Image pc is infs-inheriting by Th56;
  then subrelstr(rng pc)is infs-inheriting by YELLOW_2:def 2;
  then A4: subrelstr(rng pc) is complete by A3,YELLOW_2:32;
A5:   the carrier of Image p
    = the carrier of subrelstr(rng p) by YELLOW_2:def 2
   .= rng p by YELLOW_0:def 15;
A6:  the carrier of subrelstr Lc = Lc by YELLOW_0:def 15;
     rng p = Lc /\ Lk by A1,Th45;
then A7:  the carrier of Image p c= the carrier of subrelstr Lc by A5,A6,
XBOOLE_1:17
;
A8:  the carrier of Image pc
         = the carrier of subrelstr(rng pc) by YELLOW_2:def 2
        .= rng(pc) by YELLOW_0:def 15
        .= the carrier of Image p by A1,A5,Th47;
   then the InternalRel of Image pc
     = (the InternalRel of subrelstr Lc)|_2 the carrier of Image p
       by YELLOW_0:def 14
    .= ((the InternalRel of L)|_2 the carrier of subrelstr Lc)
        |_2 the carrier of Image p by YELLOW_0:def 14
    .= (the InternalRel of L)|_2 the carrier of Image p by A7,WELLORD1:29
    .= the InternalRel of Image p by YELLOW_0:def 14;
  hence Image p is complete by A4,A8,YELLOW_2:def 2;
 end;

:: Proposition 3.12 (iii)
theorem
    for L being non empty Poset, c being map of L,L
    st c is_a_closure_operator
   holds corestr c is sups-preserving &
    for X being Subset of L
     st X c= the carrier of Image c & ex_sup_of X,L holds
      ex_sup_of X,Image c & "\/"(X,Image c) = c.("\/"(X,L))
 proof let L be non empty Poset, c be map of L,L;
  assume
A1:  c is_a_closure_operator;
  then [inclusion c,corestr c] is Galois by Th39;
  then corestr c is lower_adjoint by Def12;
  hence
A2:  corestr c is sups-preserving by Th14;
   let X be Subset of L such that
A3:  X c= the carrier of Image c and
A4:  ex_sup_of X,L;
A5:  corestr c preserves_sup_of X by A2,WAYBEL_0:def 33;
A6:  (corestr c) = c by Th32;
A7:  X c= rng c by A3,YELLOW_2:11;
    c is projection by A1,Def14;
  then c is idempotent by Def13;
  then c.:X = X by A7,YELLOW_2:22;
  hence thesis by A4,A5,A6,WAYBEL_0:def 31;
 end;

:: Proposition 3.12 (iv)
theorem
    for L being non empty Poset, k being map of L,L
    st k is_a_kernel_operator
   holds (corestr k) is infs-preserving &
    for X being Subset of L
     st X c= the carrier of Image k & ex_inf_of X,L holds
      ex_inf_of X,Image k & "/\"(X,Image k) = k.("/\"(X,L))
 proof let L be non empty Poset, k be map of L,L;
  assume
A1:  k is_a_kernel_operator;
  then [corestr k,inclusion k] is Galois by Th42;
  then corestr k is upper_adjoint by Def11;
  hence
A2:  (corestr k) is infs-preserving by Th13;
   let X be Subset of L such that
A3:  X c= the carrier of Image k and
A4:  ex_inf_of X,L;
A5:  corestr k preserves_inf_of X by A2,WAYBEL_0:def 32;
A6:  (corestr k) = k by Th32;
A7:  X c= rng k by A3,YELLOW_2:11;
    k is projection by A1,Def15;
  then k is idempotent by Def13;
  then k.:X = X by A7,YELLOW_2:22;
  hence thesis by A4,A5,A6,WAYBEL_0:def 30;
 end;

begin :: Heyting algebras

:: Proposition 3.15 (i)
theorem Th60:
   for L being complete (non empty Poset)
    holds [IdsMap L,SupMap L] is Galois & SupMap L is sups-preserving
 proof let L be complete (non empty Poset);
  set g = IdsMap L, d = SupMap L;
    now let I be Element of InclPoset(Ids L), x be Element of L;
   reconsider I' = I as Ideal of L by YELLOW_2:43;
   hereby
    assume I <= g.x;
    then I c= g.x by YELLOW_1:3;
    then I' c= downarrow x by YELLOW_2:def 4;
    then x is_>=_than I' by YELLOW_2:1;
    then sup I' <= x by YELLOW_0:32;
    hence d.I <= x by YELLOW_2:def 3;
   end;
   assume d.I <= x;
then A1:  sup I' <= x by YELLOW_2:def 3;
     sup I' is_>=_than I' by YELLOW_0:32;
   then x is_>=_than I' by A1,YELLOW_0:4;
   then I' c= downarrow x by YELLOW_2:1;
   then I c= g.x by YELLOW_2:def 4;
   hence I <= g.x by YELLOW_1:3;
  end;
  hence [IdsMap L,SupMap L] is Galois by Th9;
  then SupMap L is lower_adjoint by Th10;
  hence SupMap L is sups-preserving by Th14;
 end;

:: Proposition 3.15 (ii)
theorem
     for L being complete (non empty Poset)
    holds (IdsMap L)*(SupMap L) is_a_closure_operator &
     Image ((IdsMap L)*(SupMap L)),L are_isomorphic
 proof let L be complete (non empty Poset);
   set i = (IdsMap L)*(SupMap L);
A1: i is monotone by YELLOW_2:14;
    [IdsMap L,SupMap L] is Galois by Th60;
  hence i is_a_closure_operator by A1,Th41;
  take f = (SupMap L)*(inclusion i);
A2: now
     let I be Ideal of L;
       I is Element of InclPoset(Ids L) by YELLOW_2:43;
     hence i.I = (IdsMap L).((SupMap L).I) by FUNCT_2:21
             .= (IdsMap L).(sup I) by YELLOW_2:def 3
             .= downarrow (sup I) by YELLOW_2:def 4;
    end;
A3: now
     let x be Element of Image i;
     let I be Ideal of L; assume
A4:   x = I;
     hence f.I = (SupMap L).((inclusion i).I) by FUNCT_2:21
              .= (SupMap L).I by A4,Th34
              .= sup I by YELLOW_2:def 3;
    end;
A5: f is one-to-one
   proof let x,y be Element of Image i; assume
A6:  f.x = f.y;
    consider Ix being Element of InclPoset(Ids L) such that
A7:  i.Ix = x by YELLOW_2:12;
    consider Iy being Element of InclPoset(Ids L) such that
A8:  i.Iy = y by YELLOW_2:12;
    reconsider Ix,Iy as Ideal of L by YELLOW_2:43;
A9:  i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A2;
      x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L)
     by YELLOW_0:59;
    then reconsider x,y as Ideal of L by YELLOW_2:43;
    A10: f.x = sup x & f.y = sup y by A3;
      sup downarrow (sup Ix) = sup Ix & sup downarrow (sup Iy) = sup Iy
     by WAYBEL_0:34;
    hence thesis by A6,A7,A8,A9,A10;
   end;
A11: f is monotone by YELLOW_2:14;
A12:  rng f = the carrier of L
  proof thus rng f c= the carrier of L;
   let x be set;
   assume x in the carrier of L;
   then reconsider x as Element of L;
A13: (SupMap L).(downarrow x) = sup downarrow x by YELLOW_2:def 3
                            .= x by WAYBEL_0:34;
A14:  downarrow x is Element of InclPoset(Ids L) by YELLOW_2:43;
    then i.(downarrow x) = (IdsMap L).((SupMap L).(downarrow x)) by FUNCT_2:21
                   .= downarrow x by A13,YELLOW_2:def 4;
    then downarrow x in rng i by A14,FUNCT_2:6;
then A15:  downarrow x in the carrier of Image i by YELLOW_2:11;
then A16:  downarrow x is Element of Image i;
     f.(downarrow x) = (SupMap L).((inclusion i).(downarrow x)) by A15,FUNCT_2:
21
                  .= (SupMap L).(downarrow x) by A16,Th34;
   hence thesis by A13,A15,FUNCT_2:6;
  end;
    now let x,y be Element of Image i;
   thus x <= y implies f.x <= f.y by A11,Def2;
   assume
A17:   f.x <= f.y;
    consider Ix being Element of InclPoset(Ids L) such that
A18:  i.Ix = x by YELLOW_2:12;
    consider Iy being Element of InclPoset(Ids L) such that
A19:  i.Iy = y by YELLOW_2:12;
    reconsider Ix,Iy as Ideal of L by YELLOW_2:43;
A20:  i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A2;
      x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L)
      by YELLOW_0:59;
    then reconsider x'=x, y'=y as Ideal of L by YELLOW_2:43;
    reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy)
     as Element of InclPoset(Ids L) by YELLOW_2:43;
A21:    f.x' = sup x' & f.y' = sup y' by A3;
      sup downarrow (sup Ix) = sup Ix & sup downarrow (sup Iy) = sup Iy
     by WAYBEL_0:34;
    then downarrow (sup Ix) c= downarrow (sup Iy) by A17,A18,A19,A20,A21,
WAYBEL_0:21;
    then i1 <= i2 by YELLOW_1:3;
   hence x <= y by A18,A19,A20,YELLOW_0:61;
  end;
  hence f is isomorphic by A5,A12,WAYBEL_0:66;
 end;

definition let S be non empty RelStr; let x be Element of S;
 func x "/\" -> map of S,S means
:Def18: for s being Element of S holds it.s = x"/\"s;
  existence
   proof
     deffunc F(Element of S) = x"/\"$1;
     thus ex f being map of S,S st for x being Element of S holds f.x = F(x)
     from LambdaMD;
   end;
  uniqueness
 proof let f1,f2  be map of S,S such that
A1: for s being Element of S holds f1.s = x"/\"s and
A2: for s being Element of S holds f2.s = x"/\"s;
    now let s be Element of S;
   thus f1.s = x"/\"s by A1 .= f2.s by A2;
  end;
  hence thesis by YELLOW_2:9;
 end;
end;

theorem Th62:
  for S being non empty RelStr, x,t being Element of S
   holds {s where s is Element of S: x"/\"s <= t} = (x "/\")"(downarrow t)
 proof let S be non empty RelStr, x,t be Element of S;
  hereby let a be set;
   assume a in {s where s is Element of S: x"/\"s <= t};
   then consider s being Element of S such that
A1:  a = s and
A2:  x"/\"s <= t;
     (x "/\").s <= t by A2,Def18;
   then (x"/\").s in downarrow t by WAYBEL_0:17;
   hence a in (x "/\")"(downarrow t) by A1,FUNCT_2:46;
  end;
  let s be set;
  assume
A3:  s in (x "/\")"(downarrow t);
  then reconsider s as Element of S;
    (x "/\").s in downarrow t by A3,FUNCT_2:46;
  then x"/\"s in downarrow t by Def18;
  then x"/\"s <= t by WAYBEL_0:17;
  hence thesis;
end;

theorem Th63:
  for S being Semilattice, x be Element of S
   holds x "/\" is monotone
 proof let S be Semilattice, x be Element of S;
  let s1,s2 be Element of S;
  assume
A1:  s1 <= s2;
A2:  ex_inf_of {x,s2},S by YELLOW_0:21;
A3:  ex_inf_of {x,s1},S by YELLOW_0:21;
  then x"/\"s1 <= s1 by YELLOW_0:19;
  then x"/\"s1 <= s2 & x"/\"s1 <= x by A1,A3,ORDERS_1:26,YELLOW_0:19;
  then x"/\"s1 <= x"/\"s2 by A2,YELLOW_0:19;
  then (x "/\").s1 <= x"/\"s2 by Def18;
  hence (x "/\").s1 <= (x "/\").s2 by Def18;
 end;

definition let S be Semilattice, x be Element of S;
 cluster x "/\" -> monotone;
  coherence by Th63;
end;

theorem Th64:
   for S being non empty RelStr, x being Element of S, X being Subset of S
    holds (x "/\").:X = {x"/\"y where y is Element of S: y in X}
 proof let S be non empty RelStr, x be Element of S, X be Subset of S;
  set Y = {x"/\"y where y is Element of S: y in X};
  hereby
   let y be set;
   assume y in (x "/\").:X;
   then consider z being set such that
A1:  z in the carrier of S and
A2:  z in X and
A3:  y = (x "/\").z by FUNCT_2:115;
   reconsider z as Element of S by A1;
     y = x "/\" z by A3,Def18;
   hence y in Y by A2;
  end;
  let y be set;
  assume y in Y;
  then consider z being Element of S such that
A4:  y = x "/\" z and
A5:  z in X;
    y = (x "/\").z by A4,Def18;
  hence y in (x "/\").:X by A5,FUNCT_2:43;
 end;

:: Lemma 3.16 (1) iff (2)
theorem Th65:
  for S being Semilattice
   holds (for x being Element of S holds x "/\" has_an_upper_adjoint)
    iff (for x,t being Element of S
         holds ex_max_of {s where s is Element of S: x"/\"s <= t},S)
 proof let S be Semilattice;
  hereby
   assume
A1:  for x being Element of S holds x "/\" has_an_upper_adjoint;
   let x,t be Element of S;
   set X = {s where s is Element of S: x"/\"s <= t};
     (x "/\") has_an_upper_adjoint by A1;
   then consider g being map of S,S such that
A2:  [g, x "/\"] is Galois by Def12;
A3:  X = (x "/\")"(downarrow t) by Th62;
     g.t is_maximum_of (x "/\")"(downarrow t) by A2,Th12;
   then ex_sup_of X,S & "\/"(X,S)in X by A3,Def7;
   hence ex_max_of X,S by Def5;
  end;
  assume
A4:  for x,t being Element of S
      holds ex_max_of {s where s is Element of S: x"/\"s <= t},S;
   let x be Element of S;
   deffunc F(Element of S) = "\/"((x "/\")"(downarrow $1),S);
   consider g being map of S,S such that
A5:  for s being Element of S holds g.s = F(s) from LambdaMD;
     now let t be Element of S;
    set X = {s where s is Element of S: x"/\"s <= t};
      ex_max_of X,S by A4;
then A6:  ex_sup_of X,S & "\/"(X,S) in X by Def5;
A7:  X = (x "/\")"(downarrow t) by Th62;
      g.t = "\/"((x "/\")"(downarrow t),S) by A5;
    hence g.t is_maximum_of (x "/\")"(downarrow t) by A6,A7,Def7;
   end;
  then [g, x "/\"] is Galois by Th12;
  hence x "/\" has_an_upper_adjoint by Def12;
 end;

:: Lemma 3.16 (1) implies (3)
theorem Th66:
  for S being Semilattice
    st for x being Element of S holds x "/\" has_an_upper_adjoint
   for X being Subset of S st ex_sup_of X,S
    for x being Element of S holds
     x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S)
 proof let S be Semilattice such that
A1: for x being Element of S holds x "/\" has_an_upper_adjoint;
  let X be Subset of S such that
A2:  ex_sup_of X,S;
  let x be Element of S;
    x "/\" has_an_upper_adjoint by A1;
  then x "/\" is sups-preserving by Th14;
  then x "/\" preserves_sup_of X by WAYBEL_0:def 33;
  then ex_sup_of (x "/\").:X,S & sup ((x "/\").:X) = (x "/\").(sup X)
    by A2,WAYBEL_0:def 31;
  hence x "/\" "\/"(X,S) = sup ((x "/\").:X) by Def18
                    .= "\/"({x"/\"
y where y is Element of S: y in X},S) by Th64;
 end;

:: Lemma 3.16 (1) iff (3)
theorem
    for S being complete (non empty Poset) holds
    (for x being Element of S holds x "/\" has_an_upper_adjoint)
   iff for X being Subset of S, x being Element of S
     holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S)
 proof let S be complete (non empty Poset);
  hereby
   assume
A1:  for x being Element of S holds x "/\" has_an_upper_adjoint;
   let X be Subset of S, x be Element of S;
     ex_sup_of X,S by YELLOW_0:17;
   hence x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in
 X},S) by A1,Th66;
  end;
  assume
A2: for X being Subset of S, x being Element of S
     holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S);
  let x be Element of S;
    x "/\" is sups-preserving
   proof let X be Subset of S;
    assume ex_sup_of X,S;
    thus ex_sup_of (x "/\").:X,S by YELLOW_0:17;
    thus (x "/\").(sup X) = x "/\" "\/"(X,S) by Def18
                       .= "\/"({x"/\"
y where y is Element of S: y in X},S) by A2
                       .= sup ((x "/\").:X) by Th64;
   end;
  hence x "/\" has_an_upper_adjoint by Th18;
 end;

:: Lemma 3.16 (3) implies (D)
theorem Th68:
  for S being LATTICE
   st for X being Subset of S st ex_sup_of X,S for x being Element of S
       holds x"/\"("\/"(X,S)) = "\/"({x"/\"
y where y is Element of S: y in X},S)
   holds S is distributive
 proof let S be LATTICE such that
A1: for X being Subset of S st ex_sup_of X,S for x being Element of S
     holds x"/\"("\/"(X,S)) = "\/"({x"/\"y where y is Element of S: y in X},S);
  let x,y,z be Element of S;
  set Y = {x"/\"s where s is Element of S: s in {y,z}};
    now let t be set;
   hereby
    assume t in Y;
    then consider s being Element of S such that
A2:  t = x"/\"s and
A3:  s in {y,z};
    thus t = x"/\"y or t = x"/\"z by A2,A3,TARSKI:def 2;
   end;
   assume
A4:  t = x"/\"y or t = x"/\"z;
   per cases by A4;
   suppose
A5:  t = x"/\"y;
      y in {y,z} by TARSKI:def 2;
    hence t in Y by A5;
   suppose
A6:  t = x"/\"z;
      z in {y,z} by TARSKI:def 2;
    hence t in Y by A6;
  end;
then A7:  Y = {x"/\"y,x"/\"z} by TARSKI:def 2;
A8:  ex_sup_of {y,z},S by YELLOW_0:20;
  thus x "/\" (y "\/" z)
     = x "/\" (sup {y,z}) by YELLOW_0:41
    .= "\/"({x"/\"y,x"/\"z},S) by A1,A7,A8
    .= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41;
 end;

definition let H be non empty RelStr;
 attr H is Heyting means
:Def19: H is LATTICE & for x being Element of H holds x "/\"
has_an_upper_adjoint;
 synonym H is_a_Heyting_algebra;
end;

definition
 cluster Heyting -> with_infima with_suprema
                     reflexive transitive antisymmetric (non empty RelStr);
 coherence by Def19;
end;

definition let H be non empty RelStr, a be Element of H;
 assume
A1: H is Heyting;
 func a => -> map of H,H means
:Def20: [it,a "/\"] is Galois;
  existence
 proof a "/\" has_an_upper_adjoint by A1,Def19;
  hence ex g being map of H,H st [g, a "/\"] is Galois by Def12;
 end;
  uniqueness
 proof let g1,g2 be map of H,H such that
A2: [g1,a "/\"] is Galois and
A3: [g2,a "/\"] is Galois;
    now let x be Element of H;
     H is LATTICE by A1,Def19;
   then g1.x is_maximum_of (a "/\")"(downarrow x) &
    g2.x is_maximum_of (a "/\")"(downarrow x) by A2,A3,Th12;
   then g1.x = "\/"((a "/\")"(downarrow x),H) & g2.x = "\/"((a "/\"
)"(downarrow x),H)
    by Def7;
   hence g1.x = g2.x;
  end;
  hence g1 = g2 by YELLOW_2:9;
 end;
end;

theorem Th69:
   for H being non empty RelStr st H is_a_Heyting_algebra
    holds H is distributive
 proof let H be non empty RelStr;
  assume
A1:  H is LATTICE &
  for x being Element of H holds x "/\" has_an_upper_adjoint;
  then for X being Subset of H st ex_sup_of X,H
    for x being Element of H
     holds x "/\" "\/"(X,H) = "\/"({x"/\"y where y is Element of H: y in X},H)
    by Th66;
  hence H is distributive by A1,Th68;
 end;

definition
 cluster Heyting -> distributive (non empty RelStr);
  coherence by Th69;
end;

definition let H be non empty RelStr, a,y be Element of H;
 func a => y -> Element of H equals
:Def21:  (a=>).y;
  correctness;
end;

theorem Th70:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for x,a,y being Element of H holds x >= a "/\" y iff a => x >= y
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let x,a,y be Element of H;
    [a =>, a "/\"] is Galois by A1,Def20;
  then x >= (a "/\").y iff (a =>).x >= y by A2,Th9;
  hence thesis by Def18,Def21;
 end;

theorem Th71:
   for H being non empty RelStr st H is_a_Heyting_algebra
    holds H is upper-bounded
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  consider a being Element of H;
  take x = a => a;
  let y be Element of H;
  assume y in the carrier of H;
    a >= a "/\" y by A2,YELLOW_0:23;
  hence x >= y by A1,Th70;
 end;

definition
 cluster Heyting -> upper-bounded (non empty RelStr);
  coherence by Th71;
end;

theorem Th72:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds Top H = a => b iff a <= b
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
A3:  H is upper-bounded by A1,Th71;
  let a,b be Element of H;
A4:  a "/\" Top H = Top H "/\" a by A2,LATTICE3:15
            .= a by A2,A3,Th5;
  hereby
   assume Top H = a => b;
   then a => b >= Top H by A2,ORDERS_1:24;
   hence a <= b by A1,A4,Th70;
  end;
  assume a <= b;
then A5:  a => b >= Top H by A1,A4,Th70;
    a => b <= Top H by A2,A3,YELLOW_0:45;
  hence Top H = a => b by A2,A5,ORDERS_1:25;
 end;

theorem
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a being Element of H holds Top H = a => a
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a be Element of H;
    a >= a "/\" Top H by A2,YELLOW_0:23;
then A3:  Top H <= a => a by A1,Th70;
    H is upper-bounded by A1,Th71;
  then Top H >= a => a by A2,YELLOW_0:45;
  hence Top H = a => a by A2,A3,ORDERS_1:25;
 end;

theorem
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H st Top H = a => b & Top H = b => a holds a = b
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a,b be Element of H;
  assume Top H = a => b;
then A3: a <= b by A1,Th72;
  assume Top H = b => a;
  then b <= a by A1,Th72;
  hence thesis by A2,A3,ORDERS_1:25;
 end;

theorem Th75:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds b <= (a => b)
 proof let H be non empty RelStr; assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a,b be Element of H;
    a"/\"b <= b by A2,YELLOW_0:23;
  hence b <= (a => b) by A1,Th70;
 end;

theorem
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a being Element of H holds Top H = a => Top H
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a be Element of H;
    H is upper-bounded by A1,Th71;
  then a <= Top H by A2,YELLOW_0:45;
  hence thesis by A1,Th72;
 end;

theorem
     for H being non empty RelStr st H is_a_Heyting_algebra
    for b being Element of H holds b = (Top H) => b
 proof let H be non empty RelStr;
  assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
A3:  H is upper-bounded by A1,Th71;
  let b be Element of H;
     (Top H) => b <= (Top H) => b by A2,ORDERS_1:24;
   then Top H "/\" ((Top H) => b) <= b by A1,Th70;
then A4:  (Top H) => b <= b by A2,A3,Th5;
     (Top H) => b >= b by A1,Th75;
   hence thesis by A2,A4,ORDERS_1:25;
 end;

Lm6:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds a"/\"(a => b) <= b
 proof let H be non empty RelStr; assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a,b be Element of H;
    (a => b) <= (a => b) by A2,ORDERS_1:24;
  hence a"/\"(a => b) <= b by A1,Th70;
 end;

theorem Th78:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b,c being Element of H st a <= b holds (b => c) <= (a => c)
 proof let H be non empty RelStr; assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a,b,c be Element of H;
  assume a <= b;
then A3:  a"/\"(b => c) <= b"/\"(b => c) by A2,Th2;
    b"/\"(b => c) <= c by A1,Lm6;
  then a"/\"(b => c) <= c by A2,A3,ORDERS_1:26;
  hence (b => c) <= (a => c) by A1,Th70;
 end;

theorem
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b,c being Element of H st b <= c holds (a => b) <= (a => c)
 proof let H be non empty RelStr; assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a,b,c be Element of H;
  assume
A3:  b <= c;
    a"/\"(a => b) <= b by A1,Lm6;
  then a"/\"(a => b) <= c by A2,A3,ORDERS_1:26;
  hence thesis by A1,Th70;
 end;

theorem Th80:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds a"/\"(a => b) = a"/\"b
 proof let H be non empty RelStr; assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
  let a,b be Element of H;
    a"/\"(a => b) <= b by A1,Lm6;
  then (a"/\"(a => b))"/\"a <= b"/\"a by A2,Th2;
  then a"/\"(a"/\"(a => b)) <= b"/\"a by A2,LATTICE3:15;
  then a"/\"(a"/\"(a => b)) <= a"/\"b by A2,LATTICE3:15;
  then (a"/\"a)"/\"(a => b) <= a"/\"b by A2,LATTICE3:16;
  then A3:  a"/\"(a => b) <= a"/\"b by A2,YELLOW_0:25;
    b <= (a => b) by A1,Th75;
  then b"/\"a <= (a => b)"/\"a by A2,Th2;
  then a"/\"b <= (a => b)"/\"a by A2,LATTICE3:15;
  then a"/\"b <= a"/\"(a => b) by A2,LATTICE3:15;
  hence thesis by A2,A3,ORDERS_1:25;
 end;

theorem Th81:
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b,c being Element of H holds (a"\/"b)=> c = (a => c) "/\" (b => c)
 proof let H be non empty RelStr; assume
A1:  H is_a_Heyting_algebra;
then A2:  H is LATTICE by Def19;
A3:  H is distributive by A1,Th69;
  let a,b,c be Element of H;
    a <= a"\/"b & b <= a"\/"b by A2,YELLOW_0:22;
  then (a"\/"b)=> c <= (a => c) & (a"\/"b)=> c <= (b => c) by A1,Th78;
then A4: (a"\/"b)=> c <= (a => c) "/\" (b => c) by A2,YELLOW_0:23;
  set d = (a => c) "/\" (b => c);
A5:  (a"\/"b)"/\"d
   = d"/\"(a"\/"b) by A2,LATTICE3:15
  .= (d"/\"a)"\/"(d"/\"b) by A3,Def3
  .= (a"/\"d)"\/"(d"/\"b) by A2,LATTICE3:15
  .= (a"/\"d)"\/"(b"/\"d) by A2,LATTICE3:15
  .= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"d) by A2,LATTICE3:16
  .= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"((b=>c)"/\"(a=>c))) by A2,LATTICE3:15
  .= ((a"/\"(a=>c))"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A2,LATTICE3:16
  .= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A1,Th80
  .= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"c)"/\"(a=>c)) by A1,Th80;
    ((a"/\"c)"/\"(b=>c)) <= a"/\"c & a"/\"c <= c by A2,YELLOW_0:23;
then A6:  ((a"/\"c)"/\"(b=>c)) <= c by A2,ORDERS_1:26;
    ((b"/\"c)"/\"(a=>c)) <= b"/\"c & b"/\"c <= c by A2,YELLOW_0:23;
  then ((b"/\"c)"/\"(a=>c)) <= c by A2,ORDERS_1:26;
  then (a"\/"b)"/\"d <= c by A2,A5,A6,YELLOW_0:22;
  then (a"\/"b)=> c >= d by A1,Th70;
  hence (a"\/"b)=> c = d by A2,A4,ORDERS_1:25;
 end;

definition let H be non empty RelStr, a be Element of H;
  func 'not' a -> Element of H equals
:Def22:  a => Bottom H;
 correctness;
end;

theorem
     for H being non empty RelStr st H is_a_Heyting_algebra & H is
lower-bounded
    for a being Element of H
     holds 'not' a is_maximum_of {x where x is Element of H: a"/\"x = Bottom H}
 proof let H be non empty RelStr such that
A1:  H is_a_Heyting_algebra and
A2:  H is lower-bounded;
  let a be Element of H;
A3:  H is LATTICE by A1,Def19;
  set X = {x where x is Element of H: a"/\"x = Bottom H},
      Y = {x where x is Element of H: a"/\"x <= Bottom H};
A4:  X = Y
   proof
    hereby let y be set;
     assume y in X;
     then consider x being Element of H such that
A5:   y = x and
A6:   a"/\"x = Bottom H;
       a"/\"x <= Bottom H by A3,A6,ORDERS_1:24;
     hence y in Y by A5;
    end;
    let y be set;
    assume y in Y;
    then consider x being Element of H such that
A7:  y = x and
A8:  a"/\"x <= Bottom H;
      Bottom H <= a"/\"x by A2,A3,YELLOW_0:44;
    then Bottom H = a"/\"x by A3,A8,ORDERS_1:25;
    hence y in X by A7;
   end;
    for x being Element of H holds x "/\" has_an_upper_adjoint by A1,Def19;
then A9:  ex_max_of X,H by A3,A4,Th65;
  hence ex_sup_of X,H by Def5;
A10:  'not' a is_>=_than X
   proof let b be Element of H;
    assume b in X;
    then consider x being Element of H such that
A11:  x = b and
A12:  a"/\"x <= Bottom H by A4;
      a => Bottom H >= x by A1,A12,Th70;
    hence 'not' a >= b by A11,Def22;
   end;
    now let b be Element of H such that
A13:  b is_>=_than X;
     a => (Bottom H) <= a => (Bottom H) by A3,ORDERS_1:24;
   then 'not' a <= a => (Bottom H) by Def22;
   then a"/\"'not' a <= Bottom H by A1,Th70;
   then 'not' a in X by A4;
   hence 'not' a <= b by A13,LATTICE3:def 9;
  end;
  hence 'not' a = "\/"(X,H) by A3,A10,YELLOW_0:30;
  thus "\/"(X,H) in X by A9,Def5;
 end;

theorem Th83:
   for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded
    holds 'not' Bottom H = Top H & 'not' Top H = Bottom H
 proof let H be non empty RelStr such that
A1:  H is_a_Heyting_algebra and
A2:  H is lower-bounded;
A3:  H is LATTICE by A1,Def19;
   then Bottom H >= Bottom H "/\" Top H by YELLOW_0:23;
   then Top H <= (Bottom H) => (Bottom H) by A1,Th70;
then A4:  'not' Bottom H >= Top H by Def22;
A5:  H is upper-bounded by A1,Th71;
   then 'not' Bottom H <= Top H by A3,YELLOW_0:45;
   hence Top H = 'not' Bottom H by A3,A4,ORDERS_1:25;
     (Top H) => (Bottom H) <= (Top H) => (Bottom H) by A3,ORDERS_1:24;
   then 'not' Top H <= (Top H) => (Bottom H) by Def22;
   then Bottom H >= Top H "/\" 'not' Top H & Bottom H <= Top H "/\" 'not'
Top H by A1,A2,A3,Th70,YELLOW_0:44;
then A6:  Bottom H = Top H "/\" 'not' Top H by A3,ORDERS_1:25;
     'not' Top H <= Top H by A3,A5,YELLOW_0:45;
   hence 'not' Top H = 'not' Top H"/\"Top H by A3,YELLOW_0:25
            .= Bottom H by A3,A6,LATTICE3:15;
 end;

:: Exercise 3.18 (i)
theorem
     for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
     for a,b being Element of H holds 'not' a >= b iff 'not' b >= a
 proof let H be non empty lower-bounded RelStr such that
A1:  H is_a_Heyting_algebra;
  let a,b be Element of H;
  A2: H is LATTICE by A1,Def19;
    (Bottom H >= b "/\" a iff b => Bottom H >= a) & (Bottom H >= a "/\"
 b iff a => Bottom H >= b) by A1,Th70;
  hence 'not' a >= b iff 'not' b >= a by A2,Def22,LATTICE3:15;
 end;

:: Exercise 3.18 (ii)
theorem Th85:
   for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
     for a,b being Element of H holds 'not' a >= b iff a "/\" b = Bottom H
 proof let H be non empty lower-bounded RelStr; assume
A1: H is_a_Heyting_algebra;
then A2: H is LATTICE by Def19;
  let a,b be Element of H;
A3:  a =>Bottom H = 'not' a by Def22;
  hereby
A4:  a "/\" b >= Bottom H by A2,YELLOW_0:44;
   assume 'not' a >= b;
   then a "/\" b <= Bottom H by A1,A3,Th70;
   hence a "/\" b = Bottom H by A2,A4,ORDERS_1:25;
  end;
  assume a "/\" b = Bottom H;
  then a "/\" b <= Bottom H by A2,ORDERS_1:24;
  hence 'not' a >= b by A1,A3,Th70;
 end;

theorem
     for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
     for a,b being Element of H st a <= b holds 'not' b <= 'not' a
 proof let H be non empty lower-bounded RelStr such that
A1: H is_a_Heyting_algebra;
  let a,b be Element of H;
A2: H is LATTICE by A1,Def19;
then A3: 'not' b >= 'not' b by ORDERS_1:24;
  assume a <= b;
  then a "/\" 'not' b = (a"/\"b)"/\"'not' b by A2,YELLOW_0:25
         .= a"/\"(b"/\"'not' b) by A2,LATTICE3:16
         .= a"/\"Bottom H by A1,A3,Th85
         .= Bottom H"/\"a by A2,LATTICE3:15
         .= Bottom H by A2,Th4;
  hence thesis by A1,Th85;
 end;

theorem Th87:
   for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b
 proof let H be non empty lower-bounded RelStr; assume
A1: H is_a_Heyting_algebra;
  let a,b be Element of H;
  thus 'not' (a"\/"b) = (a"\/"b)=> Bottom H by Def22
              .= (a => Bottom H) "/\" (b => Bottom H) by A1,Th81
              .= 'not' a "/\" (b => Bottom H) by Def22
              .= 'not' a"/\"'not' b by Def22;
 end;

theorem
     for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds 'not' (a"/\"b) >= 'not' a"\/"'not' b
 proof let H be non empty lower-bounded RelStr; assume
A1: H is_a_Heyting_algebra;
then A2: H is distributive by Th69;
  let a,b be Element of H;
A3: H is LATTICE by A1,Def19;
then A4: 'not' a <= 'not' a by ORDERS_1:24;
A5: 'not' b <= 'not' b by A3,ORDERS_1:24;
A6: Bottom H<=Bottom H by A3,ORDERS_1:24;
    (a"/\"b)"/\"('not' a"\/"'not' b) = ((a"/\"b)"/\"'not' a)"\/"((a"/\"b)"/\"
'not' b) by A2,Def3
                  .= ((b"/\"a)"/\"'not' a)"\/"((a"/\"b)"/\"
'not' b) by A3,LATTICE3:15
                  .= (b"/\"(a"/\"'not' a))"\/"((a"/\"b)"/\"
'not' b) by A3,LATTICE3:16
                  .= (b"/\"(a"/\"'not' a))"\/"(a"/\"(b"/\"
'not' b)) by A3,LATTICE3:16
                  .= (b"/\"Bottom H)"\/"(a"/\"(b"/\"'not' b)) by A1,A4,Th85
                  .= (b"/\"Bottom H)"\/"(a"/\"Bottom H) by A1,A5,Th85
                  .= (Bottom H"/\"b)"\/"(a"/\"Bottom H) by A3,LATTICE3:15
                  .= (Bottom H"/\"b)"\/"(Bottom H"/\"a) by A3,LATTICE3:15
                  .= Bottom H"\/"(Bottom H"/\"a) by A3,Th4
                  .= Bottom H"\/"Bottom H by A3,Th4
                  .= Bottom H by A3,A6,YELLOW_0:24;
  hence thesis by A1,Th85;
 end;

definition let L be non empty RelStr, x,y be Element of L;
 pred y is_a_complement_of x means
:Def23: x "\/" y = Top L & x "/\" y = Bottom L;
end;

definition let L be non empty RelStr;
 attr L is complemented means
:Def24:
  for x being Element of L ex y being Element of L st y is_a_complement_of x;
end;

definition let X be set;
 cluster BoolePoset X -> complemented;
  coherence
 proof
  let x be Element of BoolePoset X;
A1: the carrier of BoolePoset X
     = the carrier of LattPOSet BooleLatt X by YELLOW_1:def 2
    .= the carrier of RelStr (#the carrier of BooleLatt X,
                              LattRel BooleLatt X#) by LATTICE3:def 2
    .= bool X by LATTICE3:def 1;
    X\x c= X by XBOOLE_1:109;
  then reconsider y = X\x as Element of BoolePoset X by A1;
  take y;
  thus x "\/" y = x \/ y by YELLOW_1:17
             .= X \/ x by XBOOLE_1:39
             .= X by A1,XBOOLE_1:12
             .= Top (BoolePoset X) by YELLOW_1:19;
A2:x misses y by XBOOLE_1:79;
  thus x "/\" y = x /\ y by YELLOW_1:17
             .= {} by A2,XBOOLE_0:def 7
             .= Bottom (BoolePoset X) by YELLOW_1:18;
 end;
end;

:: Exercise 3.19  (1) implies (3)
Lm7:
   for L being bounded LATTICE
     st L is distributive complemented
    for x being Element of L ex x' being Element of L st
     for y being Element of L holds (y "\/" x') "/\" x <= y & y <= (y "/\" x)
"\/" x'
 proof let L be bounded LATTICE such that
A1:  L is distributive and
A2:  L is complemented;
  let x be Element of L;
  consider x' being Element of L such that
A3: x' is_a_complement_of x by A2,Def24;
  take x';
  let y be Element of L;
    (y "\/" x') "/\" x = (x "/\" y) "\/" (x "/\" x') by A1,Def3
                .= Bottom L "\/" (x "/\" y) by A3,Def23
                .= x "/\" y by Th4;
  hence (y "\/" x') "/\" x <= y by YELLOW_0:23;
     (y "/\" x) "\/" x' = (x' "\/" y) "/\" (x' "\/" x) by A1,Th6
                 .= (x' "\/" y) "/\" Top L by A3,Def23
                 .= x' "\/" y by Th5;
  hence y <= (y "/\" x) "\/" x' by YELLOW_0:22;
 end;

:: Exercise 3.19  (3) implies (2)
Lm8:
   for L being bounded LATTICE
    st for x being Element of L ex x' being Element of L st
     for y being Element of L holds (y "\/" x') "/\" x <= y & y <= (y "/\" x)
"\/" x'
    holds L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not'
 x = x
 proof let L be bounded LATTICE;
   defpred P[Element of L, Element of L] means
    for y being Element of L holds
      (y "\/" $2) "/\" $1 <= y & y <= (y "/\" $1) "\/" $2;
   assume
A1: for x being Element of L ex x' being Element of L st P[x,x'];
  consider g' being map of L,L such that
A2:  for x being Element of L holds P[x,g'.x]  from NonUniqExMD(A1);
A3: now
   let y be Element of L;
   let g be map of L,L such that
A4:  for z being Element of L holds g.z = g'.y "\/" z;
A5:  g is monotone
    proof let z1,z2 be Element of L;
     assume z1 <= z2;
     then g'.y "\/" z1 <= z2 "\/" g'.y by Th3;
     then g.z1 <= g'.y "\/" z2 by A4;
     hence thesis by A4;
    end;
     now let x be Element of L, z be Element of L;
    hereby
     assume x <= g.z;
     then x <= g'.y "\/" z by A4;
then A6:    x "/\" y <= (g'.y "\/" z) "/\" y by Th2;
       (g'.y "\/" z) "/\" y <= z by A2;
     then x "/\" y <= z by A6,ORDERS_1:26;
     hence (y "/\").x <= z by Def18;
    end;
    assume (y "/\").x <= z;
    then y "/\" x <= z by Def18;
then A7:   (x "/\" y) "\/" g'.y <= z "\/" g'.y by Th3;
      x <= (x "/\" y) "\/" g'.y by A2;
    then x <= z "\/" g'.y by A7,ORDERS_1:26;
    hence x <= g.z by A4;
   end;
   hence [g,y "/\"] is Galois by A5,Th9;
  end;
  thus
A8: L is_a_Heyting_algebra
   proof
    thus L is LATTICE;
    let y be Element of L;
    deffunc F(Element of L) = g'.y "\/" $1;
    consider g being map of L,L such that
A9:   for z being Element of L holds g.z = F(z) from LambdaMD;
       [g,y "/\"] is Galois by A3,A9;
    hence y "/\" has_an_upper_adjoint by Def12;
   end;
then A10:  L is distributive by Th69;
A11: now let x be Element of L;
      deffunc F(Element of L) = g'.x "\/" $1;
     consider g being map of L,L such that
A12:    for z being Element of L holds g.z = F(z) from LambdaMD;
       [g,x "/\"] is Galois by A3,A12;
then A13:    g = x => by A8,Def20;
     thus 'not' x = x => Bottom L by Def22
            .= g.Bottom L by A13,Def21
            .= Bottom L "\/" g'.x by A12
            .= g'.x by Th4;
    end;
A14: now let x be Element of L;
       Top L <= (Top L "/\" x) "\/" g'.x by A2;
then A15:   Top L <= x "\/" g'.x by Th5;
       x "\/" g'.x <= Top L by YELLOW_0:45;
     hence Top L = x "\/" g'.x by A15,ORDERS_1:25
             .= x "\/" 'not' x by A11;
    end;
A16: now let x be Element of L;
        (Bottom L "\/" g'.x) "/\" x <= Bottom L by A2;
      then (x "/\" Bottom L) "\/" (x "/\" g'.x) <= Bottom L by A10,Def3;
      then Bottom L "\/" (x "/\" g'.x) <= Bottom L by Th4;
then A17:     x "/\" g'.x <= Bottom L by Th4;
       Bottom L <= x "/\" g'.x by YELLOW_0:44;
     hence Bottom L = x "/\" g'.x by A17,ORDERS_1:25
             .= x "/\" 'not' x by A11;
    end;
  let x be Element of L;
     ('not' x "\/" 'not' 'not' x) "/\" x = Top L "/\" x by A14;
   then x = x "/\" ('not' x "\/" 'not' 'not' x) by Th5
         .= (x "/\" 'not' x) "\/" (x "/\" 'not' 'not' x) by A10,Def3
         .= Bottom L "\/" (x "/\" 'not' 'not' x) by A16
         .= x "/\" 'not' 'not' x by Th4;
   then A18:  x <= 'not' 'not' x by YELLOW_0:25;
     Bottom L "\/" x = ('not' x "/\" 'not' 'not' x) "\/" x by A16;
   then x = x "\/" ('not' x "/\" 'not' 'not' x) by Th4
         .= (x "\/" 'not' x) "/\" (x "\/" 'not' 'not' x) by A10,Th6
         .= Top L "/\" (x "\/" 'not' 'not' x) by A14
         .= x "\/" 'not' 'not' x by Th5;
   hence thesis by A18,YELLOW_0:24;
 end;

:: Exercise 3.19
theorem Th89:
   for L being bounded LATTICE
    st L is_a_Heyting_algebra & for x being Element of L holds
    'not' 'not' x = x
   for x being Element of L holds 'not' x is_a_complement_of x
 proof let L be bounded LATTICE such that
A1:  L is_a_Heyting_algebra and
A2:  for x being Element of L holds 'not' 'not' x = x;
  let x be Element of L;
  A3: 'not' x >= 'not' x by ORDERS_1:24;
then A4: x "/\" 'not' x = Bottom L by A1,Th85;
    'not' (x "\/" 'not' x) = 'not' x "/\" 'not' 'not' x by A1,Th87
            .= x "/\" 'not' x by A2;
  hence x "\/" 'not' x = 'not' (Bottom L) by A2,A4
               .= Top L by A1,Th83;
  thus thesis by A1,A3,Th85;
 end;

:: Exercise 3.19  (1) iff (2)
theorem Th90:
   for L being bounded LATTICE
    holds L is distributive complemented
      iff L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not'
 x = x
 proof let L be bounded LATTICE;
  hereby assume L is distributive complemented;
   then for x being Element of L ex x' being Element of L st
     for y being Element of L holds (y "\/" x') "/\" x <= y & y <= (y "/\" x)
"\/" x'
    by Lm7;
   hence L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not'
 x = x
    by Lm8;
  end;
 assume that
A1: L is_a_Heyting_algebra and
A2: for x being Element of L holds 'not' 'not' x = x;
  thus L is distributive by A1,Th69;
  let x be Element of L;
  take 'not' x;
  thus 'not' x is_a_complement_of x by A1,A2,Th89;
 end;

:: Definition 3.20
definition let B be non empty RelStr;
 attr B is Boolean means
:Def25: B is LATTICE & B is bounded distributive complemented;
  synonym B is_a_Boolean_algebra;
  synonym B is_a_Boolean_lattice;
end;

definition
 cluster Boolean -> reflexive transitive antisymmetric with_infima with_suprema
    bounded distributive complemented (non empty RelStr);
  coherence by Def25;
end;

definition
 cluster reflexive transitive antisymmetric with_infima with_suprema
    bounded distributive complemented -> Boolean (non empty RelStr);
  coherence by Def25;
end;

definition
 cluster Boolean -> Heyting (non empty RelStr);
  coherence
 proof let B be non empty RelStr;
  assume B is LATTICE & B is bounded distributive complemented;
  hence thesis by Th90;
 end;
end;

definition
 cluster strict Boolean non empty LATTICE;
  existence
 proof consider X being set;
  take BoolePoset X;
  thus thesis;
 end;
end;

definition
 cluster strict Heyting non empty LATTICE;
  existence
 proof consider L being strict Boolean non empty LATTICE;
  take L;
  thus thesis;
 end;
end;


Back to top