:: Properties of Relational Structures, Posets, Lattices and Maps
::  by Mariusz \.Zynel and Czes{\l}aw Byli\'nski
::
:: Received September 20, 1996
:: Copyright (c) 1996-2018 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, ORDERS_2, SUBSET_1, TARSKI, WAYBEL_0, LATTICE3,
      XXREAL_0, RELAT_2, YELLOW_0, EQREL_1, LATTICES, RELAT_1, WELLORD1, CAT_1,
      STRUCT_0, FUNCT_1, GROUP_6, SEQM_3, ORDINAL2, BINOP_1, REWRITE1,
      SETFAM_1, CARD_FIL, YELLOW_1, ZFMISC_1, WELLORD2, YELLOW_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, SETFAM_1, LATTICE3, WELLORD1, DOMAIN_1, ORDERS_1,
      STRUCT_0, ORDERS_2, QUANTAL1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0;
 constructors SETFAM_1, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_0,
      YELLOW_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, WAYBEL_0;
 equalities WAYBEL_0, STRUCT_0;
 expansions TARSKI, LATTICE3, ORDERS_3, WAYBEL_0;
 theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, WELLORD1, ORDERS_2,
      YELLOW_0, YELLOW_1, WAYBEL_0, XBOOLE_0, XBOOLE_1;
 schemes FUNCT_2, DOMAIN_1;

begin :: Basic Facts

reserve x, X, Y for set;

theorem
  for L being non empty RelStr for x being Element of L for X being
  Subset of L holds X c= downarrow x iff X is_<=_than x
by WAYBEL_0:17;

theorem
  for L being non empty RelStr for x being Element of L for X being
  Subset of L holds X c= uparrow x iff x is_<=_than X
by WAYBEL_0:18;

theorem
  for L being antisymmetric transitive with_suprema RelStr for X, Y
being set st ex_sup_of X,L & ex_sup_of Y,L holds ex_sup_of (X \/ Y),L & "\/"(X
  \/ Y, L) = "\/"(X, L) "\/" "\/"(Y, L)
proof
  let L be antisymmetric transitive with_suprema RelStr;
  let X, Y be set such that
A1: ex_sup_of X,L and
A2: ex_sup_of Y,L;
  set a = "\/"(X, L) "\/" "\/"(Y, L);
A3: X \/ Y is_<=_than a
  proof
    let x be Element of L;
    assume
A4: x in X \/ Y;
    per cases by A4,XBOOLE_0:def 3;
    suppose
A5:   x in X;
      X is_<=_than "\/"(X, L) by A1,YELLOW_0:30;
      then
A6:   x <= "\/"(X, L) by A5;
      "\/"(X, L) <= a by YELLOW_0:22;
      hence thesis by A6,ORDERS_2:3;
    end;
    suppose
A7:   x in Y;
      Y is_<=_than "\/"(Y, L) by A2,YELLOW_0:30;
      then
A8:   x <= "\/"(Y, L) by A7;
      "\/"(Y, L) <= a by YELLOW_0:22;
      hence thesis by A8,ORDERS_2:3;
    end;
  end;
  for b being Element of L st X \/ Y is_<=_than b holds a <= b
  proof
    let b be Element of L;
    assume
A9: X \/ Y is_<=_than b;
    Y c= X \/ Y by XBOOLE_1:7;
    then Y is_<=_than b by A9;
    then
A10: "\/"(Y, L) <= b by A2,YELLOW_0:30;
    X c= X \/ Y by XBOOLE_1:7;
    then X is_<=_than b by A9;
    then "\/"(X, L) <= b by A1,YELLOW_0:30;
    hence thesis by A10,YELLOW_0:22;
  end;
  hence thesis by A3,YELLOW_0:30;
end;

theorem
  for L being antisymmetric transitive with_infima RelStr for X, Y being
set st ex_inf_of X,L & ex_inf_of Y,L holds ex_inf_of (X \/ Y),L & "/\"(X \/ Y,
  L) = "/\"(X, L) "/\" "/\"(Y, L)
proof
  let L be antisymmetric transitive with_infima RelStr;
  let X, Y be set such that
A1: ex_inf_of X,L and
A2: ex_inf_of Y,L;
  set a = "/\"(X, L) "/\" "/\"(Y, L);
A3: X \/ Y is_>=_than a
  proof
    let x be Element of L;
    assume
A4: x in X \/ Y;
    per cases by A4,XBOOLE_0:def 3;
    suppose
A5:   x in X;
      X is_>=_than "/\"(X, L) by A1,YELLOW_0:31;
      then
A6:   x >= "/\"(X, L) by A5;
      "/\"(X, L) >= a by YELLOW_0:23;
      hence thesis by A6,ORDERS_2:3;
    end;
    suppose
A7:   x in Y;
      Y is_>=_than "/\"(Y, L) by A2,YELLOW_0:31;
      then
A8:   x >= "/\"(Y, L) by A7;
      "/\"(Y, L) >= a by YELLOW_0:23;
      hence thesis by A8,ORDERS_2:3;
    end;
  end;
  for b being Element of L st X \/ Y is_>=_than b holds a >= b
  proof
    let b be Element of L;
    assume
A9: X \/ Y is_>=_than b;
    Y c= X \/ Y by XBOOLE_1:7;
    then Y is_>=_than b by A9;
    then
A10: "/\"(Y, L) >= b by A2,YELLOW_0:31;
    X c= X \/ Y by XBOOLE_1:7;
    then X is_>=_than b by A9;
    then "/\"(X, L) >= b by A1,YELLOW_0:31;
    hence thesis by A10,YELLOW_0:23;
  end;
  hence thesis by A3,YELLOW_0:31;
end;

begin :: Relational Substructures

theorem Th5:
  for R being Relation for X, Y being set holds X c= Y implies R
  |_2 X c= R |_2 Y
proof
  let R be Relation, X,Y be set;
  assume
A1: X c= Y;
  then X|`R c= Y|`R by RELAT_1:100;
  then
A2: X|`R|X c= Y|`R|X by RELAT_1:76;
  Y|`R|X c= Y|`R|Y by A1,RELAT_1:75;
  then X|`R|X c= Y|`R|Y by A2;
  then R|_2 X c= Y|`R|Y by WELLORD1:10;
  hence thesis by WELLORD1:10;
end;

theorem
  for L being RelStr for S, T being full SubRelStr of L st the carrier
  of S c= the carrier of T holds the InternalRel of S c= the InternalRel of T
proof
  let L be RelStr, S1,S2 be full SubRelStr of L;
  the InternalRel of S1 = (the InternalRel of L)|_2 the carrier of S1 &
the InternalRel of S2 = (the InternalRel of L)|_2 the carrier of S2 by
YELLOW_0:def 14;
  hence thesis by Th5;
end;

theorem Th7:
  for L being non empty RelStr for S being non empty SubRelStr of L
  holds (X is directed Subset of S implies X is directed Subset of L) & (X is
  filtered Subset of S implies X is filtered Subset of L)
proof
  let L be non empty RelStr;
  let S be non empty SubRelStr of L;
  thus X is directed Subset of S implies X is directed Subset of L
  proof
    assume
A1: X is directed Subset of S;
    the carrier of S c= the carrier of L by YELLOW_0:def 13;
    then reconsider X as Subset of L by A1,XBOOLE_1:1;
    for x, y being Element of L st x in X & y in X ex z being Element of L
    st z in X & x <= z & y <= z
    proof
      let x, y be Element of L;
      assume
A2:   x in X & y in X;
      then reconsider x9= x, y9= y as Element of S by A1;
      consider z being Element of S such that
A3:   z in X & x9 <= z & y9 <= z by A1,A2,WAYBEL_0:def 1;
      reconsider z as Element of L by YELLOW_0:58;
      take z;
      thus thesis by A3,YELLOW_0:59;
    end;
    hence thesis by WAYBEL_0:def 1;
  end;
  thus X is filtered Subset of S implies X is filtered Subset of L
  proof
    assume
A4: X is filtered Subset of S;
    the carrier of S c= the carrier of L by YELLOW_0:def 13;
    then reconsider X as Subset of L by A4,XBOOLE_1:1;
    for x, y being Element of L st x in X & y in X ex z being Element of L
    st z in X & z <= x & z <= y
    proof
      let x, y be Element of L;
      assume
A5:   x in X & y in X;
      then reconsider x9= x, y9= y as Element of S by A4;
      consider z being Element of S such that
A6:   z in X & z <= x9 & z <= y9 by A4,A5,WAYBEL_0:def 2;
      reconsider z as Element of L by YELLOW_0:58;
      take z;
      thus thesis by A6,YELLOW_0:59;
    end;
    hence thesis by WAYBEL_0:def 2;
  end;
end;

theorem
  for L being non empty RelStr for S, T being non empty full SubRelStr
of L st the carrier of S c= the carrier of T for X being Subset of S holds X is
  Subset of T & for Y being Subset of T st X = Y holds (X is filtered implies Y
  is filtered) & (X is directed implies Y is directed)
proof
  let L be non empty RelStr, S1,S2 be non empty full SubRelStr of L;
  assume
A1: the carrier of S1 c= the carrier of S2;
  let X be Subset of S1;
  thus X is Subset of S2 by A1,XBOOLE_1:1;
  let X2 be Subset of S2 such that
A2: X = X2;
  hereby
    assume
A3: X is filtered;
    thus X2 is filtered
    proof
      let x, y be Element of S2;
      assume
A4:   x in X2 & y in X2;
      then reconsider x9= x, y9= y as Element of S1 by A2;
      consider z being Element of S1 such that
A5:   z in X and
A6:   z <= x9 & z <= y9 by A2,A3,A4;
      reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58;
      reconsider z as Element of S2 by A2,A5;
      take z;
      z1 <= x1 & z1 <= y1 by A6,YELLOW_0:59;
      hence thesis by A2,A5,YELLOW_0:60;
    end;
  end;
  assume
A7: X is directed;
  let x, y be Element of S2;
  assume
A8: x in X2 & y in X2;
  then reconsider x9= x, y9= y as Element of S1 by A2;
  consider z being Element of S1 such that
A9: z in X and
A10: x9 <= z & y9 <= z by A2,A7,A8;
  reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58;
  reconsider z as Element of S2 by A2,A9;
  take z;
  x1 <= z1 & y1 <= z1 by A10,YELLOW_0:59;
  hence thesis by A2,A9,YELLOW_0:60;
end;

begin :: Maps

definition
  let J be set, L be RelStr;
  let f, g be Function of J, the carrier of L;
  pred f <= g means

  for j being set st j in J ex a, b being Element of
  L st a = f.j & b = g.j & a <= b;
end;

notation
  let J be set, L be RelStr;
  let f, g be Function of J, the carrier of L;
  synonym g >= f for f <= g;
end;

theorem
  for L, M being non empty RelStr, f,g being Function of L, M holds f <=
  g iff for x being Element of L holds f.x <= g.x
proof
  let L, M be non empty RelStr, f,g be Function of L, M;
  hereby
    assume
A1: f <= g;
    let x be Element of L;
    ex m1,m2 being Element of M st m1 = f.x & m2 = g.x & m1 <= m2 by A1;
    hence f.x <= g.x;
  end;
  assume
A2: for x being Element of L holds f.x <= g.x;
  let x be set;
  assume x in the carrier of L;
  then reconsider x as Element of L;
  take f.x, g.x;
  thus thesis by A2;
end;

begin :: The Image of a Map

definition
  let L, M be non empty RelStr;
  let f be Function of L, M;
  func Image f -> strict full SubRelStr of M equals
  subrelstr rng f;
  correctness;
end;

theorem
  for L, M being non empty RelStr for f being Function of L, M for y
  being Element of Image f ex x being Element of L st f.x = y
proof
  let L1, L2 be non empty RelStr, g be Function of L1,L2;
  let s be Element of Image g;
  dom g = the carrier of L1 by FUNCT_2:def 1;
  then
A1: rng g is non empty by RELAT_1:42;
  rng g = the carrier of Image g by YELLOW_0:def 15;
  then consider l being object such that
A2: l in dom g and
A3: s = g.l by A1,FUNCT_1:def 3;
  reconsider l as Element of L1 by A2;
  take l;
  thus thesis by A3;
end;

registration
  let L be non empty RelStr;
  let X be non empty Subset of L;
  cluster subrelstr X -> non empty;
  coherence by YELLOW_0:def 15;
end;

registration
  let L, M be non empty RelStr;
  let f be Function of L, M;
  cluster Image f -> non empty;
  coherence
  proof
    dom f = the carrier of L by FUNCT_2:def 1;
    then rng f is non empty by RELAT_1:42;
    hence thesis;
  end;
end;

begin :: Monotone Maps

theorem
  for L being non empty RelStr holds id L is monotone
proof
  let L be non empty RelStr;
  let l1,l2 be Element of L;
  assume l1 <= l2;
  then l1 <= (id L).l2 by FUNCT_1:18;
  hence thesis by FUNCT_1:18;
end;

theorem
  for L, M, N being non empty RelStr for f being Function of L, M, g
  being Function of M, N holds f is monotone & g is monotone implies g*f is
  monotone
proof
  let L1,L2,L3 be non empty RelStr;
  let g1 be Function of L1,L2, g2 be Function of L2,L3 such that
A1: g1 is monotone and
A2: g2 is monotone;
  let s1,s2 be Element of L1;
  assume s1 <= s2;
  then g1.s1 <= g1.s2 by A1;
  then g2.(g1.s1) <= g2.(g1.s2) by A2;
  then (g2*g1).s1 <= g2.(g1.s2) by FUNCT_2:15;
  hence thesis by FUNCT_2:15;
end;

theorem
  for L, M being non empty RelStr for f being Function of L, M for X
  being Subset of L, x being Element of L holds f is monotone & x is_<=_than X
  implies f.x is_<=_than f.:X
proof
  let L1,L2 be non empty RelStr, g be Function of L1,L2;
  let X be Subset of L1, x be Element of L1 such that
A1: g is monotone and
A2: x is_<=_than X;
  let y2 be Element of L2;
  assume y2 in g.:X;
  then consider x2 being Element of L1 such that
A3: x2 in X and
A4: y2 = g.x2 by FUNCT_2:65;
  reconsider x2 as Element of L1;
  x <= x2 by A2,A3;
  hence thesis by A1,A4;
end;

theorem
  for L, M being non empty RelStr for f being Function of L, M for X
  being Subset of L, x being Element of L holds f is monotone & X is_<=_than x
  implies f.:X is_<=_than f.x
proof
  let L1,L2 be non empty RelStr, g be Function of L1,L2;
  let X be Subset of L1, x be Element of L1 such that
A1: g is monotone and
A2: x is_>=_than X;
  let y2 be Element of L2;
  assume y2 in g.:X;
  then consider x2 being Element of L1 such that
A3: x2 in X and
A4: y2 = g.x2 by FUNCT_2:65;
  reconsider x2 as Element of L1;
  x >= x2 by A2,A3;
  hence thesis by A1,A4;
end;

theorem
  for S, T being non empty RelStr for f being Function of S, T for X
  being directed Subset of S holds f is monotone implies f.:X is directed
proof
  let S, T be non empty RelStr;
  let f be Function of S, T;
  let X be directed Subset of S;
  set Y = f.:X;
  assume
A1: f is monotone;
  for y1, y2 being Element of T st y1 in Y & y2 in Y ex z being Element of
  T st z in Y & y1 <= z & y2 <= z
  proof
    let y1, y2 be Element of T;
    assume that
A2: y1 in Y and
A3: y2 in Y;
    consider x1 being object such that
    x1 in dom f and
A4: x1 in X and
A5: y1 = f.x1 by A2,FUNCT_1:def 6;
    consider x2 being object such that
    x2 in dom f and
A6: x2 in X and
A7: y2 = f.x2 by A3,FUNCT_1:def 6;
    reconsider x1, x2 as Element of S by A4,A6;
    consider z being Element of S such that
A8: z in X and
A9: x1 <= z & x2 <= z by A4,A6,WAYBEL_0:def 1;
    take f.z;
    thus f.z in Y by A8,FUNCT_2:35;
    thus thesis by A1,A5,A7,A9;
  end;
  hence thesis;
end;

theorem Th16:
  for L being with_suprema Poset for f being Function of L, L
  holds f is directed-sups-preserving implies f is monotone
proof
  let L be with_suprema Poset;
  let f be Function of L, L;
  assume
A1: f is directed-sups-preserving;
  let x, y be Element of L such that
A2: x <= y;
A3: y = y"\/"x by A2,YELLOW_0:24;
  for a, b being Element of L st a in {x, y} & b in {x, y} ex z being
  Element of L st z in {x, y} & a <= z & b <= z
  proof
    let a, b be Element of L such that
A4: a in {x, y} & b in {x, y};
    take y;
    thus y in {x, y} by TARSKI:def 2;
    thus thesis by A2,A4,TARSKI:def 2;
  end;
  then {x, y} is directed non empty;
  then
A5: f preserves_sup_of {x, y} by A1;
A6: dom f = the carrier of L by FUNCT_2:def 1;
  y <= y;
  then
A7: {x, y} is_<=_than y by A2,YELLOW_0:8;
  for b being Element of L st {x, y} is_<=_than b holds y <= b by YELLOW_0:8;
  then ex_sup_of {x, y},L by A7,YELLOW_0:30;
  then sup(f.:{x, y}) = f.sup{x, y} by A5
    .= f.y by A3,YELLOW_0:41;
  then
A8: f.y = sup{f.x, f.y} by A6,FUNCT_1:60
    .= f.y"\/"f.x by YELLOW_0:41;
  let afx, bfy be Element of L;
  assume afx = f.x & bfy = f.y;
  hence afx <= bfy by A8,YELLOW_0:22;
end;

theorem
  for L being with_infima Poset for f being Function of L, L holds f is
  filtered-infs-preserving implies f is monotone
proof
  let L be with_infima Poset;
  let f be Function of L, L;
  assume
A1: f is filtered-infs-preserving;
  let x, y be Element of L such that
A2: x <= y;
A3: x = x"/\"y by A2,YELLOW_0:25;
  for c, d being Element of L st c in {x, y} & d in {x, y} ex z being
  Element of L st z in {x, y} & z <= c & z <= d
  proof
    let c, d be Element of L such that
A4: c in {x, y} & d in {x, y};
    take x;
    thus x in {x, y} by TARSKI:def 2;
    thus thesis by A2,A4,TARSKI:def 2;
  end;
  then {x, y} is filtered non empty;
  then
A5: f preserves_inf_of {x, y} by A1;
A6: dom f = the carrier of L by FUNCT_2:def 1;
  x <= x;
  then
A7: x is_<=_than {x, y} by A2,YELLOW_0:8;
  for c being Element of L st c is_<=_than {x, y} holds c <= x by YELLOW_0:8;
  then ex_inf_of {x, y},L by A7,YELLOW_0:31;
  then inf(f.:{x, y}) = f.inf{x, y} by A5
    .= f.x by A3,YELLOW_0:40;
  then
A8: f.x = inf{f.x, f.y} by A6,FUNCT_1:60
    .= f.x"/\"f.y by YELLOW_0:40;
  let a, b be Element of L;
  assume a = f.x & b = f.y;
  hence a <= b by A8,YELLOW_0:23;
end;

begin :: Idempotent Maps

theorem
  for S being non empty 1-sorted for f being Function of S, S holds f is
  idempotent implies for x being Element of S holds f.(f.x) = f.x
proof
  let L be non empty 1-sorted, p be Function of L,L;
  assume
A1: p*p = p;
  let l be Element of L;
  thus thesis by A1,FUNCT_2:15;
end;

theorem Th19:
  for S being non empty 1-sorted for f being Function of S, S
  holds f is idempotent implies rng f = {x where x is Element of S: x = f.x}
proof
  let S be non empty 1-sorted;
  let f be Function of S, S;
  set M = {x where x is Element of S: x = f.x};
  assume
A1: f = f*f;
A2: rng f c= M
  proof
    let y be object;
    assume
A3: y in rng f;
    then reconsider y9= y as Element of S;
    ex x being object st x in dom f & y = f.x by A3,FUNCT_1:def 3;
    then y9= f.y9 by A1,FUNCT_1:13;
    hence thesis;
  end;
  M c= rng f
  proof
    let y be object;
    assume y in M;
    then
A4: ex y9 being Element of S st y9 = y & y9 = f.y9;
    dom f = the carrier of S by FUNCT_2:def 1;
    hence thesis by A4,FUNCT_1:def 3;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th20:
  for S being non empty 1-sorted for f being Function of S, S st f
  is idempotent holds X c= rng f implies f.:X = X
proof
  let S be non empty 1-sorted;
  let f be Function of S, S such that
A1: f is idempotent;
  set M = {x where x is Element of S: x = f.x};
  assume X c= rng f;
  then
A2: X c= M by A1,Th19;
A3: f.:X c= X
  proof
    let y be object;
    assume y in f.:X;
    then consider x being object such that
    x in dom f and
A4: x in X and
A5: y = f.x by FUNCT_1:def 6;
    x in M by A2,A4;
    then ex x9 being Element of S st x9 = x & x9 = f.x9;
    hence thesis by A4,A5;
  end;
  X c= f.:X
  proof
    let y be object;
    assume
A6: y in X;
    then y in M by A2;
    then ex x being Element of S st x = y & x = f.x;
    hence thesis by A6,FUNCT_2:35;
  end;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem
  for L being non empty RelStr holds id L is idempotent
proof
  let L be non empty RelStr;
  thus (id L)*(id L) = id ((the carrier of L) /\ (the carrier of L)) by
FUNCT_1:22
    .= (id L);
end;

begin :: Complete Lattices (CCL Chapter 0, Section 2, pp. 8 -- 9)

reserve L for complete LATTICE,
  a for Element of L;

theorem Th22:
  a in X implies a <= "\/"(X, L) & "/\"(X, L) <= a
proof
  assume
A1: a in X;
  X is_<=_than "\/"(X, L) by YELLOW_0:32;
  hence a <= "\/"(X, L) by A1;
  X is_>=_than "/\"(X, L) by YELLOW_0:33;
  hence thesis by A1;
end;

theorem Th23:
  for L being non empty RelStr holds (for X holds ex_sup_of X,L)
  iff (for Y holds ex_inf_of Y,L)
proof
  let L be non empty RelStr;
  hereby
    assume
A1: for X holds ex_sup_of X,L;
    let Y;
    set X = {x where x is Element of L: x is_<=_than Y};
    ex_sup_of X,L by A1;
    then consider a being Element of L such that
A2: X is_<=_than a and
A3: for b being Element of L st X is_<=_than b holds b >= a and
A4: for c being Element of L st X is_<=_than c & for b being Element
    of L st X is_<=_than b holds b >= c holds c = a by YELLOW_0:def 7;
A5: a is_<=_than Y
    proof
      let b be Element of L;
      assume
A6:   b in Y;
      b is_>=_than X
      proof
        let c be Element of L;
        assume c in X;
        then ex x being Element of L st c = x & x is_<=_than Y;
        hence thesis by A6;
      end;
      hence thesis by A3;
    end;
A7: for c being Element of L st Y is_>=_than c & for b being Element of L
    st Y is_>=_than b holds b <= c holds c = a
    proof
      let c be Element of L such that
A8:   Y is_>=_than c and
A9:   for b being Element of L st Y is_>=_than b holds b <= c;
A10:  for b being Element of L st X is_<=_than b holds b >= c
      proof
        let b be Element of L;
        assume
A11:    X is_<=_than b;
        c in X by A8;
        hence thesis by A11;
      end;
      X is_<=_than c
      proof
        let b be Element of L;
        assume b in X;
        then ex x being Element of L st b = x & x is_<=_than Y;
        hence thesis by A9;
      end;
      hence thesis by A4,A10;
    end;
    for b being Element of L st Y is_>=_than b holds a >= b
    proof
      let b be Element of L;
      assume b is_<=_than Y;
      then b in X;
      hence thesis by A2;
    end;
    hence ex_inf_of Y,L by A5,A7,YELLOW_0:def 8;
  end;
  assume
A12: for Y holds ex_inf_of Y,L;
  let X;
  set Y = {y where y is Element of L: X is_<=_than y};
  ex_inf_of Y,L by A12;
  then consider a being Element of L such that
A13: Y is_>=_than a and
A14: for b being Element of L st Y is_>=_than b holds b <= a and
A15: for c being Element of L st Y is_>=_than c & for b being Element of
  L st Y is_>=_than b holds b <= c holds c = a by YELLOW_0:def 8;
A16: X is_<=_than a
  proof
    let b be Element of L;
    assume
A17: b in X;
    b is_<=_than Y
    proof
      let c be Element of L;
      assume c in Y;
      then ex y being Element of L st c = y & X is_<=_than y;
      hence thesis by A17;
    end;
    hence thesis by A14;
  end;
A18: for c being Element of L st X is_<=_than c & for b being Element of L
  st X is_<=_than b holds b >= c holds c = a
  proof
    let c be Element of L such that
A19: X is_<=_than c and
A20: for b being Element of L st X is_<=_than b holds b >= c;
A21: for b being Element of L st Y is_>=_than b holds b <= c
    proof
      let b be Element of L;
      assume
A22:  Y is_>=_than b;
      c in Y by A19;
      hence thesis by A22;
    end;
    Y is_>=_than c
    proof
      let b be Element of L;
      assume b in Y;
      then ex x being Element of L st b = x & x is_>=_than X;
      hence thesis by A20;
    end;
    hence thesis by A15,A21;
  end;
  for b being Element of L st X is_<=_than b holds a <= b
  proof
    let b be Element of L;
    assume X is_<=_than b;
    then b in Y;
    hence thesis by A13;
  end;
  hence thesis by A16,A18,YELLOW_0:def 7;
end;

theorem Th24: ::Proposition 2.2 (i)  (variant 1)   cf YELLOW_0
  for L being non empty RelStr holds (for X holds ex_sup_of X,L)
  implies L is complete
proof
  let L be non empty RelStr;
  assume
A1: for X holds ex_sup_of X,L;
  L is complete
  proof
    let X be set;
    take a = "\/"(X, L);
A2: ex_sup_of X,L by A1;
    hence X is_<=_than a by YELLOW_0:def 9;
    thus thesis by A2,YELLOW_0:def 9;
  end;
  hence thesis;
end;

theorem Th25: ::Proposition 2.2 (i)  (variant 2)   cf variant 3
  for L being non empty RelStr holds (for X holds ex_inf_of X,L)
  implies L is complete
proof
  let L be non empty RelStr;
  assume for X holds ex_inf_of X,L;
  then for X holds ex_sup_of X,L by Th23;
  hence thesis by Th24;
end;

theorem Th26:
  for L being non empty RelStr holds (for A being Subset of L
  holds ex_inf_of A, L) implies for X holds ex_inf_of X,L & "/\"(X, L) = "/\"(X
  /\ the carrier of L, L)
proof
  let L be non empty RelStr;
  assume
A1: for A being Subset of L holds ex_inf_of A, L;
  let X;
  set Y = X /\ the carrier of L;
  set a = "/\"(Y, L);
  reconsider Y as Subset of L by XBOOLE_1:17;
A2: ex_inf_of Y,L by A1;
A3: a is_<=_than X
  proof
    let x be Element of L;
    assume x in X;
    then
A4: x in Y by XBOOLE_0:def 4;
    a is_<=_than Y by A2,YELLOW_0:def 10;
    hence thesis by A4;
  end;
A5: for b being Element of L st b is_<=_than X holds b <= a
  proof
    let b be Element of L;
A6: Y c= X by XBOOLE_1:17;
    assume b is_<=_than X;
    then b is_<=_than Y by A6;
    hence thesis by A2,YELLOW_0:def 10;
  end;
  ex_inf_of X,L by A2,YELLOW_0:50;
  hence thesis by A3,A5,YELLOW_0:def 10;
end;

theorem
  for L being non empty RelStr holds (for A being Subset of L holds
ex_sup_of A, L) implies for X holds ex_sup_of X,L & "\/"(X, L) = "\/"(X /\ the
  carrier of L, L)
proof
  let L be non empty RelStr;
  assume
A1: for A being Subset of L holds ex_sup_of A, L;
  let X;
  set Y = X /\ the carrier of L;
  set a = "\/"(Y, L);
  reconsider Y as Subset of L by XBOOLE_1:17;
A2: ex_sup_of Y,L by A1;
A3: X is_<=_than a
  proof
    let x be Element of L;
    assume x in X;
    then
A4: x in Y by XBOOLE_0:def 4;
    Y is_<=_than a by A2,YELLOW_0:def 9;
    hence thesis by A4;
  end;
A5: for b being Element of L st X is_<=_than b holds a <= b
  proof
    let b be Element of L;
A6: Y c= X by XBOOLE_1:17;
    assume X is_<=_than b;
    then Y is_<=_than b by A6;
    hence thesis by A2,YELLOW_0:def 9;
  end;
  ex_sup_of X,L by A2,YELLOW_0:50;
  hence thesis by A3,A5,YELLOW_0:def 9;
end;

theorem Th28: ::Proposition 2.2 (i)  (variant 3)
  for L being non empty RelStr holds (for A being Subset of L
  holds ex_inf_of A,L) implies L is complete
proof
  let L be non empty RelStr;
  assume for A being Subset of L holds ex_inf_of A,L;
  then for X holds ex_inf_of X, L by Th26;
  hence thesis by Th25;
end;

registration
  cluster up-complete /\-complete upper-bounded -> complete for
non empty Poset;
  correctness;
end;

theorem Th29: :: Theorem 2.3 (The Fixed-Point Theorem)
  for f being Function of L, L st f is monotone for M being Subset
of L st M = {x where x is Element of L: x = f.x} holds subrelstr M is complete
  LATTICE
proof
  let f be Function of L, L such that
A1: f is monotone;
  let M be Subset of L such that
A2: M = {x where x is Element of L: x = f.x};
  set S = subrelstr M;
A3: for X being Subset of S for Y being Subset of L st Y = {y where y is
  Element of L: X is_<=_than f.y & f.y <= y} holds inf Y in M
  proof
    let X be Subset of S;
    let Y be Subset of L such that
A4: Y = {y where y is Element of L: X is_<=_than f.y & f.y <= y};
    set z = inf Y;
A5: f.z is_<=_than Y
    proof
      let u be Element of L;
      assume
A6:   u in Y;
      then consider y being Element of L such that
A7:   y = u and
      X is_<=_than f.y and
A8:   f.y <= y by A4;
      z <= u by A6,Th22;
      then f.z <= f.y by A1,A7;
      hence f.z <= u by A7,A8,ORDERS_2:3;
    end;
A9: X is_<=_than f.(f.z)
    proof
      let m be Element of L;
      assume
A10:  m in X;
      m is_<=_than Y
      proof
        let u be Element of L;
        assume u in Y;
        then consider y being Element of L such that
A11:    y = u and
A12:    X is_<=_than f.y and
A13:    f.y <= y by A4;
        m <= f.y by A10,A12;
        hence m <= u by A11,A13,ORDERS_2:3;
      end;
      then m <= z by YELLOW_0:33;
      then
A14:  f.m <= f.z by A1;
      X c= the carrier of S;
      then X c= M by YELLOW_0:def 15;
      then m in M by A10;
      then ex x being Element of L st x = m & x = f.x by A2;
      hence m <= f.(f.z) by A1,A14;
    end;
    ex_inf_of Y,L by YELLOW_0:17;
    then
A15: f.z <= z by A5,YELLOW_0:31;
    then f.(f.z) <= f.z by A1;
    then f.z in Y by A4,A9;
    then z <= f.z by Th22;
    then z = f.z by A15,ORDERS_2:2;
    hence thesis by A2;
  end;
  M c= the carrier of S by YELLOW_0:def 15;
  then reconsider M as Subset of S;
  defpred P[Element of L] means M is_<=_than f.$1 & f.$1 <= $1;
  reconsider Y = {y where y is Element of L: P[y]} as Subset of L from
  DOMAIN_1:sch 7;
  inf Y in M by A3;
  then reconsider S as non empty Poset;
  for X being Subset of S holds ex_sup_of X, S
  proof
    let X be Subset of S;
    defpred Q[Element of L] means X is_<=_than f.$1 & f.$1 <= $1;
    reconsider Y = {y where y is Element of L: Q[y]} as Subset of L from
    DOMAIN_1:sch 7;
    set z = inf Y;
    z in M by A3;
    then reconsider z as Element of S;
A16: X is_<=_than z
    proof
      let x be Element of S;
      x in the carrier of S;
      then x in M by YELLOW_0:def 15;
      then consider m being Element of L such that
A17:  x = m and
      m = f.m by A2;
      assume
A18:  x in X;
      m is_<=_than Y
      proof
        let u be Element of L;
        assume u in Y;
        then consider y being Element of L such that
A19:    y = u and
A20:    X is_<=_than f.y and
A21:    f.y <= y;
        m <= f.y by A18,A17,A20;
        hence m <= u by A19,A21,ORDERS_2:3;
      end;
      then m <= inf Y by YELLOW_0:33;
      hence x <= z by A17,YELLOW_0:60;
    end;
    for b being Element of S st X is_<=_than b holds z <= b
    proof
      let b be Element of S;
      b in the carrier of S;
      then b in M by YELLOW_0:def 15;
      then consider x being Element of L such that
A22:  x = b and
A23:  x = f.x by A2;
      assume X is_<=_than b;
      then X is_<=_than f.x by A22,A23,YELLOW_0:62;
      then x in Y by A23;
      hence thesis by A22,Th22,YELLOW_0:60;
    end;
    hence thesis by A16,YELLOW_0:30;
  end;
  then reconsider S as complete non empty Poset by YELLOW_0:53;
  S is complete LATTICE;
  hence thesis;
end;

theorem Th30:
  for S being infs-inheriting non empty full SubRelStr of L holds
  S is complete LATTICE
proof
  let S be infs-inheriting non empty full SubRelStr of L;
  for X being Subset of S holds ex_inf_of X,S
  proof
    let X be Subset of S;
A1: ex_inf_of X,L by YELLOW_0:17;
    then "/\"(X,L) in the carrier of S by YELLOW_0:def 18;
    hence thesis by A1,YELLOW_0:63;
  end;
  then S is complete by Th28;
  hence thesis;
end;

theorem Th31:
  for S being sups-inheriting non empty full SubRelStr of L holds
  S is complete LATTICE
proof
  let S be sups-inheriting non empty full SubRelStr of L;
  for X being Subset of S holds ex_sup_of X, S
  proof
    let X be Subset of S;
A1: ex_sup_of X,L by YELLOW_0:17;
    then "\/"(X,L) in the carrier of S by YELLOW_0:def 19;
    hence thesis by A1,YELLOW_0:64;
  end;
  then S is complete by YELLOW_0:53;
  hence thesis;
end;

theorem Th32: ::Remark 2.4 (Part I, variant 1)
  for M being non empty RelStr for f being Function of L, M st f
  is sups-preserving holds Image f is sups-inheriting
proof
  let M be non empty RelStr;
  let f be Function of L, M such that
A1: f is sups-preserving;
  set S = subrelstr(rng f);
  for Y being Subset of S st ex_sup_of Y,M holds "\/"(Y, M) in the carrier of S
  proof
    let Y be Subset of S;
    assume ex_sup_of Y,M;
A2: f preserves_sup_of (f"Y) & ex_sup_of f"Y,L by A1,YELLOW_0:17;
    Y c= the carrier of S;
    then Y c= rng f by YELLOW_0:def 15;
    then "\/"(Y, M) = sup(f.:(f"Y)) by FUNCT_1:77
      .= f.sup(f"Y) by A2;
    then "\/"(Y, M) in rng f by FUNCT_2:4;
    hence thesis by YELLOW_0:def 15;
  end;
  hence thesis by YELLOW_0:def 19;
end;

theorem Th33: ::Remark 2.4  (Part I, variant 2)
  for M being non empty RelStr for f being Function of L, M st f
  is infs-preserving holds Image f is infs-inheriting
proof
  let M be non empty RelStr;
  let f be Function of L, M such that
A1: f is infs-preserving;
  set S = subrelstr(rng f);
  for Y being Subset of S st ex_inf_of Y,M holds "/\"(Y, M) in the carrier of S
  proof
    let Y be Subset of S;
    assume ex_inf_of Y,M;
A2: f preserves_inf_of (f"Y) & ex_inf_of f"Y,L by A1,YELLOW_0:17;
    Y c= the carrier of S;
    then Y c= rng f by YELLOW_0:def 15;
    then "/\"(Y, M) = inf(f.:(f"Y)) by FUNCT_1:77
      .= f.inf(f"Y) by A2;
    then "/\"(Y, M) in rng f by FUNCT_2:4;
    hence thesis by YELLOW_0:def 15;
  end;
  hence thesis by YELLOW_0:def 18;
end;

theorem ::Remark 2.4  (Part II)
  for L, M being complete LATTICE for f being Function of L, M st f is
  sups-preserving or f is infs-preserving holds Image f is complete LATTICE
proof
  let L, M be complete LATTICE;
  let f be Function of L, M such that
A1: f is sups-preserving or f is infs-preserving;
  per cases by A1;
  suppose
    f is sups-preserving;
    then Image f is sups-inheriting by Th32;
    hence thesis by Th31;
  end;
  suppose
    f is infs-preserving;
    then Image f is infs-inheriting by Th33;
    hence thesis by Th30;
  end;
end;

theorem ::Remark 2.5
  for f being Function of L, L st f is idempotent
directed-sups-preserving holds Image f is directed-sups-inheriting & Image f is
  complete LATTICE
proof
  let f be Function of L, L;
  set S = subrelstr(rng f);
  set a = the Element of L;
  dom f = the carrier of L by FUNCT_2:def 1;
  then f.a in rng f by FUNCT_1:def 3;
  then reconsider S9= S as non empty full SubRelStr of L;
  assume
A1: f is idempotent directed-sups-preserving;
  for X being directed Subset of S st X <> {} & ex_sup_of X,L holds "\/"(X
  ,L) in the carrier of S
  proof
    let X be directed Subset of S;
    X c= the carrier of S;
    then
A2: X c= rng f by YELLOW_0:def 15;
    assume X <> {};
    then X is non empty directed Subset of S9;
    then reconsider X9= X as non empty directed Subset of L by Th7;
    assume
A3: ex_sup_of X,L;
    f preserves_sup_of X9 by A1;
    then sup(f.:X9) = f.sup X9 by A3;
    then sup X9 = f.sup X9 by A1,A2,Th20;
    then "\/"(X, L) in rng f by FUNCT_2:4;
    hence thesis by YELLOW_0:def 15;
  end;
  hence Image f is directed-sups-inheriting;
  rng f = {x where x is Element of L: x = f.x} by A1,Th19;
  hence thesis by A1,Th16,Th29;
end;

begin :: A Lattice of Ideals

theorem Th36:
  for L being RelStr for F being Subset-Family of L st for X being
  Subset of L st X in F holds X is lower holds meet F is lower Subset of L
proof
  let L be RelStr;
  let F be Subset-Family of L;
  reconsider F9 = F as Subset-Family of L;
  assume
A1: for X being Subset of L st X in F holds X is lower;
  reconsider M = meet F9 as Subset of L;
  per cases;
  suppose
    F = {};
    then for x, y being Element of L st x in M & y <= x holds y in M by
SETFAM_1:def 1;
    hence thesis by WAYBEL_0:def 19;
  end;
  suppose
A2: F <> {};
    for x, y being Element of L st x in M & y <= x holds y in M
    proof
      let x, y be Element of L;
      assume that
A3:   x in M and
A4:   y <= x;
      for Y being set st Y in F holds y in Y
      proof
        let Y be set;
        assume
A5:     Y in F;
        then reconsider X = Y as Subset of L;
        X is lower & x in X by A1,A3,A5,SETFAM_1:def 1;
        hence thesis by A4;
      end;
      hence thesis by A2,SETFAM_1:def 1;
    end;
    hence thesis by WAYBEL_0:def 19;
  end;
end;

theorem
  for L being RelStr for F being Subset-Family of L st for X being
  Subset of L st X in F holds X is upper holds meet F is upper Subset of L
proof
  let L be RelStr;
  let F be Subset-Family of L;
  reconsider F9 = F as Subset-Family of L;
  assume
A1: for X being Subset of L st X in F holds X is upper;
  reconsider M = meet F9 as Subset of L;
  per cases;
  suppose
    F = {};
    then for x, y being Element of L st x in M & x <= y holds y in M by
SETFAM_1:def 1;
    hence thesis by WAYBEL_0:def 20;
  end;
  suppose
A2: F <> {};
    for x, y being Element of L st x in M & x <= y holds y in M
    proof
      let x, y be Element of L;
      assume that
A3:   x in M and
A4:   x <= y;
      for Y being set st Y in F holds y in Y
      proof
        let Y be set;
        assume
A5:     Y in F;
        then reconsider X = Y as Subset of L;
        X is upper & x in X by A1,A3,A5,SETFAM_1:def 1;
        hence thesis by A4;
      end;
      hence thesis by A2,SETFAM_1:def 1;
    end;
    hence thesis by WAYBEL_0:def 20;
  end;
end;

theorem Th38:
  for L being with_suprema antisymmetric RelStr for F being
  Subset-Family of L st for X being Subset of L st X in F holds X is lower
  directed holds meet F is directed Subset of L
proof
  let L be with_suprema antisymmetric RelStr;
  let F be Subset-Family of L;
  assume
A1: for X being Subset of L st X in F holds X is lower directed;
  reconsider F9 = F as Subset-Family of L;
  reconsider M = meet F9 as Subset of L;
  per cases;
  suppose
A2: F = {};
    M is directed
    by A2,SETFAM_1:def 1;
    hence thesis;
  end;
  suppose
A3: F <> {};
    M is directed
    proof
      let x, y be Element of L such that
A4:   x in M and
A5:   y in M;
      take z = x"\/"y;
      for Y being set st Y in F holds z in Y
      proof
        let Y be set;
        assume
A6:     Y in F;
        then reconsider X = Y as Subset of L;
A7:     y in X by A5,A6,SETFAM_1:def 1;
        X is lower directed & x in X by A1,A4,A6,SETFAM_1:def 1;
        hence thesis by A7,WAYBEL_0:40;
      end;
      hence z in M by A3,SETFAM_1:def 1;
      thus thesis by YELLOW_0:22;
    end;
    hence thesis;
  end;
end;

theorem
  for L being with_infima antisymmetric RelStr for F being Subset-Family
of L st for X being Subset of L st X in F holds X is upper filtered holds meet
  F is filtered Subset of L
proof
  let L be with_infima antisymmetric RelStr;
  let F be Subset-Family of L;
  assume
A1: for X being Subset of L st X in F holds X is upper filtered;
  reconsider F9 = F as Subset-Family of L;
  reconsider M = meet F9 as Subset of L;
  per cases;
  suppose
A2: F = {};
    M is filtered
    by A2,SETFAM_1:def 1;
    hence thesis;
  end;
  suppose
A3: F <> {};
    M is filtered
    proof
      let x, y be Element of L such that
A4:   x in M and
A5:   y in M;
      take z = x"/\"y;
      for Y being set st Y in F holds z in Y
      proof
        let Y be set;
        assume
A6:     Y in F;
        then reconsider X = Y as Subset of L;
A7:     y in X by A5,A6,SETFAM_1:def 1;
        X is upper filtered & x in X by A1,A4,A6,SETFAM_1:def 1;
        hence thesis by A7,WAYBEL_0:41;
      end;
      hence z in M by A3,SETFAM_1:def 1;
      thus thesis by YELLOW_0:23;
    end;
    hence thesis;
  end;
end;

theorem Th40:
  for L being with_infima Poset for I, J being Ideal of L holds I
  /\ J is Ideal of L
proof
  let L be with_infima Poset;
  let I, J be Ideal of L;
  set i = the Element of I,j = the Element of J;
  set a = i"/\"j;
  a <= j by YELLOW_0:23;
  then
A1: a in J by WAYBEL_0:def 19;
  a <= i by YELLOW_0:23;
  then a in I by WAYBEL_0:def 19;
  hence thesis by A1,WAYBEL_0:27,44,XBOOLE_0:def 4;
end;

registration
  let L be non empty reflexive transitive RelStr;
  cluster Ids L -> non empty;
  correctness
  proof
    set x = the Element of L;
    downarrow x in the set of all Y where Y is Ideal of L;
    hence thesis;
  end;
end;

theorem Th41:
  for L being non empty reflexive transitive RelStr holds (x is
  Element of InclPoset(Ids L) iff x is Ideal of L)
proof
  let L be non empty reflexive transitive RelStr;
  hereby
    assume x is Element of InclPoset(Ids L);
    then x in the carrier of InclPoset(Ids L);
    then x in Ids L by YELLOW_1:1;
    then ex J being Ideal of L st J = x;
    hence x is Ideal of L;
  end;
  assume x is Ideal of L;
  then x in the set of all Y where Y is Ideal of L;
  hence thesis by YELLOW_1:1;
end;

theorem Th42:
  for L being non empty reflexive transitive RelStr for I being
  Element of InclPoset(Ids L) holds x in I implies x is Element of L
proof
  let L be non empty reflexive transitive RelStr;
  let I be Element of InclPoset(Ids L);
  reconsider I9= I as non empty Subset of L by Th41;
  assume x in I;
  then reconsider x9= x as Element of I9;
  x9 in the carrier of L;
  hence thesis;
end;

theorem
  for L being with_infima Poset for x, y being Element of InclPoset(Ids
  L) holds x "/\" y = x /\ y
proof
  let L be with_infima Poset;
  let x, y be Element of InclPoset(Ids L);
  reconsider x9= x, y9= y as Ideal of L by Th41;
  x9 /\ y9 is Ideal of L by Th40;
  then x9 /\ y9 in the set of all X where X is Ideal of L;
  hence thesis by YELLOW_1:9;
end;

registration
  let L be with_infima Poset;
  cluster InclPoset(Ids L) -> with_infima;
  correctness
  proof
    for x, y be set st x in Ids L & y in Ids L holds x /\ y in Ids L
    proof
      let x, y be set;
      assume that
A1:   x in Ids L and
A2:   y in Ids L;
      consider I being Ideal of L such that
A3:   I = x by A1;
      consider J being Ideal of L such that
A4:   J = y by A2;
      I /\ J is Ideal of L by Th40;
      hence thesis by A3,A4;
    end;
    hence thesis by YELLOW_1:12;
  end;
end;

theorem Th44:
  for L being with_suprema Poset for x, y being Element of
InclPoset(Ids L) holds ex Z being Subset of L st Z = {z where z is Element of L
  : z in x or z in y or ex a, b being Element of L st a in x & b in y & z = a
  "\/" b} & ex_sup_of {x, y},InclPoset(Ids L) & x "\/" y = downarrow Z
proof
  let L be with_suprema Poset;
  set P = InclPoset(Ids L);
  let x, y be Element of P;
  defpred P[Element of L] means $1 in x or $1 in y or ex a, b being Element of
  L st a in x & b in y & $1 = a "\/" b;
  reconsider Z = {z where z is Element of L: P[z]} as Subset of L from
  DOMAIN_1:sch 7;
  take Z;
  reconsider x9= x, y9= y as Ideal of L by Th41;
  set z = the Element of x9;
  z in Z;
  then reconsider Z as non empty Subset of L;
  set DZ = downarrow Z;
  for u, v being Element of L st u in Z & v in Z ex z being Element of L
  st z in Z & u <= z & v <= z
  proof
A1: for p, q being Element of L st p in y & ex a, b being Element of L st
a in x & b in y & q = a "\/" b holds ex z being Element of L st z in Z & p <= z
    & q <= z
    proof
      let p, q be Element of L such that
A2:   p in y and
A3:   ex a, b being Element of L st a in x & b in y & q = a "\/" b;
      consider a, b being Element of L such that
A4:   a in x and
A5:   b in y and
A6:   q = a "\/" b by A3;
      reconsider c = b "\/" p as Element of L;
      take z = a "\/" c;
      c in y9 by A2,A5,WAYBEL_0:40;
      hence z in Z by A4;
A7:   c <= z by YELLOW_0:22;
A8:   p <= c & a <= z by YELLOW_0:22;
      b <= c by YELLOW_0:22;
      then b <= z by A7,ORDERS_2:3;
      hence thesis by A6,A7,A8,ORDERS_2:3,YELLOW_0:22;
    end;
A9: for p, q being Element of L st p in x & ex a, b being Element of L st
a in x & b in y & q = a "\/" b holds ex z being Element of L st z in Z & p <= z
    & q <= z
    proof
      let p, q be Element of L such that
A10:  p in x and
A11:  ex a, b being Element of L st a in x & b in y & q = a "\/" b;
      consider a, b being Element of L such that
A12:  a in x and
A13:  b in y and
A14:  q = a "\/" b by A11;
      reconsider c = a "\/" p as Element of L;
      take z = c "\/" b;
      c in x9 by A10,A12,WAYBEL_0:40;
      hence z in Z by A13;
A15:  c <= z by YELLOW_0:22;
A16:  p <= c & b <= z by YELLOW_0:22;
      a <= c by YELLOW_0:22;
      then a <= z by A15,ORDERS_2:3;
      hence thesis by A14,A15,A16,ORDERS_2:3,YELLOW_0:22;
    end;
    let u, v be Element of L such that
A17: u in Z and
A18: v in Z;
    consider p being Element of L such that
A19: p = u and
A20: p in x or p in y or ex a, b being Element of L st a in x & b in y
    & p = a "\/" b by A17;
    consider q being Element of L such that
A21: q = v and
A22: q in x or q in y or ex a, b being Element of L st a in x & b in y
    & q = a "\/" b by A18;
    per cases by A20,A22;
    suppose
      p in x & q in x;
      then consider z being Element of L such that
A23:  z in x9 & p <= z & q <= z by WAYBEL_0:def 1;
      take z;
      thus thesis by A19,A21,A23;
    end;
    suppose
A24:  p in x & q in y;
      take p "\/" q;
      thus thesis by A19,A21,A24,YELLOW_0:22;
    end;
    suppose
      p in x & ex a, b being Element of L st a in x & b in y & q = a "\/" b;
      then consider z being Element of L such that
A25:  z in Z & p <= z & q <= z by A9;
      take z;
      thus thesis by A19,A21,A25;
    end;
    suppose
A26:  p in y & q in x;
      take q "\/" p;
      thus thesis by A19,A21,A26,YELLOW_0:22;
    end;
    suppose
      p in y & q in y;
      then consider z being Element of L such that
A27:  z in y9 & p <= z & q <= z by WAYBEL_0:def 1;
      take z;
      thus thesis by A19,A21,A27;
    end;
    suppose
      p in y & ex a, b being Element of L st a in x & b in y & q = a "\/" b;
      then consider z being Element of L such that
A28:  z in Z & p <= z & q <= z by A1;
      take z;
      thus thesis by A19,A21,A28;
    end;
    suppose
      q in x & ex a, b being Element of L st a in x & b in y & p = a "\/" b;
      then consider z being Element of L such that
A29:  z in Z & q <= z & p <= z by A9;
      take z;
      thus thesis by A19,A21,A29;
    end;
    suppose
      q in y & ex a, b being Element of L st a in x & b in y & p = a "\/" b;
      then consider z being Element of L such that
A30:  z in Z & q <= z & p <= z by A1;
      take z;
      thus thesis by A19,A21,A30;
    end;
    suppose
      (ex a, b being Element of L st a in x & b in y & p = a "\/" b)
      & ex a, b being Element of L st a in x & b in y & q = a "\/" b;
      then consider a, b, c, d being Element of L such that
A31:  a in x & b in y and
A32:  p = a "\/" b and
A33:  c in x & d in y and
A34:  q = c "\/" d;
      reconsider ac = a "\/" c, bd = b "\/" d as Element of L;
      take z = ac "\/" bd;
      ac in x9 & bd in y9 by A31,A33,WAYBEL_0:40;
      hence z in Z;
A35:  ac <= z by YELLOW_0:22;
A36:  bd <= z by YELLOW_0:22;
      b <= bd by YELLOW_0:22;
      then
A37:  b <= z by A36,ORDERS_2:3;
      a <= ac by YELLOW_0:22;
      then a <= z by A35,ORDERS_2:3;
      hence u <= z by A19,A32,A37,YELLOW_0:22;
      d <= bd by YELLOW_0:22;
      then
A38:  d <= z by A36,ORDERS_2:3;
      c <= ac by YELLOW_0:22;
      then c <= z by A35,ORDERS_2:3;
      hence thesis by A21,A34,A38,YELLOW_0:22;
    end;
  end;
  then Z is directed;
  then reconsider DZ as Element of P by Th41;
A39: for d being Element of P st d >= x & d >= y holds DZ <= d
  proof
    let d be Element of P;
    assume that
A40: x <= d and
A41: y <= d;
A42: y c= d by A41,YELLOW_1:3;
A43: x c= d by A40,YELLOW_1:3;
    DZ c= d
    proof
      let p be object;
      assume p in DZ;
      then p in {q where q is Element of L: ex u being Element of L st q <= u
      & u in Z} by WAYBEL_0:14;
      then consider p9 being Element of L such that
A44:  p9 = p and
A45:  ex u being Element of L st p9 <= u & u in Z;
      consider u being Element of L such that
A46:  p9 <= u and
A47:  u in Z by A45;
      consider z being Element of L such that
A48:  z = u and
A49:  z in x or z in y or ex a, b being Element of L st a in x & b in
      y & z = a "\/" b by A47;
      per cases by A49;
      suppose
        z in x;
        then p in x9 by A44,A46,A48,WAYBEL_0:def 19;
        hence thesis by A43;
      end;
      suppose
        z in y;
        then p in y9 by A44,A46,A48,WAYBEL_0:def 19;
        hence thesis by A42;
      end;
      suppose
A50:    ex a, b being Element of L st a in x & b in y & z = a "\/" b;
        reconsider d9= d as Ideal of L by Th41;
        u in d9 by A43,A42,A48,A50,WAYBEL_0:40;
        hence thesis by A44,A46,WAYBEL_0:def 19;
      end;
    end;
    hence thesis by YELLOW_1:3;
  end;
  y c= DZ
  proof
    let a be object;
A51: Z c= DZ by WAYBEL_0:16;
    assume
A52: a in y;
    then reconsider a9= a as Element of L by Th42;
    a9 in Z by A52;
    hence thesis by A51;
  end;
  then
A53: y <= DZ by YELLOW_1:3;
  x c= DZ
  proof
    let a be object;
A54: Z c= DZ by WAYBEL_0:16;
    assume
A55: a in x;
    then reconsider a9= a as Element of L by Th42;
    a9 in Z by A55;
    hence thesis by A54;
  end;
  then x <= DZ by YELLOW_1:3;
  hence thesis by A53,A39,YELLOW_0:18;
end;

registration
  let L be with_suprema Poset;
  cluster InclPoset(Ids L) -> with_suprema;
  correctness
  proof
    set P = InclPoset(Ids L);
    for x, y being Element of P ex z being Element of P st x <= z & y <= z
    & for z9 being Element of P st x <= z9 & y <= z9 holds z <= z9
    proof
      let x, y be Element of P;
      take x "\/" y;
      ex Z being Subset of L st Z = {z where z is Element of L: z in x or z
      in y or ex a, b being Element of L st a in x & b in y & z = a "\/" b} &
      ex_sup_of {x, y},InclPoset(Ids L) & x "\/" y = downarrow Z by Th44;
      hence thesis by YELLOW_0:18;
    end;
    hence thesis;
  end;
end;

theorem Th45:
  for L being lower-bounded sup-Semilattice for X being non empty
  Subset of Ids L holds meet X is Ideal of L
proof
  let L be lower-bounded sup-Semilattice;
  let X be non empty Subset of Ids L;
A1: for J being set st J in X holds J is Ideal of L
  proof
    let J be set;
    assume J in X;
    then J in Ids L;
    then ex Y being Ideal of L st Y = J;
    hence thesis;
  end;
  X c= bool the carrier of L
  proof
    let x be object;
    assume x in X;
    then x is Ideal of L by A1;
    hence thesis;
  end;
  then reconsider F = X as Subset-Family of L;
  for J being Subset of L st J in F holds J is lower by A1;
  then reconsider I = meet X as lower Subset of L by Th36;
  for J being set st J in X holds Bottom L in J
  proof
    let J be set;
    assume J in X;
    then reconsider J9= J as Ideal of L by A1;
    set j = the Element of J9;
    Bottom L <= j by YELLOW_0:44;
    hence thesis by WAYBEL_0:def 19;
  end;
  then reconsider I as non empty lower Subset of L by SETFAM_1:def 1;
  for J being Subset of L st J in F holds J is lower directed by A1;
  then I is Ideal of L by Th38;
  hence thesis;
end;

theorem Th46:
  for L being lower-bounded sup-Semilattice for A being non empty
Subset of InclPoset(Ids L) holds ex_inf_of A,InclPoset(Ids L) & inf A = meet A
proof
  let L be lower-bounded sup-Semilattice;
  let A be non empty Subset of InclPoset(Ids L);
  set P = InclPoset(Ids L);
  reconsider A9= A as non empty Subset of Ids L by YELLOW_1:1;
  meet A9 is Ideal of L by Th45;
  then reconsider I = meet A as Element of P by Th41;
A1: for b being Element of P st b is_<=_than A holds I >= b
  proof
    let b be Element of P;
    assume
A2: A is_>=_than b;
A3: for J being set st J in A holds b c= J
    by A2,YELLOW_1:3;
    b c= I
    proof
      let c be object;
      assume
A4:   c in b;
      for J being set st J in A holds c in J
      proof
        let J be set;
        assume J in A;
        then b c= J by A3;
        hence thesis by A4;
      end;
      hence thesis by SETFAM_1:def 1;
    end;
    hence thesis by YELLOW_1:3;
  end;
  I is_<=_than A
  proof
    let y be Element of P;
    assume
A5: y in A;
    I c= y
    by A5,SETFAM_1:def 1;
    hence I <= y by YELLOW_1:3;
  end;
  hence thesis by A1,YELLOW_0:31;
end;

theorem Th47:
  for L being with_suprema Poset holds ex_inf_of {},InclPoset(Ids
  L) & "/\"({}, InclPoset(Ids L)) = [#]L
proof
  let L be with_suprema Poset;
  set P = InclPoset(Ids L);
  reconsider I = [#]L as Element of P by Th41;
A1: for b being Element of P st b is_<=_than {} holds I >= b
  proof
    let b be Element of P;
    reconsider b9= b as Ideal of L by Th41;
    assume {} is_>=_than b;
    b9 c= [#]L;
    hence thesis by YELLOW_1:3;
  end;
  I is_<=_than {};
  hence thesis by A1,YELLOW_0:31;
end;

theorem Th48:
  for L being lower-bounded sup-Semilattice holds InclPoset(Ids L) is complete
proof
  let L be lower-bounded sup-Semilattice;
  set P = InclPoset(Ids L);
  for A being Subset of P holds ex_inf_of A,InclPoset(Ids L)
  proof
    let A be Subset of P;
    per cases;
    suppose
      A = {};
      hence thesis by Th47;
    end;
    suppose
      A <> {};
      hence thesis by Th46;
    end;
  end;
  hence thesis by Th28;
end;

registration
  let L be lower-bounded sup-Semilattice;
  cluster InclPoset(Ids L) -> complete;
  correctness by Th48;
end;

begin :: Special Maps

definition
  let L be non empty Poset;
  func SupMap L -> Function of InclPoset(Ids L), L means
  :Def3:
  for I being Ideal of L holds it.I = sup I;
  existence
  proof
    deffunc F(set) = "\/"($1, L);
    set P = InclPoset(Ids L);
A1: for I being set st I in the carrier of P
       holds F(I) in the carrier of L;
    ex f being Function of the carrier of P, the carrier of L st for I
    being set st I in the carrier of P holds f.I = F(I)
     from FUNCT_2:sch 11(A1);
    then consider
    f being Function of the carrier of P, the carrier of L such that
A2: for I being set st I in the carrier of P holds f.I = "\/"(I, L);
    reconsider f as Function of P, L;
   take f;
    for I being Ideal of L holds f.I = sup I
    proof
      let I be Ideal of L;
      I in the carrier of RelStr(#Ids L, RelIncl Ids L#);
      then I in the carrier of P by YELLOW_1:def 1;
      hence thesis by A2;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    set P = InclPoset(Ids L);
    let f, g be Function of InclPoset(Ids L), L;
    assume that
A3: for I being Ideal of L holds f.I = sup I and
A4: for I being Ideal of L holds g.I = sup I;
A5: the carrier of P = the carrier of RelStr(#Ids L, RelIncl(Ids L)#) by
YELLOW_1:def 1
      .= Ids L;
A6: now
      let x be object;
      assume x in the carrier of P;
      then ex I being Ideal of L st x = I by A5;
      then reconsider I = x as Ideal of L;
      f.I = sup I by A3;
      hence f.x = g.x by A4;
    end;
    dom f = the carrier of P & dom g = the carrier of P by FUNCT_2:def 1;
    hence f = g by A6,FUNCT_1:2;
  end;
end;

theorem Th49:
  for L being non empty Poset holds dom SupMap L = Ids L & rng
  SupMap L is Subset of L
proof
  let L be non empty Poset;
  set P = InclPoset(Ids L);
  thus dom(SupMap L) = the carrier of P by FUNCT_2:def 1
    .= the carrier of RelStr(#Ids L, RelIncl(Ids L)#) by YELLOW_1:def 1
    .= Ids L;
  thus thesis;
end;

theorem
  for L being non empty Poset holds x in dom SupMap L iff x is Ideal of L
proof
  let L be non empty Poset;
  hereby
    assume x in dom SupMap L;
    then x in Ids L by Th49;
    then ex I being Ideal of L st x = I;
    hence x is Ideal of L;
  end;
  assume x is Ideal of L;
  then x in the set of all X where X is Ideal of L;
  hence thesis by Th49;
end;

theorem Th51:
  for L being up-complete non empty Poset holds SupMap L is monotone
proof
  let L be up-complete non empty Poset;
  set P = InclPoset Ids L;
  set f = SupMap L;
  for x, y being Element of P st x <= y for a, b being Element of L st a =
  f.x & b = f.y holds a <= b
  proof
    let x, y be Element of P such that
A1: x <= y;
    reconsider I = x, J = y as Ideal of L by Th41;
A2: I c= J by A1,YELLOW_1:3;
A3: ex_sup_of I,L & ex_sup_of J,L by WAYBEL_0:75;
A4: f.x = sup I & f.y = sup J by Def3;
    let a, b be Element of L;
    assume a = f.x & b = f.y;
    hence thesis by A3,A2,A4,YELLOW_0:34;
  end;
  hence thesis;
end;

registration
  let L be up-complete non empty Poset;
  cluster SupMap L -> monotone;
  correctness by Th51;
end;

definition
  let L be non empty Poset;
  func IdsMap L -> Function of L, InclPoset(Ids L) means
  :Def4:
  for x being Element of L holds it.x = downarrow x;
  existence
  proof
    deffunc F(Element of L) = downarrow $1;
A1: for x being Element of L holds F(x) is Element of InclPoset(Ids L) by Th41;
    thus ex m being Function of L, InclPoset Ids L st for x being Element of L
    holds m.x = F(x) from FUNCT_2:sch 9(A1);
  end;
  uniqueness
  proof
    let f1,f2 be Function of L,InclPoset(Ids L) such that
A2: for x being Element of L holds f1.x = downarrow x and
A3: for x being Element of L holds f2.x = downarrow x;
    now
      let x be Element of L;
      thus f1.x = downarrow x by A2
        .= f2.x by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th52:
  for L being non empty Poset holds IdsMap L is monotone
proof
  let L be non empty Poset;
  let x1,x2 be Element of L;
  assume x1 <= x2;
  then downarrow x1 c= downarrow x2 by WAYBEL_0:21;
  then (IdsMap L).x1 c= downarrow x2 by Def4;
  then
A1: (IdsMap L).x1 c= (IdsMap L).x2 by Def4;
  let a, b be Element of InclPoset(Ids L);
  assume a = (IdsMap L).x1 & b = (IdsMap L).x2;
  hence a <= b by A1,YELLOW_1:3;
end;

registration
  let L be non empty Poset;
  cluster IdsMap L -> monotone;
  correctness by Th52;
end;

begin :: A Family of Elements in a Lattice

definition
  let L be non empty RelStr;
  let F be Relation;
  func \\/(F, L) -> Element of L equals
  "\/"(rng F, L);
  coherence;
  func //\(F, L) -> Element of L equals
  "/\"(rng F, L);
  coherence;
end;

notation
  let J be set, L be non empty RelStr;
  let F be Function of J, the carrier of L;
  synonym Sup F for \\/(F, L);
  synonym Inf F for //\(F, L);
end;

reserve J for non empty set,
  j for Element of J;

theorem
  for F being Function of J, the carrier of L holds F.j <= Sup F & Inf F <= F.j
proof
  let F be Function of J, the carrier of L;
  F.j in rng F by FUNCT_2:4;
  hence thesis by Th22;
end;

theorem
  for F being Function of J, the carrier of L holds (for j holds F.j <=
  a) implies Sup F <= a
proof
  let F be Function of J, the carrier of L;
  assume
A1: for j holds F.j <= a;
  now
    let c be Element of L;
    assume c in rng F;
    then consider j being object such that
A2: j in dom F and
A3: c = F.j by FUNCT_1:def 3;
    reconsider j as Element of J by A2;
    c = F.j by A3;
    hence c <= a by A1;
  end;
  then rng F is_<=_than a;
  hence thesis by YELLOW_0:32;
end;

theorem
  for F being Function of J, the carrier of L holds (for j holds a <= F.
  j) implies a <= Inf F
proof
  let F be Function of J, the carrier of L;
  assume
A1: for j holds a <= F.j;
  now
    let c be Element of L;
    assume c in rng F;
    then consider j being object such that
A2: j in dom F and
A3: c = F.j by FUNCT_1:def 3;
    reconsider j as Element of J by A2;
    c = F.j by A3;
    hence a <= c by A1;
  end;
  then a is_<=_than rng F;
  hence thesis by YELLOW_0:33;
end;