:: Galois Connections
::  by Czes\law Byli\'nski
::
:: Received September 25, 1996
:: Copyright (c) 1996-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, STRUCT_0, FUNCT_1, SUBSET_1, ORDERS_2, SEQM_3,
      XXREAL_0, RELAT_2, LATTICE3, LATTICES, EQREL_1, WAYBEL_0, YELLOW_1,
      YELLOW_0, RELAT_1, CAT_1, WELLORD1, ORDINAL2, TARSKI, REWRITE1, CARD_FIL,
      BINOP_1, FUNCT_2, GROUP_6, YELLOW_2, LATTICE2, XBOOLEAN, ZFMISC_1,
      XXREAL_2, WAYBEL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      DOMAIN_1, STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, QUANTAL1, ORDERS_3,
      YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2;
 constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, RELSET_1;
 registrations RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0,
      WAYBEL_0, YELLOW_1, YELLOW_2, RELSET_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, WAYBEL_0,
      XBOOLE_0;
 equalities TARSKI, LATTICE3, WAYBEL_0, XBOOLE_0, YELLOW_2, STRUCT_0;
 expansions TARSKI, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, XBOOLE_0, STRUCT_0;
 theorems ORDERS_2, FUNCT_1, FUNCT_2, LATTICE3, RELAT_1, TARSKI, WELLORD1,
      YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, RELSET_1, XBOOLE_0, XBOOLE_1,
      XTUPLE_0;
 schemes FUNCT_2, DOMAIN_1;

begin :: Preliminaries

definition
  let L1,L2 be non empty 1-sorted, f be Function 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:19;
    assume for x,y being Element of L1 st f.x = f.y holds x=y;
    then for x,y be object st x in the carrier of L1 & y in the carrier of L1
    holds f.x = f.y implies x=y;
    hence thesis by FUNCT_2:19;
  end;
end;

definition
  let L1,L2 be non empty RelStr, f be Function of L1,L2;
  redefine attr f is monotone means

  for x,y being Element of L1 st x <= y holds f.x <= f.y;
  compatibility;
end;

theorem Th1:
  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;
A1: x"/\"z <= x by YELLOW_0:23;
A2: x"/\"z <= z by YELLOW_0:23;
  assume x <= y;
  then x"/\"z <= y by A1,ORDERS_2:3;
  hence thesis by A2,YELLOW_0:23;
end;

theorem Th2:
  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;
A1: y <= y"\/"z by YELLOW_0:22;
A2: z <= y"\/"z by YELLOW_0:22;
  assume x <= y;
  then x <= y"\/"z by A1,ORDERS_2:3;
  hence thesis by A2,YELLOW_0:22;
end;

theorem Th3:
  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 thesis by ORDERS_2:2;
  end;
  assume
A1: L is with_suprema;
  then
A2: x <= Bottom L "\/" x by YELLOW_0:22;
  assume L is reflexive transitive;
  then
A3: x <= x;
  Bottom L <= x by YELLOW_0:44;
  then Bottom L "\/" x <= x by A1,A3,YELLOW_0:22;
  hence thesis by A2,ORDERS_2:2;
end;

theorem Th4:
  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;
    then x "/\" x <= Top L "/\" x by Th1,YELLOW_0:45;
    then
A2: x <= Top L "/\" x by A1,YELLOW_0:25;
    Top L "/\" x <= x by A1,YELLOW_0:23;
    hence thesis by A2,ORDERS_2:2;
  end;
  assume L is with_suprema;
  then Top L "\/" x <= Top L & Top L <= Top L "\/" x by YELLOW_0:22,45;
  hence thesis by ORDERS_2:2;
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 Th5:
  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
      .= ((x"\/"y)"/\"x)"\/"((x"\/"y)"/\"z) by LATTICE3:18
      .= (x"\/"y)"/\"(x"\/"z) by A1;
  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;

registration
  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;
  pred ex_max_of X,S means

  ex_sup_of X,S & "\/"(X,S) in X;
end;

notation
  let S be non empty RelStr, X be set;
  synonym X has_the_min_in S for ex_min_of X,S;
  synonym X has_the_max_in S for ex_max_of X,S;
end;

definition
  let S be non empty RelStr, s be Element of S, X be set;
  pred s is_minimum_of X means

  ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S ) in X;
  pred s is_maximum_of X means

  ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S )in X;
end;

registration
  let L be RelStr;
  cluster id L -> isomorphic;
  coherence
  proof
    per cases;
    suppose
A1:   L is non empty;
A2:   id L = (id L)" by FUNCT_1:45;
      id L is monotone;
      hence thesis by A1,A2,WAYBEL_0:def 38;
    end;
    suppose
      L is empty;
      hence thesis by WAYBEL_0:def 38;
    end;
  end;
end;

definition
  let L1,L2 be RelStr;
  pred L1,L2 are_isomorphic means

  ex f being Function 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 Function of L1,L2 such that
A1: f is isomorphic;
  consider g being Function of L2,L1 such that
A2: g = (f qua Function)" and
A3: g is monotone by A1,WAYBEL_0:def 38;
  f = (g qua Function)" by A1,A2,FUNCT_1:43;
  then g is isomorphic by A1,A2,A3,WAYBEL_0:def 38;
  hence thesis;
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 Function of L1,L2 such that
A1: f1 is isomorphic;
  given f2 being Function of L2,L3 such that
A2: f2 is isomorphic;
A3: L1 is empty implies f2*f1 is Function of L1,L3 by FUNCT_2:13;
  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 Function of L1,L2;
    reconsider f2 as Function of L2,L3;
    consider g1 being Function of L2,L1 such that
A4: g1 = (f1 qua Function)" & g1 is monotone by A1,WAYBEL_0:def 38;
    consider g2 being Function of L3,L2 such that
A5: g2 = (f2 qua Function)" & g2 is monotone by A2,WAYBEL_0:def 38;
A6: f2*f1 is monotone by A1,A2,YELLOW_2:12;
    g1*g2 is monotone & g1*g2 = ((f2*f1) qua Function)" by A1,A2,A4,A5,
FUNCT_1:44,YELLOW_2:12;
    then f2*f1 is isomorphic by A1,A2,A6,WAYBEL_0:def 38;
    hence thesis;
  end;
  suppose
A7: L1 is empty;
    then reconsider f = f2*f1 as Function of L1,L3 by A3;
    L2 is empty by A1,A7,WAYBEL_0:def 38;
    then L3 is empty by A2,WAYBEL_0:def 38;
    then f is isomorphic by A7,WAYBEL_0:def 38;
    hence thesis;
  end;
  suppose
A8: L2 is empty;
    then reconsider f = f2*f1 as Function of L1,L3 by A1,A3,WAYBEL_0:def 38;
    L1 is empty & L3 is empty by A1,A2,A8,WAYBEL_0:def 38;
    then f is isomorphic by WAYBEL_0:def 38;
    hence thesis;
  end;
  suppose
A9: L3 is empty;
    then
A10: L2 is empty by A2,WAYBEL_0:def 38;
    then reconsider f = f2*f1 as Function of L1,L3 by A1,A3,WAYBEL_0:def 38;
    L1 is empty by A1,A10,WAYBEL_0:def 38;
    then f is isomorphic by A9,WAYBEL_0:def 38;
    hence thesis;
  end;
end;

begin :: Galois Connections

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

definition
  let S,T be RelStr, g be Function of S,T, d be Function 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

  ex g being Function of S,T, d being Function
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 Th8:
  for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
  hereby
    assume [g,d] is Galois;
    then consider g9 being Function of S,T, d9 being Function of T,S such that
A1: [g,d] = [g9,d9] and
A2: g9 is monotone & d9 is monotone & for t being Element of T, s
    being Element of S holds t <= g9.s iff d9.t <= s;
    g = g9 & d = d9 by A1,XTUPLE_0:1;
    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;
end;

:: Definition 3.1

definition
  let S,T be non empty RelStr, g be Function of S,T;
  attr g is upper_adjoint means

  ex d being Function of T,S st [g,d] is Galois;
end;

:: Definition 3.1

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

theorem
  for S,T being non empty Poset,g being Function of S,T, d being
  Function of T,S st [g,d] is Galois holds g is upper_adjoint & d is
  lower_adjoint;

:: Theorem 3.2  (1) iff (2)

theorem Th10:
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function of T,S;
  hereby
    assume
A1: [g,d] is Galois;
    hence g is monotone by Th8;
    let t be Element of T;
    thus d.t is_minimum_of g"(uparrow t)
    proof
      set X = g"(uparrow t);
      t <= g.(d.t) by A1,Th8;
      then g.(d.t) in uparrow t by WAYBEL_0:18;
      then
A2:   d.t in X by FUNCT_2:38;
      then
A3:   for s being Element of S st s is_<=_than X holds d.t >= s;
A4:   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 7;
        then t <= g.s by WAYBEL_0:18;
        hence d.t <= s by A1,Th8;
      end;
      hence ex_inf_of X,S & d.t = inf X by A3,YELLOW_0:31;
      thus thesis by A4,A2,A3,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: 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);
    hereby
      assume t <= g.s;
      then g.s in uparrow t by WAYBEL_0:18;
      then
A8:   s in X by FUNCT_2:38;
A9:   d.t is_minimum_of g"(uparrow t) by A6;
      then ex_inf_of X,S;
      then X is_>=_than inf X by YELLOW_0:def 10;
      then s >= inf X by A8;
      hence d.t <= s by A9;
    end;
A10: d.t is_minimum_of X by A6;
    then inf X in X;
    then g.(inf X) in uparrow t by FUNCT_1:def 7;
    then g.(inf X) >= t by WAYBEL_0:18;
    then
A11: g.(d.t) >= t by A10;
    assume d.t <= s;
    then g.(d.t) <= g.s by A5;
    hence thesis by A11,ORDERS_2:3;
  end;
  d is monotone
  proof
    let t1,t2 be Element of T;
    assume t1 <= t2;
    then
A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
A13: d.t2 is_minimum_of g"(uparrow t2) by A6;
    then
A14: ex_inf_of g"(uparrow t2),S;
A15: d.t1 is_minimum_of g"(uparrow t1) by A6;
    then ex_inf_of g"(uparrow t1),S;
    then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A14,A12,RELAT_1:143
,YELLOW_0:35;
    then d.t1 <= inf (g"(uparrow t2)) by A15;
    hence d.t1 <= d.t2 by A13;
  end;
  hence thesis by A5,A7;
end;

:: Theorem 3.2 (1) iff (3)

theorem Th11:
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function of T,S;
  hereby
    assume
A1: [g,d] is Galois;
    hence d is monotone by Th8;
    let s be Element of S;
    thus g.s is_maximum_of d"(downarrow s)
    proof
      set X = d"(downarrow s);
      s >= d.(g.s) by A1,Th8;
      then d.(g.s) in downarrow s by WAYBEL_0:17;
      then
A2:   g.s in X by FUNCT_2:38;
      then
A3:   for t being Element of T st t is_>=_than X holds g.s <= t;
A4:   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 7;
        then s >= d.t by WAYBEL_0:17;
        hence thesis by A1,Th8;
      end;
      hence ex_sup_of X,T & g.s = sup X by A3,YELLOW_0:30;
      thus thesis by A4,A2,A3,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: 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);
A8: g.s is_maximum_of X by A6;
    then sup X in X;
    then d.(sup X) in downarrow s by FUNCT_1:def 7;
    then d.(sup X) <= s by WAYBEL_0:17;
    then
A9: d.(g.s) <= s by A8;
    hereby
      assume s >= d.t;
      then d.t in downarrow s by WAYBEL_0:17;
      then
A10:  t in X by FUNCT_2:38;
      ex_sup_of X,T by A8;
      then X is_<=_than sup X by YELLOW_0:def 9;
      then t <= sup X by A10;
      hence g.s >= t by A8;
    end;
    assume g.s >= t;
    then d.(g.s) >= d.t by A5;
    hence thesis by A9,ORDERS_2:3;
  end;
  g is monotone
  proof
    let s1,s2 be Element of S;
    assume s1 <= s2;
    then
A11: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
A12: g.s2 is_maximum_of d"(downarrow s2) by A6;
    then
A13: ex_sup_of d"(downarrow s2),T;
A14: g.s1 is_maximum_of d"(downarrow s1) by A6;
    then ex_sup_of d"(downarrow s1),T;
    then sup (d"(downarrow s1)) <= sup (d"(downarrow s2)) by A13,A11,
RELAT_1:143,YELLOW_0:34;
    then g.s1 <= sup (d"(downarrow s2)) by A14;
    hence g.s1 <= g.s2 by A12;
  end;
  hence thesis by A5,A7;
end;

:: Theorem 3.3 (first part)

theorem Th12:
  for S,T being non empty Poset,g being Function of S,T st g is
  upper_adjoint holds g is infs-preserving
proof
  let S,T be non empty Poset,g be Function of S,T;
  given d being Function of T,S such that
A1: [g,d] is Galois;
  let X be Subset of S;
  set s = inf X;
  assume
A2: ex_inf_of X,S;
A3: for t being Element of T st t is_<=_than g.:X holds g.s >= t
  proof
    let t be Element of T;
    assume
A4: 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:35;
      then t <= g.si by A4;
      hence d.t <= si by A1,Th8;
    end;
    then d.t <= s by A2,YELLOW_0:31;
    hence thesis by A1,Th8;
  end;
  g.s is_<=_than g.:X
  proof
    let t be Element of T;
    assume t in g.:X;
    then consider si being Element of S such that
A5: si in X and
A6: t = g.si by FUNCT_2:65;
A7: g is monotone by A1,Th8;
    reconsider si as Element of S;
    s is_<=_than X by A2,YELLOW_0:31;
    then s <= si by A5;
    hence g.s <= t by A7,A6;
  end;
  hence thesis by A3,YELLOW_0:31;
end;

registration
  let S,T be non empty Poset;
  cluster upper_adjoint -> infs-preserving for Function of S,T;
  coherence by Th12;
end;

:: Theorem 3.3 (second part)

theorem Th13:
  for S,T being non empty Poset, d being Function of T,S st d is
  lower_adjoint holds d is sups-preserving
proof
  let S,T be non empty Poset, d be Function of T,S;
  given g being Function of S,T such that
A1: [g,d] is Galois;
  let X be Subset of T;
  set t = sup X;
  assume
A2: ex_sup_of X,T;
A3: for s being Element of S st s is_>=_than d.:X holds d.t <= s
  proof
    let s be Element of S;
    assume
A4: 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:35;
      then s >= d.ti by A4;
      hence thesis by A1,Th8;
    end;
    then g.s >= t by A2,YELLOW_0:30;
    hence thesis by A1,Th8;
  end;
  d.t is_>=_than d.:X
  proof
    let s be Element of S;
    assume s in d.:X;
    then consider ti being Element of T such that
A5: ti in X and
A6: s = d.ti by FUNCT_2:65;
A7: d is monotone by A1,Th8;
    reconsider ti as Element of T;
    t is_>=_than X by A2,YELLOW_0:30;
    then t >= ti by A5;
    hence thesis by A7,A6;
  end;
  hence thesis by A3,YELLOW_0:30;
end;

registration
  let S,T be non empty Poset;
  cluster lower_adjoint -> sups-preserving for Function of S,T;
  coherence by Th13;
end;

:: Theorem 3.4

theorem Th14:
  for S,T being non empty Poset,g being Function of S,T st S is
complete & g is infs-preserving ex d being Function 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 Function of S,T;
  assume that
A1: S is complete and
A2: g is infs-preserving;
  defpred P[object,object] means
ex t being Element of T st t = $1 & $2 = inf (g"(
  uparrow t));
A3: for e being object st e in the carrier of T
   ex u being object st u in the carrier of S & P[e,u]
  proof
    let e be object;
    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 object st e in the carrier of T holds P[e,d.e] from FUNCT_2
  :sch 1(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 Function of T,S;
  for X being Filter of S holds g preserves_inf_of X by A2;
  then
A6: g is monotone by WAYBEL_0:69;
A7: 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;
A8: ex_inf_of uparrow t,T by WAYBEL_0:39;
A9: 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
A10: 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:38;
      hence d.t <= s by A10;
    end;
    g preserves_inf_of (g"(uparrow t)) by A2;
    then
    ex_inf_of g.:(g"(uparrow t)),T & g.(inf (g"(uparrow t))) = inf (g.:(g
    "( uparrow t))) by A9;
    then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A8,FUNCT_1:75,YELLOW_0:35
;
    then
A11: g.(inf (g"(uparrow t))) >= t by WAYBEL_0:39;
    assume d.t <= s;
    then g.(d.t) <= g.s by A6;
    then g.(inf (g"(uparrow t))) <= g.s by A5;
    hence thesis by A11,ORDERS_2:3;
  end;
  take d;
  d is monotone
  proof
    let t1,t2 be Element of T;
    assume t1 <= t2;
    then
A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
    ex_inf_of g"(uparrow t1),S & ex_inf_of g"(uparrow t2),S by A1,YELLOW_0:17;
    then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A12,RELAT_1:143
,YELLOW_0:35;
    then d.t1 <= inf (g"(uparrow t2)) by A5;
    hence d.t1 <= d.t2 by A5;
  end;
  hence [g,d] is Galois by A6,A7;
  let t be Element of T;
  thus
A13: ex_inf_of g"(uparrow t),S by A1,YELLOW_0:17;
  thus
A14: d.t = inf (g"(uparrow t)) by A5;
A15: ex_inf_of uparrow t,T by WAYBEL_0:39;
  g preserves_inf_of (g"(uparrow t)) by A2;
  then
  ex_inf_of g.:(g"(uparrow t)),T & g.(inf (g"(uparrow t))) = inf (g.:(g"(
  uparrow t))) by A13;
  then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A15,FUNCT_1:75,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 thesis by A14,FUNCT_2:38;
end;

:: Theorem 3.4 (dual)

theorem Th15:
  for S,T being non empty Poset, d being Function of T,S st T is
complete & d is sups-preserving ex g being Function 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 Function of T,S;
  assume that
A1: T is complete and
A2: d is sups-preserving;
  defpred P[object,object] means
ex s being Element of S st s = $1 & $2 = sup (d"(
  downarrow s));
A3: for e being object st e in the carrier of S
    ex u being object st u in the carrier of T & P[e,u]
  proof
    let e be object;
    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 object st e in the carrier of S holds P[e,g.e] from FUNCT_2
  :sch 1(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 Function of S,T;
  for X being Ideal of T holds d preserves_sup_of X by A2;
  then
A6: d is monotone by WAYBEL_0:72;
A7: 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;
A8: ex_sup_of downarrow s,S by WAYBEL_0:34;
A9: 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
A10: 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:38;
      hence g.s >= t by A10;
    end;
    d preserves_sup_of (d"(downarrow s)) by A2;
    then
    ex_sup_of d.:(d"(downarrow s)),S & d.(sup (d"(downarrow s))) = sup (d
    .:(d"( downarrow s))) by A9;
    then d.(sup (d"(downarrow s))) <= sup(downarrow s) by A8,FUNCT_1:75
,YELLOW_0:34;
    then
A11: d.(sup (d"(downarrow s))) <= s by WAYBEL_0:34;
    assume g.s >= t;
    then d.(g.s) >= d.t by A6;
    then d.(sup (d"(downarrow s))) >= d.t by A5;
    hence thesis by A11,ORDERS_2:3;
  end;
  take g;
  g is monotone
  proof
    let s1,s2 be Element of S;
    assume s1 <= s2;
    then
A12: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
    ex_sup_of d"(downarrow s1),T & ex_sup_of d"(downarrow s2),T by A1,
YELLOW_0:17;
    then sup (d"(downarrow s1)) <= sup (d"(downarrow s2)) by A12,RELAT_1:143
,YELLOW_0:34;
    then g.s1 <= sup (d"(downarrow s2)) by A5;
    hence g.s1 <= g.s2 by A5;
  end;
  hence [g,d] is Galois by A6,A7;
  let s be Element of S;
  thus
A13: ex_sup_of d"(downarrow s),T by A1,YELLOW_0:17;
  thus
A14: g.s = sup (d"(downarrow s)) by A5;
A15: ex_sup_of downarrow s,S by WAYBEL_0:34;
  d preserves_sup_of (d"(downarrow s)) by A2;
  then
  ex_sup_of d.:(d"(downarrow s)),S & d.(sup (d"(downarrow s))) = sup (d.:
  (d"( downarrow s))) by A13;
  then d.(sup (d"(downarrow s))) <= sup(downarrow s) by A15,FUNCT_1:75
,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 thesis by A14,FUNCT_2:38;
end;

:: Corollary 3.5 (i)

theorem
  for S,T being non empty Poset, g being Function of S,T st S is
  complete holds (g is infs-preserving iff g is monotone & g is upper_adjoint)
proof
  let S,T be non empty Poset,g be Function of S,T;
  assume
A1: S is complete;
  hereby
    assume g is infs-preserving;
    then
    ex d being Function 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,Th14;
    hence g is monotone & g is upper_adjoint by Th10;
  end;
  assume g is monotone;
  assume ex d being Function of T,S st [g,d] is Galois;
  then g is upper_adjoint;
  hence thesis;
end;

:: Corollary 3.5 (ii)

theorem Th17:
  for S,T being non empty Poset, d being Function of T,S st T is
  complete holds d is sups-preserving iff d is monotone & d is lower_adjoint
proof
  let S,T be non empty Poset, d be Function of T,S;
  assume
A1: T is complete;
  hereby
    assume d is sups-preserving;
    then
    ex g being Function 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,Th15;
    hence d is monotone & d is lower_adjoint by Th11;
  end;
  assume d is monotone;
  assume ex g being Function of S,T st [g,d] is Galois;
  then d is lower_adjoint;
  hence thesis;
end;

:: Theorem 3.6 (1) iff (2)

theorem Th18:
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function 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,Th8;
    then (d*g).s <= s by FUNCT_2:15;
    hence thesis;
  end;
  hence d*g <= id S by YELLOW_2:9;
  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,Th8;
    then t <= (g*d).t by FUNCT_2:15;
    hence thesis;
  end;
  hence thesis by YELLOW_2:9;
end;

:: Theorem 3.6 (2) implies (1)

theorem Th19:
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function 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
      (d*g).s <= (id S).s by A3,YELLOW_2:9;
      then d.(g.s) <= (id S).s by FUNCT_2:15;
      then
A5:   d.(g.s) <= s;
      assume t <= g.s;
      then d.t <= d.(g.s) by A2;
      hence d.t <= s by A5,ORDERS_2:3;
    end;
    (id T).t <= (g*d).t by A4,YELLOW_2:9;
    then (id T).t <= g.(d.t) by FUNCT_2:15;
    then
A6: t <= g.(d.t);
    assume d.t <= s;
    then g.(d.t) <= g.s by A1;
    hence thesis by A6,ORDERS_2:3;
  end;
  hence thesis by A1,A2;
end;

:: Theorem 3.6 (2) implies (3)

theorem Th20:
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function 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:9;
    then t <= (g*d).t;
    then d.t <= d.((g*d).t) by A2;
    then d.t <= (d*(g*d)).t by FUNCT_2:15;
    then
A5: d.t <= (d*g*d).t by RELAT_1:36;
    (d*g).(d.t) <= (id S).(d.t) by A3,YELLOW_2:9;
    then (d*g).(d.t) <= d.t;
    then d.t >= (d*g*d).t by FUNCT_2:15;
    hence thesis by A5,ORDERS_2:2;
  end;
  hence d = d*g*d by FUNCT_2:63;
  for s being Element of S holds g.s = (g*d*g).s
  proof
    let s be Element of S;
    (d*g).s <= (id S).s by A3,YELLOW_2:9;
    then (d*g).s <= s;
    then g.((d*g).s) <= g.s by A1;
    then (g*(d*g)).s <= g.s by FUNCT_2:15;
    then
A6: g.s >= (g*d*g).s by RELAT_1:36;
    (id T).(g.s) <= (g*d).(g.s) by A4,YELLOW_2:9;
    then (g.s) <= (g*d).(g.s);
    then g.s <= (g*d*g).s by FUNCT_2:15;
    hence thesis by A6,ORDERS_2:2;
  end;
  hence thesis by FUNCT_2:63;
end;

:: Theorem 3.6 (3) implies (4)

theorem Th21:
  for S,T being non empty RelStr, g being Function of S,T, d being
  Function of T,S st g = g*d*g holds g*d is idempotent
proof
  let S,T be non empty RelStr, g be Function of S,T, d be Function of T,S;
  assume g = g*d*g;
  hence (g*d)*(g*d) = g*d by RELAT_1:36;
end;

:: Proposition 3.7 (1) implies (2)

theorem Th22:
  for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
  assume that
A1: [g,d] is Galois and
A2: g is onto;
A3: g is monotone by A1,Th8;
  let t be Element of T;
A4: rng g = the carrier of T by A2,FUNCT_2:def 3;
  then
A5: g.:(g"(uparrow t)) = uparrow t by FUNCT_1:77;
A6: d.t is_minimum_of g"(uparrow t) by A1,Th10;
  then
A7: d.t = inf (g"(uparrow t));
  d.t in g"(uparrow t) by A6;
  then g.(d.t) in g.:(g"(uparrow t)) by FUNCT_2:35;
  then
A8: t <= g.(d.t) by A5,WAYBEL_0:18;
  ex_inf_of g"(uparrow t),S by A6;
  then
A9: d.t is_<=_than g"(uparrow t) by A7,YELLOW_0:31;
  consider s being object such that
A10: s in the carrier of S and
A11: g.s = t by A4,FUNCT_2:11;
  reconsider s as Element of S by A10;
A12: t in {t} by TARSKI:def 1;
A13: {t} c= uparrow {t} by WAYBEL_0:16;
  then s in g"(uparrow t) by A11,A12,FUNCT_2:38;
  then d.t <= s by A9;
  then g.(d.t) <= t by A11,A3;
  then
A14: g.(d.t) = t by A8,ORDERS_2:2;
  then
A15: d.t in g"{t} by A12,FUNCT_2:38;
A16: g"{t} c= g"(uparrow t) by RELAT_1:143,WAYBEL_0:16;
  thus
A17: ex_inf_of g"{t},S
  proof
    take d.t;
    thus g"{t} is_>=_than d.t by A9,A16;
    thus for b be Element of S st g"{t} is_>=_than b holds b <= d.t by A15;
    let c be Element of S;
    assume g"{t} is_>=_than c;
    then
A18: c <= d.t by A15;
    assume for b being Element of S st g"{t} is_>=_than b holds b <= c;
    then d.t <= c by A9,A16,YELLOW_0:9;
    hence thesis by A18,ORDERS_2:2;
  end;
  then inf (g"{t}) is_<=_than g"{t} by YELLOW_0:31;
  then
A19: inf (g"{t}) <= d.t by A15;
  ex_inf_of g"(uparrow t),S by A6;
  then inf (g"{t}) >= d.t by A7,A13,A17,RELAT_1:143,YELLOW_0:35;
  hence d.t = inf(g"{t}) by A19,ORDERS_2:2;
  hence thesis by A12,A14,FUNCT_2:38;
end;

:: Proposition 3.7 (2) implies (3)

theorem Th23:
  for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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};
    then g.(d.t) in {t} by FUNCT_2:38;
    then g.(d.t) = t by TARSKI:def 1;
    hence thesis by FUNCT_2:15;
  end;
  hence thesis by FUNCT_2:124;
end;

:: Proposition 3.7 (4) iff (1)

theorem
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function of T,S;
A1: the carrier of T = dom d & the carrier of T = dom (g*d) by FUNCT_2:def 1;
  assume
A2: [g,d] is Galois;
  then
A3: d*g <= id S & id T <= g*d by Th18;
  hereby
    assume g is onto;
    then for t being Element of T holds d.t is_minimum_of g"{t} by A2,Th22;
    then g*d = id T by Th23;
    hence d is one-to-one by FUNCT_2:23;
  end;
A4: rng (g*d) c= the carrier of T;
  g is monotone & d is monotone by A2,Th8;
  then
A5: d = d*g*d by A3,Th20
    .= d*(g*d) by RELAT_1:36;
  assume d is one-to-one;
  then g*d = id T by A1,A4,A5,FUNCT_1:28;
  hence thesis by FUNCT_2:23;
end;

:: Proposition 3.7 (1*) implies (2*)

theorem Th25:
  for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
  assume that
A1: [g,d] is Galois and
A2: d is onto;
A3: d is monotone by A1,Th8;
  let s be Element of S;
A4: rng d = the carrier of S by A2,FUNCT_2:def 3;
  then
A5: d.:(d"(downarrow s)) = downarrow s by FUNCT_1:77;
A6: g.s is_maximum_of (d"(downarrow s)) by A1,Th11;
  then
A7: g.s = sup (d"(downarrow s));
  g.s in d"(downarrow s) by A6;
  then d.(g.s) in d.:(d"(downarrow s)) by FUNCT_2:35;
  then
A8: s >= d.(g.s) by A5,WAYBEL_0:17;
  ex_sup_of d"(downarrow s),T by A6;
  then
A9: g.s is_>=_than d"(downarrow s) by A7,YELLOW_0:30;
  consider t being object such that
A10: t in the carrier of T and
A11: d.t = s by A4,FUNCT_2:11;
  reconsider t as Element of T by A10;
A12: s in {s} by TARSKI:def 1;
A13: {s} c= downarrow {s} by WAYBEL_0:16;
  then t in d"(downarrow s) by A11,A12,FUNCT_2:38;
  then g.s >= t by A9;
  then d.(g.s) >= s by A11,A3;
  then
A14: d.(g.s) = s by A8,ORDERS_2:2;
  then
A15: g.s in d"{s} by A12,FUNCT_2:38;
A16: d"{s} c= d"(downarrow s) by RELAT_1:143,WAYBEL_0:16;
  thus
A17: ex_sup_of d"{s},T
  proof
    take g.s;
    thus d"{s} is_<=_than g.s by A9,A16;
    thus for b be Element of T st d"{s} is_<=_than b holds b >= g.s by A15;
    let c be Element of T;
    assume d"{s} is_<=_than c;
    then
A18: c >= g.s by A15;
    assume for b being Element of T st d"{s} is_<=_than b holds b >= c;
    then g.s >= c by A9,A16,YELLOW_0:9;
    hence thesis by A18,ORDERS_2:2;
  end;
  then sup (d"{s}) is_>=_than d"{s} by YELLOW_0:30;
  then
A19: sup (d"{s}) >= g.s by A15;
  ex_sup_of d"(downarrow s),T by A6;
  then sup (d"{s}) <= g.s by A7,A13,A17,RELAT_1:143,YELLOW_0:34;
  hence g.s = sup(d"{s}) by A19,ORDERS_2:2;
  hence thesis by A12,A14,FUNCT_2:38;
end;

:: Proposition 3.7 (2*) implies (3*)

theorem Th26:
  for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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};
    then d.(g.s) in {s} by FUNCT_2:38;
    then d.(g.s) = s by TARSKI:def 1;
    hence thesis by FUNCT_2:15;
  end;
  hence thesis by FUNCT_2:124;
end;

:: Proposition 3.7 (1*) iff (4*)

theorem
  for S,T being non empty Poset,g being Function of S,T, d being
  Function 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 Function of S,T, d be Function of T,S;
  assume
A1: [g,d] is Galois;
  hereby
A2: d*g <= id S & id T <= g*d by A1,Th18;
    g is monotone & d is monotone by A1,Th8;
    then
A3: g = g*d*g by A2,Th20
      .= g*(d*g) by RELAT_1:36;
A4: the carrier of S = dom g & the carrier of S = dom (d*g) by FUNCT_2:def 1;
A5: rng (d*g) c= the carrier of S;
    assume g is one-to-one;
    then d*g = id S by A4,A5,A3,FUNCT_1:28;
    hence d is onto by FUNCT_2:23;
  end;
  assume d is onto;
  then for s being Element of S holds g.s is_maximum_of d"{s} by A1,Th25;
  then d*g = id S by Th26;
  hence thesis by FUNCT_2:23;
end;

:: Definition 3.8 (i)

definition
  let L be non empty RelStr, p be Function of L,L;
  attr p is projection means
  :Def13:
  p is idempotent monotone;
end;

registration
  let L be non empty RelStr;
  cluster id L -> projection;
  coherence
  by YELLOW_2:21;
end;

registration
  let L be non empty RelStr;
  cluster projection for Function 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 Function of L,L;
  attr c is closure means

  c is projection & id(L) <= c;
end;

registration
  let L be non empty RelStr;
  cluster closure -> projection for Function of L,L;
  coherence;
end;

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

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

registration
  let L be non empty reflexive RelStr;
  cluster id L -> closure;
  coherence
  by Lm1;
end;

:: Definition 3.8 (iii)

definition
  let L be non empty RelStr, k be Function of L,L;
  attr k is kernel means

  k is projection & k <= id(L);
end;

registration
  let L be non empty RelStr;
  cluster kernel -> projection for Function of L,L;
  coherence;
end;

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

registration
  let L be non empty reflexive RelStr;
  cluster id L -> kernel;
  coherence
  by Lm1;
end;

Lm2: for L being non empty 1-sorted, p being Function 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 Function of L,L such that
A1: p is idempotent;
  let x be set;
  assume x in rng p;
  then ex a being object st a in dom p & x = p.a by FUNCT_1:def 3;
  hence thesis by A1,YELLOW_2:18;
end;

theorem Th28:
  for L being non empty Poset, c being Function of L,L, X being
Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c.(inf X
  )
proof
  let L be non empty Poset, c be Function of L,L, X be Subset of L such that
A1: c is projection and
A2: id(L) <= c and
A3: ex_inf_of X,L and
A4: X c= rng c;
A5: c is monotone by A1;
A6: c is idempotent by A1;
  c.(inf X) is_<=_than X
  proof
    let x be Element of L;
    assume
A7: x in X;
    inf X is_<=_than X by A3,YELLOW_0:31;
    then inf X <= x by A7;
    then c.(inf X) <= c.x by A5;
    hence thesis by A4,A6,A7,Lm2;
  end;
  then
A8: c.(inf X) <= inf X by A3,YELLOW_0:31;
  id(L).(inf X) <= c.(inf X) by A2,YELLOW_2:9;
  then inf X <= c.(inf X);
  hence thesis by A8,ORDERS_2:2;
end;

theorem Th29:
  for L being non empty Poset, k being Function of L,L, X being
Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds sup X = k.(sup X)
proof
  let L be non empty Poset, k be Function of L,L, X be Subset of L such that
A1: k is projection and
A2: k <= id(L) and
A3: ex_sup_of X,L and
A4: X c= rng k;
A5: k is monotone by A1;
A6: k is idempotent by A1;
  k.(sup X) is_>=_than X
  proof
    let x be Element of L;
    assume
A7: x in X;
    sup X is_>=_than X by A3,YELLOW_0:30;
    then sup X >= x by A7;
    then k.(sup X) >= k.x by A5;
    hence thesis by A4,A6,A7,Lm2;
  end;
  then
A8: k.(sup X) >= sup X by A3,YELLOW_0:30;
  id(L).(sup X) >= k.(sup X) by A2,YELLOW_2:9;
  then sup X >= k.(sup X);
  hence thesis by A8,ORDERS_2:2;
end;

definition
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  func corestr(g) -> Function of L1,Image g equals
  (the carrier of Image g)|`g;
  coherence
  proof
A1: the carrier of L1 = dom g by FUNCT_2:def 1;
A2: the carrier of Image g = rng g by YELLOW_0:def 15;
    thus thesis by A2,A1,FUNCT_2:1;
  end;
end;

theorem Th30:
  for L1, L2 being non empty RelStr,g being Function of L1,L2
  holds corestr g = g
proof
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  the carrier of Image g = rng g by YELLOW_0:def 15;
  hence thesis;
end;

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

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

theorem Th31:
  for L1, L2 being non empty RelStr, g being Function of L1,L2 st
  g is monotone holds corestr g is monotone
proof
  let L1, L2 be non empty RelStr, g be Function of L1,L2 such that
A1: g is monotone;
  let s1,s2 be Element of L1;
  assume s1 <= s2;
  then
A2: g.s1 <= g.s2 by A1;
  reconsider s19 = g.s1, s29 = g.s2 as Element of L2;
  s19 = (corestr g).s1 & s29 = (corestr g).s2 by Th30;
  hence thesis by A2,YELLOW_0:60;
end;

definition
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  func inclusion(g) -> Function of Image g,L2 equals
  id Image g;
  coherence
  proof
A1: rng id Image g = the carrier of Image g
      .= rng g by YELLOW_0:def 15;
    dom id Image g = the carrier of Image g;
    hence thesis by A1,RELSET_1:4;
  end;
end;

Lm4: for L1, L2 being non empty RelStr,g being Function of L1,L2 holds
inclusion g is monotone
by YELLOW_0:59;

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

theorem Th32:
  for L being non empty RelStr, f being Function of L,L holds (
  inclusion f)*(corestr f) = f
proof
  let L be non empty RelStr, f be Function of L,L;
  thus (inclusion f)*(corestr f) = (id the carrier of Image f)*f by Th30
    .= (id rng f)*f by YELLOW_0:def 15
    .= f by RELAT_1:54;
end;

::Theorem 3.10 (1) implies (2)

theorem Th33:
  for L being non empty Poset, f being Function of L,L st f is
  idempotent holds (corestr f)*(inclusion f) = id(Image f)
proof
  let L be non empty Poset, f be Function 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 object such that
A2: l in the carrier of L and
A3: (corestr f).l = s by FUNCT_2:11;
    reconsider l as Element of L by A2;
A4: (corestr f).l = f.l by Th30;
    thus ((corestr f)*(inclusion f)).s = (corestr f).((inclusion f).s) by
FUNCT_2:15
      .= (corestr f).s
      .= f.(f.l) by A3,A4,Th30
      .= s by A1,A3,A4,YELLOW_2:18;
  end;
  hence thesis by FUNCT_2:124;
end;

::Theorem 3.10 (1) implies (3)

theorem
  for L being non empty Poset, f being Function of L,L st f is
  projection ex T being non empty Poset, q being Function of L,T, i being
Function 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 Function of L,L;
  reconsider T = Image f as non empty Poset;
  reconsider q = corestr f as Function of L,T;
  reconsider i = inclusion f as Function of T,L;
  assume f is projection;
  then
A1: f is monotone idempotent;
  take T,q,i;
  thus q is monotone by A1,Th31;
  thus q is onto;
  thus i is monotone one-to-one;
  thus f = i*q by Th32;
  thus thesis by A1,Th33;
end;

::Theorem 3.10 (3) implies (1)

theorem
  for L being non empty Poset, f being Function of L,L st (ex T being
  non empty Poset, q being Function of L,T, i being Function of T,L st q is
  monotone & i is monotone & f = i*q & id(T) = q*i) holds f is projection
proof
  let L be non empty Poset, f be Function of L,L;
  given T being non empty Poset, q being Function of L,T, i being Function of
  T,L such that
A1: q is monotone & i is monotone and
A2: f = i*q and
A3: id(T) = q*i;
  i*q*i = i*(id the carrier of T) by A3,RELAT_1:36
    .= i by FUNCT_2:17;
  hence f is idempotent by A2,Th21;
  thus thesis by A1,A2,YELLOW_2:12;
end;

::Theorem 3.10 (1_1) implies (2_1)

theorem Th36:
  for L being non empty Poset, f being Function of L,L st f is
  closure holds [inclusion f,corestr f] is Galois
proof
  let L be non empty Poset, f be Function of L,L;
  assume that
A1: f is idempotent monotone and
A2: id L <= f;
  set g = (corestr f), d = inclusion f;
  g*d = id(Image f) by A1,Th33;
  then
A3: g*d <= id(Image f) by Lm1;
  g is monotone & id L <= d*g by A1,A2,Th31,Th32;
  hence thesis by A3,Th19;
end;

::Theorem 3.10 (2_1) implies (3_1)

theorem
  for L being non empty Poset, f being Function of L,L st f is closure
ex S being non empty Poset, g being Function of S,L, d being Function of L,S st
  [g,d] is Galois & f = g*d
proof
  let L be non empty Poset, f be Function of L,L;
  assume
A1: f is closure;
  reconsider S = Image f as non empty Poset;
  reconsider g = inclusion f as Function of S,L;
  reconsider d = corestr f as Function of L,S;
  take S,g,d;
  thus [g,d] is Galois by A1,Th36;
  thus thesis by Th32;
end;

::Theorem 3.10 (3_1) implies (1_1)

theorem Th38:
  for L being non empty Poset, f being Function of L,L st f is
  monotone & ex S being non empty Poset, g being Function of S,L, d being
  Function of L,S st [g,d] is Galois & f = g*d holds f is closure
proof
  let L be non empty Poset, f be Function of L,L such that
A1: f is monotone;
  given S being non empty Poset, g being Function of S,L, d being Function of
  L,S such that
A2: [g,d] is Galois and
A3: f = g*d;
A4: d is monotone & g is monotone by A2,Th8;
  d*g <= id S & id L <= g*d by A2,Th18;
  then g = g*d*g by A4,Th20;
  hence f is idempotent monotone by A1,A3,Th21;
  thus thesis by A2,A3,Th18;
end;

::Theorem 3.10 (1_2) implies (2_2)

theorem Th39:
  for L being non empty Poset, f being Function of L,L st f is
  kernel holds [corestr f,inclusion f] is Galois
proof
  let L be non empty Poset, f be Function of L,L;
  assume that
A1: f is idempotent monotone and
A2: f <= id(L);
  set g = (corestr f), d = inclusion f;
  g*d = id(Image f) by A1,Th33;
  then
A3: id(Image f) <= g*d by Lm1;
  g is monotone & d*g <= id L by A1,A2,Th31,Th32;
  hence thesis by A3,Th19;
end;

::Theorem 3.10 (2_2) implies (3_2)

theorem
  for L being non empty Poset, f being Function of L,L st f is kernel ex
T being non empty Poset, g being Function of L,T, d being Function of T,L st [g
  ,d] is Galois & f = d*g
proof
  let L be non empty Poset, f be Function of L,L;
  assume
A1: f is kernel;
  reconsider T = Image f as non empty Poset;
  reconsider g = corestr f as Function of L,T;
  reconsider d = inclusion f as Function of T,L;
  take T,g,d;
  thus [g,d] is Galois by A1,Th39;
  thus thesis by Th32;
end;

::Theorem 3.10 (3_2) implies (1_2)

theorem
  for L being non empty Poset, f being Function of L,L st f is monotone
& ex T being non empty Poset, g being Function of L,T, d being Function of T,L
  st [g,d] is Galois & f = d*g holds f is kernel
proof
  let L be non empty Poset, f be Function of L,L;
  assume
A1: f is monotone;
  given T being non empty Poset, g being Function of L,T, d being Function of
  T,L such that
A2: [g,d] is Galois and
A3: f = d*g;
A4: d is monotone & g is monotone by A2,Th8;
  d*g <= id L & id T <= g*d by A2,Th18;
  then d = d*g*d by A4,Th20;
  hence f is idempotent monotone by A1,A3,Th21;
  thus thesis by A2,A3,Th18;
end;

:: Lemma 3.11 (i) (part I)

theorem Th42:
  for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L such that
A1: p is idempotent and
  p is monotone;
  set Lk = {k where k is Element of L: p.k <= k};
  set Lc = {c where c is Element of L: c <= p.c};
  thus rng p c= Lc /\ Lk
  proof
    let x be object;
    assume
A2: x in rng p;
    then reconsider x9=x as Element of L;
A3: ex l being object st l in dom p & p.l = x by A2,FUNCT_1:def 3;
    then p.x9 <= x9 by A1,YELLOW_2:18;
    then
A4: x in Lk;
    x9 <= p.x9 by A1,A3,YELLOW_2:18;
    then x in Lc;
    hence thesis by A4,XBOOLE_0:def 4;
  end;
  let x be object;
  assume
A5: x in Lc /\ Lk;
  then x in Lc by XBOOLE_0:def 4;
  then
A6: ex lc being Element of L st x = lc & lc <= p.lc;
  x in Lk by A5,XBOOLE_0:def 4;
  then ex lk being Element of L st x = lk & p.lk <= lk;
  then dom p = the carrier of L & x = p.x by A6,FUNCT_2:def 1,ORDERS_2:2;
  hence thesis by A6,FUNCT_1:def 3;
end;

theorem Th43:
  for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L such that
A1: p is projection;
  defpred Q[Element of L] means p.$1 <= $1;
  defpred P[Element of L] means $1 <= p.$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,Th42;
  Lc is Subset of L from DOMAIN_1:sch 7;
  hence Lc is non empty Subset of L by A2;
  Lk is Subset of L from DOMAIN_1:sch 7;
  hence thesis by A2;
end;

:: Lemma 3.11 (i) (part II)

theorem Th44:
  for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L such that
A1: p is projection;
  set Lk = {k where k is Element of L: p.k <= k};
  set Lc = {c where c is Element of L: c <= p.c};
A2: rng p = Lc /\ Lk by A1,Th42;
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:70;
    let y be object;
    assume
A4: y in rng p;
    then
A5: y in Lc by A2,XBOOLE_0:def 4;
    then
A6: ex lc being Element of L st y = lc & lc <= p.lc;
    y in Lk by A2,A4,XBOOLE_0:def 4;
    then ex lk being Element of L st y = lk & p.lk <= lk;
    then y = p.y by A6,ORDERS_2:2;
    hence thesis by A3,A5,A6,FUNCT_1:50;
  end;
  thus rng(p|Lk) c= rng p by RELAT_1:70;
  let y be object;
  assume
A7: y in rng p;
  then y in Lc by A2,XBOOLE_0:def 4;
  then
A8: ex lc being Element of L st y = lc & lc <= p.lc;
A9: y in Lk by A2,A7,XBOOLE_0:def 4;
  then ex lk being Element of L st y = lk & p.lk <= lk;
  then y = p.y by A8,ORDERS_2:2;
  hence thesis by A3,A9,A8,FUNCT_1:50;
end;

theorem Th45:
  for L being non empty Poset, p being Function of L,L st p is
  projection 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 Function of
  subrelstr Lc,subrelstr Lc
proof
  let L be non empty Poset, p be Function of L,L such that
A1: p is projection;
  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,Th42;
  then rng(p|Lc) = Lc /\ Lk by A1,A2,Th44;
  then
A3: rng(p|Lc) c= Lc by XBOOLE_1:17;
  Lc = the carrier of subrelstr Lc & p|Lc is Function of Lc,the carrier of
  L by FUNCT_2:32,YELLOW_0:def 15;
  hence thesis by A3,FUNCT_2:6;
end;

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

:: Lemma 3.11 (i) (part IIIa)

theorem Th47:
  for L being non empty Poset, p being Function of L,L st p is
projection for Lc being non empty Subset of L st Lc = {c where c is Element of
L: c <= p.c} for pc being Function of subrelstr Lc,subrelstr Lc st pc = p|Lc
  holds pc is closure
proof
  let L be non empty Poset, p be Function 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 Function 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:   x is Element of L by YELLOW_0:58;
A7:   pc.x = p.x by A4,A5,FUNCT_1:47;
      then p.(p.x) = pc.(pc.x) by A4,A5,FUNCT_1:47
        .= (pc*pc).x by A5,FUNCT_1:13;
      hence (pc*pc).x = pc.x by A1,A7,A6,YELLOW_2:18;
    end;
    hence pc*pc = pc by FUNCT_2:63;
    thus pc is monotone
    proof
      let x1,x2 be Element of subrelstr Lc;
      reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
      assume x1 <= x2;
      then x19 <= x29 by YELLOW_0:59;
      then
A8:   p.x19 <= p.x29 by A2;
      pc.x1 = p.x19 & pc.x2 = p.x29 by A4,A5,FUNCT_1:47;
      hence thesis by A8,YELLOW_0:60;
    end;
  end;
  now
    let x be Element of subrelstr Lc;
    reconsider x9=x as Element of L by YELLOW_0:58;
    x in the carrier of subrelstr Lc;
    then x in Lc by YELLOW_0:def 15;
    then
A9: ex c being Element of L st x = c & c <= p.c by A3;
    pc.x = p.x9 by A4,A5,FUNCT_1:47;
    then x <= pc.x by A9,YELLOW_0:60;
    hence (id subrelstr Lc).x <= pc.x;
  end;
  hence thesis by YELLOW_2:9;
end;

:: Lemma 3.11 (i) (part IIIb)

theorem
  for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} for pk being Function of subrelstr Lk,subrelstr Lk st pk = p|Lk
  holds pk is kernel
proof
  let L be non empty Poset, p be Function 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 Function 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:   x is Element of L by YELLOW_0:58;
A7:   pk.x = p.x by A4,A5,FUNCT_1:47;
      then p.(p.x) = pk.(pk.x) by A4,A5,FUNCT_1:47
        .= (pk*pk).x by A5,FUNCT_1:13;
      hence (pk*pk).x = pk.x by A1,A7,A6,YELLOW_2:18;
    end;
    hence pk*pk = pk by FUNCT_2:63;
    thus pk is monotone
    proof
      let x1,x2 be Element of subrelstr Lk;
      reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
      assume x1 <= x2;
      then x19 <= x29 by YELLOW_0:59;
      then
A8:   p.x19 <= p.x29 by A2;
      pk.x1 = p.x19 & pk.x2 = p.x29 by A4,A5,FUNCT_1:47;
      hence thesis by A8,YELLOW_0:60;
    end;
  end;
  now
    let x be Element of subrelstr Lk;
    reconsider x9=x as Element of L by YELLOW_0:58;
    x in the carrier of subrelstr Lk;
    then x in Lk by YELLOW_0:def 15;
    then
A9: ex c being Element of L st x = c & p.c <= c by A3;
    pk.x = p.x9 by A4,A5,FUNCT_1:47;
    then pk.x <= x by A9,YELLOW_0:60;
    hence pk.x <= (id subrelstr Lk).x;
  end;
  hence thesis by YELLOW_2:9;
end;

:: Lemma 3.11 (ii) (part I)

theorem Th49:
  for L being non empty Poset, p being Function 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 Function 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
A5: ex l being Element of L st x = l & l <= p.l by A2;
    ("\/"(X,L)) is_>=_than X by A3,YELLOW_0:30;
    then x <= "\/"(X,L) by A4;
    then p.x <= p.("\/"(X,L)) by A1;
    hence x <= p.("\/"(X,L)) by A5,ORDERS_2:3;
  end;
  then "\/"(X,L) <= p.("\/"(X,L)) by A3,YELLOW_0:30;
  then "\/"(X,L) in Lc by A2;
  hence thesis by YELLOW_0:def 15;
end;

:: Lemma 3.11 (ii) (part II)

theorem Th50:
  for L being non empty Poset, p being Function 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 Function 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
A5: ex l being Element of L st x = l & l >= p.l by A2;
    ("/\"(X,L)) is_<=_than X by A3,YELLOW_0:31;
    then x >= "/\"(X,L) by A4;
    then p.x >= p.("/\"(X,L)) by A1;
    hence thesis by A5,ORDERS_2:3;
  end;
  then "/\"(X,L) >= p.("/\"(X,L)) by A3,YELLOW_0:31;
  then "/\"(X,L) in Lk by A2;
  hence thesis by YELLOW_0:def 15;
end;

:: Lemma 3.11 (iii) (part I)

theorem
  for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L;
  assume
A1: p is projection;
  then reconsider
  Lk = {k where k is Element of L: p.k <= k} as non empty Subset of
  L by Th43;
  let Lc be non empty Subset of L such that
A2: Lc = {c where c is Element of L: c <= p.c};
A3: p is monotone by A1;
  then
A4: subrelstr Lk is infs-inheriting by Th50;
A5: Lc = the carrier of subrelstr Lc by YELLOW_0:def 15;
A6: the carrier of Image p = rng p by YELLOW_0:def 15
    .= Lc /\ Lk by A1,A2,Th42;
  then
A7: the carrier of Image p c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of subrelstr Lk by YELLOW_0:def 15;
A9: the carrier of Image p c= Lc by A6,XBOOLE_1:17;
  hereby
    assume
A10: p is infs-preserving;
    thus
A11: 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 reconsider X9 = X as Subset of L by XBOOLE_1:1;
      assume
A12:  ex_inf_of X,L;
A13:  inf X9 is_<=_than p.:X9
      proof
        let y be Element of L;
        assume y in p.:X9;
        then consider x being Element of L such that
A14:    x in X9 and
A15:    y = p.x by FUNCT_2:65;
        reconsider x as Element of L;
        x in Lc by A5,A14;
        then
A16:    ex x9 being Element of L st x9 = x & x9 <= p.x9 by A2;
        inf X9 is_<=_than X9 by A12,YELLOW_0:31;
        then inf X9 <= x by A14;
        hence inf X9 <= y by A15,A16,ORDERS_2:3;
      end;
      p preserves_inf_of X9 by A10;
      then ex_inf_of p.:X,L & inf (p.:X9) = p.(inf X9) by A12;
      then inf X9 <= p.(inf X9) by A13,YELLOW_0:31;
      hence thesis by A2,A5;
    end;
    thus Image p is infs-inheriting
    proof
      let X be Subset of Image p such that
A17:  ex_inf_of X,L;
      X c= Lc by A9;
      then
A18:  "/\"(X,L) in the carrier of subrelstr Lc by A5,A11,A17;
      subrelstr Lk is infs-inheriting & X c= the carrier of subrelstr Lk
      by A3,A7,A8,Th50;
      then "/\"(X,L) in the carrier of subrelstr Lk by A17;
      hence thesis by A6,A5,A8,A18,XBOOLE_0:def 4;
    end;
  end;
  assume
A19: p is filtered-infs-preserving;
  thus
A20: subrelstr Lc is filtered-infs-inheriting
  proof
    let X be filtered Subset of subrelstr Lc;
    assume X <> {};
    then reconsider X9 = X as non empty filtered Subset of L by YELLOW_2:7;
    assume
A21: ex_inf_of X,L;
A22: inf X9 is_<=_than p.:X9
    proof
      let y be Element of L;
      assume y in p.:X9;
      then consider x being Element of L such that
A23:  x in X9 and
A24:  y = p.x by FUNCT_2:65;
      reconsider x as Element of L;
      x in Lc by A5,A23;
      then
A25:  ex x9 being Element of L st x9 = x & x9 <= p.x9 by A2;
      inf X9 is_<=_than X9 by A21,YELLOW_0:31;
      then inf X9 <= x by A23;
      hence inf X9 <= y by A24,A25,ORDERS_2:3;
    end;
    p preserves_inf_of X9 by A19;
    then ex_inf_of p.:X,L & inf (p.:X9) = p.(inf X9) by A21;
    then inf X9 <= p.(inf X9) by A22,YELLOW_0:31;
    hence thesis by A2,A5;
  end;
  let X be filtered Subset of Image p such that
A26: X <> {} and
A27: ex_inf_of X,L;
  the carrier of Image p c= the carrier of subrelstr Lc by A9,YELLOW_0:def 15;
  then X is filtered Subset of subrelstr Lc by YELLOW_2:8;
  then
A28: "/\"(X,L) in the carrier of subrelstr Lc by A20,A26,A27;
  X c= the carrier of subrelstr Lk by A7,A8;
  then "/\"(X,L) in the carrier of subrelstr Lk by A27,A4;
  hence thesis by A6,A5,A8,A28,XBOOLE_0:def 4;
end;

:: Lemma 3.11 (iii) (part II)

theorem
  for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L;
  assume
A1: p is projection;
  then reconsider
  Lc = {c where c is Element of L: c <= p.c} as non empty Subset of
  L by Th43;
  let Lk be non empty Subset of L such that
A2: Lk = {k where k is Element of L: p.k <= k};
A3: p is monotone by A1;
  then
A4: subrelstr Lc is sups-inheriting by Th49;
A5: Lc = the carrier of subrelstr Lc by YELLOW_0:def 15;
A6: the carrier of Image p = rng p by YELLOW_0:def 15
    .= Lc /\ Lk by A1,A2,Th42;
  then
A7: the carrier of Image p c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of subrelstr Lk by YELLOW_0:def 15;
A9: the carrier of Image p c= Lc by A6,XBOOLE_1:17;
  hereby
    assume
A10: p is sups-preserving;
    thus
A11: 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 reconsider X9 = X as Subset of L by XBOOLE_1:1;
      assume
A12:  ex_sup_of X,L;
A13:  sup X9 is_>=_than p.:X9
      proof
        let y be Element of L;
        assume y in p.:X9;
        then consider x being Element of L such that
A14:    x in X9 and
A15:    y = p.x by FUNCT_2:65;
        reconsider x as Element of L;
        x in Lk by A8,A14;
        then
A16:    ex x9 being Element of L st x9 = x & x9 >= p.x9 by A2;
        sup X9 is_>=_than X9 by A12,YELLOW_0:30;
        then sup X9 >= x by A14;
        hence thesis by A15,A16,ORDERS_2:3;
      end;
      p preserves_sup_of X9 by A10;
      then ex_sup_of p.:X,L & sup (p.:X9) = p.(sup X9) by A12;
      then sup X9 >= p.(sup X9) by A13,YELLOW_0:30;
      hence thesis by A2,A8;
    end;
    thus Image p is sups-inheriting
    proof
      let X be Subset of Image p such that
A17:  ex_sup_of X,L;
      X c= Lk by A7;
      then
A18:  "\/"(X,L) in the carrier of subrelstr Lk by A8,A11,A17;
      subrelstr Lc is sups-inheriting & X c= the carrier of subrelstr Lc
      by A3,A9,A5,Th49;
      then "\/"(X,L) in the carrier of subrelstr Lc by A17;
      hence thesis by A6,A5,A8,A18,XBOOLE_0:def 4;
    end;
  end;
  assume
A19: p is directed-sups-preserving;
  thus
A20: subrelstr Lk is directed-sups-inheriting
  proof
    let X be directed Subset of subrelstr Lk;
    assume X <> {};
    then reconsider X9 = X as non empty directed Subset of L by YELLOW_2:7;
    assume
A21: ex_sup_of X,L;
A22: sup X9 is_>=_than p.:X9
    proof
      let y be Element of L;
      assume y in p.:X9;
      then consider x being Element of L such that
A23:  x in X9 and
A24:  y = p.x by FUNCT_2:65;
      reconsider x as Element of L;
      x in Lk by A8,A23;
      then
A25:  ex x9 being Element of L st x9 = x & x9 >= p.x9 by A2;
      sup X9 is_>=_than X9 by A21,YELLOW_0:30;
      then sup X9 >= x by A23;
      hence thesis by A24,A25,ORDERS_2:3;
    end;
    p preserves_sup_of X9 by A19;
    then ex_sup_of p.:X,L & sup (p.:X9) = p.(sup X9) by A21;
    then sup X9 >= p.(sup X9) by A22,YELLOW_0:30;
    hence thesis by A2,A8;
  end;
  let X be directed Subset of Image p such that
A26: X <> {} and
A27: ex_sup_of X,L;
  the carrier of Image p c= the carrier of subrelstr Lk by A7,YELLOW_0:def 15;
  then X is directed Subset of subrelstr Lk by YELLOW_2:8;
  then
A28: "\/"(X,L) in the carrier of subrelstr Lk by A20,A26,A27;
  X c= the carrier of subrelstr Lc by A9,A5;
  then "\/"(X,L) in the carrier of subrelstr Lc by A27,A4;
  hence thesis by A6,A5,A8,A28,XBOOLE_0:def 4;
end;

:: Proposition 3.12 (i)

theorem Th53:
  for L being non empty Poset, p being Function of L,L holds (p is
  closure implies Image p is infs-inheriting) & (p is kernel implies Image p is
  sups-inheriting)
proof
  let L be non empty Poset, p be Function of L,L;
  hereby
    assume
A1: p is closure;
    thus Image p is infs-inheriting
    proof
      let X be Subset of Image p;
A2:   the carrier of Image p = rng p by YELLOW_0:def 15;
      then reconsider X9=X as Subset of L by XBOOLE_1:1;
      assume ex_inf_of X,L;
      then p.("/\"(X9,L)) = "/\"(X9,L) by A1,A2,Th28;
      hence thesis by A2,FUNCT_2:4;
    end;
  end;
  assume
A3: p is kernel;
  let X be Subset of Image p;
A4: the carrier of Image p = rng p by YELLOW_0:def 15;
  then reconsider X9=X as Subset of L by XBOOLE_1:1;
  assume ex_sup_of X,L;
  then p.("\/"(X9,L)) = "\/"(X9,L) by A3,A4,Th29;
  hence thesis by A4,FUNCT_2:4;
end;

:: Proposition 3.12 (ii)

theorem
  for L being complete non empty Poset, p being Function of L,L st p
  is projection holds Image p is complete
proof
  let L be complete non empty Poset, p be Function of L,L;
A1: the carrier of Image p = rng p by YELLOW_0:def 15;
  assume
A2: p is projection;
  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 Th43;
A3: the carrier of subrelstr Lc = Lc & rng p = Lc /\ Lk by A2,Th42,
YELLOW_0:def 15;
  p is monotone by A2;
  then subrelstr Lc is sups-inheriting by Th49;
  then
A4: subrelstr Lc is complete LATTICE by YELLOW_2:31;
  reconsider pc = p|Lc as Function of subrelstr Lc,subrelstr Lc by A2,Th45;
A5: Image pc is infs-inheriting by A2,Th47,Th53;
A6: the carrier of Image pc = rng(pc) by YELLOW_0:def 15
    .= the carrier of Image p by A2,A1,Th44;
  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 A1,A3,WELLORD1:22
,XBOOLE_1:17
    .= the InternalRel of Image p by YELLOW_0:def 14;
  hence thesis by A4,A5,A6,YELLOW_2:30;
end;

:: Proposition 3.12 (iii)

theorem
  for L being non empty Poset, c being Function of L,L st c is closure
  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 Function of L,L;
A1: (corestr c) = c by Th30;
  assume
A2: c is closure;
  then
A3: c is idempotent by Def13;
  [inclusion c,corestr c] is Galois by A2,Th36;
  then
A4: corestr c is lower_adjoint;
  hence corestr c is sups-preserving;
  let X be Subset of L such that
A5: X c= the carrier of Image c and
A6: ex_sup_of X,L;
  X c= rng c by A5,YELLOW_0:def 15;
  then
A7: c.:X = X by A3,YELLOW_2:20;
  corestr c preserves_sup_of X by A4,WAYBEL_0:def 33;
  hence thesis by A6,A1,A7;
end;

:: Proposition 3.12 (iv)

theorem
  for L being non empty Poset, k being Function of L,L st k is kernel
  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 Function of L,L;
A1: (corestr k) = k by Th30;
  assume
A2: k is kernel;
  then
A3: k is idempotent by Def13;
  [corestr k,inclusion k] is Galois by A2,Th39;
  then
A4: corestr k is upper_adjoint;
  hence (corestr k) is infs-preserving;
  let X be Subset of L such that
A5: X c= the carrier of Image k and
A6: ex_inf_of X,L;
  X c= rng k by A5,YELLOW_0:def 15;
  then
A7: k.:X = X by A3,YELLOW_2:20;
  corestr k preserves_inf_of X by A4,WAYBEL_0:def 32;
  hence thesis by A6,A1,A7;
end;

begin :: Heyting algebras
:: Proposition 3.15 (i)

theorem Th57:
  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 I9 = I as Ideal of L by YELLOW_2:41;
    hereby
      assume I <= g.x;
      then I c= g.x by YELLOW_1:3;
      then I9 c= downarrow x by YELLOW_2:def 4;
      then x is_>=_than I9 by YELLOW_2:1;
      then sup I9 <= x by YELLOW_0:32;
      hence d.I <= x by YELLOW_2:def 3;
    end;
    assume d.I <= x;
    then
A1: sup I9 <= x by YELLOW_2:def 3;
    sup I9 is_>=_than I9 by YELLOW_0:32;
    then x is_>=_than I9 by A1,YELLOW_0:4;
    then I9 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;
  then SupMap L is lower_adjoint;
  hence thesis;
end;

:: Proposition 3.15 (ii)

theorem
  for L being complete non empty Poset holds (IdsMap L)*(SupMap L) is
  closure & Image ((IdsMap L)*(SupMap L)),L are_isomorphic
proof
  let L be complete non empty Poset;
  set i = (IdsMap L)*(SupMap L);
A1: now
    let I be Ideal of L;
    I is Element of InclPoset(Ids L) by YELLOW_2:41;
    hence i.I = (IdsMap L).((SupMap L).I) by FUNCT_2:15
      .= (IdsMap L).(sup I) by YELLOW_2:def 3
      .= downarrow (sup I) by YELLOW_2:def 4;
  end;
  i is monotone & [IdsMap L,SupMap L] is Galois by Th57,YELLOW_2:12;
  hence i is closure by Th38;
  take f = (SupMap L)*(inclusion i);
A2: now
    let x be Element of Image i;
    let I be Ideal of L;
    assume
A3: x = I;
    hence f.I = (SupMap L).((inclusion i).I) by FUNCT_2:15
      .= (SupMap L).I by A3
      .= sup I by YELLOW_2:def 3;
  end;
A4: f is monotone by YELLOW_2:12;
A5: now
    let x,y be Element of Image i;
    consider Ix being Element of InclPoset(Ids L) such that
A6: i.Ix = x by YELLOW_2:10;
    thus x <= y implies f.x <= f.y by A4;
    assume
A7: f.x <= f.y;
    x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L)
    by YELLOW_0:58;
    then reconsider x9=x, y9=y as Ideal of L by YELLOW_2:41;
    consider Iy being Element of InclPoset(Ids L) such that
A8: i.Iy = y by YELLOW_2:10;
    reconsider Ix,Iy as Ideal of L by YELLOW_2:41;
    reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of
    InclPoset(Ids L) by YELLOW_2:41;
A9: i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A1;
A10: f.x9 = sup x9 & f.y9 = sup y9 by A2;
    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 A7,A6,A8,A9,A10,
WAYBEL_0:21;
    then i1 <= i2 by YELLOW_1:3;
    hence x <= y by A6,A8,A9,YELLOW_0:60;
  end;
A11: rng f = the carrier of L
  proof
    thus rng f c= the carrier of L;
    let x be object;
    assume x in the carrier of L;
    then reconsider x as Element of L;
A12: (SupMap L).(downarrow x) = sup downarrow x by YELLOW_2:def 3
      .= x by WAYBEL_0:34;
A13: downarrow x is Element of InclPoset(Ids L) by YELLOW_2:41;
    then i.(downarrow x) = (IdsMap L).((SupMap L).(downarrow x)) by FUNCT_2:15
      .= downarrow x by A12,YELLOW_2:def 4;
    then downarrow x in rng i by A13,FUNCT_2:4;
    then
A14: downarrow x in the carrier of Image i by YELLOW_0:def 15;
    then f.(downarrow x) = (SupMap L).((inclusion i).(downarrow x)) by
FUNCT_2:15
      .= (SupMap L).(downarrow x) by A14,FUNCT_1:18;
    hence thesis by A12,A14,FUNCT_2:4;
  end;
  f is one-to-one
  proof
    let x,y be Element of Image i;
    assume
A15: f.x = f.y;
    consider Ix being Element of InclPoset(Ids L) such that
A16: i.Ix = x by YELLOW_2:10;
    consider Iy being Element of InclPoset(Ids L) such that
A17: i.Iy = y by YELLOW_2:10;
    x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L)
    by YELLOW_0:58;
    then reconsider x,y as Ideal of L by YELLOW_2:41;
    reconsider Ix,Iy as Ideal of L by YELLOW_2:41;
A18: sup downarrow (sup Ix) = sup Ix by WAYBEL_0:34;
A19: i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A1;
    f.x = sup x & f.y = sup y by A2;
    hence thesis by A15,A16,A17,A19,A18,WAYBEL_0:34;
  end;
  hence thesis by A11,A5,WAYBEL_0:66;
end;

definition
  let S be non empty RelStr;
  let x be Element of S;
  func x "/\" -> Function 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 Function of S,S st for x being Element of S holds f.x = F(
    x) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let f1,f2 be Function 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 FUNCT_2:63;
  end;
end;

theorem Th59:
  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 object;
    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:38;
  end;
  let s be object;
  assume
A3: s in (x "/\")"(downarrow t);
  then reconsider s as Element of S;
  (x "/\").s in downarrow t by A3,FUNCT_2:38;
  then x"/\"s in downarrow t by Def18;
  then x"/\"s <= t by WAYBEL_0:17;
  hence thesis;
end;

theorem Th60:
  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,s1},S by YELLOW_0:21;
  then
A3: x"/\"s1 <= x by YELLOW_0:19;
  x"/\"s1 <= s1 by A2,YELLOW_0:19;
  then ex_inf_of {x,s2},S & x"/\"s1 <= s2 by A1,ORDERS_2:3,YELLOW_0:21;
  then x"/\"s1 <= x"/\"s2 by A3,YELLOW_0:19;
  then (x "/\").s1 <= x"/\"s2 by Def18;
  hence (x "/\").s1 <= (x "/\").s2 by Def18;
end;

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

theorem Th61:
  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 object;
    assume y in (x "/\").:X;
    then consider z being object such that
A1: z in the carrier of S and
A2: z in X and
A3: y = (x "/\").z by FUNCT_2:64;
    reconsider z as Element of S by A1;
    y = x "/\" z by A3,Def18;
    hence y in Y by A2;
  end;
  let y be object;
  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 thesis by A5,FUNCT_2:35;
end;

:: Lemma 3.16 (1) iff (2)

theorem Th62:
  for S being Semilattice holds (for x being Element of S holds x
"/\" is lower_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 "/\" is lower_adjoint;
    let x,t be Element of S;
    (x "/\") is lower_adjoint by A1;
    then consider g being Function of S,S such that
A2: [g, x "/\"] is Galois;
    set X = {s where s is Element of S: x"/\"s <= t};
A3: X = (x "/\")"(downarrow t) by Th59;
    g.t is_maximum_of (x "/\")"(downarrow t) by A2,Th11;
    then ex_sup_of X,S & "\/"(X,S)in X by A3;
    hence ex_max_of X,S;
  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 Function of S,S such that
A5: for s being Element of S holds g.s = F(s) from FUNCT_2:sch 4;
  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;
    X = (x "/\")"(downarrow t) & g.t = "\/"((x "/\")"(downarrow t),S) by A5
,Th59;
    hence g.t is_maximum_of (x "/\")"(downarrow t) by A6;
  end;
  then [g, x "/\"] is Galois by Th11;
  hence thesis;
end;

:: Lemma 3.16 (1) implies (3)

theorem Th63:
  for S being Semilattice st for x being Element of S holds x "/\"
  is lower_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 "/\" is lower_adjoint;
  let X be Subset of S such that
A2: ex_sup_of X,S;
  let x be Element of S;
  x "/\" is sups-preserving by A1,Th13;
  then x "/\" preserves_sup_of X;
  then sup ((x "/\").:X) = (x "/\").(sup X) by A2;
  hence x "/\" "\/"(X,S) = sup ((x "/\").:X) by Def18
    .= "\/"({x"/\" y where y is Element of S: y in X},S) by Th61;
end;

:: Lemma 3.16 (1) iff (3)

theorem
  for S being complete non empty Poset holds (for x being Element of S
holds x "/\" is lower_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;
  thus (for x being Element of S holds x "/\" is lower_adjoint) implies 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) by Th63,YELLOW_0:17;
  assume
A1: 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 A1
      .= sup ((x "/\").:X) by Th61;
  end;
  hence thesis by Th17;
end;

:: Lemma 3.16 (3) implies (D)

theorem Th65:
  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}};
A2: ex_sup_of {y,z},S by YELLOW_0:20;
  now
    let t be object;
    hereby
      assume t in Y;
      then ex s being Element of S st t = x"/\"s & s in {y,z};
      hence t = x"/\"y or t = x"/\"z by TARSKI:def 2;
    end;
    assume
A3: t = x"/\"y or t = x"/\"z;
    per cases by A3;
    suppose
A4:   t = x"/\"y;
      y in {y,z} by TARSKI:def 2;
      hence t in Y by A4;
    end;
    suppose
A5:   t = x"/\"z;
      z in {y,z} by TARSKI:def 2;
      hence t in Y by A5;
    end;
  end;
  then
A6: Y = {x"/\"y,x"/\"z} by TARSKI:def 2;
  thus x "/\" (y "\/" z) = x "/\" (sup {y,z}) by YELLOW_0:41
    .= "\/"({x"/\"y,x"/\"z},S) by A1,A6,A2
    .= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41;
end;

definition
  let H be non empty RelStr;
  attr H is Heyting means

  H is LATTICE & for x being Element of H holds x "/\" is lower_adjoint;
end;

registration
  cluster Heyting -> with_infima with_suprema reflexive transitive
    antisymmetric for non empty RelStr;
  coherence;
end;

definition
  let H be non empty RelStr, a be Element of H;
  assume
A1: H is Heyting;
  func a => -> Function of H,H means
  :Def20:
  [it,a "/\"] is Galois;
  existence
  by A1,Def12;
  uniqueness
  proof
    let g1,g2 be Function of H,H such that
A2: [g1,a "/\"] is Galois and
A3: [g2,a "/\"] is Galois;
    now
      let x be Element of H;
      g1.x is_maximum_of (a "/\")"(downarrow x) by A1,A2,Th11;
      then
A4:   g1.x = "\/"((a "/\")"(downarrow x),H);
      g2.x is_maximum_of (a "/\")"(downarrow x) by A1,A3,Th11;
      hence g1.x = g2.x by A4;
    end;
    hence g1 = g2 by FUNCT_2:63;
  end;
end;

theorem Th66:
  for H being non empty RelStr st H is Heyting holds H is distributive
proof
  let H be non empty RelStr;
  assume that
A1: H is LATTICE and
A2: for x being Element of H holds x "/\" is lower_adjoint;
  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 A1,A2
,Th63;
  hence thesis by A1,Th65;
end;

registration
  cluster Heyting -> distributive for non empty RelStr;
  coherence by Th66;
end;

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

theorem Th67:
  for H being non empty RelStr st H is Heyting 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 Heyting;
  let x,a,y be Element of H;
  [a =>, a "/\"] is Galois by A1,Def20;
  then x >= (a "/\").y iff (a =>).x >= y by A1,Th8;
  hence thesis by Def18;
end;

theorem Th68:
  for H being non empty RelStr st H is Heyting holds H is upper-bounded
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  set a = the Element of H;
  take a => a;
  let y be Element of H;
  assume y in the carrier of H;
  a >= a "/\" y by A1,YELLOW_0:23;
  hence thesis by A1,Th67;
end;

registration
  cluster Heyting -> upper-bounded for non empty RelStr;
  coherence by Th68;
end;

theorem Th69:
  for H being non empty RelStr st H is Heyting 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 Heyting;
  let a,b be Element of H;
A2: a "/\" Top H = Top H "/\" a by A1,LATTICE3:15
    .= a by A1,Th4;
  hereby
    assume Top H = a => b;
    then a => b >= Top H by A1,ORDERS_2:1;
    hence a <= b by A1,A2,Th67;
  end;
  assume a <= b;
  then
A3: a => b >= Top H by A1,A2,Th67;
  a => b <= Top H by A1,YELLOW_0:45;
  hence thesis by A1,A3,ORDERS_2:2;
end;

theorem
  for H being non empty RelStr st H is Heyting for a being Element of H
  holds Top H = a => a
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  let a be Element of H;
  a >= a "/\" Top H by A1,YELLOW_0:23;
  then
A2: Top H <= a => a by A1,Th67;
  Top H >= a => a by A1,YELLOW_0:45;
  hence thesis by A1,A2,ORDERS_2:2;
end;

theorem
  for H being non empty RelStr st H is Heyting 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 Heyting;
  let a,b be Element of H;
  assume
A2: Top H = a => b;
  assume Top H = b => a;
  then
A3: b <= a by A1,Th69;
  a <= b by A1,A2,Th69;
  hence thesis by A1,A3,ORDERS_2:2;
end;

theorem Th72:
  for H being non empty RelStr st H is Heyting for a,b being
  Element of H holds b <= (a => b)
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  let a,b be Element of H;
  a"/\"b <= b by A1,YELLOW_0:23;
  hence thesis by A1,Th67;
end;

theorem
  for H being non empty RelStr st H is Heyting for a being Element of H
  holds Top H = a => Top H
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  let a be Element of H;
  a <= Top H by A1,YELLOW_0:45;
  hence thesis by A1,Th69;
end;

theorem
  for H being non empty RelStr st H is Heyting for b being Element of H
  holds b = (Top H) => b
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  let b be Element of H;
  (Top H) => b <= (Top H) => b by A1,ORDERS_2:1;
  then Top H "/\" ((Top H) => b) <= b by A1,Th67;
  then
A2: (Top H) => b <= b by A1,Th4;
  (Top H) => b >= b by A1,Th72;
  hence thesis by A1,A2,ORDERS_2:2;
end;

Lm5: for H being non empty RelStr st H is Heyting for a,b being Element of H
holds a"/\"(a => b) <= b
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  let a,b be Element of H;
  (a => b) <= (a => b) by A1,ORDERS_2:1;
  hence thesis by A1,Th67;
end;

theorem Th75:
  for H being non empty RelStr st H is Heyting 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 Heyting;
  let a,b,c be Element of H;
  assume a <= b;
  then
A2: a"/\"(b => c) <= b"/\"(b => c) by A1,Th1;
  b"/\"(b => c) <= c by A1,Lm5;
  then a"/\"(b => c) <= c by A1,A2,ORDERS_2:3;
  hence thesis by A1,Th67;
end;

theorem
  for H being non empty RelStr st H is Heyting 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 Heyting;
  let a,b,c be Element of H;
  assume
A2: b <= c;
  a"/\"(a => b) <= b by A1,Lm5;
  then a"/\"(a => b) <= c by A1,A2,ORDERS_2:3;
  hence thesis by A1,Th67;
end;

theorem Th77:
  for H being non empty RelStr st H is Heyting for a,b being
  Element of H holds a"/\"(a => b) = a"/\"b
proof
  let H be non empty RelStr;
  assume
A1: H is Heyting;
  let a,b be Element of H;
  (a"/\"(a => b))"/\"a <= b"/\"a by A1,Lm5,Th1;
  then a"/\"(a"/\"(a => b)) <= b"/\"a by A1,LATTICE3:15;
  then a"/\"(a"/\"(a => b)) <= a"/\"b by A1,LATTICE3:15;
  then (a"/\"a)"/\"(a => b) <= a"/\"b by A1,LATTICE3:16;
  then
A2: a"/\"(a => b) <= a"/\"b by A1,YELLOW_0:25;
  b"/\"a <= (a => b)"/\"a by A1,Th1,Th72;
  then a"/\"b <= (a => b)"/\"a by A1,LATTICE3:15;
  then a"/\"b <= a"/\"(a => b) by A1,LATTICE3:15;
  hence thesis by A1,A2,ORDERS_2:2;
end;

theorem Th78:
  for H being non empty RelStr st H is Heyting 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 Heyting;
  let a,b,c be Element of H;
  ((a"/\"c)"/\"(b=>c)) <= a"/\"c & a"/\"c <= c by A1,YELLOW_0:23;
  then
A2: ((a"/\"c)"/\"(b=>c)) <= c by A1,ORDERS_2:3;
  ((b"/\"c)"/\"(a=>c)) <= b"/\"c & b"/\"c <= c by A1,YELLOW_0:23;
  then
A3: ((b"/\"c)"/\"(a=>c)) <= c by A1,ORDERS_2:3;
  set d = (a => c) "/\" (b => c);
  (a"\/"b)"/\"d = d"/\"(a"\/"b) by A1,LATTICE3:15
    .= (d"/\"a)"\/"(d"/\"b) by A1,Def3
    .= (a"/\"d)"\/"(d"/\"b) by A1,LATTICE3:15
    .= (a"/\"d)"\/"(b"/\"d) by A1,LATTICE3:15
    .= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"d) by A1,LATTICE3:16
    .= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"((b=>c)"/\"(a=>c))) by A1,LATTICE3:15
    .= ((a"/\"(a=>c))"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A1,LATTICE3:16
    .= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A1,Th77
    .= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"c)"/\"(a=>c)) by A1,Th77;
  then (a"\/"b)"/\"d <= c by A1,A2,A3,YELLOW_0:22;
  then
A4: (a"\/"b)=> c >= d by A1,Th67;
  b <= a"\/"b by A1,YELLOW_0:22;
  then
A5: (a"\/"b)=> c <= (b => c) by A1,Th75;
  a <= a"\/"b by A1,YELLOW_0:22;
  then (a"\/"b)=> c <= (a => c) by A1,Th75;
  then (a"\/"b)=> c <= (a => c) "/\" (b => c) by A1,A5,YELLOW_0:23;
  hence thesis by A1,A4,ORDERS_2:2;
end;

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

theorem
  for H being non empty RelStr st H is Heyting & 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 Heyting and
A2: H is lower-bounded;
  let a be Element of H;
  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};
A3: X = Y
  proof
    hereby
      let y be object;
      assume y in X;
      then consider x being Element of H such that
A4:   y = x and
A5:   a"/\"x = Bottom H;
      a"/\"x <= Bottom H by A1,A5,ORDERS_2:1;
      hence y in Y by A4;
    end;
    let y be object;
    assume y in Y;
    then consider x being Element of H such that
A6: y = x and
A7: a"/\"x <= Bottom H;
    Bottom H <= a"/\"x by A1,A2,YELLOW_0:44;
    then Bottom H = a"/\"x by A1,A7,ORDERS_2:2;
    hence thesis by A6;
  end;
A8: now
    a => (Bottom H) <= a => (Bottom H) by A1,ORDERS_2:1;
    then a"/\"'not' a <= Bottom H by A1,Th67;
    then
A9: 'not' a in X by A3;
    let b be Element of H;
    assume b is_>=_than X;
    hence 'not' a <= b by A9;
  end;
A10: ex_max_of X,H by A1,A3,Th62;
  hence ex_sup_of X,H;
  'not' a is_>=_than X
  proof
    let b be Element of H;
    assume b in X;
    then ex x being Element of H st x = b & a"/\"x <= Bottom H by A3;
    hence thesis by A1,Th67;
  end;
  hence 'not' a = "\/"(X,H) by A1,A8,YELLOW_0:30;
  thus thesis by A10;
end;

theorem Th80:
  for H being non empty RelStr st H is Heyting & 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 Heyting and
A2: H is lower-bounded;
  (Top H) => (Bottom H) <= (Top H) => (Bottom H) by A1,ORDERS_2:1;
  then
A3: Bottom H >= Top H "/\" 'not' Top H by A1,Th67;
  Bottom H >= Bottom H "/\" Top H by A1,YELLOW_0:23;
  then
A4: Top H <= (Bottom H) => (Bottom H) by A1,Th67;
  Bottom H <= Top H "/\" 'not' Top H by A1,A2,YELLOW_0:44;
  then
A5: Bottom H = Top H "/\" 'not' Top H by A1,A3,ORDERS_2:2;
  'not' Bottom H <= Top H by A1,YELLOW_0:45;
  hence Top H = 'not' Bottom H by A1,A4,ORDERS_2:2;
  'not' Top H <= Top H by A1,YELLOW_0:45;
  hence 'not' Top H = 'not' Top H"/\"Top H by A1,YELLOW_0:25
    .= Bottom H by A1,A5,LATTICE3:15;
end;

:: Exercise 3.18 (i)

theorem
  for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
  let a,b be Element of H;
A2: Bottom H >= a "/\" b iff a => Bottom H >= b by A1,Th67;
  Bottom H >= b "/\" a iff b => Bottom H >= a by A1,Th67;
  hence thesis by A1,A2,LATTICE3:15;
end;

:: Exercise 3.18 (ii)

theorem Th82:
  for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
  let a,b be Element of H;
  hereby
    assume 'not' a >= b;
    then
A2: a "/\" b <= Bottom H by A1,Th67;
    a "/\" b >= Bottom H by A1,YELLOW_0:44;
    hence a "/\" b = Bottom H by A1,A2,ORDERS_2:2;
  end;
  assume a "/\" b = Bottom H;
  then a "/\" b <= Bottom H by A1,ORDERS_2:1;
  hence thesis by A1,Th67;
end;

theorem
  for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
  let a,b be Element of H;
A2: 'not' b >= 'not' b by A1,ORDERS_2:1;
  assume a <= b;
  then a "/\" 'not' b = (a"/\"b)"/\"'not' b by A1,YELLOW_0:25
    .= a"/\"(b"/\"'not' b) by A1,LATTICE3:16
    .= a"/\"Bottom H by A1,A2,Th82
    .= Bottom H"/\"a by A1,LATTICE3:15
    .= Bottom H by A1,Th3;
  hence thesis by A1,Th82;
end;

theorem
  for H being non empty lower-bounded RelStr st H is Heyting for a,b
  being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b by Th78;

theorem
  for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
  then
A2: Bottom H<=Bottom H by ORDERS_2:1;
  let a,b be Element of H;
A3: 'not' a <= 'not' a by A1,ORDERS_2:1;
A4: 'not' b <= 'not' b by A1,ORDERS_2:1;
  (a"/\"b)"/\"('not' a"\/"'not' b) = ((a"/\"b)"/\"'not' a)"\/"((a"/\"b)
  "/\" 'not' b) by A1,Def3
    .= ((b"/\"a)"/\"'not' a)"\/"((a"/\"b)"/\" 'not' b) by A1,LATTICE3:15
    .= (b"/\"(a"/\"'not' a))"\/"((a"/\"b)"/\" 'not' b) by A1,LATTICE3:16
    .= (b"/\"(a"/\"'not' a))"\/"(a"/\"(b"/\" 'not' b)) by A1,LATTICE3:16
    .= (b"/\"Bottom H)"\/"(a"/\"(b"/\"'not' b)) by A1,A3,Th82
    .= (b"/\"Bottom H)"\/"(a"/\"Bottom H) by A1,A4,Th82
    .= (Bottom H"/\"b)"\/"(a"/\"Bottom H) by A1,LATTICE3:15
    .= (Bottom H"/\"b)"\/"(Bottom H"/\"a) by A1,LATTICE3:15
    .= Bottom H"\/"(Bottom H"/\"a) by A1,Th3
    .= Bottom H"\/"Bottom H by A1,Th3
    .= Bottom H by A1,A2,YELLOW_0:24;
  hence thesis by A1,Th82;
end;

definition
  let L be non empty RelStr, x,y be Element of L;
  pred y is_a_complement_of x means

  x "\/" y = Top L & x "/\" y = Bottom L;
end;

definition
  let L be non empty RelStr;
  attr L is complemented means

  for x being Element of L ex y being Element of L st y is_a_complement_of x;
end;

registration
  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
      .= bool X by LATTICE3:def 1;
    then reconsider y = X\x as Element of BoolePoset X by XBOOLE_1:109;
    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
      .= Bottom (BoolePoset X) by YELLOW_1:18;
  end;
end;

:: Exercise 3.19  (1) implies (3)

Lm6: for L being bounded LATTICE st L is distributive complemented for x being
Element of L ex x9 being Element of L st for y being Element of L holds (y "\/"
x9) "/\" x <= y & y <= (y "/\" x) "\/" x9
proof
  let L be bounded LATTICE such that
A1: L is distributive and
A2: L is complemented;
  let x be Element of L;
  consider x9 being Element of L such that
A3: x9 is_a_complement_of x by A2;
  take x9;
  let y be Element of L;
  (y "\/" x9) "/\" x = (x "/\" y) "\/" (x "/\" x9) by A1
    .= Bottom L "\/" (x "/\" y) by A3
    .= x "/\" y by Th3;
  hence (y "\/" x9) "/\" x <= y by YELLOW_0:23;
  (y "/\" x) "\/" x9 = (x9 "\/" y) "/\" (x9 "\/" x) by A1,Th5
    .= (x9 "\/" y) "/\" Top L by A3
    .= x9 "\/" y by Th4;
  hence thesis by YELLOW_0:22;
end;

:: Exercise 3.19  (3) implies (2)

Lm7: for L being bounded LATTICE st for x being Element of L ex x9 being
Element of L st for y being Element of L holds (y "\/" x9) "/\" x <= y & y <= (
y "/\" x) "\/" x9 holds L is Heyting & 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 x9 being Element of L st P[x,x9];
  consider g9 being Function of L,L such that
A2: for x being Element of L holds P[x,g9.x] from FUNCT_2:sch 3(A1);
A3: now
    let y be Element of L;
    let g be Function of L,L such that
A4: for z being Element of L holds g.z = g9.y "\/" z;
A5: now
      let x be Element of L, z be Element of L;
      hereby
        assume x <= g.z;
        then x <= g9.y "\/" z by A4;
        then
A6:     x "/\" y <= (g9.y "\/" z) "/\" y by Th1;
        (g9.y "\/" z) "/\" y <= z by A2;
        then x "/\" y <= z by A6,ORDERS_2:3;
        hence (y "/\").x <= z by Def18;
      end;
      assume (y "/\").x <= z;
      then y "/\" x <= z by Def18;
      then
A7:   (x "/\" y) "\/" g9.y <= z "\/" g9.y by Th2;
      x <= (x "/\" y) "\/" g9.y by A2;
      then x <= z "\/" g9.y by A7,ORDERS_2:3;
      hence x <= g.z by A4;
    end;
    g is monotone
    proof
      let z1,z2 be Element of L;
      assume z1 <= z2;
      then g9.y "\/" z1 <= z2 "\/" g9.y by Th2;
      then g.z1 <= g9.y "\/" z2 by A4;
      hence thesis by A4;
    end;
    hence [g,y "/\"] is Galois by A5;
  end;
  thus
A8: L is Heyting
  proof
    thus L is LATTICE;
    let y be Element of L;
    deffunc F(Element of L) = g9.y "\/" $1;
    consider g being Function of L,L such that
A9: for z being Element of L holds g.z = F(z) from FUNCT_2:sch 4;
    [g,y "/\"] is Galois by A3,A9;
    hence thesis;
  end;
A10: now
    let x be Element of L;
    deffunc F(Element of L) = g9.x "\/" $1;
    consider g being Function of L,L such that
A11: for z being Element of L holds g.z = F(z) from FUNCT_2:sch 4;
    [g,x "/\"] is Galois by A3,A11;
    then g = x => by A8,Def20;
    hence 'not' x = Bottom L "\/" g9.x by A11
      .= g9.x by Th3;
  end;
A12: now
    let x be Element of L;
    (Bottom L "\/" g9.x) "/\" x <= Bottom L by A2;
    then (x "/\" Bottom L) "\/" (x "/\" g9.x) <= Bottom L by A8,Def3;
    then Bottom L "\/" (x "/\" g9.x) <= Bottom L by Th3;
    then
A13: x "/\" g9.x <= Bottom L by Th3;
    Bottom L <= x "/\" g9.x by YELLOW_0:44;
    hence Bottom L = x "/\" g9.x by A13,ORDERS_2:2
      .= x "/\" 'not' x by A10;
  end;
  let x be Element of L;
A14: now
    let x be Element of L;
    Top L <= (Top L "/\" x) "\/" g9.x by A2;
    then
A15: Top L <= x "\/" g9.x by Th4;
    x "\/" g9.x <= Top L by YELLOW_0:45;
    hence Top L = x "\/" g9.x by A15,ORDERS_2:2
      .= x "\/" 'not' x by A10;
  end;
  then ('not' x "\/" 'not' 'not' x) "/\" x = Top L "/\" x;
  then x = x "/\" ('not' x "\/" 'not' 'not' x) by Th4
    .= (x "/\" 'not' x) "\/" (x "/\" 'not' 'not' x) by A8,Def3
    .= Bottom L "\/" (x "/\" 'not' 'not' x) by A12
    .= x "/\" 'not' 'not' x by Th3;
  then
A16: x <= 'not' 'not' x by YELLOW_0:25;
  Bottom L "\/" x = ('not' x "/\" 'not' 'not' x) "\/" x by A12;
  then x = x "\/" ('not' x "/\" 'not' 'not' x) by Th3
    .= (x "\/" 'not' x) "/\" (x "\/" 'not' 'not' x) by A8,Th5
    .= Top L "/\" (x "\/" 'not' 'not' x) by A14
    .= x "\/" 'not' 'not' x by Th4;
  hence thesis by A16,YELLOW_0:24;
end;

:: Exercise 3.19

theorem Th86:
  for L being bounded LATTICE st L is Heyting & 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 Heyting and
A2: for x being Element of L holds 'not' 'not' x = x;
  let x be Element of L;
A3: 'not' (x "\/" 'not' x) = 'not' x "/\" 'not' 'not' x by A1,Th78
    .= x "/\" 'not' x by A2;
A4: 'not' x >= 'not' x by ORDERS_2:1;
  then x "/\" 'not' x = Bottom L by A1,Th82;
  hence x "\/" 'not' x = 'not' (Bottom L) by A2,A3
    .= Top L by A1,Th80;
  thus thesis by A1,A4,Th82;
end;

:: Exercise 3.19  (1) iff (2)

theorem Th87:
  for L being bounded LATTICE holds L is distributive complemented
  iff L is Heyting & 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 x9 being Element of L st for y being
Element of L holds (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 by Lm6;
    hence L is Heyting & for x being Element of L holds 'not' 'not' x = x by
Lm7;
  end;
  assume that
A1: L is Heyting and
A2: for x being Element of L holds 'not' 'not' x = x;
  thus L is distributive by A1;
  let x be Element of L;
  take 'not' x;
  thus thesis by A1,A2,Th86;
end;

:: Definition 3.20

definition
  let B be non empty RelStr;
  attr B is Boolean means

  B is LATTICE & B is bounded distributive complemented;
end;

registration
  cluster Boolean -> reflexive transitive antisymmetric with_infima
    with_suprema bounded distributive complemented for non empty RelStr;
  coherence;
end;

registration
  cluster reflexive transitive antisymmetric with_infima with_suprema bounded
    distributive complemented -> Boolean for non empty RelStr;
  coherence;
end;

registration
  cluster Boolean -> Heyting for non empty RelStr;
  coherence by Th87;
end;

registration
  cluster strict Boolean non empty for LATTICE;
  existence
  proof
    take BoolePoset {};
    thus thesis;
  end;
end;

registration
  cluster strict Heyting non empty for LATTICE;
  existence
  proof
    set L = the strict Boolean non empty LATTICE;
    take L;
    thus thesis;
  end;
end;