:: Algebraic Lattices
::  by Robert Milewski
::
:: Received December 1, 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, RELAT_2, ORDERS_2, STRUCT_0, CAT_1, YELLOW_0, SUBSET_1,
      RCOMP_1, WELLORD1, TARSKI, LATTICES, REWRITE1, WAYBEL_0, XXREAL_0,
      WAYBEL_3, WAYBEL_6, CARD_FIL, LATTICE3, EQREL_1, ORDINAL2, FINSET_1,
      ZFMISC_1, WAYBEL_4, MSSUBFAM, WAYBEL_7, INT_2, WAYBEL_1, FUNCT_1,
      GROUP_6, RELAT_1, BINOP_1, SEQM_3, YELLOW_1, FILTER_1, SETFAM_1,
      WAYBEL_8, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, CARD_1, FINSET_1,
      RELAT_1, TOLER_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, RELAT_2,
      STRUCT_0, ORDERS_2, LATTICE3, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2,
      WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7;
 constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_1, YELLOW_3,
      WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, RELSET_1, PRALG_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3,
      WAYBEL_4, WAYBEL_6;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI, RELAT_2, ORDERS_2;
 equalities YELLOW_2, STRUCT_0;
 expansions TARSKI, RELAT_2, ORDERS_2;
 theorems TARSKI, STRUCT_0, FINSET_1, FUNCT_1, FUNCT_2, ORDERS_2, LATTICE3,
      YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_5, WAYBEL_0, WAYBEL_1,
      WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, RELAT_1, YELLOW_7, XBOOLE_0,
      XBOOLE_1;
 schemes SUBSET_1, FUNCT_1;

begin :: The Subset of All Compact Elements

definition :: DEFINITION 4.1
  let L be non empty reflexive RelStr;
  func CompactSublatt L -> strict full SubRelStr of L means
  :Def1:
  for x be Element of L holds x in the carrier of it iff x is compact;
  existence
  proof
    defpred P[set] means ex y be Element of L st y = $1 & y is compact;
    consider X being Subset of L such that
A1: for x be set holds x in X iff x in the carrier of L & P[x] from
    SUBSET_1:sch 1;
    reconsider S = RelStr(#X, (the InternalRel of L)|_2 X#) as strict full
    SubRelStr of L by YELLOW_0:56;
    take S;
    let x be Element of L;
    thus x in the carrier of S implies x is compact
    proof
      assume x in the carrier of S;
      then ex y be Element of L st y = x & y is compact by A1;
      hence thesis;
    end;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let K1,K2 be strict full SubRelStr of L such that
A2: for x be Element of L holds x in the carrier of K1 iff x is compact and
A3: for x be Element of L holds x in the carrier of K2 iff x is compact;
    now
      let x be object;
      thus x in the carrier of K1 implies x in the carrier of K2
      proof
        assume
A4:     x in the carrier of K1;
        the carrier of K1 c= the carrier of L by YELLOW_0:def 13;
        then reconsider x9 = x as Element of L by A4;
        x9 is compact by A2,A4;
        hence thesis by A3;
      end;
      thus x in the carrier of K2 implies x in the carrier of K1
      proof
        assume
A5:     x in the carrier of K2;
        the carrier of K2 c= the carrier of L by YELLOW_0:def 13;
        then reconsider x9 = x as Element of L by A5;
        x9 is compact by A3,A5;
        hence thesis by A2;
      end;
    end;
    then the carrier of K1 = the carrier of K2 by TARSKI:2;
    hence thesis by YELLOW_0:57;
  end;
end;

registration
  let L be lower-bounded non empty reflexive antisymmetric RelStr;
  cluster CompactSublatt L -> non empty;
  coherence
  proof
    Bottom L is compact by WAYBEL_3:15;
    hence thesis by Def1;
  end;
end;

theorem
  for L be complete LATTICE for x,y,k be Element of L holds x <= k & k
  <= y & k in the carrier of CompactSublatt L implies x << y
proof
  let L be complete LATTICE;
  let x,y,k be Element of L;
  assume that
A1: x <= k & k <= y and
A2: k in the carrier of CompactSublatt L;
  k is compact by A2,Def1;
  then k << k by WAYBEL_3:def 2;
  hence thesis by A1,WAYBEL_3:2;
end;

theorem :: REMARK 4.2
  for L be complete LATTICE for x be Element of L holds uparrow x is
  Open Filter of L iff x is compact
proof
  let L be complete LATTICE;
  let x be Element of L;
  thus uparrow x is Open Filter of L implies x is compact
  proof
    x <= x;
    then
A1: x in uparrow x by WAYBEL_0:18;
    assume uparrow x is Open Filter of L;
    then consider y be Element of L such that
A2: y in uparrow x and
A3: y << x by A1,WAYBEL_6:def 1;
    x <= y by A2,WAYBEL_0:18;
    then x << x by A3,WAYBEL_3:2;
    hence thesis by WAYBEL_3:def 2;
  end;
  assume
A4: x is compact;
  now
    let u be Element of L;
    assume u in uparrow x;
    then
A5: x <= u by WAYBEL_0:18;
    take x2 = x;
    x <= x2;
    hence x2 in uparrow x by WAYBEL_0:18;
    x << x by A4,WAYBEL_3:def 2;
    hence x2 << u by A5,WAYBEL_3:2;
  end;
  hence thesis by WAYBEL_6:def 1;
end;

theorem :: REMARK 4.3
  for L be lower-bounded with_suprema non empty Poset holds
CompactSublatt L is join-inheriting & Bottom L in the carrier of CompactSublatt
  L
proof
  let L be lower-bounded with_suprema non empty Poset;
  now
    let x,y be Element of L;
    assume that
A1: x in the carrier of CompactSublatt L and
A2: y in the carrier of CompactSublatt L and
A3: ex_sup_of {x,y},L;
    y is compact by A2,Def1;
    then
A4: y << y by WAYBEL_3:def 2;
    x is compact by A1,Def1;
    then
A5: x << x by WAYBEL_3:def 2;
    y <= x "\/" y by A3,YELLOW_0:18;
    then
A6: y << x "\/" y by A4,WAYBEL_3:2;
    x <= x "\/" y by A3,YELLOW_0:18;
    then x << x "\/" y by A5,WAYBEL_3:2;
    then x "\/" y << x "\/" y by A6,WAYBEL_3:3;
    then x "\/" y is compact by WAYBEL_3:def 2;
    then sup {x,y} is compact by YELLOW_0:41;
    hence sup {x,y} in the carrier of CompactSublatt L by Def1;
  end;
  hence CompactSublatt L is join-inheriting by YELLOW_0:def 17;
  Bottom L is compact by WAYBEL_3:15;
  hence thesis by Def1;
end;

definition
  let L be non empty reflexive RelStr;
  let x be Element of L;
  func compactbelow x -> Subset of L equals
  {y where y is Element of L: x >= y
  & y is compact};
  coherence
  proof
    set Z = {y where y is Element of L: x >= y & y is compact};
    defpred P[Element of L] means x >= $1 & $1 is compact;
    consider X being Subset of L such that
A1: for y being Element of L holds y in X iff P[y] from SUBSET_1:sch 3;
    now
      let z be object;
      thus z in X implies z in Z
      proof
        assume
A2:     z in X;
        then reconsider z1 = z as Element of L;
        x >= z1 & z1 is compact by A1,A2;
        hence thesis;
      end;
      thus z in Z implies z in X
      proof
        assume z in Z;
        then ex v be Element of L st v = z & x >= v & v is compact;
        hence thesis by A1;
      end;
    end;
    hence thesis by TARSKI:2;
  end;
end;

theorem Th4:
  for L be non empty reflexive RelStr for x,y be Element of L holds
  y in compactbelow x iff x >= y & y is compact
proof
  let L be non empty reflexive RelStr;
  let x,y be Element of L;
  thus y in compactbelow x implies x >= y & y is compact
  proof
    assume y in compactbelow x;
    then ex z be Element of L st z = y & x >= z & z is compact;
    hence thesis;
  end;
  assume x >= y & y is compact;
  hence thesis;
end;

theorem Th5:
  for L be non empty reflexive RelStr for x be Element of L holds
  compactbelow x = downarrow x /\ the carrier of CompactSublatt L
proof
  let L be non empty reflexive RelStr;
  let x be Element of L;
  now
    let y be object;
    assume
A1: y in downarrow x /\ the carrier of CompactSublatt L;
    then reconsider y9 = y as Element of L;
    y in downarrow x by A1,XBOOLE_0:def 4;
    then
A2: y9 <= x by WAYBEL_0:17;
    y in the carrier of CompactSublatt L by A1,XBOOLE_0:def 4;
    then y9 is compact by Def1;
    hence y in compactbelow x by A2;
  end;
  then
A3: downarrow x /\ the carrier of CompactSublatt L c= compactbelow x;
  now
    let y be object;
    assume y in compactbelow x;
    then consider y9 be Element of L such that
A4: y9 = y and
A5: y9 <= x & y9 is compact;
    y9 in downarrow x & y9 in the carrier of CompactSublatt L by A5,Def1,
WAYBEL_0:17;
    hence y in downarrow x /\ the carrier of CompactSublatt L by A4,
XBOOLE_0:def 4;
  end;
  then compactbelow x c= downarrow x /\ the carrier of CompactSublatt L;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem Th6:
  for L be non empty reflexive transitive RelStr for x be Element
  of L holds compactbelow x c= waybelow x
proof
  let L be non empty reflexive transitive RelStr;
  let x be Element of L;
  now
    let z be object;
    assume z in compactbelow x;
    then consider z9 be Element of L such that
A1: z9 = z and
A2: x >= z9 and
A3: z9 is compact;
    z9 << z9 by A3,WAYBEL_3:def 2;
    then z9 << x by A2,WAYBEL_3:2;
    hence z in waybelow x by A1,WAYBEL_3:7;
  end;
  hence thesis;
end;

registration
  let L be non empty lower-bounded reflexive antisymmetric RelStr;
  let x be Element of L;
  cluster compactbelow x -> non empty;
  coherence
  proof
    x >= Bottom L & Bottom L is compact by WAYBEL_3:15,YELLOW_0:44;
    then Bottom L in {y where y is Element of L: x >= y & y is compact};
    hence thesis;
  end;
end;

begin :: Algebraic Lattices

definition
  let L be non empty reflexive RelStr;
  attr L is satisfying_axiom_K means
  :Def3:
  for x be Element of L holds x = sup compactbelow x;
end;

definition :: DEFINITION 4.4
  let L be non empty reflexive RelStr;
  attr L is algebraic means
  :Def4:
  (for x being Element of L holds
  compactbelow x is non empty directed) & L is up-complete satisfying_axiom_K;
end;

theorem Th7: :: PROPOSITION 4.5
  for L be LATTICE holds L is algebraic iff ( L is continuous & for
  x,y be Element of L st x << y ex k be Element of L st k in the carrier of
  CompactSublatt L & x <= k & k <= y )
proof
  let L be LATTICE;
  thus L is algebraic implies ( L is continuous & for x,y be Element of L st x
<< y ex k be Element of L st k in the carrier of CompactSublatt L & x <= k & k
  <= y )
  proof
    assume
A1: L is algebraic;
    then
A2: L is up-complete satisfying_axiom_K;
    now
      let x be Element of L;
A3:   compactbelow x is non empty directed by A1;
      then
A4:   ex s be object st s in compactbelow x by XBOOLE_0:def 1;
      compactbelow x c= waybelow x by Th6;
      then
A5:   ex_sup_of waybelow x,L by A2,A4,WAYBEL_0:75;
      ex_sup_of compactbelow x,L by A2,A3,WAYBEL_0:75;
      then sup compactbelow x <= sup waybelow x by A5,Th6,YELLOW_0:34;
      then
A6:   x <= sup waybelow x by A2;
      waybelow x is_<=_than x by WAYBEL_3:9;
      then sup waybelow x <= x by A5,YELLOW_0:def 9;
      hence x = sup waybelow x by A6,ORDERS_2:2;
    end;
    then
A7: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
    for x be Element of L holds waybelow x is non empty directed
    proof
      let x be Element of L;
      compactbelow x c= waybelow x by Th6;
      hence thesis by A1;
    end;
    hence L is continuous by A2,A7,WAYBEL_3:def 6;
    let x,y be Element of L;
    reconsider D = compactbelow y as non empty directed Subset of L by A1;
    assume
A8: x << y;
    y = sup D by A2;
    then consider d being Element of L such that
A9: d in D and
A10: x <= d by A8,WAYBEL_3:def 1;
    take d;
    d is compact by A9,Th4;
    hence d in the carrier of CompactSublatt L by Def1;
    thus thesis by A9,A10,Th4;
  end;
  assume that
A11: L is continuous and
A12: for x,y be Element of L st x << y ex k be Element of L st k in the
  carrier of CompactSublatt L & x <= k & k <= y;
  now

    let x be Element of L;
A13: now
      let z be Element of L;
      thus z is_>=_than waybelow x implies z is_>=_than compactbelow x
      proof
        assume
A14:    z is_>=_than waybelow x;
        now
          let d be Element of L;
          assume
A15:      d in compactbelow x;
          then d is compact by Th4;
          then
A16:      d << d by WAYBEL_3:def 2;
          d <= x by A15,Th4;
          then d << x by A16,WAYBEL_3:2;
          then d in waybelow x by WAYBEL_3:7;
          hence d <= z by A14,LATTICE3:def 9;
        end;
        hence thesis by LATTICE3:def 9;
      end;
      thus z is_>=_than compactbelow x implies z is_>=_than waybelow x
      proof
        assume
A17:    z is_>=_than compactbelow x;
        now
          let d be Element of L;
          assume d in waybelow x;
          then d << x by WAYBEL_3:7;
          then consider k be Element of L such that
A18:      k in the carrier of CompactSublatt L and
A19:      d <= k and
A20:      k <= x by A12;
          k is compact by A18,Def1;
          then k in compactbelow x by A20;
          then k <= z by A17,LATTICE3:def 9;
          hence d <= z by A19,ORDERS_2:3;
        end;
        hence thesis by LATTICE3:def 9;
      end;
    end;
    x = sup waybelow x & ex_sup_of waybelow x,L by A11,WAYBEL_0:75
,WAYBEL_3:def 5;
    hence x = sup compactbelow x by A13,YELLOW_0:47;
  end;
  then
A21: L is satisfying_axiom_K;
  for x be Element of L holds compactbelow x is non empty directed
  proof
    let x be Element of L;
    now
      let Y be finite Subset of compactbelow x;
      compactbelow x c= waybelow x by Th6;
      then Y is finite Subset of waybelow x by XBOOLE_1:1;
      then consider b be Element of L such that
A22:  b in waybelow x and
A23:  b is_>=_than Y by A11,WAYBEL_0:1;
      b << x by A22,WAYBEL_3:7;
      then consider c be Element of L such that
A24:  c in the carrier of CompactSublatt L and
A25:  b <= c and
A26:  c <= x by A12;
      take c;
      c is compact by A24,Def1;
      hence c in compactbelow x by A26;
      thus c is_>=_than Y by A23,A25,YELLOW_0:4;
    end;
    hence thesis by WAYBEL_0:1;
  end;
  hence thesis by A11,A21;
end;

registration
  cluster algebraic -> continuous for LATTICE;
  coherence by Th7;
end;

registration
  cluster algebraic -> up-complete satisfying_axiom_K for non empty reflexive
    RelStr;
  coherence;
end;

registration
  let L be non empty with_suprema Poset;
  cluster CompactSublatt L -> join-inheriting;
  coherence
  proof
    now
      let x,y be Element of L;
      assume that
A1:   x in the carrier of CompactSublatt L and
A2:   y in the carrier of CompactSublatt L and
A3:   ex_sup_of {x,y},L;
      y is compact by A2,Def1;
      then
A4:   y << y by WAYBEL_3:def 2;
      x is compact by A1,Def1;
      then
A5:   x << x by WAYBEL_3:def 2;
      y <= x "\/" y by A3,YELLOW_0:18;
      then
A6:   y << x "\/" y by A4,WAYBEL_3:2;
      x <= x "\/" y by A3,YELLOW_0:18;
      then x << x "\/" y by A5,WAYBEL_3:2;
      then x "\/" y << x "\/" y by A6,WAYBEL_3:3;
      then x "\/" y is compact by WAYBEL_3:def 2;
      then sup {x,y} is compact by YELLOW_0:41;
      hence sup {x,y} in the carrier of CompactSublatt L by Def1;
    end;
    hence thesis by YELLOW_0:def 17;
  end;
end;

definition
  let L be non empty reflexive RelStr;
  attr L is arithmetic means

  L is algebraic & CompactSublatt L is meet-inheriting;
end;

begin :: Arithmetic Lattices

registration
  cluster arithmetic -> algebraic for LATTICE;
  coherence;
end;

registration
  cluster trivial -> arithmetic for LATTICE;
  coherence
  proof
    let L be LATTICE;
    assume
A1:   L is trivial;
    reconsider L9 = L as 1-element LATTICE by A1;
A2:    for x,y be Element of L9 st x << y ex k be Element of L9 st k in the
    carrier of CompactSublatt L9 & x <= k & k <= y
    proof
      let x,y be Element of L9;
      assume
A3:   x << y;
      take k = x;
      x = y by STRUCT_0:def 10;
      then k is compact by A3,WAYBEL_3:def 2;
      hence k in the carrier of CompactSublatt L9 by Def1;
      thus thesis by STRUCT_0:def 10;
    end;
A4: L9 is algebraic by Th7,A2;
    for z,v be Element of L9 st z in the carrier of CompactSublatt L9 & v
in the carrier of CompactSublatt L9 & ex_inf_of {z,v},L9 holds inf {z,v} in the
    carrier of CompactSublatt L9 by STRUCT_0:def 10;
    then CompactSublatt L9 is meet-inheriting by YELLOW_0:def 16;
    hence thesis by A4;
  end;
end;

registration
  cluster 1-element strict for LATTICE;
  existence
  proof
    set B =the strict 1-element reflexive RelStr;
    take B;
    thus thesis;
  end;
end;

theorem Th8:
  for L1,L2 be non empty reflexive antisymmetric RelStr st the
RelStr of L1 = the RelStr of L2 & L1 is up-complete for x1,y1 be Element of L1
  for x2,y2 be Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2
proof
  let L1,L2 be non empty reflexive antisymmetric RelStr;
  assume that
A1: the RelStr of L1 = the RelStr of L2 and
A2: L1 is up-complete;
  let x1,y1 be Element of L1;
  let x2,y2 be Element of L2;
  assume that
A3: x1 = x2 and
A4: y1 = y2 and
A5: x1 << y1;
  now
    let D2 be non empty directed Subset of L2;
    reconsider D1 = D2 as Subset of L1 by A1;
    reconsider D1 as non empty directed Subset of L1 by A1,WAYBEL_0:3;
    ex_sup_of D1,L1 by A2,WAYBEL_0:75;
    then
A6: sup D1 = sup D2 by A1,YELLOW_0:26;
    assume y2 <= sup D2;
    then y1 <= sup D1 by A1,A4,A6;
    then consider d1 be Element of L1 such that
A7: d1 in D1 and
A8: x1 <= d1 by A5,WAYBEL_3:def 1;
    reconsider d2 = d1 as Element of L2 by A1;
    take d2;
    thus d2 in D2 by A7;
    thus x2 <= d2 by A1,A3,A8;
  end;
  hence thesis by WAYBEL_3:def 1;
end;

theorem Th9:
  for L1,L2 be non empty reflexive antisymmetric RelStr st the
RelStr of L1 = the RelStr of L2 & L1 is up-complete for x be Element of L1 for
  y be Element of L2 st x = y & x is compact holds y is compact
proof
  let L1,L2 be non empty reflexive antisymmetric RelStr;
  assume
A1: the RelStr of L1 = the RelStr of L2 & L1 is up-complete;
  let x be Element of L1;
  let y be Element of L2;
  assume that
A2: x = y and
A3: x is compact;
  x << x by A3,WAYBEL_3:def 2;
  then y << y by A1,A2,Th8;
  hence thesis by WAYBEL_3:def 2;
end;

theorem Th10:
  for L1,L2 be up-complete non empty reflexive antisymmetric
RelStr st the RelStr of L1 = the RelStr of L2 for x be Element of L1 for y be
  Element of L2 st x = y holds compactbelow x = compactbelow y
proof
  let L1,L2 be up-complete non empty reflexive antisymmetric RelStr;
  assume
A1: the RelStr of L1 = the RelStr of L2;
  let x be Element of L1;
  let y be Element of L2;
  assume
A2: x = y;
  now
    let z be object;
    assume
A3: z in compactbelow y;
    then reconsider z2 = z as Element of L2;
    reconsider z1 = z2 as Element of L1 by A1;
    z2 is compact by A3,Th4;
    then
A4: z1 is compact by A1,Th9;
    z2 <= y by A3,Th4;
    then z1 <= x by A1,A2;
    hence z in compactbelow x by A4;
  end;
  then
A5: compactbelow y c= compactbelow x;
  now
    let z be object;
    assume
A6: z in compactbelow x;
    then reconsider z1 = z as Element of L1;
    reconsider z2 = z1 as Element of L2 by A1;
    z1 is compact by A6,Th4;
    then
A7: z2 is compact by A1,Th9;
    z1 <= x by A6,Th4;
    then z2 <= y by A1,A2;
    hence z in compactbelow y by A7;
  end;
  then compactbelow x c= compactbelow y;
  hence thesis by A5,XBOOLE_0:def 10;
end;

theorem
  for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1 is non
  empty holds L2 is non empty;

theorem Th12:
  for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1
  is reflexive holds L2 is reflexive;

theorem Th13:
  for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1
  is transitive holds L2 is transitive;

theorem Th14:
  for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 & L1
  is antisymmetric holds L2 is antisymmetric;

theorem Th15:
  for L1,L2 be non empty reflexive RelStr st the RelStr of L1 =
  the RelStr of L2 & L1 is up-complete holds L2 is up-complete
proof
  let L1,L2 be non empty reflexive RelStr;
  assume that
A1: the RelStr of L1 = the RelStr of L2 and
A2: L1 is up-complete;
  now
    let X be non empty directed Subset of L2;
    reconsider X9 = X as Subset of L1 by A1;
    reconsider X9 as non empty directed Subset of L1 by A1,WAYBEL_0:3;
    consider x9 be Element of L1 such that
A3: x9 is_>=_than X9 and
A4: for y9 be Element of L1 st y9 is_>=_than X9 holds x9 <= y9 by A2,
WAYBEL_0:def 39;
    reconsider x = x9 as Element of L2 by A1;
    take x;
    thus x is_>=_than X by A1,A3,YELLOW_0:2;
    let y be Element of L2 such that
A5: y is_>=_than X;
    reconsider y9 = y as Element of L1 by A1;
    x9 <= y9 by A1,A4,A5,YELLOW_0:2;
    hence x <= y by A1;
  end;
  hence thesis by WAYBEL_0:def 39;
end;

theorem Th16:
  for L1,L2 be up-complete non empty reflexive antisymmetric
RelStr st the RelStr of L1 = the RelStr of L2 & L1 is satisfying_axiom_K & for
  x be Element of L1 holds compactbelow x is non empty directed holds L2 is
  satisfying_axiom_K
proof
  let L1,L2 be up-complete non empty reflexive antisymmetric RelStr;
  assume that
A1: the RelStr of L1 = the RelStr of L2 and
A2: L1 is satisfying_axiom_K and
A3: for x be Element of L1 holds compactbelow x is non empty directed;
  now
    let x be Element of L2;
    reconsider x9 = x as Element of L1 by A1;
    compactbelow x9 is non empty directed by A3;
    then
A4: ex_sup_of compactbelow x9,L1 by WAYBEL_0:75;
    x9 = sup compactbelow x9 & compactbelow x = compactbelow x9 by A1,A2,Th10;
    hence x = sup compactbelow x by A1,A4,YELLOW_0:26;
  end;
  hence thesis;
end;

theorem Th17:
  for L1,L2 be non empty reflexive antisymmetric RelStr st the
  RelStr of L1 = the RelStr of L2 & L1 is algebraic holds L2 is algebraic
proof
  let L1,L2 be non empty reflexive antisymmetric RelStr;
  assume that
A1: the RelStr of L1 = the RelStr of L2 and
A2: L1 is algebraic;
A3: L2 is up-complete by A1,A2,Th15;
A4: for x be Element of L2 holds compactbelow x is non empty directed
  proof
    let x be Element of L2;
    reconsider x9 = x as Element of L1 by A1;
    compactbelow x9 is non empty directed by A2;
    hence thesis by A1,A2,A3,Th10,WAYBEL_0:3;
  end;
  L2 is satisfying_axiom_K by A1,A2,A3,Th16;
  hence thesis by A3,A4;
end;

theorem Th18:
  for L1,L2 be LATTICE st the RelStr of L1 = the RelStr of L2 & L1
  is arithmetic holds L2 is arithmetic
proof
  let L1,L2 be LATTICE;
  assume that
A1: the RelStr of L1 = the RelStr of L2 and
A2: L1 is arithmetic;
A3: L2 is algebraic by A1,A2,Th17;
A4: CompactSublatt L1 is meet-inheriting by A2;
  now
    let x2,y2 be Element of L2;
    reconsider x1 = x2, y1 = y2 as Element of L1 by A1;
    assume that
A5: x2 in the carrier of CompactSublatt L2 and
A6: y2 in the carrier of CompactSublatt L2 and
A7: ex_inf_of {x2,y2},L2;
    x2 is compact by A5,Def1;
    then x1 is compact by A1,A3,Th9;
    then
A8: x1 in the carrier of CompactSublatt L1 by Def1;
    y2 is compact by A6,Def1;
    then y1 is compact by A1,A3,Th9;
    then
A9: y1 in the carrier of CompactSublatt L1 by Def1;
    ex_inf_of {x1,y1},L1 by A1,A7,YELLOW_0:14;
    then inf {x1,y1} in the carrier of CompactSublatt L1 by A4,A8,A9,
YELLOW_0:def 16;
    then
A10: inf {x1,y1} is compact by Def1;
    inf {x1,y1} = inf {x2,y2} by A1,A7,YELLOW_0:27;
    then inf {x2,y2} is compact by A1,A2,A10,Th9;
    hence inf {x2,y2} in the carrier of CompactSublatt L2 by Def1;
  end;
  then CompactSublatt L2 is meet-inheriting by YELLOW_0:def 16;
  hence thesis by A3;
end;

registration
  let L be non empty RelStr;
  cluster the RelStr of L -> non empty;
  coherence;
end;

registration
  let L be non empty reflexive RelStr;
  cluster the RelStr of L -> reflexive;
  coherence by Th12;
end;

registration
  let L be transitive RelStr;
  cluster the RelStr of L -> transitive;
  coherence by Th13;
end;

registration
  let L be antisymmetric RelStr;
  cluster the RelStr of L -> antisymmetric;
  coherence by Th14;
end;

registration
  let L be with_infima RelStr;
  cluster the RelStr of L -> with_infima;
  coherence by YELLOW_7:14;
end;

registration
  let L be with_suprema RelStr;
  cluster the RelStr of L -> with_suprema;
  coherence by YELLOW_7:15;
end;

registration
  let L be up-complete non empty reflexive RelStr;
  cluster the RelStr of L -> up-complete;
  coherence by Th15;
end;

registration
  let L be algebraic non empty reflexive antisymmetric RelStr;
  cluster the RelStr of L -> algebraic;
  coherence by Th17;
end;

registration
  let L be arithmetic LATTICE;
  cluster the RelStr of L -> arithmetic;
  coherence by Th18;
end;

theorem :: PROPOSITION 4.7 a)
  for L be algebraic LATTICE holds L is arithmetic iff CompactSublatt L
  is LATTICE
proof
  let L be algebraic LATTICE;
  thus L is arithmetic implies CompactSublatt L is LATTICE
  proof
    set x = the Element of L;
    assume
A1: L is arithmetic;
    compactbelow x is non empty by Def4;
    then consider z be object such that
A2: z in compactbelow x by XBOOLE_0:def 1;
    ex z9 be Element of L st z9 = z & x >= z9 & z9 is compact by A2;
    then CompactSublatt L is non empty join-inheriting meet-inheriting full
    SubRelStr of L by A1,Def1;
    hence thesis;
  end;
  assume
A3: CompactSublatt L is LATTICE;
  now
    let x,y be Element of L;
    assume that
A4: x in the carrier of CompactSublatt L and
A5: y in the carrier of CompactSublatt L and
    ex_inf_of {x,y},L;
    reconsider L9 = CompactSublatt L as non empty full SubRelStr of L by A4;
    reconsider x9 = x, y9 = y as Element of L9 by A4,A5;
    set X = compactbelow inf {x,y};
    reconsider c = "/\"({x,y},L9) as Element of L by YELLOW_0:58;
A6: inf {x,y} = sup X by Def3;
    X is non empty directed by Def4;
    then
A7: ex_sup_of X,L by WAYBEL_0:75;
A8: ex_inf_of {x9,y9},L9 by A3,YELLOW_0:21;
    then
A9: "/\"({x,y},L9) is_<=_than {x,y} by YELLOW_0:31;
    now
      let z be object;
      assume z in X;
      then consider z1 be Element of L such that
A10:  z = z1 and
A11:  inf {x,y} >= z1 and
A12:  z1 is compact;
A13:  z1 <= x "/\" y by A11,YELLOW_0:40;
      x "/\" y <= y by YELLOW_0:23;
      then z1 <= y by A13,ORDERS_2:3;
      then
A14:  z in compactbelow y by A10,A12;
      x "/\" y <= x by YELLOW_0:23;
      then z1 <= x by A13,ORDERS_2:3;
      then z in compactbelow x by A10,A12;
      hence z in compactbelow x /\ compactbelow y by A14,XBOOLE_0:def 4;
    end;
    then
A15: X c= compactbelow x /\ compactbelow y;
    now
      let b9 be Element of L9;
      reconsider b = b9 as Element of L by YELLOW_0:58;
      assume
A16:  b9 in X;
      then b9 in compactbelow y by A15,XBOOLE_0:def 4;
      then b <= y by Th4;
      then
A17:  b9 <= y9 by YELLOW_0:60;
      b9 in compactbelow x by A15,A16,XBOOLE_0:def 4;
      then b <= x by Th4;
      then b9 <= x9 by YELLOW_0:60;
      then b9 <= x9 "/\" y9 by A8,A17,YELLOW_0:19;
      hence b9 <= "/\"({x,y},L9) by A3,YELLOW_0:40;
    end;
    then
A18: X is_<=_than "/\"({x,y},L9) by LATTICE3:def 9;
    now
      let d be object;
      assume d in X;
      then
      ex d9 be Element of L st d9 = d & inf {x,y} >= d9 & d9 is compact;
      hence d in the carrier of L9 by Def1;
    end;
    then X c= the carrier of L9;
    then X is_<=_than c by A18,YELLOW_0:62;
    then
A19: sup X <= c by A7,YELLOW_0:30;
    y9 in {x,y} by TARSKI:def 2;
    then "/\"({x,y},L9) <= y9 by A9,LATTICE3:def 8;
    then
A20: c <= y by YELLOW_0:59;
    x9 in {x,y} by TARSKI:def 2;
    then "/\"({x,y},L9) <= x9 by A9,LATTICE3:def 8;
    then c <= x by YELLOW_0:59;
    then c <= x "/\" y by A20,YELLOW_0:23;
    then c <= sup X by A6,YELLOW_0:40;
    then c = sup X by A19,ORDERS_2:2;
    hence inf {x,y} in the carrier of CompactSublatt L by A6;
  end;
  then CompactSublatt L is meet-inheriting by YELLOW_0:def 16;
  hence thesis;
end;

theorem Th20: :: PROPOSITION 4.7 b)
  for L be algebraic lower-bounded LATTICE holds L is arithmetic
  iff L-waybelow is multiplicative
proof
  let L be algebraic lower-bounded LATTICE;
  thus L is arithmetic implies L-waybelow is multiplicative
  proof
    assume
A1: L is arithmetic;
    now
      reconsider C = CompactSublatt L as meet-inheriting non empty full
      SubRelStr of L by A1;
      let a,x,y be Element of L;
      assume that
A2:   [a,x] in L-waybelow and
A3:   [a,y] in L-waybelow;
      a << x by A2,WAYBEL_4:def 1;
      then consider c be Element of L such that
A4:   c in the carrier of CompactSublatt L and
A5:   a <= c and
A6:   c <= x by Th7;
      a << y by A3,WAYBEL_4:def 1;
      then consider k be Element of L such that
A7:   k in the carrier of CompactSublatt L and
A8:   a <= k and
A9:   k <= y by Th7;
A10:  c"/\"k <= x"/\"y by A6,A9,YELLOW_3:2;
      reconsider c9=c, k9=k as Element of C by A4,A7;
      c9"/\"k9 in the carrier of CompactSublatt L;
      then c"/\"k in the carrier of CompactSublatt L by YELLOW_0:69;
      then c"/\"k is compact by Def1;
      then
A11:  c"/\"k << c"/\"k by WAYBEL_3:def 2;
      a"/\"a = a by YELLOW_5:2;
      then a <= c"/\"k by A5,A8,YELLOW_3:2;
      then a << x"/\"y by A10,A11,WAYBEL_3:2;
      hence [a,x"/\"y] in L-waybelow by WAYBEL_4:def 1;
    end;
    hence thesis by WAYBEL_7:def 7;
  end;
  assume
A12: L-waybelow is multiplicative;
  now
    let x,y be Element of L;
    assume that
A13: x in the carrier of CompactSublatt L and
A14: y in the carrier of CompactSublatt L and
    ex_inf_of {x,y},L;
    y is compact by A14,Def1;
    then y << y by WAYBEL_3:def 2;
    then
A15: [y,y] in L-waybelow by WAYBEL_4:def 1;
    x is compact by A13,Def1;
    then x << x by WAYBEL_3:def 2;
    then [x,x] in L-waybelow by WAYBEL_4:def 1;
    then [x "/\" y,x "/\" y] in L-waybelow by A12,A15,WAYBEL_7:41;
    then x "/\" y << x "/\" y by WAYBEL_4:def 1;
    then x "/\" y is compact by WAYBEL_3:def 2;
    then x "/\" y in the carrier of CompactSublatt L by Def1;
    hence inf {x,y} in the carrier of CompactSublatt L by YELLOW_0:40;
  end;
  then CompactSublatt L is meet-inheriting by YELLOW_0:def 16;
  hence thesis;
end;

theorem :: COROLLARY 4.8.a)
  for L be arithmetic lower-bounded LATTICE, p be Element of L holds p
  is pseudoprime implies p is prime
proof
  let L be arithmetic lower-bounded LATTICE;
  let p be Element of L;
  L-waybelow is multiplicative by Th20;
  hence thesis by WAYBEL_7:45;
end;

theorem :: COROLLARY 4.8.b)
  for L be algebraic distributive lower-bounded LATTICE st for p being
  Element of L st p is pseudoprime holds p is prime holds L is arithmetic
proof
  let L be algebraic distributive lower-bounded LATTICE;
  assume for p be Element of L st p is pseudoprime holds p is prime;
  then L-waybelow is multiplicative by WAYBEL_7:46;
  hence thesis by Th20;
end;

registration
  let L be algebraic LATTICE;
  let c be closure Function of L,L;
  cluster non empty directed for Subset of Image c;
  existence
  proof
    set x = the Element of Image c;
    take downarrow x;
    thus thesis;
  end;
end;

theorem Th23:
  for L be algebraic LATTICE for c be closure Function of L,L st c
is directed-sups-preserving holds c.:([#]CompactSublatt L) c= [#]CompactSublatt
  Image c
proof
  let L be algebraic LATTICE;
  let c be closure Function of L,L;
  assume
A1: c is directed-sups-preserving;
  let x be object;
A2: c is idempotent monotone by WAYBEL_1:def 13;
  assume x in c.:([#]CompactSublatt L);
  then consider y be object such that
A3: y in dom c and
A4: y in [#]CompactSublatt L and
A5: x = c.y by FUNCT_1:def 6;
A6: x in rng c by A3,A5,FUNCT_1:def 3;
  then reconsider x9 = x as Element of Image c by YELLOW_0:def 15;
  reconsider x1 = x9 as Element of L by A6;
  reconsider y9 = y as Element of L by A3;
  y9 is compact by A4,Def1;
  then
A7: y9 << y9 by WAYBEL_3:def 2;
  now
    id(L) <= c by WAYBEL_1:def 14;
    then id(L).y9 <= c.y9 by YELLOW_2:9;
    then
A8: y9 <= x1 by A5,FUNCT_1:18;
    let D be non empty directed Subset of Image c;
    assume
A9: x9 <= sup D;
    D c= the carrier of Image c;
    then
A10: D c= rng c by YELLOW_0:def 15;
    then reconsider D9 = D as non empty (Subset of L) by XBOOLE_1:1;
    reconsider D9 as non empty directed (Subset of L) by YELLOW_2:7;
A11: ex_sup_of D9,L by WAYBEL_0:75;
    c preserves_sup_of D9 by A1,WAYBEL_0:def 37;
    then
A12: c.sup D9 = sup (c.:D9) by A11,WAYBEL_0:def 31
      .= sup D9 by A2,A10,YELLOW_2:20;
    c.sup D9 = sup D by A11,WAYBEL_1:55;
    then x1 <= sup D9 by A9,A12,YELLOW_0:59;
    then y9 <= sup D9 by A8,ORDERS_2:3;
    then consider d9 be Element of L such that
A13: d9 in D9 and
A14: y9 <= d9 by A7,WAYBEL_3:def 1;
    reconsider d = d9 as Element of Image c by A13;
    take d;
    thus d in D by A13;
    d in the carrier of Image c;
    then d in rng c by YELLOW_0:def 15;
    then d9 in {z where z is Element of L: z = c.z} by A2,YELLOW_2:19;
    then
A15: ex z9 be Element of L st d9 = z9 & z9 = c.z9;
    c.y9 <= c.d9 by A2,A14,WAYBEL_1:def 2;
    hence x9 <= d by A5,A15,YELLOW_0:60;
  end;
  then x9 << x9 by WAYBEL_3:def 1;
  then x9 is compact by WAYBEL_3:def 2;
  hence thesis by Def1;
end;

theorem :: PROPOSITION 4.9.(i)
  for L be algebraic lower-bounded LATTICE for c be closure Function of
  L,L st c is directed-sups-preserving holds Image c is algebraic LATTICE
proof
  let L be algebraic lower-bounded LATTICE;
  let c be closure Function of L,L;
  assume
A1: c is directed-sups-preserving;
  c is idempotent by WAYBEL_1:def 13;
  then reconsider Imc = Image c as complete LATTICE by A1,YELLOW_2:35;
A2: now
    let x be Element of Imc;
    now
      let y,z be Element of Imc;
      assume that
A3:   y in compactbelow x and
A4:   z in compactbelow x;
      y is compact by A3,Th4;
      then
A5:   y << y by WAYBEL_3:def 2;
      z is compact by A4,Th4;
      then
A6:   z << z by WAYBEL_3:def 2;
      take v = y "\/" z;
      z <= v by YELLOW_0:22;
      then
A7:   z << v by A6,WAYBEL_3:2;
      y <= v by YELLOW_0:22;
      then y << v by A5,WAYBEL_3:2;
      then v << v by A7,WAYBEL_3:3;
      then
A8:   v is compact by WAYBEL_3:def 2;
      y <= x & z <= x by A3,A4,Th4;
      then v <= x by YELLOW_0:22;
      hence v in compactbelow x & y <= v & z <= v by A8,YELLOW_0:22;
    end;
    hence compactbelow x is non empty directed by WAYBEL_0:def 1;
  end;
  now
    let x be Element of Imc;
    consider y be Element of L such that
A9: c.y = x by YELLOW_2:10;
    sup compactbelow y in the carrier of L;
    then
A10: sup compactbelow y in dom c by FUNCT_2:def 1;
    compactbelow y is non empty directed by Def4;
    then
A11: c preserves_sup_of compactbelow y & ex_sup_of compactbelow y,L by A1,
WAYBEL_0:75,def 37;
    then c.sup compactbelow y = sup (c.:(compactbelow y)) by WAYBEL_0:def 31;
    then sup (c.:(compactbelow y)) in rng c by A10,FUNCT_1:def 3;
    then
A12: ex_sup_of (c.:(compactbelow y)),L & sup (c.:(compactbelow y)) in the
    carrier of Image c by YELLOW_0:17,def 15;
    for b be Element of Imc st b in compactbelow x holds b <= x by Th4;
    then x is_>=_than compactbelow x by LATTICE3:def 9;
    then
A13: sup compactbelow x <= x by YELLOW_0:32;
A14: c.:([#]CompactSublatt L) c= [#]CompactSublatt Image c by A1,Th23;
A15: c is monotone by A1,YELLOW_2:16;
    compactbelow y = downarrow y /\ [#]CompactSublatt L by Th5;
    then
A16: c.:(compactbelow y) c= c.:(downarrow y) /\ c.: ([#]CompactSublatt L)
    by RELAT_1:121;
    now
      let z be object;
      assume
A17:  z in c.:(compactbelow y);
      then consider v be object such that
A18:  v in dom c and
A19:  v in compactbelow y and
A20:  z = c.v by FUNCT_1:def 6;
      z in rng c by A18,A20,FUNCT_1:def 3;
      then reconsider z1 = z as Element of Imc by YELLOW_0:def 15;
      reconsider v as Element of L by A18;
      v <= y by A19,Th4;
      then c.v <= c.y by A15,WAYBEL_1:def 2;
      then
A21:  z1 <= x by A9,A20,YELLOW_0:60;
      z in c.:([#]CompactSublatt L) by A16,A17,XBOOLE_0:def 4;
      then z1 is compact by A14,Def1;
      hence z in compactbelow x by A21;
    end;
    then
A22: c.:(compactbelow y) c= compactbelow x;
    compactbelow x is directed by A2;
    then
A23: ex_sup_of compactbelow x,Imc by WAYBEL_0:75;
    c.:(compactbelow y) c= rng c by RELAT_1:111;
    then c.:(compactbelow y) is Subset of Imc by YELLOW_0:def 15;
    then
A24: ex_sup_of c.:(compactbelow y),Imc & sup (c.:(compactbelow y)) = "\/"(
    c.:( compactbelow y),Imc) by A12,YELLOW_0:64;
    c.y = c.sup compactbelow y by Def3
      .= sup (c.:(compactbelow y)) by A11,WAYBEL_0:def 31;
    then x <= sup compactbelow x by A9,A23,A24,A22,YELLOW_0:34;
    hence x = sup compactbelow x by A13,ORDERS_2:2;
  end;
  then Imc is satisfying_axiom_K;
  hence thesis by A2,Def4;
end;

theorem :: PROPOSITION 4.9.(ii)
  for L be algebraic lower-bounded LATTICE, c be closure Function of L,L
  st c is directed-sups-preserving holds c.:([#]CompactSublatt L) = [#]
  CompactSublatt Image c
proof
  let L be algebraic lower-bounded LATTICE;
  let c be closure Function of L,L;
  assume
A1: c is directed-sups-preserving;
  now
    c is idempotent by WAYBEL_1:def 13;
    then
A2: rng c = {x where x is Element of L: x = c.x} by YELLOW_2:19;
    c is idempotent by WAYBEL_1:def 13;
    then reconsider Imc = Image c as complete LATTICE by A1,YELLOW_2:35;
    let a9 be object;
    assume
A3: a9 in [#]CompactSublatt Image c;
A4: the carrier of CompactSublatt Imc c= the carrier of Imc by YELLOW_0:def 13;
    then reconsider a = a9 as Element of Imc by A3;
    a is compact by A3,Def1;
    then
A5: a << a by WAYBEL_3:def 2;
    a9 in the carrier of Imc by A3,A4;
    then a in rng c by YELLOW_0:def 15;
    then consider a1 be Element of L such that
A6: a = a1 and
A7: a1 = c.a1 by A2;
    compactbelow a1 is non empty directed Subset of L by Def4;
    then
A8: c preserves_sup_of compactbelow a1 & ex_sup_of compactbelow a1,L by A1,
WAYBEL_0:75,def 37;
A9: c is monotone by A1,YELLOW_2:16;
    now
      let z be object;
      assume z in c.:(compactbelow a1);
      then consider v be object such that
A10:  v in dom c and
A11:  v in compactbelow a1 and
A12:  z = c.v by FUNCT_1:def 6;
      reconsider v9 = v as Element of L by A11;
A13:  v in downarrow a1 /\ the carrier of CompactSublatt L by A11,Th5;
      then v in downarrow a1 by XBOOLE_0:def 4;
      then v9 <= a1 by WAYBEL_0:17;
      then c.v9 <= a1 by A7,A9,WAYBEL_1:def 2;
      then
A14:  z in (downarrow a1) by A12,WAYBEL_0:17;
      v in [#]CompactSublatt L by A13,XBOOLE_0:def 4;
      then z in c.:([#]CompactSublatt L) by A10,A12,FUNCT_1:def 6;
      hence z in (downarrow a1) /\ (c.:([#]CompactSublatt L)) by A14,
XBOOLE_0:def 4;
    end;
    then
A15: c.:(compactbelow a1) c= (downarrow a1) /\ (c.:([#] CompactSublatt L));
    a = sup compactbelow a1 by A6,Def3;
    then
A16: a = sup (c.:(compactbelow a1)) by A6,A7,A8,WAYBEL_0:def 31;
    c.:(compactbelow a1) c= rng c by RELAT_1:111;
    then
A17: c.:(compactbelow a1) c= the carrier of Imc by YELLOW_0:def 15;
A18: downarrow a /\ c.:([#]CompactSublatt L) is non empty directed Subset
    of Imc
    proof
      (c.:[#]CompactSublatt L) /\ downarrow a is Subset of Imc;
      then reconsider
      D = downarrow a /\ c.:[#]CompactSublatt L as Subset of Imc;
A19:  Bottom Imc <= a by YELLOW_0:44;
A20:  now
        let x,y be Element of Imc;
        assume that
A21:    x in D and
A22:    y in D;
        x in c.:([#]CompactSublatt L) by A21,XBOOLE_0:def 4;
        then consider d be object such that
A23:    d in dom c and
A24:    d in [#]CompactSublatt L and
A25:    x = c.d by FUNCT_1:def 6;
        y in c.: ([#]CompactSublatt L) by A22,XBOOLE_0:def 4;
        then consider e be object such that
A26:    e in dom c and
A27:    e in [#]CompactSublatt L and
A28:    y = c.e by FUNCT_1:def 6;
        reconsider e as Element of L by A26;
        y in downarrow a by A22,XBOOLE_0:def 4;
        then y <= a by WAYBEL_0:17;
        then
A29:    c.e <= a1 by A6,A28,YELLOW_0:59;
        reconsider d as Element of L by A23;
A30:    d <= d "\/" e by YELLOW_0:22;
        x in downarrow a by A21,XBOOLE_0:def 4;
        then x <= a by WAYBEL_0:17;
        then c.d <= a1 by A6,A25,YELLOW_0:59;
        then
A31:    c.d "\/" c.e <= a1 by A29,YELLOW_0:22;
        d "\/" e in the carrier of L;
        then d "\/" e in dom c by FUNCT_2:def 1;
        then c.(d "\/" e) in rng c by FUNCT_1:def 3;
        then reconsider z = c.(d "\/" e) as Element of Imc by YELLOW_0:def 15;
        take z;
A32:    id(L) <= c by WAYBEL_1:def 14;
        then id(L).e <= c.e by YELLOW_2:9;
        then
A33:    e <= c.e by FUNCT_1:18;
        id(L).d <= c.d by A32,YELLOW_2:9;
        then d <= c.d by FUNCT_1:18;
        then d "\/" e <= c.d "\/" c.e by A33,YELLOW_3:3;
        then d "\/" e <= a1 by A31,ORDERS_2:3;
        then c.(d "\/" e) <= a1 by A7,A9,WAYBEL_1:def 2;
        then z <= a by A6,YELLOW_0:60;
        then
A34:    z in downarrow a by WAYBEL_0:17;
A35:    e <= d "\/" e by YELLOW_0:22;
        then
A36:    c.e <= c.(d "\/" e) by A9,WAYBEL_1:def 2;
        e is compact by A27,Def1;
        then e << e by WAYBEL_3:def 2;
        then
A37:    e << d "\/" e by A35,WAYBEL_3:2;
        d is compact by A24,Def1;
        then d << d by WAYBEL_3:def 2;
        then d << d "\/" e by A30,WAYBEL_3:2;
        then d "\/" e << d "\/" e by A37,WAYBEL_3:3;
        then d "\/" e is compact by WAYBEL_3:def 2;
        then
A38:    d "\/" e in [#]CompactSublatt L by Def1;
        d "\/" e in the carrier of L;
        then d "\/" e in dom c by FUNCT_2:def 1;
        then z in c.:([#]CompactSublatt L) by A38,FUNCT_1:def 6;
        hence z in D by A34,XBOOLE_0:def 4;
        c.d <= c.(d "\/" e) by A9,A30,WAYBEL_1:def 2;
        hence x <= z & y <= z by A25,A28,A36,YELLOW_0:60;
      end;
      Bottom L is compact by WAYBEL_3:15;
      then dom c = the carrier of L & Bottom L in [#]CompactSublatt L by Def1,
FUNCT_2:def 1;
      then
A39:  c.Bottom L in c.:([#]CompactSublatt L) by FUNCT_1:def 6;
A40:  ex_sup_of {},L & {} c= the carrier of L by YELLOW_0:42;
A41:  {} c= the carrier of Imc;
      c.Bottom L = c."\/"({},L) by YELLOW_0:def 11
        .= "\/"({},Imc) by A40,A41,WAYBEL_1:55
        .= Bottom Imc by YELLOW_0:def 11;
      then c.Bottom L in downarrow a by A19,WAYBEL_0:17;
      hence thesis by A39,A20,WAYBEL_0:def 1,XBOOLE_0:def 4;
    end;
A42: c.:([#]CompactSublatt L) c= rng c by RELAT_1:111;
    now
      let z be object;
      assume
A43:  z in (downarrow a1) /\ (c.:([#]CompactSublatt L));
      then reconsider z1 = z as Element of L;
A44:  z in c.:([#] CompactSublatt L) by A43,XBOOLE_0:def 4;
      then reconsider z2 = z1 as Element of Imc by A42,YELLOW_0:def 15;
      z in downarrow a1 by A43,XBOOLE_0:def 4;
      then z1 <= a1 by WAYBEL_0:17;
      then z2 <= a by A6,YELLOW_0:60;
      then z in (downarrow a) by WAYBEL_0:17;
      hence z in (downarrow a) /\ (c.: ([#]CompactSublatt L)) by A44,
XBOOLE_0:def 4;
    end;
    then
A45: (downarrow a1) /\ (c.:([#]CompactSublatt L)) c= (downarrow a) /\ (c
    .: ([#]CompactSublatt L));
    ex_sup_of c.:(compactbelow a1),L by A8,WAYBEL_0:def 31;
    then
A46: a = "\/"(c.:(compactbelow a1),Imc) by A6,A7,A17,A16,WAYBEL_1:55;
    ex_sup_of c.:(compactbelow a1),Imc & ex_sup_of (downarrow a) /\ (c.:(
    [#] CompactSublatt L)),Imc by YELLOW_0:17;
    then a <= "\/"((downarrow a) /\ (c.:([#]CompactSublatt L)),Imc) by A46,A15
,A45,XBOOLE_1:1,YELLOW_0:34;
    then consider k be Element of Imc such that
A47: k in ((downarrow a) /\ (c.:([#]CompactSublatt L))) and
A48: a <= k by A5,A18,WAYBEL_3:def 1;
    k in downarrow a by A47,XBOOLE_0:def 4;
    then
A49: k <= a by WAYBEL_0:17;
    k in c.:([#]CompactSublatt L) by A47,XBOOLE_0:def 4;
    hence a9 in c.:([#]CompactSublatt L) by A48,A49,ORDERS_2:2;
  end;
  then
A50: [#]CompactSublatt Image c c= c.:([#]CompactSublatt L);
  c.:([#]CompactSublatt L) c= [#]CompactSublatt Image c by A1,Th23;
  hence thesis by A50,XBOOLE_0:def 10;
end;

begin :: Boolean Posets as Algebraic Lattices

theorem Th26:
  for X,x be set holds x is Element of BoolePoset X iff x c= X
proof
  let X,x be set;
  LattPOSet BooleLatt X = RelStr(#the carrier of BooleLatt X, LattRel (
    BooleLatt X)#) by LATTICE3:def 2;
  then
A1: the carrier of BoolePoset X = the carrier of BooleLatt X by YELLOW_1:def 2
    .= bool X by LATTICE3:def 1;
  hence x is Element of BoolePoset X implies x c= X;
  thus thesis by A1;
end;

theorem Th27:
  for X be set for x,y be Element of BoolePoset X holds x << y iff
for Y be Subset-Family of X st y c= union Y ex Z be finite Subset of Y st x c=
  union Z
proof
  let X be set;
  let x,y be Element of BoolePoset X;
  LattPOSet BooleLatt X = RelStr(#the carrier of BooleLatt X, LattRel (
    BooleLatt X)#) by LATTICE3:def 2;
  then
A1: the carrier of BoolePoset X = the carrier of BooleLatt X by YELLOW_1:def 2
    .= bool X by LATTICE3:def 1;
  thus x << y implies for Y be Subset-Family of X st y c= union Y ex Z be
  finite Subset of Y st x c= union Z
  proof
    assume
A2: x << y;
    let Y be Subset-Family of X;
    reconsider Y9 = Y as Subset of BoolePoset X by A1;
    assume y c= union Y;
    then y c= sup Y9 by YELLOW_1:21;
    then y <= sup Y9 by YELLOW_1:2;
    then consider Z be finite Subset of BoolePoset X such that
A3: Z c= Y and
A4: x <= sup Z by A2,WAYBEL_3:18;
    reconsider Z9 = Z as finite Subset of Y by A3;
    take Z9;
    x c= sup Z by A4,YELLOW_1:2;
    hence thesis by YELLOW_1:21;
  end;
  thus (for Y be Subset-Family of X st y c= union Y ex Z be finite Subset of Y
  st x c= union Z) implies x << y
  proof
    assume
A5: for Y be Subset-Family of X st y c= union Y ex Z be finite Subset
    of Y st x c= union Z;
    now
      let Y be Subset of BoolePoset X;
      reconsider Y9 = Y as Subset-Family of X by A1;
      assume y <= sup Y;
      then y c= sup Y by YELLOW_1:2;
      then y c= union Y9 by YELLOW_1:21;
      then consider Z9 be finite Subset of Y9 such that
A6:   x c= union Z9 by A5;
      reconsider Z = Z9 as finite Subset of BoolePoset X by XBOOLE_1:1;
      take Z;
      thus Z c= Y;
      x c= sup Z by A6,YELLOW_1:21;
      hence x <= sup Z by YELLOW_1:2;
    end;
    hence thesis by WAYBEL_3:19;
  end;
end;

theorem Th28:
  for X be set for x be Element of BoolePoset X holds x is finite
  iff x is compact
proof
  let X be set;
  let x be Element of BoolePoset X;
  per cases;
  suppose
A1: x is empty;
    then x = Bottom BoolePoset X by YELLOW_1:18;
    hence thesis by A1,WAYBEL_3:15;
  end;
  suppose
A2: x is non empty;
    thus x is finite implies x is compact
    proof
      assume
A3:   x is finite;
      now
        defpred P[object,object] means ex A being set st A = $2 & $1 in A;
        let Y be Subset-Family of X;
        assume
A4:     x c= union Y;
A5:     for e be object st e in x ex u be object st u in Y & P[e,u]
        proof
          let e be object;
          assume e in x;
          then ex u be set st e in u & u in Y by A4,TARSKI:def 4;
          hence thesis;
        end;
        consider f be Function such that
A6:     dom f = x and
A7:     rng f c= Y and
A8:     for e be object st e in x holds P[e,f.e] from FUNCT_1:sch 6(A5);
        reconsider Z = rng f as Subset of Y by A7;
        reconsider Z as finite Subset of Y by A3,A6,FINSET_1:8;
        take Z;
        now
          let z be object;
          assume
A9:         z in x;
          then P[z,f.z] by A8;
          then z in f.z & f.z in Z by A6,FUNCT_1:def 3,A9;
          hence z in union Z by TARSKI:def 4;
        end;
        hence x c= union Z;
      end;
      then x << x by Th27;
      hence thesis by WAYBEL_3:def 2;
    end;
    thus x is compact implies x is finite
    proof
      reconsider x9 = x as non empty set by A2;
      set Y = the set of all  {y} where y is Element of x9 ;
      Y c= bool X
      proof
        let t be object;
         reconsider tt=t as set by TARSKI:1;
        assume t in Y;
        then
A10:     ex y9 be Element of x9 st t = {y9};
        for k being object st k in tt holds k in X by A10,Th26,TARSKI:def 3;
        then tt c= X;
        hence thesis;
      end;
      then reconsider Y as Subset-Family of X;
      now
        let y be object;
        assume y in x;
        then
A11:    {y} in Y;
        y in {y} by TARSKI:def 1;
        hence y in union Y by A11,TARSKI:def 4;
      end;
      then
A12:  x c= union Y;
      assume x is compact;
      then x << x by WAYBEL_3:def 2;
      then consider Z be finite Subset of Y such that
A13:  x c= union Z by A12,Th27;
      now
        let k be set;
        assume k in Z;
        then k in Y;
        then ex y9 be Element of x9 st k = {y9};
        hence k is finite;
      end;
      then union Z is finite by FINSET_1:7;
      hence thesis by A13;
    end;
  end;
end;

theorem Th29:
  for X be set for x be Element of BoolePoset X holds compactbelow
  x = the set of all y where y is finite Subset of x
proof
  let X be set;
  let x be Element of BoolePoset X;
  now
    let z be object;
    assume z in the set of all y where y is finite Subset of x ;
    then consider z9 be finite Subset of x such that
A1: z9 = z;
    x c= X by Th26;
    then z9 c= X;
    then reconsider z1 = z9 as Element of BoolePoset X by Th26;
    z1 is compact & z1 <= x by Th28,YELLOW_1:2;
    hence z in compactbelow x by A1;
  end;
  then
A2: the set of all y where y is finite Subset of x  c= compactbelow x;
  now
    let z be object;
    assume z in compactbelow x;
    then consider z9 be Element of BoolePoset X such that
A3: z9 = z and
A4: x >= z9 & z9 is compact;
    z9 is finite & z9 c= x by A4,Th28,YELLOW_1:2;
    hence z in the set of all y where y is finite Subset of x  by A3;
  end;
  then
  compactbelow x c= the set of all y where y is finite Subset of x ;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  for X be set for F be Subset of X holds F in the carrier of
  CompactSublatt BoolePoset X iff F is finite
proof
  let X be set;
  let F be Subset of X;
  reconsider F9 = F as Element of BoolePoset X by Th26;
A1: F c= F;
  thus F in the carrier of CompactSublatt BoolePoset X implies F is finite
  proof
    assume
A2: F in the carrier of CompactSublatt BoolePoset X;
    the carrier of CompactSublatt BoolePoset X c= the carrier of
    BoolePoset X by YELLOW_0:def 13;
    then reconsider F9 = F as Element of BoolePoset X by A2;
    F9 <= F9 & F9 is compact by A2,Def1;
    then F9 in compactbelow F9;
    then F9 in the set of all y where y is finite Subset of F9  by Th29;
    then ex F1 be finite Subset of F9 st F1 = F9;
    hence thesis;
  end;
  assume F is finite;
  then F in the set of all y where y is finite Subset of F9  by A1;
  then F9 in compactbelow F9 by Th29;
  then F9 is compact by Th4;
  hence thesis by Def1;
end;

registration
  let X be set;
  let x be Element of BoolePoset X;
  cluster compactbelow x -> lower directed;
  coherence
  proof
    now
      let a,b be set;
      assume that
A1:   a c= b and
A2:   b in compactbelow x;
      b in the set of all y where y is finite Subset of x  by A2,Th29;
      then ex b1 be finite Subset of x st b = b1;
      then a is finite Subset of x by A1,XBOOLE_1:1;
      then a in the set of all y where y is finite Subset of x ;
      hence a in compactbelow x by Th29;
    end;
    hence
A3: compactbelow x is lower by WAYBEL_7:6;
    now
      let a,b be set;
      assume that
A4:   a in compactbelow x and
A5:   b in compactbelow x;
      b in the set of all y where y is finite Subset of x  by A5,Th29;
      then
A6:   ex b1 be finite Subset of x st b = b1;
      a in the set of all y where y is finite Subset of x  by A4,Th29;
      then ex a1 be finite Subset of x st a = a1;
      then a \/ b is finite Subset of x by A6,XBOOLE_1:8;
      then a \/ b in the set of all y where y is finite Subset of x ;
      hence a \/ b in compactbelow x by Th29;
    end;
    hence thesis by A3,WAYBEL_7:8;
  end;
end;

theorem Th31: :: EXAMPLES 4.11.(1b)
  for X be set holds BoolePoset X is algebraic
proof
  let X be set;
  now
    let x be Element of BoolePoset X;
A1: now
      let a be Element of BoolePoset X;
      assume
A2:   a is_>=_than compactbelow x;
      now
        let t be object;
        assume
A3:     t in x;
A4:     x c= X by Th26;
        now
          let k be object;
          assume k in {t};
          then k = t by TARSKI:def 1;
          hence k in X by A3,A4;
        end;
        then {t} c= X;
        then reconsider t1 = {t} as Element of BoolePoset X by Th26;
        for k be object st k in {t} holds k in x by A3,TARSKI:def 1;
        then {t} is finite Subset of x by TARSKI:def 3;
        then {t} in the set of all y where y is finite Subset of x ;
        then {t} in compactbelow x by Th29;
        then t1 <= a by A2,LATTICE3:def 9;
        then t in {t} & {t} c= a by TARSKI:def 1,YELLOW_1:2;
        hence t in a;
      end;
      then x c= a;
      hence x <= a by YELLOW_1:2;
    end;
    for b be Element of BoolePoset X st b in compactbelow x holds b <= x
    by Th4;
    then x is_>=_than compactbelow x by LATTICE3:def 9;
    hence x = sup compactbelow x by A1,YELLOW_0:32;
  end;
  then ( for x be Element of BoolePoset X holds compactbelow x is non empty
  directed)& BoolePoset X is satisfying_axiom_K;
  hence thesis;
end;

registration
  let X be set;
  cluster BoolePoset X -> algebraic;
  coherence by Th31;
end;