lattice7.miz



    begin

    definition

      let L be 1-sorted;

      let A,B be Subset of L;

      :: original: c=

      redefine

      :: LATTICE7:def1

      pred A c= B means for x be Element of L st x in A holds x in B;

      compatibility ;

    end

    registration

      let L be LATTICE;

      cluster non empty for Chain of L;

      existence

      proof

         {( Bottom L)} is Chain of L by ORDERS_2: 8;

        hence thesis;

      end;

    end

    definition

      let L be LATTICE;

      let x,y be Element of L;

      :: LATTICE7:def2

      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_2: 9;

        

         A2: for z be Element of L st z in A holds x <= z & z <= y

        proof

          let z be Element of L;

          assume

           A3: z in A;

          per cases by A3, TARSKI:def 2;

            suppose z = x;

            hence thesis by A1;

          end;

            suppose z = y;

            hence thesis by A1;

          end;

        end;

        y in A & x in A by TARSKI:def 2;

        hence thesis by A2;

      end;

    end

    theorem :: LATTICE7:1

    

     Th1: for L be LATTICE holds 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;

      

       A1: x in {x, y} & y in {x, y} by TARSKI:def 2;

      assume

       A2: x <= y;

      

       A3: for z be Element of L st z in {x, y} holds x <= z & z <= y

      proof

        let z be Element of L;

        assume

         A4: z in {x, y};

        per cases by A4, TARSKI:def 2;

          suppose z = x;

          hence thesis by A2;

        end;

          suppose z = y;

          hence thesis by A2;

        end;

      end;

       {x, y} is Chain of L by A2, ORDERS_2: 9;

      hence thesis by A2, A1, A3, Def2;

    end;

    reserve n,k for Element of NAT ;

    definition

      let L be finite LATTICE;

      let x be Element of L;

      :: LATTICE7:def3

      func height (x) -> Element of 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);

        

         A1: {( Bottom L), x} is Chain of ( Bottom L), x by Th1, YELLOW_0: 44;

        ex k st P[k] & for n st P[n] holds n <= k

        proof

           P[( card {( Bottom L), x})] by A1;

          then

           A2: ex k be Nat st P[k];

          

           A3: for k be Nat st P[k] holds k <= ( card the carrier of L) by NAT_1: 43;

          consider k be Nat such that

           A4: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A3, A2);

          reconsider k as Element of NAT by ORDINAL1:def 12;

          take k;

          thus thesis by A4;

        end;

        then

        consider k such that

         A5: P[k] & for n st P[n] holds n <= k;

        take k;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let a,b be Element of NAT ;

        assume (ex A be Chain of ( Bottom L), x st a = ( card A)) & ((for A be Chain of ( Bottom L), x holds ( card A) <= a) & ex B be Chain of ( Bottom L), x st b = ( card B)) & for A be Chain of ( Bottom L), x holds ( card A) <= b;

        then a <= b & b <= a;

        hence thesis by XXREAL_0: 1;

      end;

    end

    theorem :: LATTICE7:2

    

     Th2: for L be finite LATTICE holds 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;

      (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

       A1: ( height a) = ( card A) and for C be Chain of ( Bottom L), a holds ( card C) <= ( height a);

      set C = (A \/ {b});

      b in {b} by TARSKI:def 1;

      then

       A2: b in C by XBOOLE_0:def 3;

      

       A3: ( Bottom L) <= a by YELLOW_0: 44;

      then ( Bottom L) in A by Def2;

      then

       A4: ( Bottom L) in C by XBOOLE_0:def 3;

      assume

       A5: a < b;

       not b in A

      proof

        assume b in A;

        then b <= a by A3, Def2;

        hence contradiction by A5, ORDERS_2: 6;

      end;

      then

       A6: ( card C) = (( card A) + 1) by CARD_2: 41;

      the InternalRel of L is_strongly_connected_in C

      proof

        let x,y be object;

        x in C & y in C implies [x, y] in the InternalRel of L or [y, x] in the InternalRel of L

        proof

          assume

           A7: x in C & y in C;

          per cases by A7, XBOOLE_0:def 3;

            suppose

             A8: x in A & y in A;

            then

            reconsider x, y as Element of L;

            x <= y or y <= x by A8, ORDERS_2: 11;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose

             A9: x in A & y in {b};

            then

            reconsider x as Element of L;

            ( Bottom L) <= a by YELLOW_0: 44;

            then x <= a by A9, Def2;

            then x < b by A5, ORDERS_2: 7;

            then

             A10: x <= b by ORDERS_2:def 6;

            y = b by A9, TARSKI:def 1;

            hence thesis by A10, ORDERS_2:def 5;

          end;

            suppose

             A11: x in {b} & y in A;

            then

            reconsider y as Element of L;

            ( Bottom L) <= a by YELLOW_0: 44;

            then y <= a by A11, Def2;

            then y < b by A5, ORDERS_2: 7;

            then

             A12: y <= b by ORDERS_2:def 6;

            x = b by A11, TARSKI:def 1;

            hence thesis by A12, ORDERS_2:def 5;

          end;

            suppose

             A13: x in {b} & y in {b};

            then

            reconsider x, y as Element of L;

            x = b by A13, TARSKI:def 1;

            then x <= y by A13, TARSKI:def 1;

            hence thesis by ORDERS_2:def 5;

          end;

        end;

        hence thesis;

      end;

      then

       A14: C is strongly_connected Subset of L by ORDERS_2:def 7;

      

       A15: for z be Element of L st z in C holds ( Bottom L) <= z & z <= b

      proof

        let z be Element of L;

        assume

         A16: z in C;

        per cases by A16, XBOOLE_0:def 3;

          suppose

           A17: z in A;

          thus ( Bottom L) <= z by YELLOW_0: 44;

          z <= a by A3, A17, Def2;

          then z < b by A5, ORDERS_2: 7;

          hence thesis by ORDERS_2:def 6;

        end;

          suppose z in {b};

          hence thesis by TARSKI:def 1, YELLOW_0: 44;

        end;

      end;

      ( Bottom L) <= b by YELLOW_0: 44;

      then C is Chain of ( Bottom L), b by A4, A2, A15, A14, Def2;

      then (( height a) + 1) <= ( height b) by A1, A6, Def3;

      hence thesis by NAT_1: 13;

    end;

    theorem :: LATTICE7:3

    

     Th3: for L be finite LATTICE holds for C be Chain of L holds 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;

      ( height x) < ( height y) implies x < y

      proof

        assume

         A2: ( height x) < ( height y);

        per cases by A1, ORDERS_2: 11;

          suppose x <= y;

          hence thesis by A2, ORDERS_2:def 6;

        end;

          suppose y <= x;

          then x = y or y < x by ORDERS_2:def 6;

          hence thesis by A2, Th2;

        end;

      end;

      hence x < y iff ( height x) < ( height y) by Th2;

    end;

    theorem :: LATTICE7:4

    

     Th4: for L be finite LATTICE holds for C be Chain of L holds 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 that

         A2: ( height x) = ( height y) and

         A3: x <> y;

        

         A4: x <= y or y <= x by A1, ORDERS_2: 11;

        ( height x) <> ( height y)

        proof

          per cases by A3, A4, ORDERS_2:def 6;

            suppose x < y;

            hence thesis by A1, Th3;

          end;

            suppose y < x;

            hence thesis by A1, Th3;

          end;

        end;

        hence contradiction by A2;

      end;

      hence thesis;

    end;

    theorem :: LATTICE7:5

    

     Th5: for L be finite LATTICE holds for C be Chain of L holds 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;

      

       A2: ( height x) <= ( height y) implies x <= y

      proof

        assume ( height x) <= ( height y);

        then ( height x) < ( height y) or ( height x) = ( height y) by XXREAL_0: 1;

        then x < y or ( height x) = ( height y) by A1, Th3;

        hence thesis by A1, Th4, ORDERS_2:def 6;

      end;

      x <= y implies ( height x) <= ( height y)

      proof

        assume x <= y;

        then x < y or x = y by ORDERS_2:def 6;

        hence thesis by A1, Th3;

      end;

      hence x <= y iff ( height x) <= ( height y) by A2;

    end;

    theorem :: LATTICE7:6

    for L be finite LATTICE holds 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: x = ( Bottom L) implies ( height x) = 1

      proof

        

         A2: for B be Chain of ( Bottom L), ( Bottom L) holds B = {( Bottom L)}

        proof

          let B be Chain of ( Bottom L), ( Bottom L);

          

           A3: 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_2: 2;

              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 A3, XBOOLE_0:def 10;

        end;

        assume

         A4: x = ( Bottom L);

        (ex A be Chain of ( Bottom L), ( Bottom L) st ( height ( Bottom L)) = ( card A)) & ( card {( Bottom L)}) = 1 by Def3, CARD_1: 30;

        hence thesis by A4, A2;

      end;

      ( height x) = 1 implies x = ( Bottom L)

      proof

        

         A5: 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

           A6: z in {( Bottom L), x};

          per cases by A6, TARSKI:def 2;

            suppose z = ( Bottom L);

            hence thesis by YELLOW_0: 44;

          end;

            suppose z = x;

            hence thesis by YELLOW_0: 44;

          end;

        end;

        

         A7: x in {( Bottom L), x} & ( Bottom L) in {( Bottom L), x} by TARSKI:def 2;

        

         A8: ( Bottom L) <= x by YELLOW_0: 44;

        then {( Bottom L), x} is Chain of L by ORDERS_2: 9;

        then

         A9: {( Bottom L), x} is Chain of ( Bottom L), x by A8, A7, A5, Def2;

        assume that

         A10: ( height x) = 1 and

         A11: x <> ( Bottom L);

        ( card {( Bottom L), x}) = 2 by A11, CARD_2: 57;

        hence contradiction by A10, A9, Def3;

      end;

      hence thesis by A1;

    end;

    theorem :: LATTICE7:7

    

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

    proof

      let L be non empty finite LATTICE;

      let x be Element of L;

      

       A1: {( Bottom L), x} is Chain of ( Bottom L), x by Th1, YELLOW_0: 44;

      then

       A2: ( card {( Bottom L), x}) <= ( height x) by Def3;

      per cases ;

        suppose x <> ( Bottom L);

        then ( card {( Bottom L), x}) = 2 by CARD_2: 57;

        hence thesis by A2, XXREAL_0: 2;

      end;

        suppose

         A3: x = ( Bottom L);

        

         A4: {( 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;

         {( 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;

        then

         A5: {( Bottom L), ( Bottom L)} = {( Bottom L)} by A4, XBOOLE_0:def 10;

        ( card {( Bottom L), ( Bottom L)}) <= ( height ( Bottom L)) by A1, A3, Def3;

        hence thesis by A3, A5, CARD_1: 30;

      end;

    end;

    scheme :: LATTICE7:sch1

    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];

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

      

       A2: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: Q[n];

        for x be Element of L() st ( height x) <= (n + 1) holds P[x]

        proof

          let x be Element of L();

          assume

           A4: ( height x) <= (n + 1);

          per cases by A3, A4, NAT_1: 8;

            suppose

             A5: ( 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 A5, NAT_1: 13;

              hence thesis by A3;

            end;

            hence thesis by A1;

          end;

            suppose P[x];

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      let x be Element of L();

      

       A6: (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 that

         A7: for x be Element of L() st ( height x) <= ( height x) holds P[x] and

         A8: not (for x be Element of L() holds P[x]);

        consider x be Element of L() such that

         A9: not P[x] by A8;

        ( height x) <= ( height x) implies P[x] by A7;

        hence contradiction by A9;

      end;

      

       A10: Q[ 0 ] by Th7;

      for n be Nat holds Q[n] from NAT_1:sch 2( A10, A2);

      hence thesis by A6;

    end;

    begin

    registration

      cluster distributive finite for LATTICE;

      existence

      proof

        set D = { {} };

        set R = the 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;

      :: LATTICE7:def4

      pred x <(1) y means x < y & not (ex z be Element of L st x < z & z < y);

    end

    theorem :: LATTICE7:8

    

     Th8: for L be finite LATTICE holds 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 be Nat st P[k] holds k <= ( card the carrier of L)

        proof

          let k be Nat;

          assume P[k];

          then

          consider x be Element of L such that x in X and

           A2: k = ( height x);

          ex B be Chain of ( Bottom L), x st k = ( card B) by A2, Def3;

          hence thesis by NAT_1: 43;

        end;

        

         A3: ex k be Nat st P[k]

        proof

          consider x be object such that

           A4: x in X by XBOOLE_0:def 1;

          reconsider x as Element of L by A4;

          ex B be Chain of ( Bottom L), x st ( height x) = ( card B) by Def3;

          hence thesis by A4;

        end;

        consider k be Nat such that

         A5: P[k] and

         A6: for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A1, A3);

        for n be Element of NAT st P[n] holds n <= k by A6;

        hence thesis by A5;

      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 and

       A9: 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 that

         A10: y in X and

         A11: x < y;

        ( height x) < ( height y) by A11, Th2;

        hence contradiction by A9, A10;

      end;

      hence thesis by A8;

    end;

    definition

      let L be finite LATTICE;

      let A be non empty Chain of L;

      :: LATTICE7:def5

      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 be Nat st P[k] holds k <= ( card the carrier of L)

          proof

            let k be Nat;

            assume P[k];

            then

            consider x be Element of L such that x in A and

             A2: k = ( height x);

            ex B be Chain of ( Bottom L), x st k = ( card B) by A2, Def3;

            hence thesis by NAT_1: 43;

          end;

          

           A3: ex k be Nat st P[k]

          proof

            consider x be object such that

             A4: x in A by XBOOLE_0:def 1;

            reconsider x as Element of L by A4;

            ex B be Chain of ( Bottom L), x st ( height x) = ( card B) by Def3;

            hence thesis by A4;

          end;

          consider k be Nat such that

           A5: P[k] and

           A6: for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A1, A3);

          for n be Element of NAT st P[n] holds n <= k by A6;

          hence thesis by A5;

        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 and

         A9: k = ( height x) & 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 A9;

          hence thesis by A8, A10, Th5;

        end;

        thus thesis by A8;

      end;

      uniqueness

      proof

        let s,t be Element of L;

        assume (for x be Element of L st x in A holds x <= s) & (s in A & for y be Element of L st y in A holds y <= t) & t in A;

        then t <= s & s <= t;

        hence thesis by ORDERS_2: 2;

      end;

    end

    theorem :: LATTICE7:9

    

     Th9: for L be finite LATTICE holds 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;

      (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

       A1: ( height y) = ( card A) & for A be Chain of ( Bottom L), y holds ( card A) <= ( height y);

      set B = (A \ {y});

      

       A2: the InternalRel of L is_strongly_connected_in B

      proof

        let p,q be object;

        p in B & q in B implies [p, q] in the InternalRel of L or [q, p] in the InternalRel of L

        proof

          assume

           A3: p in B & q in B;

          then

           A4: p in A & q in A by XBOOLE_0:def 5;

          reconsider p, q as Element of L by A3;

          p <= q or q <= p by A4, ORDERS_2: 11;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis;

      end;

      assume

       A5: y <> ( Bottom L);

      B is non empty

      proof

        ( Bottom L) <= y by YELLOW_0: 44;

        then

         A6: ( Bottom L) in A by Def2;

        assume

         A7: B is empty;

         not ( Bottom L) in {y} by A5, TARSKI:def 1;

        hence contradiction by A7, A6, XBOOLE_0:def 5;

      end;

      then

      reconsider B as non empty Chain of L by A2, ORDERS_2:def 7;

      take x = ( max B);

      

       A8: not ex z be Element of L st x < z & z < y

      proof

        given z be Element of L such that

         A9: x < z and

         A10: z < y;

        

         A11: ( Bottom L) <= y by YELLOW_0: 44;

        then y in A by Def2;

        then

         A12: y in (A \/ {z}) by XBOOLE_0:def 3;

        set C = (A \/ {z});

         {y} c= A

        proof

          let h be Element of L;

          assume h in {y};

          then

           A13: h = y by TARSKI:def 1;

          ( Bottom L) <= y by YELLOW_0: 44;

          hence thesis by A13, Def2;

        end;

        then

         A14: A = ((A \ {y}) \/ {y}) by XBOOLE_1: 45;

        the InternalRel of L is_strongly_connected_in C

        proof

          let x1,y1 be object;

          x1 in C & y1 in C implies [x1, y1] in the InternalRel of L or [y1, x1] in the InternalRel of L

          proof

            assume

             A15: x1 in C & y1 in C;

            per cases by A15, XBOOLE_0:def 3;

              suppose

               A16: x1 in A & y1 in A;

              then

              reconsider x1, y1 as Element of L;

              x1 <= y1 or y1 <= x1 by A16, ORDERS_2: 11;

              hence thesis by ORDERS_2:def 5;

            end;

              suppose

               A17: x1 in A & y1 in {z};

              then

               A18: y1 = z by TARSKI:def 1;

              reconsider x1, y1 as Element of L by A17;

              x1 in (A \ {y}) or x1 in {y} by A14, A17, XBOOLE_0:def 3;

              then x1 <= x or x1 = y by Def5, TARSKI:def 1;

              then x1 < y1 or x1 = y by A9, A18, ORDERS_2: 7;

              then x1 <= y1 or y1 < x1 by A10, A17, ORDERS_2:def 6, TARSKI:def 1;

              then x1 <= y1 or y1 <= x1 by ORDERS_2:def 6;

              hence thesis by ORDERS_2:def 5;

            end;

              suppose

               A19: y1 in A & x1 in {z};

              then

               A20: x1 = z by TARSKI:def 1;

              reconsider x1, y1 as Element of L by A19;

              y1 in (A \ {y}) or y1 in {y} by A14, A19, XBOOLE_0:def 3;

              then y1 <= x or y1 = y by Def5, TARSKI:def 1;

              then y1 < x1 or y1 = y by A9, A20, ORDERS_2: 7;

              then y1 <= x1 or x1 <= y1 by A10, A20, ORDERS_2:def 6;

              hence thesis by ORDERS_2:def 5;

            end;

              suppose

               A21: x1 in {z} & y1 in {z};

              then

              reconsider x1, y1 as Element of L;

              x1 = z by A21, TARSKI:def 1;

              then x1 <= y1 by A21, TARSKI:def 1;

              hence thesis by ORDERS_2:def 5;

            end;

          end;

          hence thesis;

        end;

        then

         A22: C is strongly_connected Subset of L by ORDERS_2:def 7;

        

         A23: z <= y by A10, ORDERS_2:def 6;

        

         A24: 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

           A25: v in (A \/ {z});

          per cases by A25, XBOOLE_0:def 3;

            suppose

             A26: v in A;

            thus ( Bottom L) <= v by YELLOW_0: 44;

            thus thesis by A11, A26, Def2;

          end;

            suppose v in {z};

            hence thesis by A23, TARSKI:def 1, YELLOW_0: 44;

          end;

        end;

         not z in A

        proof

          assume

           A27: z in A;

           not z in {y} by A10, TARSKI:def 1;

          then z in B by A27, XBOOLE_0:def 5;

          then z <= x by Def5;

          hence contradiction by A9, ORDERS_2: 7;

        end;

        then

         A28: ( card (A \/ {z})) = (( card A) + 1) by CARD_2: 41;

        ( Bottom L) in A by A11, Def2;

        then ( Bottom L) in (A \/ {z}) by XBOOLE_0:def 3;

        then (A \/ {z}) is Chain of ( Bottom L), y by A22, A11, A12, A24, Def2;

        then (( card A) + 1) <= ( card A) by A1, A28;

        hence contradiction by NAT_1: 13;

      end;

      

       A29: x in B by Def5;

      then not x in {y} by XBOOLE_0:def 5;

      then

       A30: not x = y by TARSKI:def 1;

      ( Bottom L) <= y & x in A by A29, XBOOLE_0:def 5, YELLOW_0: 44;

      then x <= y by Def2;

      then x < y by A30, ORDERS_2:def 6;

      hence thesis by A8;

    end;

    definition

      let L be LATTICE;

      :: LATTICE7:def6

      func Join-IRR L -> Subset of L equals { a where a be 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 be 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 object;

          assume x in { a where a be 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 be 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 :: LATTICE7:10

    

     Th10: for L be LATTICE holds 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;

      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 be 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;

      thus thesis;

    end;

    theorem :: LATTICE7:11

    

     Th11: for L be finite distributive LATTICE holds 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) by Th10;

      then

      consider z be Element of L such that

       A2: z <(1) x by Th9;

      

       A3: z < x by A2;

      for y be Element of L st y < x holds y <= z

      proof

        let y be Element of L;

        consider Y be set such that

         A4: Y = { g where g be Element of L : g < x & not (g <= z) };

        

         A5: Y is empty

        proof

          

           A6: Y c= the carrier of L

          proof

            let f be object;

            assume f in Y;

            then ex g be Element of L st g = f & g < x & not g <= z by A4;

            hence thesis;

          end;

          assume Y is non empty;

          then

          consider a be Element of L such that

           A7: a in Y and

           A8: for b be Element of L st b in Y holds not a < b by A6, Th8;

          

           A9: 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 ex g be Element of L st g = t & g < x & not g <= z by A4;

              hence thesis;

            end;

            hence thesis by A4;

          end;

          then

           A10: not a <= z by A7;

          

           A11: z <= x by A3, ORDERS_2:def 6;

          a < x by A9, A7;

          then

           A12: (a "\/" z) <> x by A1, A3, Th10;

          a < x by A9, A7;

          then a <= x by ORDERS_2:def 6;

          then (a "\/" z) <= x by A11, YELLOW_5: 9;

          then

           A13: (a "\/" z) < x by A12, ORDERS_2:def 6;

          (a "/\" a) <= (a "\/" z) by YELLOW_5: 5;

          then

           A14: a <= (a "\/" z) by YELLOW_5: 2;

          a <> (a "\/" z)

          proof

            assume a = (a "\/" z);

            (z "/\" z) <= (a "\/" z) by YELLOW_5: 5;

            then z <= (a "\/" z) by YELLOW_5: 2;

            then z < (a "\/" z) by A10, A14, ORDERS_2:def 6;

            hence contradiction by A2, A13;

          end;

          then

           A15: (a "\/" z) > a by A14, ORDERS_2:def 6;

           not (a "\/" z) <= z by A10, YELLOW_5: 3;

          then (a "\/" z) in Y by A9, A13;

          hence contradiction by A8, A15;

        end;

        assume y < x & not y <= z;

        then y in Y by A4;

        hence contradiction by A5;

      end;

      hence thesis by A3;

    end;

    

     Lm1: for L be finite distributive LATTICE holds for a be 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);

          

           A3: ( {( Bottom L)} /\ ( Join-IRR L)) = {}

          proof

            set x = the Element of ( {( Bottom L)} /\ ( Join-IRR L));

            assume

             A4: ( {( Bottom L)} /\ ( Join-IRR L)) <> {} ;

            then x in {( Bottom L)} by XBOOLE_0:def 4;

            then

             A5: x = ( Bottom L) by TARSKI:def 1;

            x in ( Join-IRR L) by A4, XBOOLE_0:def 4;

            hence contradiction by A5, Th10;

          end;

          ( downarrow a) = {( Bottom L)} by A2, WAYBEL_4: 23;

          hence thesis by A2, A3, YELLOW_0:def 11;

        end;

          suppose ( not a in ( Join-IRR L)) & a <> ( Bottom L);

          then

          consider y,z be Element of L such that

           A6: a = (y "\/" z) and

           A7: a <> y and

           A8: a <> z;

          

           A9: y <= a by A6, YELLOW_0: 22;

          then

           A10: y < a by A7, ORDERS_2:def 6;

          

           A11: (( downarrow a) /\ ( Join-IRR L)) c= ((( downarrow y) /\ ( Join-IRR L)) \/ (( downarrow z) /\ ( Join-IRR L)))

          proof

            let x be Element of L;

            set x1 = x, y1 = y, a1 = a, z1 = z;

            assume

             A12: x in (( downarrow a) /\ ( Join-IRR L));

            then

             A13: x in ( Join-IRR L) by XBOOLE_0:def 4;

            x in ( downarrow a) by A12, XBOOLE_0:def 4;

            then

             A14: x1 <= a1 by WAYBEL_0: 17;

            (x1 "/\" a1) = ((x1 "/\" y1) "\/" (x1 "/\" z1)) by A6, WAYBEL_1:def 3;

            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 4;

            hence thesis by XBOOLE_0:def 3;

          end;

          

           A15: ex_sup_of (((( downarrow y) /\ ( Join-IRR L)) \/ (( downarrow z) /\ ( Join-IRR L))),L) & ex_sup_of ((( downarrow y) /\ ( Join-IRR L)),L) by YELLOW_0: 17;

          

           A16: ex_sup_of ((( downarrow z) /\ ( Join-IRR L)),L) by YELLOW_0: 17;

          

           A17: z <= a by A6, YELLOW_0: 22;

          ((( downarrow y) /\ ( Join-IRR L)) \/ (( downarrow z) /\ ( Join-IRR L))) c= (( downarrow a) /\ ( Join-IRR L))

          proof

            let x be Element of L;

            (( downarrow y) /\ ( Join-IRR L)) c= (( downarrow a) /\ ( Join-IRR L)) & (( downarrow z) /\ ( Join-IRR L)) c= (( downarrow a) /\ ( Join-IRR L)) by A9, A17, WAYBEL_0: 21, XBOOLE_1: 26;

            then

             A18: ((( downarrow y) /\ ( Join-IRR L)) \/ (( downarrow z) /\ ( Join-IRR L))) c= (( downarrow a) /\ ( Join-IRR L)) by XBOOLE_1: 8;

            assume x in ((( downarrow y) /\ ( Join-IRR L)) \/ (( downarrow z) /\ ( Join-IRR L)));

            hence thesis by A18;

          end;

          then (( downarrow a) /\ ( Join-IRR L)) = ((( downarrow y) /\ ( Join-IRR L)) \/ (( downarrow z) /\ ( Join-IRR L))) by A11, XBOOLE_0:def 10;

          then ( sup (( downarrow a) /\ ( Join-IRR L))) = (( sup (( downarrow y) /\ ( Join-IRR L))) "\/" ( sup (( downarrow z) /\ ( Join-IRR L)))) by A15, A16, YELLOW_0: 36;

          then

           A19: ( sup (( downarrow a) /\ ( Join-IRR L))) = (y "\/" ( sup (( downarrow z) /\ ( Join-IRR L)))) by A1, A10;

          z < a by A8, A17, ORDERS_2:def 6;

          hence thesis by A1, A6, A19;

        end;

          suppose

           A20: a in ( Join-IRR L);

          a <= a;

          then a in ( downarrow a) by WAYBEL_0: 17;

          then a in (( downarrow a) /\ ( Join-IRR L)) by A20, XBOOLE_0:def 4;

          then

           A21: a <= ( sup (( downarrow a) /\ ( Join-IRR L))) by YELLOW_0: 17, YELLOW_4: 1;

           ex_sup_of ((( downarrow a) /\ ( Join-IRR L)),L) & ex_sup_of (( downarrow a),L) by YELLOW_0: 17;

          then ( sup (( downarrow a) /\ ( Join-IRR L))) <= ( sup ( downarrow a)) by XBOOLE_1: 17, YELLOW_0: 34;

          then ( sup (( downarrow a) /\ ( Join-IRR L))) <= a by WAYBEL_0: 34;

          hence thesis by A21, ORDERS_2: 2;

        end;

      end;

    end;

    theorem :: LATTICE7:12

    

     Th12: for L be distributive finite LATTICE holds 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: x <= ( sup (( downarrow x) /\ ( Join-IRR L)))

      proof

        defpred X[ Element of L] means ( sup (( downarrow $1) /\ ( Join-IRR L))) = $1;

        

         A2: for x be Element of L st for b be Element of L st b < x holds X[b] holds X[x] by Lm1;

        for x be Element of L holds X[x] from LattInd( A2);

        hence thesis;

      end;

       ex_sup_of ((( downarrow x) /\ ( Join-IRR L)),L) & ex_sup_of (( downarrow x),L) by YELLOW_0: 17;

      then ( sup (( downarrow x) /\ ( Join-IRR L))) <= ( sup ( downarrow x)) by XBOOLE_1: 17, YELLOW_0: 34;

      then ( sup (( downarrow x) /\ ( Join-IRR L))) <= x by WAYBEL_0: 34;

      hence thesis by A1, ORDERS_2: 2;

    end;

    begin

    definition

      let P be RelStr;

      :: LATTICE7:def7

      func LOWER (P) -> non empty set equals { X where X be Subset of P : X is lower };

      coherence

      proof

        ( {} P) in { X where X be Subset of P : X is lower };

        hence thesis;

      end;

    end

    theorem :: LATTICE7:13

    

     Th13: for L be distributive finite LATTICE holds ex r be Function of L, ( InclPoset ( LOWER ( subrelstr ( Join-IRR L)))) st r is isomorphic & for a be 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 PBOOLE:sch 5;

      

       A2: ( rng r) c= the carrier of I

      proof

        let t be object;

        reconsider tt = t as set by TARSKI: 1;

        assume t in ( rng r);

        then

        consider x be object such that

         A3: x in ( dom r) and

         A4: t = (r . x) by FUNCT_1:def 3;

        reconsider x as Element of L by A3;

        

         A5: t = (( downarrow x) /\ ( Join-IRR L)) by A1, A4;

        then tt c= ( Join-IRR L) by XBOOLE_1: 17;

        then

        reconsider t as Subset of ( subrelstr ( Join-IRR L)) by YELLOW_0:def 15;

        

         A6: t is lower

        proof

          let c,d be Element of ( subrelstr ( Join-IRR L));

          assume that

           A7: c in t and

           A8: d <= c;

          

           A9: d is Element of ( Join-IRR L) by YELLOW_0:def 15;

          

           A10: ( Join-IRR L) is non empty by A5, A7;

          then d in ( Join-IRR L) by A9;

          then

          reconsider c1 = c, d1 = d as Element of L by A5, A7;

          c in ( downarrow x) by A5, A7, XBOOLE_0:def 4;

          then

           A11: c1 <= x by WAYBEL_0: 17;

          d1 <= c1 by A8, YELLOW_0: 59;

          then d1 <= x by A11, ORDERS_2: 3;

          then d1 in ( downarrow x) by WAYBEL_0: 17;

          hence thesis by A5, A10, A9, XBOOLE_0:def 4;

        end;

        the carrier of I = ( LOWER ( subrelstr ( Join-IRR L))) by YELLOW_1: 1;

        hence thesis by A6;

      end;

      ( dom r) = the carrier of L by PARTFUN1:def 2;

      then

      reconsider r as Function of L, I by A2, FUNCT_2:def 1, RELSET_1: 4;

      

       A12: for x,y be 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

           A13: 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

             A14: a in ( downarrow x) & a in ( Join-IRR L) by XBOOLE_0:def 4;

            ( downarrow x) c= ( downarrow y) by A13, WAYBEL_0: 21;

            hence thesis by A14, XBOOLE_0:def 4;

          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

          (r . x) = (( downarrow x) /\ ( Join-IRR L)) & (r . y) = (( downarrow y) /\ ( Join-IRR L)) by A1;

          then

          reconsider rx = (r . x), ry = (r . y) as Subset of L;

          assume (r . x) <= (r . y);

          then

           A15: rx c= ry by YELLOW_1: 3;

           ex_sup_of (rx,L) & ex_sup_of (ry,L) by YELLOW_0: 17;

          then ( sup rx) <= ( sup ry) by A15, 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;

      the carrier of I c= ( rng r)

      proof

        let x be object;

        assume

         A16: x in the carrier of I;

        thus x in ( rng r)

        proof

          x in ( LOWER ( subrelstr ( Join-IRR L))) by A16, YELLOW_1: 1;

          then

          consider X be Subset of ( subrelstr ( Join-IRR L)) such that

           A17: x = X and

           A18: X is lower;

          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

          reconsider X1 = X as Subset of L by XBOOLE_1: 1;

          ex y be 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);

            

             A19: (( downarrow ( sup X1)) /\ ( Join-IRR L)) c= X1

            proof

              let r be Element of L;

              reconsider r1 = r as Element of L;

              assume

               A20: r in (( downarrow ( sup X1)) /\ ( Join-IRR L));

              then r in ( downarrow ( sup X1)) by XBOOLE_0:def 4;

              then

               A21: r1 <= ( sup X1) by WAYBEL_0: 17;

              per cases ;

                suppose r1 in X1;

                hence thesis;

              end;

                suppose

                 A22: not r1 in X1;

                

                 A23: r1 in ( Join-IRR L) by A20, XBOOLE_0:def 4;

                then

                consider z be Element of L such that

                 A24: z < r1 and

                 A25: for y be Element of L st y < r1 holds y <= z by Th11;

                ( {r1} "/\" X1) is_<=_than z

                proof

                  let a be Element of L;

                  

                   A26: r1 in the carrier of ( subrelstr ( Join-IRR L)) by A23, YELLOW_0:def 15;

                  assume a in ( {r1} "/\" X1);

                  then a in { (r1 "/\" k) where k be Element of L : k in X1 } by YELLOW_4: 42;

                  then

                  consider x be Element of L such that

                   A27: a = (r1 "/\" x) and

                   A28: x in X1;

                  reconsider r9 = r1, x9 = x as Element of ( subrelstr ( Join-IRR L)) by A23, A28, YELLOW_0:def 15;

                  

                   A29: ex_inf_of ( {r1, x},L) by YELLOW_0: 17;

                  then

                   A30: a <= x by A27, YELLOW_0: 19;

                  

                   A31: a <> r1 by A18, A22, A28, A30, A26, YELLOW_0: 60;

                  a <= r1 by A27, A29, YELLOW_0: 19;

                  then a < r1 by A31, ORDERS_2:def 6;

                  hence thesis by A25;

                end;

                then

                 A32: ( sup ( {r1} "/\" X1)) <= z by YELLOW_0: 32;

                r1 = (r1 "/\" ( sup X1)) & (r1 "/\" ( sup X1)) = ( sup ( {r1} "/\" X1)) by A21, WAYBEL_2: 15, YELLOW_0: 25;

                hence thesis by A24, A32, ORDERS_2: 7;

              end;

            end;

            X1 c= (( downarrow ( sup X1)) /\ ( Join-IRR L))

            proof

              let a be Element of L;

              assume

               A33: a in X1;

              set A = a;

               ex_sup_of (X1,L) by YELLOW_0: 17;

              then

               A34: X1 is_<=_than ( "\/" (X1,L)) by YELLOW_0:def 9;

              ex y be 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 thesis by A33, A34;

              end;

              then

               A35: A in ( downarrow {( sup X1)}) by WAYBEL_0:def 15;

              X is Subset of ( Join-IRR L) by YELLOW_0:def 15;

              hence a in (( downarrow ( sup X1)) /\ ( Join-IRR L)) by A33, A35, XBOOLE_0:def 4;

            end;

            then X1 = (( downarrow ( sup X1)) /\ ( Join-IRR L)) by A19, XBOOLE_0:def 10;

            hence x = (r . y) by A1, A17;

          end;

          hence thesis by FUNCT_1:def 3;

        end;

      end;

      then

       A36: ( rng r) = the carrier of I by XBOOLE_0:def 10;

      r is one-to-one

      proof

        let x,y be Element of L;

        (r . y) = (( downarrow y) /\ ( Join-IRR L)) by A1;

        then

        reconsider ry = (r . y) as Subset of L;

        assume (r . x) = (r . y);

        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;

      then r is isomorphic by A36, A12, WAYBEL_0: 66;

      hence thesis by A1;

    end;

    theorem :: LATTICE7:14

    

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

    proof

      let L be distributive finite LATTICE;

      ex r be Function of L, ( InclPoset ( LOWER ( subrelstr ( Join-IRR L)))) st r is isomorphic & for a be Element of L holds (r . a) = (( downarrow a) /\ ( Join-IRR L)) by Th13;

      hence thesis;

    end;

    definition

      :: LATTICE7:def8

      mode Ring_of_sets -> set means

      : Def8: it includes_lattice_of it ;

      existence

      proof

        set X = the set;

        take R = ( bool X);

        let a,b be set;

        assume that

         A1: a in R and

         A2: b in R;

        (a /\ b) c= X by A1, XBOOLE_1: 108;

        hence (a /\ b) in R;

        (a \/ b) c= X by A1, A2, XBOOLE_1: 8;

        hence thesis;

      end;

    end

    registration

      cluster non empty for Ring_of_sets;

      existence

      proof

        take A = { {} };

        A includes_lattice_of A

        proof

          let a,b be set;

          assume that

           A1: a in A and

           A2: b in A;

          a = {} by A1, TARSKI:def 1;

          hence thesis by A2, TARSKI:def 1;

        end;

        hence thesis by Def8;

      end;

    end

    

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

    

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

    registration

      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 distributive

        proof

          let x,y,z be Element of ( InclPoset X);

          x in the carrier of ( InclPoset X);

          then

           A3: x in X by YELLOW_1: 1;

          z in the carrier of ( InclPoset X);

          then

           A4: z in X by YELLOW_1: 1;

          then

           A5: (x /\ z) in X by A1, A3;

          then

           A6: (x "/\" z) = (x /\ z) by YELLOW_1: 9;

          y in the carrier of ( InclPoset X);

          then

           A7: y in X by YELLOW_1: 1;

          then

           A8: (y \/ z) in X by A1, A4;

          then

          reconsider r = (y \/ z) as Element of ( InclPoset X) by YELLOW_1: 1;

          

           A9: (x /\ y) in X by A1, A3, A7;

          then

          reconsider r1 = (x /\ y), r2 = (x /\ z) as Element of ( InclPoset X) by A5, YELLOW_1: 1;

          r1 in the carrier of ( InclPoset X);

          then

           A10: r1 in X by YELLOW_1: 1;

          r in the carrier of ( InclPoset X);

          then r in X by YELLOW_1: 1;

          then (x /\ r) in X by A1, A3;

          then (x "/\" r) = (x /\ r) by YELLOW_1: 9;

          then

           A11: (x /\ (y \/ z)) = ((x /\ y) \/ (x /\ z)) & (x /\ (y \/ z)) = (x "/\" (y "\/" z)) by A8, XBOOLE_1: 23, YELLOW_1: 8;

          r2 in the carrier of ( InclPoset X);

          then r2 in X by YELLOW_1: 1;

          then

           A12: (r1 \/ r2) in X by A1, A10;

          (x "/\" y) = (x /\ y) by A9, YELLOW_1: 9;

          hence thesis by A11, A6, A12, YELLOW_1: 8;

        end;

        (for x,y be set st x in X & y in X holds (x /\ y) in X) & for x,y be set st x in X & y in X holds (x \/ y) in X by A1;

        hence thesis by A2, YELLOW_1: 11, YELLOW_1: 12;

      end;

    end

    theorem :: LATTICE7:15

    

     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 that

         A1: a in X and

         A2: b in X;

        

         A3: (a \/ b) in X

        proof

          consider Z1 be Subset of ( subrelstr ( Join-IRR L)) such that

           A4: b = Z1 and

           A5: Z1 is lower by A2;

          consider Z be Subset of ( subrelstr ( Join-IRR L)) such that

           A6: a = Z and

           A7: Z is lower by A1;

          (Z \/ Z1) is lower by A7, A5, WAYBEL_0: 27;

          hence thesis by A6, A4;

        end;

        (a /\ b) in X

        proof

          consider Z1 be Subset of ( subrelstr ( Join-IRR L)) such that

           A8: b = Z1 and

           A9: Z1 is lower by A2;

          consider Z be Subset of ( subrelstr ( Join-IRR L)) such that

           A10: a = Z and

           A11: Z is lower by A1;

          (Z /\ Z1) is lower by A11, A9, WAYBEL_0: 27;

          hence thesis by A10, A8;

        end;

        hence thesis by A3;

      end;

      hence thesis by Def8;

    end;

    theorem :: LATTICE7:16

    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

        consider X be set such that

         A1: X = ( LOWER ( subrelstr ( Join-IRR L)));

        

         A2: X is Ring_of_sets by A1, Th15;

        assume L is distributive;

        then (L,( InclPoset X)) are_isomorphic by A1, Th14;

        hence thesis by A1, A2;

      end;

      given X be non empty Ring_of_sets such that

       A3: (L,( InclPoset X)) are_isomorphic ;

      consider f be Function of L, ( InclPoset X) such that

       A4: f is isomorphic by A3;

      

       A5: f is one-to-one by A4, WAYBEL_0: 66;

      f is infs-preserving & f is join-preserving by A4, Lm3, WAYBEL13: 20;

      hence thesis by A5, Lm2, WAYBEL_6: 3;

    end;