The Mizar article:

Representation Theorem for Finite Distributive Lattices

by
Marek Dudzicz

Received January 6, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: LATTICE7
[ MML identifier index ]


environ

 vocabulary WAYBEL_0, ORDERS_1, LATTICES, FINSET_1, TREES_1, CARD_1, BOOLE,
      RELAT_2, LATTICE3, SQUARE_1, ORDINAL2, YELLOW_0, PRE_TOPC, YELLOW_1,
      CAT_1, FUNCT_1, PBOOLE, RELAT_1, WELLORD1, COHSP_1, LATTICE7;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
      FUNCT_2, PRE_TOPC, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2,
      YELLOW_4, WAYBEL_1, GROUP_1, WAYBEL_0, CARD_1, XREAL_0, NAT_1, RELAT_2,
      PBOOLE, COHSP_1;
 constructors YELLOW_4, ORDERS_3, WAYBEL_1, YELLOW_3, GROUP_6, NAT_1, COHSP_1,
      MEMBERED, PRE_TOPC;
 clusters STRUCT_0, LATTICE3, YELLOW_0, ORDERS_1, YELLOW_1, WAYBEL_2, WAYBEL11,
      YELLOW11, YELLOW13, SUBSET_1, RELSET_1, ARYTM_3, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, WAYBEL_0, WAYBEL_1, LATTICE3, RELAT_2, COHSP_1, XBOOLE_0;
 theorems WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_0, YELLOW_1, YELLOW_4, LATTICE3,
      TARSKI, FUNCT_1, FUNCT_2, ORDERS_1, WAYBEL_4, CARD_1, CARD_2, NAT_1,
      AXIOMS, YELLOW_5, REAL_1, PBOOLE, COHSP_1, WAYBEL13, WAYBEL_6, RELSET_1,
      XBOOLE_0, XBOOLE_1;
 schemes NAT_1, PRALG_2;

begin :: Induction in a finite lattice

definition
 let L be 1-sorted;
 let A,B be Subset of L;
 redefine pred A c= B means
    for x be Element of L st x in A holds x in B;
   compatibility
    proof
     thus A c= B iff (for x be Element of L st x in A holds x in B)
      proof
       thus A c= B implies (for x be Element of L st x in A holds x in B);
          (for x be Element of L st x in A holds x in B) implies A c= B
         proof
          assume A1: for x be Element of L st x in A holds x in B;
           thus A c= B
            proof
             let x be set;
             assume  x in A;
             hence x in B by A1;
            end;
         end;
       hence thesis;
      end;
    end;
end;

definition
let L be LATTICE;
cluster non empty Chain of L;
existence
 proof
    {Bottom L} is Chain of L by ORDERS_1:35;
  hence thesis;
 end;
end;

definition
let L be LATTICE;
let x,y be Element of L such that A1: x <= y;
mode Chain of x,y -> non empty Chain of L means :Def2:
 x in it & y in it & for z be Element of L st z in it holds x <= z & z <= y;
existence
proof
     reconsider A={x,y} as non empty Chain of L by A1,ORDERS_1:36;
A2:  y in A by TARSKI:def 2;
A3:  x in A by TARSKI:def 2;
    for z be Element of L st z in A holds x <= z & z <= y
      proof
      let z be Element of L;
       assume A4: z in A;
       per cases by A4,TARSKI:def 2;
        suppose z=x;
         hence thesis by A1;
        suppose z=y;
         hence thesis by A1;
      end;
     hence thesis by A2,A3;
 end;
end;

theorem Th1:
for L be LATTICE
 for x,y be Element of L holds
  x <= y implies {x,y} is Chain of x,y
   proof
    let L be LATTICE;
    let x,y be Element of L;
     assume A1: x <= y;
then A2:   {x,y} is Chain of L by ORDERS_1:36;
A3:  x in {x,y} by TARSKI:def 2;
A4:  y in {x,y} by TARSKI:def 2;
       for z be Element of L st z in {x,y} holds x <= z & z <= y
      proof
      let z be Element of L;
       assume A5: z in {x,y};
       per cases by A5,TARSKI:def 2;
        suppose z=x;
         hence thesis by A1;
        suppose z=y;
         hence thesis by A1;
      end;
     hence thesis by A1,A2,A3,A4,Def2;
    end;

reserve n,k for Nat;

definition
let L be finite LATTICE;
let x be Element of L;
func height(x) -> Nat means :Def3:
 (ex A be Chain of Bottom L,x st it= card A) &
  for A be Chain of Bottom L,x holds card A <= it;

existence
proof

 defpred
  P[Nat] means ex A be Chain of Bottom L,x st $1=card A;

   Bottom L <= x by YELLOW_0:44;
 then A1: {Bottom L,x} is Chain of Bottom L,x by Th1;
   ex k st P[k] & for n st P[n] holds n <= k
   proof
    A2: for k st P[k] holds k <= card the carrier of L by CARD_1:80;
    A3: ex k st P[k]
     proof
        P[card{Bottom L,x}] by A1;
      hence thesis;
     end;
    thus thesis from Max (A2,A3);
   end;
 then consider k such that A4: P[k] & for n st P[n] holds n <= k;
 take k;
 thus P[k] by A4;
 let A be Chain of Bottom L,x;
 thus thesis by A4;
end;

uniqueness
 proof
 let a,b be Nat such that
  A5: (ex A be Chain of Bottom L,x st a= card A) and
  A6:  (for A be Chain of Bottom L,x holds card A <= a) and
  A7: (ex B be Chain of Bottom L,x st b= card B) and
  A8: (for A be Chain of Bottom L,x holds card A <= b);
  consider A be Chain of Bottom L,x such that A9: a= card A &
   (for A be Chain of Bottom L,x holds card A <= a) by A5,A6;
  consider B be Chain of Bottom L,x such that A10: b= card B &
   (for A be Chain of Bottom L,x holds card A <= b) by A7,A8;
  A11: a<=b by A9,A10;
    b<=a by A9,A10;
  hence thesis by A11,AXIOMS:21;
 end;
end;

theorem Th2:
for L be finite LATTICE
 for a,b be Element of L holds
  a < b implies height(a) < height(b)
proof
let L be finite LATTICE;
let a,b be Element of L;
 assume
  A1: a < b;
    (ex A be Chain of Bottom L,a st height(a) = card A) &
   for C be Chain of Bottom L,a holds card C <= height(a) by Def3;
  then consider A be Chain of Bottom L,a such that
  A2: height(a) = card A and
    (for C be Chain of Bottom L,a holds card C <= height(a));
    (ex B be Chain of Bottom L,b st height(b) = card B) &
   for D be Chain of Bottom L,b holds card D <= height(b) by Def3;
  then consider B be Chain of Bottom L,b such that
    height(b) = card B and
  A3: (for B be Chain of Bottom L,b holds card B <= height(b));
A4:    Bottom L<=a by YELLOW_0:44;
A5: not b in A
   proof
    assume b in A;
    then Bottom L <= b & b <= a by A4,Def2;
    hence contradiction by A1,ORDERS_1:30;
   end;
  set C=A \/ {b};
      Bottom L in A by A4,Def2;
then A6: Bottom L in C by XBOOLE_0:def 2;
A7: b in C
     proof
        b in {b} by TARSKI:def 1;
      hence thesis by XBOOLE_0:def 2;
     end;
A8: for z be Element of L st z in C holds Bottom L <= z & z <= b
     proof
      let z be Element of L;
      assume A9: z in C;
       per cases by A9,XBOOLE_0:def 2;
       suppose A10: z in A;
       thus Bottom L<=z by YELLOW_0:44;
         z<=a by A4,A10,Def2;
       then z<b by A1,ORDERS_1:32;
       hence thesis by ORDERS_1:def 10;
       suppose z in {b};
       hence thesis by TARSKI:def 1,YELLOW_0:44;
     end;
A11:   C is strongly_connected Subset of L
      proof
      the InternalRel of L is_strongly_connected_in C
        proof
         let x,y be set;
           x in C & y in C implies [x,y] in the InternalRel of L
          or [y,x] in the InternalRel of L
           proof
            assume A12: x in C & y in C;
              per cases by A12,XBOOLE_0:def 2;
               suppose A13: x in A & y in A;
               then reconsider x,y as Element of L;
                 x <= y or y <= x by A13,ORDERS_1:38;
               hence thesis by ORDERS_1:def 9;
               suppose A14: x in A & y in {b};
then A15:             y=b by TARSKI:def 1;
                reconsider x as Element of L by A14;
                  Bottom L<=a by YELLOW_0:44;
                then x <= a by A14,Def2;
                then x < b by A1,ORDERS_1:32;
                then x <= b by ORDERS_1:def 10;
               hence thesis by A15,ORDERS_1:def 9;
               suppose A16: x in {b} & y in A;
then A17:             x=b by TARSKI:def 1;
                reconsider y as Element of L by A16;
                  Bottom L<=a by YELLOW_0:44;
                then y <= a by A16,Def2;
                then y < b by A1,ORDERS_1:32;
                then y <= b by ORDERS_1:def 10;
               hence thesis by A17,ORDERS_1:def 9;
               suppose A18: x in {b} & y in {b};
                then reconsider x,y as Element of L;
                  x=b & y=b by A18,TARSKI:def 1;
                then x <= y;
               hence thesis by ORDERS_1:def 9;
           end;
         hence thesis;
        end;
       hence thesis by ORDERS_1:def 11;
      end;
     Bottom L <= b by YELLOW_0:44;
then A19: C is Chain of Bottom L,b by A6,A7,A8,A11,Def2;
     card C = (card A)+1 by A5,CARD_2:54;
 then height(a) + 1 <= height(b) by A2,A3,A19;
 hence thesis by NAT_1:38;
end;

theorem Th3:
for L be finite LATTICE
 for C be Chain of L
  for x,y be Element of L holds
  x in C & y in C implies
   ( x < y iff height(x) < height(y) )

proof
let L be finite LATTICE;
let C be Chain of L;
let x,y be Element of L;
assume A1: x in C & y in C;
thus x < y iff height(x) < height(y)
 proof
  thus x < y implies height(x) < height(y) by Th2;
    height(x) < height(y) implies x < y
   proof
    assume A2: height(x) < height(y);
    per cases by A1,ORDERS_1:38;
     suppose x <= y;
     hence thesis by A2,ORDERS_1:def 10;

     suppose y <= x;
     then x=y or y < x by ORDERS_1:def 10;
     hence thesis by A2,Th2;
   end;
  hence thesis;
 end;
end;

theorem Th4:
for L be finite LATTICE
 for C be Chain of L
  for x,y be Element of L holds
  x in C & y in C implies
   ( x = y iff height(x) = height(y) )

proof
let L be finite LATTICE;
let C be Chain of L;
let x,y be Element of L;
 assume A1: x in C & y in C;
 thus x = y implies height(x) = height(y);
  height(x) = height(y) implies x=y
  proof
   assume A2: height(x) = height(y) & x<>y;
then A3:(x<=y or y<=x) & x<>y by A1,ORDERS_1:38;
     height(x)<>height(y)
    proof
     per cases by A3,ORDERS_1:def 10;
      suppose x < y;
      hence thesis by A1,Th3;
      suppose y < x;
      hence thesis by A1,Th3;
    end;
   hence contradiction by A2;
  end;
hence thesis;
end;

theorem Th5:
for L be finite LATTICE
 for C be Chain of L
  for x,y be Element of L holds
  x in C & y in C implies
   ( x <= y iff height(x) <= height(y) )

proof
let L be finite LATTICE;
let C be Chain of L;
let x,y be Element of L;
 assume A1: x in C & y in C;
 thus x <= y iff height(x) <= height(y)
  proof
A2: x <= y implies height(x) <= height(y)
    proof
     assume x<=y;
      then x<y or x=y by ORDERS_1:def 10;
     hence thesis by A1,Th3;
    end;
  height(x) <= height(y) implies x<=y
    proof
     assume height(x) <= height(y);
      then height(x) < height(y) or height(x) = height(y) by REAL_1:def 5;
      then x<y or height(x) = height(y) by A1,Th3;
     hence thesis by A1,Th4,ORDERS_1:def 10;
    end;
   hence thesis by A2;
  end;
end;

theorem
  for L be finite LATTICE
 for x be Element of L holds
  height (x) = 1 iff x = Bottom L
   proof
    let L be finite LATTICE;
    let x be Element of L;
A1:   height (x) = 1 implies x = Bottom L
      proof
       assume A2: height (x) = 1 & x <> Bottom L;
         (ex A be Chain of Bottom L,x st height (x)= card A) &
       for A be Chain of Bottom L,x holds card A <= height (x) by Def3;
       then consider A be Chain of Bottom L,x such that A3: height (x)= card A
          & for A be Chain of Bottom L,x holds card A <= height (x);
A4:    {Bottom L,x} is Chain of Bottom L,x
        proof
A5:      Bottom L<=x by YELLOW_0:44;
then A6:      {Bottom L,x} is Chain of L by ORDERS_1:36;
A7:       x in {Bottom L,x} by TARSKI:def 2;
A8:      Bottom L in {Bottom L,x} by TARSKI:def 2;
           for z be Element of L st z in {Bottom L,x} holds Bottom
L <= z & z <= x
          proof
           let z be Element of L;
            assume A9: z in {Bottom L,x};
             per cases by A9,TARSKI:def 2;
              suppose z=Bottom L;
              hence thesis by YELLOW_0:44;
              suppose z=x;
              hence thesis by YELLOW_0:44;
          end;
         hence thesis by A5,A6,A7,A8,Def2;
        end;
         card {Bottom L,x} = 2 by A2,CARD_2:76;
       hence contradiction by A2,A3,A4;
      end;

       x = Bottom L implies height (x) = 1
      proof
       assume A10: x = Bottom L;
          (ex A be Chain of Bottom L,Bottom L st height(Bottom L)= card A) &
           for A be Chain of Bottom L,Bottom L holds card A <= height(Bottom
L) by Def3;
        then consider A be Chain of Bottom L,Bottom L such that A11: height(
Bottom
L)= card A &
           for A be Chain of Bottom L,Bottom L holds card A <= height(Bottom
L);
A12:      for B be Chain of Bottom L,Bottom L holds B = {Bottom L}
         proof
          let B be Chain of Bottom L,Bottom L;
A13:        B c= {Bottom L}
           proof
            let r be set;
              r in B implies r in {Bottom L}
             proof
              assume r in B;
               then reconsider r as Element of B;
                 Bottom L <= r & r <= Bottom L by Def2;
               then Bottom L = r by ORDERS_1:25;
              hence thesis by TARSKI:def 1;
             end;
            hence thesis;
           end;
            {Bottom L} c= B
           proof
            let r be set;
              r in {Bottom L} implies r in B
             proof
              assume r in {Bottom L};
               then r = Bottom L by TARSKI:def 1;
              hence thesis by Def2;
             end;
            hence thesis;
           end;
          hence thesis by A13,XBOOLE_0:def 10;
         end;
          card {Bottom L} = 1 by CARD_1:79;
       hence thesis by A10,A11,A12;
      end;
    hence thesis by A1;
   end;

theorem Th7:
for L be non empty finite LATTICE
 for x be Element of L holds
  height (x) >= 1

proof
 let L be non empty finite LATTICE;
 let x be Element of L;
   (ex A be Chain of Bottom L,x st height (x)= card A) &
   for A be Chain of Bottom L,x holds card A <= height (x) by Def3;
   then consider A be Chain of Bottom L,x such that height (x)= card A
    and A1: (for B be Chain of Bottom L,x holds card B <= height (x));
     Bottom L<=x by YELLOW_0:44;
then A2: {Bottom L,x} is Chain of Bottom L,x by Th1;
then A3: card {Bottom L,x} <= height (x) by A1;
   per cases;
   suppose x<>Bottom L;
    then card {Bottom L,x} = 2 by CARD_2:76;
   hence thesis by A3,AXIOMS:22;
   suppose A4: x=Bottom L;
then A5:  card {Bottom L,Bottom L} <= height (Bottom L) by A1,A2;
      {Bottom L,Bottom L}={Bottom L}
     proof
A6:    {Bottom L,Bottom L}c={Bottom L}
       proof
        let d be Element of L;
        assume d in {Bottom L,Bottom L};
         then d =Bottom L or d =Bottom L by TARSKI:def 2;
        hence thesis by TARSKI:def 1;
       end;
        {Bottom L}c={Bottom L,Bottom L}
       proof
        let d be Element of L;
        assume d in{Bottom L};
         then d =Bottom L by TARSKI:def 1;
        hence thesis by TARSKI:def 2;
       end;
      hence thesis by A6,XBOOLE_0:def 10;
     end;
    hence thesis by A4,A5,CARD_1:79;
end;

scheme LattInd
 { L() -> finite LATTICE, P[set]}:
  for x be Element of L() holds P[x]
   provided
  A1: for x be Element of L()
     st for b be Element of L() st b < x
      holds P[b]
       holds P[x]

proof
let x be Element of L();

defpred Q[Nat] means
  for x be Element of L() st height(x) <= $1
   holds P[x];

A2: for n be Nat holds Q[n]
 proof
A3: Q[0]
  proof
     for x be Element of L() st height(x) <= 0 holds P[x]
    proof
     let x be Element of L();
     assume (height(x) <= 0) & not P[x];
     then height(x) < 0 + 1 by NAT_1:38;
     hence contradiction by Th7;
    end;
   hence thesis;
  end;
A4: for n be Nat st Q[n] holds Q[n+1]
    proof
     let n be Nat;
     assume A5: Q[n];
       for x be Element of L() st height(x) <= n+1 holds P[x]
      proof
       let x be Element of L();
       assume height(x) <= n+1;
then A6:    height(x) = n+1 or height(x) <= n by NAT_1:26;
       per cases by A5,A6;
       suppose A7: height(x) = n+1;
         for y be Element of L() st y < x holds P[y]
        proof
         let y be Element of L();
         assume y < x;
         then height(y) < height(x) by Th2;
         then height(y) <= n by A7,NAT_1:38;
         hence thesis by A5;
        end;
       hence thesis by A1;
       suppose P[x];
       hence thesis;
      end;
     hence thesis;
    end;
  thus thesis from Ind (A3,A4);
 end;
  ( for x be Element of L() st height(x) <= height(x) holds P[x] ) implies
 (for x be Element of L() holds P[x])
  proof
   assume A8: (for x be Element of L() st height(x) <= height(x) holds P[x])
     & not (for x be Element of L() holds P[x]);
    then consider x be Element of L() such that A9: not P[x];
      height(x) <= height(x) implies P[x] by A8;
   hence contradiction by A9;
  end;
hence thesis by A2;
end;

begin :: Join irreducible elements in a finite distributive lattice

definition
cluster distributive finite LATTICE;
existence
 proof
  consider s being set;
  set D = {s};
  consider R being Order of D;
  reconsider A = RelStr (#D,R#) as with_infima with_suprema Poset;
  take A;
  thus thesis;
 end;
end;

definition
let L be LATTICE;
let x,y be Element of L;
pred x <(1) y means :Def4:
  x < y & not (ex z be Element of L st x < z & z < y);
end;

theorem Th8:
for L be finite LATTICE
 for X be non empty Subset of L holds
  ex x be Element of L st x in X & for y be Element of L st y in X
     holds not (x < y)

proof
let L be finite LATTICE;
let X be non empty Subset of L;
  defpred
   P[Nat] means ex x be Element of L st x in X & $1=height(x);
  ex k st P[k] & for n st P[n] holds n <= k
   proof
    A1: for k st P[k] holds k <= card the carrier of L
     proof
        let k;
        assume P[k];
        then consider x be Element of L such that A2: x in X & k=height(x);
        consider B be Chain of Bottom L,x such that A3: k=card B by A2,Def3;
        thus thesis by A3,CARD_1:80;
     end;
    A4: ex k st P[k]
     proof
      consider x be set such that A5: x in X by XBOOLE_0:def 1;
      reconsider x as Element of L by A5;
        (ex B be Chain of Bottom L,x st height(x)= card B) &
         for B be Chain of Bottom L,x holds card B <= height(x) by Def3;
      then consider B be Chain of Bottom L,x such that A6: height(x)= card B &
         for B be Chain of Bottom L,x holds card B <= height(x);
      thus thesis by A5,A6;
     end;
    thus thesis from Max (A1,A4);
   end;

  then consider k such that A7: P[k] & for n st P[n] holds n <= k;
  consider x be Element of L such that A8: x in X & k=height(x) &
   for n st ex y be Element of L st y in X & n=height(y) holds n <= k by A7;
    for y be Element of L st y in X holds not (x < y)
   proof
    let y be Element of L;
     assume A9: y in X & x < y;
     then height(x)<height(y) by Th2;
    hence contradiction by A8,A9;
   end;
  hence thesis by A8;
end;

definition
let L be finite LATTICE;
let A be non empty Chain of L;
func max(A) -> Element of L means :Def5:
 (for x be Element of L st x in A holds x <= it) & it in A;

existence
 proof
  defpred
   P[Nat] means ex x be Element of L st x in A & $1=height(x);
  ex k st P[k] & for n st P[n] holds n <= k
   proof
    A1: for k st P[k] holds k <= card the carrier of L
     proof
        let k;
        assume P[k];
        then consider x be Element of L such that A2: x in A & k=height(x);
        consider B be Chain of Bottom L,x such that A3: k=card B by A2,Def3;
        thus thesis by A3,CARD_1:80;
     end;
    A4: ex k st P[k]
     proof
      consider x be set such that A5: x in A by XBOOLE_0:def 1;
      reconsider x as Element of L by A5;
        (ex B be Chain of Bottom L,x st height(x)= card B) &
         for B be Chain of Bottom L,x holds card B <= height(x) by Def3;
      then consider B be Chain of Bottom L,x such that A6: height(x)= card B &
         for B be Chain of Bottom L,x holds card B <= height(x);
      thus thesis by A5,A6;
     end;
    thus thesis from Max (A1,A4);
   end;

  then consider k such that A7: P[k] & for n st P[n] holds n <= k;
  consider x be Element of L such that A8: x in A & k=height(x) and
     A9: for n st ex z be Element of L st z in
 A & n=height(z) holds n<=k by A7
;
  take x;
  thus for w be Element of L st w in A holds w <= x
    proof
     let w be Element of L;
     assume A10: w in A;
      then height(w)<=height(x) by A8,A9;
     hence thesis by A8,A10,Th5;
    end;
  thus x in A by A8;
 end;
uniqueness
 proof
  let s,t be Element of L such that
   A11: for x be Element of L st x in A holds x <= s and A12: s in A and
    A13: for y be Element of L st y in A holds y <= t and A14: t in A;
  consider A be non empty Chain of L such that
   A15: (for x be Element of L st x in A holds x <= s) & s in A and
    A16: (for y be Element of L st y in A holds y <= t) & t in A by A11,A12,A13
,A14;
A17:  t <= s by A15,A16;
      s <= t by A15,A16;
  hence s=t by A17,ORDERS_1:25;
 end;
end;

theorem Th9:
for L be finite LATTICE
 for y be Element of L st y <> Bottom L holds
  ex x be Element of L st x <(1) y

proof
let L be finite LATTICE;
let y be Element of L;
 assume A1: y <> Bottom L;
   (ex A be Chain of Bottom L,y st height(y)= card A) &
     for A be Chain of Bottom L,y holds card A <= height(y) by Def3;
 then consider A be Chain of Bottom L,y such that A2: height(y)= card A &
     for A be Chain of Bottom L,y holds card A <= height(y);
 set B=A\{y};
A3:B is strongly_connected Subset of L
      proof
      the InternalRel of L is_strongly_connected_in B
        proof
         let p,q be set;
           p in B & q in B implies [p,q] in the InternalRel of L
          or [q,p] in the InternalRel of L
           proof
            assume A4:p in B & q in B;
then A5:          p in A & not (p in {y}) & q in A & not (q in {y}) by XBOOLE_0
:def 4;
             reconsider p,q as Element of L by A4;
               p <= q or q <= p by A5,ORDERS_1:38;
            hence thesis by ORDERS_1:def 9;
           end;
         hence thesis;
        end;
       hence thesis by ORDERS_1:def 11;
      end;
  B is non empty
     proof
      assume A6: B is empty;
        Bottom L<=y by YELLOW_0:44;
then A7:   Bottom L in A by Def2;
        not (Bottom L in {y}) by A1,TARSKI:def 1;
      hence contradiction by A6,A7,XBOOLE_0:def 4;
     end;
 then reconsider B as non empty Chain of L by A3;

 take x=max(B);

A8: x < y
  proof
A9: x in B by Def5;
A10: Bottom L<=y by YELLOW_0:44;
     x in A & not x in {y} by A9,XBOOLE_0:def 4;
   then Bottom L<=x & x<=y & not x=y by A10,Def2,TARSKI:def 1;
   hence thesis by ORDERS_1:def 10;
  end;

  not ex z be Element of L st x < z & z < y
     proof
      given z be Element of L such that A11: x < z & z < y;
A12:   not z in A
       proof
        assume A13: z in A;
          not (z in {y}) by A11,TARSKI:def 1;
        then z in B by A13,XBOOLE_0:def 4;
        then z <= x & x < z by A11,Def5;
        hence contradiction by ORDERS_1:32;
       end;
     set C=A \/ {z};
A14:  C is strongly_connected Subset of L
      proof
A15:    A=(A\{y})\/{y}
        proof
           {y} c= A
           proof
            let h be Element of L;
            assume h in {y};
then A16:         h=y by TARSKI:def 1;
              Bottom L<=y by YELLOW_0:44;
            hence thesis by A16,Def2;
           end;
         hence thesis by XBOOLE_1:45;
        end;
      the InternalRel of L is_strongly_connected_in C
        proof
         let x1,y1 be set;
           x1 in C & y1 in C implies [x1,y1] in the InternalRel of L
          or [y1,x1] in the InternalRel of L
           proof
            assume A17: x1 in C & y1 in C;
              per cases by A17,XBOOLE_0:def 2;
               suppose A18: x1 in A & y1 in A;
               then reconsider x1,y1 as Element of L;
                 x1 <= y1 or y1 <= x1 by A18,ORDERS_1:38;
               hence thesis by ORDERS_1:def 9;

               suppose A19: x1 in A & y1 in {z};
then A20:             y1=z by TARSKI:def 1;
                reconsider x1,y1 as Element of L by A19;
                  x1 in A\{y} or x1 in {y} by A15,A19,XBOOLE_0:def 2;
                then x1 <= x or x1 = y by Def5,TARSKI:def 1;
                then x1 < y1 or x1 = y by A11,A20,ORDERS_1:32;
                then x1 <= y1 or y1 < x1
                  by A11,A19,ORDERS_1:def 10,TARSKI:def 1;
                then x1 <= y1 or y1 <= x1 by ORDERS_1:def 10;
               hence thesis by ORDERS_1:def 9;

               suppose A21: y1 in A & x1 in {z};
then A22:             x1=z by TARSKI:def 1;
                reconsider x1,y1 as Element of L by A21;
                  y1 in A\{y} or y1 in {y} by A15,A21,XBOOLE_0:def 2;
                then y1 <= x or y1 = y by Def5,TARSKI:def 1;
                then y1 < x1 or y1 = y by A11,A22,ORDERS_1:32;
                then y1 <= x1 or x1 <= y1 by A11,A22,ORDERS_1:def 10;
               hence thesis by ORDERS_1:def 9;

               suppose A23: x1 in {z} & y1 in {z};
                then reconsider x1,y1 as Element of L;
                  x1=z & y1=z by A23,TARSKI:def 1;
                then x1<=y1;
               hence thesis by ORDERS_1:def 9;
           end;
         hence thesis;
        end;
       hence thesis by ORDERS_1:def 11;
      end;
A24:    Bottom L<=y by YELLOW_0:44;
then A25:    Bottom L in A by Def2;
A26:   y in A by A24,Def2;
A27:    Bottom L in A \/ {z} by A25,XBOOLE_0:def 2;
A28:   y in A \/ {z} by A26,XBOOLE_0:def 2;
A29:   Bottom L <= z & z <= y by A11,ORDERS_1:def 10,YELLOW_0:44;
       for v be Element of L st v in A \/ {z} holds Bottom L <= v & v <= y
     proof
      let v be Element of L;
      assume A30:v in A \/ {z};
       per cases by A30,XBOOLE_0:def 2;
       suppose A31: v in A;
       thus Bottom L<=v by YELLOW_0:44;
       thus thesis by A24,A31,Def2;
       suppose v in {z};
       hence thesis by A29,TARSKI:def 1;
     end;
then A32:   A \/ {z} is Chain of Bottom L,y by A14,A24,A27,A28,Def2;
     card (A \/ {z})=card A + 1 by A12,CARD_2:54;
      then card A + 1 <= card A by A2,A32;
      hence contradiction by NAT_1:38;
     end;
 hence thesis by A8,Def4;
end;

definition
let L be LATTICE;
func Join-IRR L -> Subset of L equals :Def6:
           {a where a is Element of L: a<>Bottom L &
               for b,c be Element of L holds a= b"\/"c implies a=b or a=c};
  coherence
   proof
        {a where a is Element of L:a<>Bottom L & for b,c be Element of
          L holds a= b"\/"c implies a=b or a=c} c= the carrier of L
        proof
         let x be set;
         assume x in {a where a is Element of L:a<>Bottom
L & for b,c be Element of
                L holds a= b"\/"c implies a=b or a=c};
         then ex a being Element of L st x=a & a <> Bottom L &
                  for b,c be Element of L holds a= b"\/"c implies a=b or a=c;
         hence thesis;
        end;
       hence thesis;
   end;
end;

theorem Th10:
for L be LATTICE
 for x be Element of L
    holds x in Join-IRR L iff x<>Bottom L & for b,c be Element of
                           L holds x= b"\/"c implies x=b or x=c
proof
 let L be LATTICE;
 let x be Element of L;
A1: Join-IRR L = {a where a is Element of L:a<>Bottom L &
       for b,c be Element of L holds a= b"\/"c implies a=b or a=c} by Def6;
thus x in Join-IRR L implies x <> Bottom L & for b,c be Element of L holds
                           x= b"\/"c implies x=b or x=c
 proof
  assume
     x in Join-IRR L;
    then ex a being Element of L st x = a &
    a<>Bottom L & for b,c be Element of L holds a= b"\/"c
         implies a=b or a=c by A1;
  hence thesis;
 end;

thus x <> Bottom
L & (for b,c be Element of L holds x= b"\/"c implies x=b or x=c)
        implies x in Join-IRR L by A1;
end;

theorem Th11:
for L be finite distributive LATTICE
 for x be Element of L
  holds x in Join-IRR L implies
   ex z be Element of L st z < x & for y be Element of L st y < x
    holds y <= z
proof
 let L be finite distributive LATTICE;
 let x be Element of L;
 assume
A1: x in Join-IRR L;
 then x<>Bottom
L & for b,c be Element of L holds x= b"\/"c implies x=b or x=c by Th10;
  then consider z be Element of L such that A2: z <(1) x by Th9;
A3: z < x & not (ex v be Element of L st z < v & v < x) by A2,Def4;

    for y be Element of L st y < x holds y <= z
    proof
     let y be Element of L;
     assume A4: (y < x) & not (y <= z);
     consider Y be set such that
          A5: Y={g where g is Element of L : g < x & not (g <= z)};
A6:  Y is empty
      proof
        assume A7: Y is non empty;

A8:     for t be Element of L holds t in Y iff t < x & not t <= z
         proof
          let t be Element of L;
         t in Y implies t < x & not t <= z
           proof
            assume t in Y;
            then consider g be Element of L
                such that A9: g=t & g < x & not (g <= z) by A5;
            thus thesis by A9;
           end;
          hence thesis by A5;
         end;

          Y is Subset of L
         proof
            Y c= the carrier of L
           proof
            let f be set;
            assume f in Y;
            then consider g be Element of L such that A10: g=f & g<x & not(g<=z
)
             by A5;
            thus thesis by A10;
           end;
          hence thesis;
          thus thesis;
         end;
        then consider a be Element of L such that
A11:         a in Y and
A12:        for b be Element of L st b in Y holds not (a < b) by A7,Th8;
A13:     a<x & not(a<=z) by A8,A11;
A14:     a"\/"z<x
         proof
            a<x by A8,A11;
then A15:       a<=x by ORDERS_1:def 10;
            z<=x by A3,ORDERS_1:def 10;
then A16:       a"\/"z <= x by A15,YELLOW_5:9;
            a"\/"z<>x by A1,A3,A13,Th10;
          hence thesis by A16,ORDERS_1:def 10;
         end;

          not(a"\/"z <= z) by A13,YELLOW_5:3;
then A17:     a"\/"z in Y by A8,A14;
          (a"\/"z)>a
         proof
            a"/\"a <= a"\/"z by YELLOW_5:5;
then A18:        a <= a"\/"z by YELLOW_5:2;
            a<>a"\/"z
           proof
            assume a=a"\/"z;
               z<a"\/"z
              proof
                 z"/\"z<=a"\/"z by YELLOW_5:5;
               then z<=a"\/"z by YELLOW_5:2;
               hence thesis by A13,A18,ORDERS_1:def 10;
              end;
             hence contradiction by A2,A14,Def4;
           end;
          hence thesis by A18,ORDERS_1:def 10;
         end;

       hence contradiction by A12,A17;
      end;
       y in Y by A4,A5;
     hence contradiction by A6;
    end;
   hence thesis by A3;
end;

Lm1:
for L be finite distributive LATTICE
 for a being Element of L
     st for b be Element of L st b < a holds sup(downarrow b /\ Join-IRR L) =b
      holds sup(downarrow a /\ Join-IRR L) =a
proof
       let L be finite distributive LATTICE;
       let a be Element of L;
       assume
A1:     for b be Element of L st b < a holds sup(downarrow b /\ Join-IRR L) =b;
        thus sup(downarrow a /\ Join-IRR L) = a
    proof
        per cases;

         suppose
A2:       a = Bottom L;
then A3:      downarrow a = {Bottom L} by WAYBEL_4:23;
           {Bottom L} /\ Join-IRR L= {}
          proof
           assume
A4:          {Bottom L} /\ Join-IRR L <> {};
            consider x be Element of {Bottom L} /\ Join-IRR L;
              x in {Bottom L} & x in Join-IRR L by A4,XBOOLE_0:def 3;
            then x = Bottom L & x<>Bottom L & (for b,c be Element of L holds
                 x= b"\/"c implies x=b or x=c) by Th10,TARSKI:def 1;
           hence contradiction;
          end;
         hence thesis by A2,A3,YELLOW_0:def 11;

         suppose (not a in Join-IRR L) & a <> Bottom L;
           then consider y,z be Element of L such that
A5:           a= y"\/"z and
A6:          a <> y and
A7:          (a <> z) by Th10;
A8:       y <= a by A5,YELLOW_0:22;
then A9:       y < a by A6,ORDERS_1:def 10;
A10:        z <= a by A5,YELLOW_0:22;
then A11:       z < a by A7,ORDERS_1:def 10;

A12:     downarrow a /\ Join-IRR L =
             (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L)
        proof
         thus downarrow a /\ Join-IRR L c=
                 (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L)
          proof
           let x be Element of L;
           assume
              x in downarrow a /\ Join-IRR L;
then A13:         x in downarrow a & x in Join-IRR L by XBOOLE_0:def 3;
               set x1=x,y1=y,a1=a,z1=z;
A14:            x1 "/\" a1 = (x1"/\"y1) "\/" (x1"/\"z1) by A5,WAYBEL_1:def 3;
                 x1 <= a1 by A13,WAYBEL_0:17;
               then x1 = (x1"/\"y1) "\/" (x1"/\"z1) by A14,YELLOW_0:25;
               then x1 = x1"/\"y1 or x1 = x1"/\"z1 by A13,Th10;
               then x1 <= y1 or x1 <= z1 by YELLOW_0:25;
               then x1 in downarrow y1 or x1 in downarrow z1 by WAYBEL_0:17;
               then x1 in downarrow y1 /\ Join-IRR L or
                  x1 in downarrow z1 /\ Join-IRR L
                     by A13,XBOOLE_0:def 3;
               hence thesis by XBOOLE_0:def 2;
          end;

         thus (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L) c=
                  downarrow a /\ Join-IRR L
          proof
           let x be Element of L;
           assume
A15:       x in (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L);
             downarrow y c= downarrow a by A8,WAYBEL_0:21;
then A16:        (downarrow y /\ Join-IRR L) c= (downarrow a /\ Join-IRR L)
                                           by XBOOLE_1:26;
             downarrow z c= downarrow a by A10,WAYBEL_0:21;
           then (downarrow z /\ Join-IRR L) c= (downarrow a /\ Join-IRR L)
                                           by XBOOLE_1:26;
           then (downarrow y /\ Join-IRR L) \/ (downarrow z /\ Join-IRR L) c=
                  downarrow a /\ Join-IRR L by A16,XBOOLE_1:8;
           hence thesis by A15;
          end;
        end;
A17:      ex_sup_of (downarrow y /\ Join-IRR L \/ downarrow z /\ Join-IRR L),L
            by YELLOW_0:17;
A18:      ex_sup_of downarrow y /\ Join-IRR L,L by YELLOW_0:17;
        ex_sup_of downarrow z /\ Join-IRR L,L by YELLOW_0:17;
        then sup (downarrow a /\ Join-IRR L) =
          sup(downarrow y /\ Join-IRR L) "\/" sup(downarrow z /\ Join-IRR L)
                       by A12,A17,A18,YELLOW_0:36;
        then sup (downarrow a /\ Join-IRR L) = y "\/" sup(downarrow z /\
Join-IRR L)
          by A1,A9;
        hence thesis by A1,A5,A11;

         suppose
A19:       a in Join-IRR L;
A20:        downarrow a /\ Join-IRR L c= downarrow a by XBOOLE_1:17;
A21:       ex_sup_of downarrow a /\ Join-IRR L,L by YELLOW_0:17;
         ex_sup_of downarrow a,L by YELLOW_0:17;
          then sup(downarrow a /\ Join-IRR L) <= sup(downarrow a) by A20,A21,
YELLOW_0:34;
then A22:       sup(downarrow a /\ Join-IRR L) <= a by WAYBEL_0:34;
            a <= sup(downarrow a /\ Join-IRR L)
           proof
              a <= a;
            then a in downarrow a by WAYBEL_0:17;
            then a in downarrow a /\ Join-IRR L by A19,XBOOLE_0:def 3;
            hence thesis by A21,YELLOW_4:1;
           end;
          hence sup(downarrow a /\ Join-IRR L) = a by A22,ORDERS_1:25;
    end;
end;

theorem Th12:
for L be distributive finite LATTICE
 for x be Element of L
  holds sup (downarrow x /\ Join-IRR L) = x

proof
 let L be distributive finite LATTICE;
 let x be Element of L;
A1:  downarrow x /\ Join-IRR L c= downarrow x by XBOOLE_1:17;
A2: ex_sup_of downarrow x /\ Join-IRR L,L by YELLOW_0:17;
   ex_sup_of downarrow x,L by YELLOW_0:17;
then sup(downarrow x /\ Join-IRR L) <= sup(downarrow x) by A1,A2,YELLOW_0:34;
    then A3: sup(downarrow x /\ Join-IRR L) <= x by WAYBEL_0:34;
  x <= sup( downarrow x /\ Join-IRR L)
 proof
   defpred X[Element of L] means sup(downarrow $1 /\ Join-IRR L) = $1;
A4: for x being Element of L
      st for b be Element of L st b < x holds X[b]
       holds X[x] by Lm1;
       for x being Element of L holds X[x] from LattInd(A4);
     hence thesis;
 end;
hence sup(downarrow x /\ Join-IRR L)= x by A3,ORDERS_1:25;
end;

begin :: Representation theorem

definition
let P be RelStr;
func LOWER(P) -> non empty set equals :Def7:
{X where X is Subset of P:X is lower};
  coherence
   proof
      {}P in {X where X is Subset of P:X is lower};
    hence thesis;
   end;
 end;

theorem Th13:
for L be distributive finite LATTICE
 ex r be map of L, InclPoset LOWER(subrelstr Join-IRR L) st
   r is isomorphic &
    for a being Element of L holds r.a= downarrow a /\ Join-IRR L
proof
  let L be distributive finite LATTICE;
  set I = InclPoset LOWER(subrelstr Join-IRR L);
  deffunc U(Element of L) = downarrow $1 /\ Join-IRR L;
  consider r be ManySortedSet of the carrier of L such that
     A1: for d be Element of L holds
        r.d= U(d) from LambdaDMS;
A2: for a being Element of L holds r.a= downarrow a /\ Join-IRR L by A1;
A3:  dom r = the carrier of L by PBOOLE:def 3;
       rng r c= the carrier of I
      proof
       let t be set;
       assume t in rng r;
        then consider x be set such that A4: x in dom r & t = r.x by FUNCT_1:
def 5;
          x in the carrier of L by A4,PBOOLE:def 3;
        then reconsider x as Element of L;
A5:     the carrier of I = LOWER(subrelstr Join-IRR L) by YELLOW_1:1;
A6:    t=downarrow x /\ Join-IRR L by A1,A4;
then t c= Join-IRR L by XBOOLE_1:17;
        then t c= the carrier of subrelstr Join-IRR L by YELLOW_0:def 15;
        then reconsider t as Subset of subrelstr Join-IRR L;

          t is lower
        proof
         let c,d be Element of subrelstr Join-IRR L;
         assume A7: c in t & d <= c;
then A8:      c in downarrow x & c in Join-IRR L by A6,XBOOLE_0:def 3;
A9:      Join-IRR L is non empty by A6,A7;
A10:       d is Element of Join-IRR L by YELLOW_0:def 15;
      then d in Join-IRR L by A9;
         then reconsider c1=c,d1=d as Element of L
           by A6,A7;
A11:      d1 <= c1 by A7,YELLOW_0:60;
           c1 <= x by A8,WAYBEL_0:17;
         then d1 <= x by A11,ORDERS_1:26;
         then d1 in downarrow x by WAYBEL_0:17;
         hence thesis by A6,A9,A10,XBOOLE_0:def 3;
        end;
        then t in {X where X is Subset of subrelstr Join-IRR L : X is lower};
       hence thesis by A5,Def7;
      end;
     then r is Function of the carrier of L, the carrier of I
      by A3,FUNCT_2:def 1,RELSET_1:11;
     then reconsider r as map of L,I;
A12:  r is one-to-one
      proof
       let x,y be Element of L;
       assume
A13:     r.x = r.y;
       r.y= downarrow y /\ Join-IRR L by A1;
       then reconsider ry= r.y as Subset of L;
         sup (downarrow x /\ Join-IRR L) = sup (ry) by A1,A13;
       then sup (downarrow x /\ Join-IRR L) = sup (downarrow y /\ Join-IRR L)
by A1;
       then x = sup (downarrow y /\ Join-IRR L) by Th12;
       hence x=y by Th12;
      end;

A14:  rng r = the carrier of I
      proof
       thus rng r c= the carrier of I;
       thus the carrier of I c= rng r
        proof
         let x be set;
         assume
A15:      x in the carrier of I;
         thus x in rng r
          proof
             x in LOWER(subrelstr Join-IRR L) by A15,YELLOW_1:1;
           then x in {X where X is Subset of subrelstr Join-IRR L : X is lower
}
           by Def7;
           then consider X being Subset of subrelstr Join-IRR L such that
A16:         x=X & X is lower;
          X is Subset of L
             proof
              the carrier of subrelstr Join-IRR L c= Join-IRR L
                by YELLOW_0:def 15;
then the carrier of subrelstr Join-IRR L c= the carrier of L
                    by XBOOLE_1:1;
              then X c= the carrier of L by XBOOLE_1:1;
              hence thesis;
             end;
           then reconsider X1=X as Subset of L;
             ex y being set st y in dom r & x = r.y
            proof
             take y = sup X1;
               dom r = the carrier of L by FUNCT_2:def 1;
             hence y in dom r;
               X1 = downarrow(sup X1) /\ Join-IRR L
              proof
               thus X1 c= downarrow(sup X1) /\ Join-IRR L
                proof
                 let a be Element of L;
                 assume
A17:               a in X1;
                 set A = a;
                 thus a in downarrow(sup X1) /\ Join-IRR L
                  proof
                    ex_sup_of X1,L by YELLOW_0:17;
then A18:                 X1 is_<=_than "\/"(X1,L) by YELLOW_0:def 9;
                     A in downarrow {sup X1}
                    proof
                       ex y being Element of L st y in {sup X1} & A <= y
                      proof
                       take y = sup X1;
                       thus y in {sup X1} by TARSKI:def 1;
                       thus A <= y by A17,A18,LATTICE3:def 9;
                      end;
                     hence thesis by WAYBEL_0:def 15;
                    end;
                   then A19:                a in downarrow(sup X1) by WAYBEL_0:
def 17;
                     X is Subset of Join-IRR L by YELLOW_0:def 15;
                   hence thesis by A17,A19,XBOOLE_0:def 3;
                  end;
                end;
               thus downarrow(sup X1) /\ Join-IRR L c= X1
                proof
                 let r be Element of L;
                 assume A20: r in downarrow(sup X1) /\ Join-IRR L;
then A21:               r in downarrow(sup X1) & r in Join-IRR L by XBOOLE_0:
def 3;
                 reconsider r1=r as Element of L;
A22:              r1 <= sup X1 by A21,WAYBEL_0:17;
                 per cases;
                 suppose r1 in X1;
                 hence thesis;
                 suppose
A23:               not (r1 in X1);
A24:                r1 in Join-IRR L by A20,XBOOLE_0:def 3;
A25:               r1 = r1 "/\" sup X1 by A22,YELLOW_0:25;
A26:               r1 "/\" sup X1 = sup ({r1} "/\" X1) by WAYBEL_2:15;
                  consider z be Element of L such that
A27:                    z < r1 & for y be Element of L st y < r1 holds y <= z
                      by A24,Th11;
                    {r1} "/\" X1 is_<=_than z
                   proof
                    let a be Element of L;
                    assume a in {r1} "/\" X1;
                    then a in {r1"/\"k where k is Element of L:k in
 X1} by YELLOW_4:42;
                    then consider x be Element of L such that A28: a=r1"/\"x &
                     x in X1;
A29:                  ex_inf_of {r1,x},L by YELLOW_0:17;
then A30:                 a <= r1 by A28,YELLOW_0:19;
A31:                a <= x by A28,A29,YELLOW_0:19;
A32:                 r1 in the carrier of subrelstr Join-IRR L
                      by A24,YELLOW_0:def 15;
                    then reconsider r'=r1,x'=x as Element of subrelstr Join-IRR
L
                     by A28;
                      now assume a=r1;
                     then r' <= x' by A31,A32,YELLOW_0:61;
                     hence contradiction by A16,A23,A28,WAYBEL_0:def 19;
                    end;
                    then a < r1 by A30,ORDERS_1:def 10;
                    hence thesis by A27;
                   end;
                  then sup ({r1} "/\" X1) <= z by YELLOW_0:32;
                 hence thesis by A25,A26,A27,ORDERS_1:32;
                end;
              end;
             hence x=r.y by A1,A16;
            end;
           hence thesis by FUNCT_1:def 5;
          end;
        end;
      end;

       for x,y being Element of L holds (x <= y iff r.x <= r.y)
      proof
       let x,y be Element of L;
        thus x <= y implies r.x <= r.y
         proof
          assume
A33:        x <= y;
         downarrow x /\ Join-IRR L c= downarrow y /\ Join-IRR L
            proof
             let a be Element of L;
             assume a in downarrow x /\ Join-IRR L;
then A34:          a in downarrow x & a in Join-IRR L by XBOOLE_0:def 3;
               downarrow x c= downarrow y by A33,WAYBEL_0:21;
             hence thesis by A34,XBOOLE_0:def 3;
            end;
           then r.x c= downarrow y /\ Join-IRR L by A1;
           then r.x c= r.y by A1;
          hence thesis by YELLOW_1:3;
         end;

        thus r.x <= r.y implies x <= y
         proof
          assume
A35:        r.x <= r.y;
A36:        r.x= downarrow x /\ Join-IRR L by A1;
          r.y= downarrow y /\ Join-IRR L by A1;
          then reconsider rx = r.x,ry= r.y as Subset of L by A36;
A37:        rx c= ry by A35,YELLOW_1:3;
A38:        ex_sup_of rx,L by YELLOW_0:17;
            ex_sup_of ry,L by YELLOW_0:17;
          then sup(rx) <= sup(ry) by A37,A38,YELLOW_0:34;
          then sup (downarrow x /\ Join-IRR L) <= sup (ry) by A1;
          then sup (downarrow x /\ Join-IRR L) <= sup (downarrow y /\ Join-IRR
L)
                                                by A1;
          then x <= sup (downarrow y /\ Join-IRR L) by Th12;
          hence thesis by Th12;
         end;
      end;
     then r is isomorphic by A12,A14,WAYBEL_0:66;
     hence thesis by A2;
end;

theorem Th14:
for L be distributive finite LATTICE
 holds
    L, InclPoset LOWER(subrelstr Join-IRR L) are_isomorphic

proof
 let L be distributive finite LATTICE;
  consider r be map of L, InclPoset LOWER(subrelstr Join-IRR L) such that A1:
   r is isomorphic &
    for a being Element of L holds r.a= downarrow a /\ Join-IRR L by Th13;
  thus thesis by A1,WAYBEL_1:def 8;
end;

definition
 mode Ring_of_sets means :Def8: it includes_lattice_of it;
 existence
  proof
   consider X be set;
   take R = bool X;
   let a,b be set;
   assume A1: a in R & b in R;
    then a /\ b c= X by XBOOLE_1:108;
   hence a /\ b in R;
      a \/ b c= X by A1,XBOOLE_1:8;
   hence a \/ b in R;
  end;
end;

definition
cluster non empty Ring_of_sets;

existence
 proof
  take A={{}};
    A includes_lattice_of A
   proof
    let a,b be set;
    assume a in A & b in A;
then a={} & b={} by TARSKI:def 1;
    hence thesis by TARSKI:def 1;
   end;
  hence thesis by Def8;
 end;
end;

Lm2:
for L1,L2 be non empty RelStr
    for f be map of L1,L2 holds
      f is infs-preserving implies f is meet-preserving

proof
  let L1,L2 be non empty RelStr;
  let f be map of L1,L2;
  assume f is infs-preserving;
  then for x,y being Element of L1 holds f preserves_inf_of {x,y}
    by WAYBEL_0:def 32;
  hence thesis by WAYBEL_0:def 34;
 end;

Lm3:
for L1,L2 be non empty RelStr
  for f be map of L1,L2 holds
     f is sups-preserving implies f is join-preserving

proof
  let L1,L2 be non empty RelStr;
  let f be map of L1,L2;
  assume f is sups-preserving;
  then for x,y being Element of L1 holds f preserves_sup_of {x,y}
    by WAYBEL_0:def 33;
  hence thesis by WAYBEL_0:def 35;
end;

definition
 let X be non empty Ring_of_sets;
 cluster InclPoset X -> with_suprema with_infima distributive;

 coherence
  proof

A1: X includes_lattice_of X by Def8;
A2: InclPoset X is LATTICE
    proof
A3:  InclPoset X is with_infima
       proof
          for x,y be set st (x in X & y in X) holds x /\ y in
 X by A1,COHSP_1:def 8;
        hence thesis by YELLOW_1:12;
       end;
       InclPoset X is with_suprema
       proof
          for x,y be set st (x in X & y in X) holds x \/ y in
 X by A1,COHSP_1:def 8;
        hence thesis by YELLOW_1:11;
       end;
     hence thesis by A3;
    end;

     InclPoset X is distributive
    proof
     let x,y,z be Element of InclPoset X;
A4:    x /\ (y \/ z) = x /\ y \/ x /\ z by XBOOLE_1:23;
        x in the carrier of InclPoset X;
then A5:   x in X by YELLOW_1:1;
        y in the carrier of InclPoset X;
then A6:   y in X by YELLOW_1:1;
        z in the carrier of InclPoset X;
then A7:   z in X by YELLOW_1:1;
then A8:    y \/ z in X by A1,A6,COHSP_1:def 8;
then y \/ z in the carrier of InclPoset X by YELLOW_1:1;
      then reconsider r = y \/ z as Element of InclPoset X;
        r in the carrier of InclPoset X;
      then r in X by YELLOW_1:1;
      then x /\ r in X by A1,A5,COHSP_1:def 8;
   then x "/\" r = x /\ r by YELLOW_1:9;
then A9:   x /\ (y \/ z) = x "/\" (y "\/" z) by A8,YELLOW_1:8;
A10:    x /\ y in X by A1,A5,A6,COHSP_1:def 8;
then A11:    x /\ y in the carrier of InclPoset X by YELLOW_1:1;
A12:    x "/\" y = x /\ y by A10,YELLOW_1:9;
A13:    x /\ z in X by A1,A5,A7,COHSP_1:def 8;
then x /\ z in the carrier of InclPoset X by YELLOW_1:1;
      then reconsider r1 = x /\ y, r2 = x /\ z as Element of InclPoset X
       by A11;
A14:   x "/\" z = x /\ z by A13,YELLOW_1:9;
        r2 in the carrier of InclPoset X;
then A15:   r2 in X by YELLOW_1:1;
        r1 in the carrier of InclPoset X;
      then r1 in X by YELLOW_1:1;
      then r1 \/ r2 in X by A1,A15,COHSP_1:def 8;
     hence thesis by A4,A9,A12,A14,YELLOW_1:8;
    end;
   hence thesis by A2;
  end;
end;

theorem Th15:
for L be finite LATTICE holds
 LOWER(subrelstr Join-IRR L) is Ring_of_sets
proof
let L be finite LATTICE;
      set X = LOWER(subrelstr Join-IRR L);
        X includes_lattice_of X
       proof
        let a,b be set;
         assume A1: a in X & b in X;
A2:      a /\ b in X
          proof
          a in {Z where Z is Subset of subrelstr Join-IRR L:Z is lower}
            by A1,Def7;
           then consider Z be Subset of subrelstr Join-IRR L
            such that A3: a=Z & Z is lower;
         b in {Z1 where Z1 is Subset of subrelstr Join-IRR L:Z1 is lower}
            by A1,Def7;
           then consider Z1 be Subset of subrelstr Join-IRR L
            such that A4: b=Z1 & Z1 is lower;
         Z /\ Z1 is lower by A3,A4,WAYBEL_0:27;
           then Z /\ Z1 in {W where W is Subset of subrelstr Join-IRR L:W is
lower};
           hence thesis by A3,A4,Def7;
          end;
           a \/ b in X
          proof
          a in {Z where Z is Subset of subrelstr Join-IRR L:Z is lower}
            by A1,Def7;
           then consider Z be Subset of subrelstr Join-IRR L
            such that A5: a=Z & Z is lower;
         b in {Z1 where Z1 is Subset of subrelstr Join-IRR L:Z1 is lower}
            by A1,Def7;
           then consider Z1 be Subset of subrelstr Join-IRR L
            such that A6: b=Z1 & Z1 is lower;
         Z \/ Z1 is lower by A5,A6,WAYBEL_0:27;
           then Z \/ Z1 in {W where W is Subset of subrelstr Join-IRR L:W is
lower};
           hence thesis by A5,A6,Def7;
          end;
        hence thesis by A2;
       end;
     hence thesis by Def8;
end;

theorem
  for L be finite LATTICE holds
 L is distributive iff
  ex X be non empty Ring_of_sets st L, InclPoset X are_isomorphic
proof
 let L be finite LATTICE;
 thus L is distributive implies ex X be non empty Ring_of_sets st
        L, InclPoset X are_isomorphic
     proof
      assume A1: L is distributive;
      consider X be set such that A2: X = LOWER(subrelstr Join-IRR L);
A3:   X is Ring_of_sets by A2,Th15;
        L,InclPoset X are_isomorphic by A1,A2,Th14;
      hence thesis by A2,A3;
     end;
     given X be non empty Ring_of_sets such that
       A4: L, InclPoset X are_isomorphic;
      consider f be map of L, InclPoset X such that A5: f is isomorphic
        by A4,WAYBEL_1:def 8;
        f is infs-preserving by A5,WAYBEL13:20;
then A6:   f is meet-preserving by Lm2;
        f is sups-preserving by A5,WAYBEL13:20;
then A7:   f is join-preserving by Lm3;
        f is one-to-one by A5,WAYBEL_0:66;
      hence thesis by A6,A7,WAYBEL_6:3;
end;


Back to top