waybel_2.miz

    begin

    registration

      let X,Y be non empty set, f be Function of X, Y, Z be non empty Subset of X;

      cluster (f .: Z) -> non empty;

      coherence

      proof

        set x = the Element of Z;



         A1: ( dom f) = X by FUNCT_2:def 1;

        thus thesis by A1;

      end;

    end

    registration

      cluster reflexive connected -> with_infima with_suprema for non empty RelStr;

      coherence

      proof

        let L be non empty RelStr such that

         A1: L is reflexive connected;

        thus L is with_infima

        proof

          let x,y be Element of L;

          per cases by A1;

            suppose

             A2: x <= y;

            take z = x;

            thus z <= x & z <= y by A1, A2;

            thus thesis;

          end;

            suppose

             A3: y <= x;

            take z = y;

            thus z <= x & z <= y by A1, A3;

            thus thesis;

          end;

        end;

        let x,y be Element of L;

        per cases by A1;

          suppose

           A4: x <= y;

          take z = y;

          thus z >= x & z >= y by A1, A4;

          thus thesis;

        end;

          suppose

           A5: y <= x;

          take z = x;

          thus z >= x & z >= y by A1, A5;

          thus thesis;

        end;

      end;

    end

    registration

      let C be Chain;

      cluster ( [#] C) -> directed;

      coherence ;

    end

    theorem :: WAYBEL_2:1



     Th1: for L be up-complete Semilattice holds for D be non empty directed Subset of L, x be Element of L holds ex_sup_of (( {x} "/\" D),L)

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of L, x be Element of L;

      reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0: 5;

       ex_sup_of ((xx "/\" D),L) by WAYBEL_0: 75;

      hence thesis;

    end;

    theorem :: WAYBEL_2:2

    for L be up-complete sup-Semilattice holds for D be non empty directed Subset of L, x be Element of L holds ex_sup_of (( {x} "\/" D),L)

    proof

      let L be up-complete sup-Semilattice, D be non empty directed Subset of L, x be Element of L;

      reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0: 5;

       ex_sup_of ((xx "\/" D),L) by WAYBEL_0: 75;

      hence thesis;

    end;

    theorem :: WAYBEL_2:3



     Th3: for L be up-complete sup-Semilattice holds for A,B be non empty directed Subset of L holds A is_<=_than ( sup (A "\/" B))

    proof

      let L be up-complete sup-Semilattice, A,B be non empty directed Subset of L;



       A1: (A "\/" B) = { (x "\/" y) where x,y be Element of L : x in A & y in B } by YELLOW_4:def 3;

      set b = the Element of B;

      let x be Element of L;

      assume x in A;

      then

       A2: (x "\/" b) in (A "\/" B) by A1;

      ex xx be Element of L st x <= xx & b <= xx & for c be Element of L st x <= c & b <= c holds xx <= c by LATTICE3:def 10;

      then

       A3: x <= (x "\/" b) by LATTICE3:def 13;

       ex_sup_of ((A "\/" B),L) by WAYBEL_0: 75;

      then (A "\/" B) is_<=_than ( sup (A "\/" B)) by YELLOW_0:def 9;

      then (x "\/" b) <= ( sup (A "\/" B)) by A2;

      hence x <= ( sup (A "\/" B)) by A3, YELLOW_0:def 2;

    end;

    theorem :: WAYBEL_2:4



     Th4: for L be up-complete sup-Semilattice holds for A,B be non empty directed Subset of L holds ( sup (A "\/" B)) = (( sup A) "\/" ( sup B))

    proof

      let L be up-complete sup-Semilattice, A,B be non empty directed Subset of L;



       A1: ex_sup_of (B,L) by WAYBEL_0: 75;

      then

       A2: B is_<=_than ( sup B) by YELLOW_0: 30;



       A3: ex_sup_of (A,L) by WAYBEL_0: 75;

      then A is_<=_than ( sup A) by YELLOW_0: 30;

      then ex_sup_of ((A "\/" B),L) & (A "\/" B) is_<=_than (( sup A) "\/" ( sup B)) by A2, WAYBEL_0: 75, YELLOW_4: 27;

      then

       A4: ( sup (A "\/" B)) <= (( sup A) "\/" ( sup B)) by YELLOW_0:def 9;

      B is_<=_than ( sup (A "\/" B)) by Th3;

      then

       A5: ( sup B) <= ( sup (A "\/" B)) by A1, YELLOW_0: 30;

      A is_<=_than ( sup (A "\/" B)) by Th3;

      then ( sup A) <= ( sup (A "\/" B)) by A3, YELLOW_0: 30;

      then

       A6: (( sup A) "\/" ( sup B)) <= (( sup (A "\/" B)) "\/" ( sup (A "\/" B))) by A5, YELLOW_3: 3;

      ( sup (A "\/" B)) <= ( sup (A "\/" B));

      then (( sup (A "\/" B)) "\/" ( sup (A "\/" B))) = ( sup (A "\/" B)) by YELLOW_0: 24;

      hence thesis by A4, A6, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_2:5



     Th5: for L be up-complete Semilattice holds for D be non empty directed Subset of [:L, L:] holds { ( sup ( {x} "/\" ( proj2 D))) where x be Element of L : x in ( proj1 D) } = { ( sup X) where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) }

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of [:L, L:];

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" ( proj2 D)) & x in ( proj1 D);

      reconsider D1 = ( proj1 D), D2 = ( proj2 D) as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;

      thus { ( sup ( {x} "/\" ( proj2 D))) where x be Element of L : x in ( proj1 D) } c= { ( sup X) where X be non empty directed Subset of L : P[X] }

      proof

        let q be object;

        assume q in { ( sup ( {x} "/\" ( proj2 D))) where x be Element of L : x in ( proj1 D) };

        then

        consider x be Element of L such that

         A1: q = ( sup ( {x} "/\" D2)) & x in D1;

        reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0: 5;

        (xx "/\" D2) is non empty directed;

        hence thesis by A1;

      end;

      let q be object;

      assume q in { ( sup X) where X be non empty directed Subset of L : P[X] };

      then ex X be non empty directed Subset of L st q = ( sup X) & P[X];

      hence thesis;

    end;

    theorem :: WAYBEL_2:6



     Th6: for L be Semilattice, D be non empty directed Subset of [:L, L:] holds ( union { X where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) }) = (( proj1 D) "/\" ( proj2 D))

    proof

      let L be Semilattice, D be non empty directed Subset of [:L, L:];

      set D1 = ( proj1 D), D2 = ( proj2 D);

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" ( proj2 D)) & x in ( proj1 D);

      reconsider T = D2 as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;



       A1: (D1 "/\" D2) = { (x "/\" y) where x,y be Element of L : x in D1 & y in D2 } by YELLOW_4:def 4;

      thus ( union { X where X be non empty directed Subset of L : P[X] }) c= (D1 "/\" D2)

      proof

        let q be object;

        assume q in ( union { X where X be non empty directed Subset of L : P[X] });

        then

        consider w be set such that

         A2: q in w and

         A3: w in { X where X be non empty directed Subset of L : P[X] } by TARSKI:def 4;

        consider e be non empty directed Subset of L such that

         A4: w = e and

         A5: P[e] by A3;

        consider p be Element of L such that

         A6: e = ( {p} "/\" D2) and

         A7: p in D1 by A5;

        ( {p} "/\" D2) = { (p "/\" y) where y be Element of L : y in D2 } by YELLOW_4: 42;

        then ex y be Element of L st q = (p "/\" y) & y in D2 by A2, A4, A6;

        hence thesis by A1, A7;

      end;

      let q be object;

      assume q in (D1 "/\" D2);

      then

      consider x,y be Element of L such that

       A8: q = (x "/\" y) and

       A9: x in D1 and

       A10: y in D2 by A1;

      reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0: 5;

      (xx "/\" T) is non empty directed;

      then

       A11: ( {x} "/\" D2) in { X where X be non empty directed Subset of L : P[X] } by A9;

      ( {x} "/\" D2) = { (x "/\" d) where d be Element of L : d in D2 } by YELLOW_4: 42;

      then q in ( {x} "/\" D2) by A8, A10;

      hence thesis by A11, TARSKI:def 4;

    end;

    theorem :: WAYBEL_2:7



     Th7: for L be up-complete Semilattice holds for D be non empty directed Subset of [:L, L:] holds ex_sup_of (( union { X where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) }),L)

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of [:L, L:];

      reconsider D1 = ( proj1 D), D2 = ( proj2 D) as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;

      set A = { X where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" D2) & x in D1 };

      ( union A) c= the carrier of L

      proof

        let q be object;

        assume q in ( union A);

        then

        consider r be set such that

         A1: q in r and

         A2: r in A by TARSKI:def 4;

        ex s be non empty directed Subset of L st r = s & ex x be Element of L st s = ( {x} "/\" D2) & x in D1 by A2;

        hence thesis by A1;

      end;

      then

      reconsider S = ( union A) as Subset of L;

      S = (D1 "/\" D2) by Th6;

      hence thesis by WAYBEL_0: 75;

    end;

    theorem :: WAYBEL_2:8



     Th8: for L be up-complete Semilattice holds for D be non empty directed Subset of [:L, L:] holds ex_sup_of ({ ( sup X) where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) },L)

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of [:L, L:];

      reconsider D1 = ( proj1 D), D2 = ( proj2 D) as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" D2) & x in D1;

      set A = { ( sup X) where X be non empty directed Subset of L : P[X] };

      A c= the carrier of L

      proof

        let q be object;

        assume q in A;

        then ex X be non empty directed Subset of L st q = ( sup X) & P[X];

        hence thesis;

      end;

      then

      reconsider A as Subset of L;

      set R = { X where X be non empty directed Subset of L : P[X] };

      ( union R) c= the carrier of L

      proof

        let q be object;

        assume q in ( union R);

        then

        consider r be set such that

         A1: q in r and

         A2: r in R by TARSKI:def 4;

        ex s be non empty directed Subset of L st r = s & ex x be Element of L st s = ( {x} "/\" D2) & x in D1 by A2;

        hence thesis by A1;

      end;

      then

      reconsider UR = ( union R) as Subset of L;

      set a = ( sup UR);



       A3: ex_sup_of (UR,L) by Th7;



       A4: for b be Element of L st A is_<=_than b holds a <= b

      proof

        let b be Element of L such that

         A5: A is_<=_than b;

        UR is_<=_than b

        proof

          let k be Element of L;

          assume k in UR;

          then

          consider k1 be set such that

           A6: k in k1 and

           A7: k1 in R by TARSKI:def 4;

          consider s be non empty directed Subset of L such that

           A8: k1 = s and

           A9: P[s] by A7;

          consider x be Element of L such that

           A10: s = ( {x} "/\" D2) and x in D1 by A9;



           A11: ( {x} "/\" D2) = { (x "/\" d2) where d2 be Element of L : d2 in D2 } by YELLOW_4: 42;

          ( sup s) in A by A9;

          then

           A12: ( sup s) <= b by A5;

          consider d2 be Element of L such that

           A13: k = (x "/\" d2) and d2 in D2 by A6, A8, A10, A11;

          (x "/\" d2) <= ( sup s) by A6, A8, A10, A13, Th1, YELLOW_4: 1;

          hence k <= b by A13, A12, YELLOW_0:def 2;

        end;

        hence thesis by A3, YELLOW_0:def 9;

      end;

      A is_<=_than a

      proof

        let b be Element of L;

        assume b in A;

        then

        consider X be non empty directed Subset of L such that

         A14: b = ( sup X) and

         A15: P[X];

         ex_sup_of (X,L) & X in R by A15, WAYBEL_0: 75;

        hence b <= a by A3, A14, YELLOW_0: 34, ZFMISC_1: 74;

      end;

      hence thesis by A4, YELLOW_0: 15;

    end;

    theorem :: WAYBEL_2:9



     Th9: for L be up-complete Semilattice holds for D be non empty directed Subset of [:L, L:] holds ( "\/" ({ ( sup X) where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) },L)) <= ( "\/" (( union { X where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) }),L))

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of [:L, L:];

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" ( proj2 D)) & x in ( proj1 D);



       A1: ( "\/" (( union { X where X be non empty directed Subset of L : P[X] }),L)) is_>=_than { ( sup X) where X be non empty directed Subset of L : P[X] }

      proof

        let a be Element of L;

        assume a in { ( sup X) where X be non empty directed Subset of L : P[X] };

        then

        consider q be non empty directed Subset of L such that

         A2: a = ( sup q) and

         A3: P[q];



         A4: q in { X where X be non empty directed Subset of L : P[X] } by A3;

         ex_sup_of (q,L) & ex_sup_of (( union { X where X be non empty directed Subset of L : P[X] }),L) by Th7, WAYBEL_0: 75;

        hence a <= ( "\/" (( union { X where X be non empty directed Subset of L : P[X] }),L)) by A2, A4, YELLOW_0: 34, ZFMISC_1: 74;

      end;

       ex_sup_of ({ ( sup X) where X be non empty directed Subset of L : P[X] },L) by Th8;

      hence thesis by A1, YELLOW_0:def 9;

    end;

    theorem :: WAYBEL_2:10



     Th10: for L be up-complete Semilattice holds for D be non empty directed Subset of [:L, L:] holds ( "\/" ({ ( sup X) where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) },L)) = ( "\/" (( union { X where X be non empty directed Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) }),L))

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of [:L, L:];

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" ( proj2 D)) & x in ( proj1 D);



       A1: ( "\/" ({ ( sup X) where X be non empty directed Subset of L : P[X] },L)) <= ( "\/" (( union { X where X be non empty directed Subset of L : P[X] }),L)) by Th9;



       A2: ( union { X where X be non empty directed Subset of L : P[X] }) is_<=_than ( "\/" ({ ( "\/" (X,L)) where X be non empty directed Subset of L : P[X] },L))

      proof

        let a be Element of L;

        assume a in ( union { X where X be non empty directed Subset of L : P[X] });

        then

        consider b be set such that

         A3: a in b and

         A4: b in { X where X be non empty directed Subset of L : P[X] } by TARSKI:def 4;

        consider c be non empty directed Subset of L such that

         A5: b = c and

         A6: P[c] by A4;

        ( "\/" (c,L)) in { ( "\/" (X,L)) where X be non empty directed Subset of L : P[X] } by A6;

        then

         A7: ( "\/" (c,L)) <= ( "\/" ({ ( "\/" (X,L)) where X be non empty directed Subset of L : P[X] },L)) by Th8, YELLOW_4: 1;

         ex_sup_of (c,L) by WAYBEL_0: 75;

        then a <= ( "\/" (c,L)) by A3, A5, YELLOW_4: 1;

        hence a <= ( "\/" ({ ( "\/" (X,L)) where X be non empty directed Subset of L : P[X] },L)) by A7, YELLOW_0:def 2;

      end;

       ex_sup_of (( union { X where X be non empty directed Subset of L : P[X] }),L) by Th7;

      then ( "\/" (( union { X where X be non empty directed Subset of L : P[X] }),L)) <= ( "\/" ({ ( "\/" (X,L)) where X be non empty directed Subset of L : P[X] },L)) by A2, YELLOW_0:def 9;

      hence thesis by A1, ORDERS_2: 2;

    end;

    registration

      let S,T be up-complete non empty reflexive RelStr;

      cluster [:S, T:] -> up-complete;

      coherence

      proof

        let X be non empty directed Subset of [:S, T:];

        reconsider X1 = ( proj1 X) as non empty directed Subset of S by YELLOW_3: 21, YELLOW_3: 22;

        reconsider X2 = ( proj2 X) as non empty directed Subset of T by YELLOW_3: 21, YELLOW_3: 22;

        consider x be Element of S such that

         A1: x is_>=_than X1 and

         A2: for z be Element of S st z is_>=_than X1 holds x <= z by WAYBEL_0:def 39;

        consider y be Element of T such that

         A3: y is_>=_than X2 and

         A4: for z be Element of T st z is_>=_than X2 holds y <= z by WAYBEL_0:def 39;

        take [x, y];

        thus [x, y] is_>=_than X by A1, A3, YELLOW_3: 31;

        let z be Element of [:S, T:] such that

         A5: z is_>=_than X;

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

         A6: z = [(z `1 ), (z `2 )] by MCART_1: 21;

        then (z `2 ) is_>=_than X2 by A5, YELLOW_3: 31;

        then

         A7: y <= (z `2 ) by A4;

        (z `1 ) is_>=_than X1 by A5, A6, YELLOW_3: 31;

        then x <= (z `1 ) by A2;

        hence thesis by A6, A7, YELLOW_3: 11;

      end;

    end

    theorem :: WAYBEL_2:11

    for S,T be non empty reflexive antisymmetric RelStr st [:S, T:] is up-complete holds S is up-complete & T is up-complete

    proof

      let S,T be non empty reflexive antisymmetric RelStr such that

       A1: [:S, T:] is up-complete;

      thus S is up-complete

      proof

        set D = the non empty directed Subset of T;

        let X be non empty directed Subset of S;

        consider x be Element of [:S, T:] such that

         A2: x is_>=_than [:X, D:] and

         A3: for y be Element of [:S, T:] st y is_>=_than [:X, D:] holds x <= y by A1;

        take (x `1 );

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

         A4: x = [(x `1 ), (x `2 )] by MCART_1: 21;

        hence (x `1 ) is_>=_than X by A2, YELLOW_3: 29;

         ex_sup_of ( [:X, D:], [:S, T:]) by A1, WAYBEL_0: 75;

        then ex_sup_of (D,T) by YELLOW_3: 39;

        then

         A5: ( sup D) is_>=_than D by YELLOW_0:def 9;

        let y be Element of S;

        assume y is_>=_than X;

        then x <= [y, ( sup D)] by A3, A5, YELLOW_3: 30;

        hence thesis by A4, YELLOW_3: 11;

      end;

      set D = the non empty directed Subset of S;

      let X be non empty directed Subset of T;

      consider x be Element of [:S, T:] such that

       A6: x is_>=_than [:D, X:] and

       A7: for y be Element of [:S, T:] st y is_>=_than [:D, X:] holds x <= y by A1;

       ex_sup_of ( [:D, X:], [:S, T:]) by A1, WAYBEL_0: 75;

      then ex_sup_of (D,S) by YELLOW_3: 39;

      then

       A8: ( sup D) is_>=_than D by YELLOW_0:def 9;

      take (x `2 );

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A9: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence (x `2 ) is_>=_than X by A6, YELLOW_3: 29;

      let y be Element of T;

      assume y is_>=_than X;

      then x <= [( sup D), y] by A7, A8, YELLOW_3: 30;

      hence thesis by A9, YELLOW_3: 11;

    end;

    theorem :: WAYBEL_2:12



     Th12: for L be up-complete antisymmetric non empty reflexive RelStr holds for D be non empty directed Subset of [:L, L:] holds ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))]

    proof

      let L be up-complete antisymmetric non empty reflexive RelStr, D be non empty directed Subset of [:L, L:];

      reconsider D1 = ( proj1 D), D2 = ( proj2 D) as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;

      reconsider C = the carrier of L as non empty set;

      reconsider D9 = D as non empty Subset of [:C, C:] by YELLOW_3:def 2;



       A1: ex_sup_of (D1,L) by WAYBEL_0: 75;

      the carrier of [:L, L:] = [:C, C:] by YELLOW_3:def 2;

      then

      consider d1,d2 be object such that

       A2: d1 in C & d2 in C and

       A3: ( sup D) = [d1, d2] by ZFMISC_1:def 2;



       A4: ex_sup_of (D2,L) by WAYBEL_0: 75;

      reconsider d1, d2 as Element of L by A2;



       A5: ex_sup_of (D, [:L, L:]) by WAYBEL_0: 75;

      D2 is_<=_than d2

      proof

        let b be Element of L;

        assume b in D2;

        then

        consider x be object such that

         A6: [x, b] in D by XTUPLE_0:def 13;

        reconsider x as Element of D1 by A6, XTUPLE_0:def 12;

        D is_<=_than [d1, d2] by A5, A3, YELLOW_0:def 9;

        then [x, b] <= [d1, d2] by A6;

        hence b <= d2 by YELLOW_3: 11;

      end;

      then

       A7: ( sup D2) <= d2 by A4, YELLOW_0:def 9;

      D1 is_<=_than d1

      proof

        let b be Element of L;

        assume b in D1;

        then

        consider x be object such that

         A8: [b, x] in D by XTUPLE_0:def 12;

        reconsider x as Element of D2 by A8, XTUPLE_0:def 13;

        D is_<=_than [d1, d2] by A5, A3, YELLOW_0:def 9;

        then [b, x] <= [d1, d2] by A8;

        hence b <= d1 by YELLOW_3: 11;

      end;

      then ( sup D1) <= d1 by A1, YELLOW_0:def 9;

      then

       A9: [( sup D1), ( sup D2)] <= ( sup D) by A3, A7, YELLOW_3: 11;



       A10: ex_sup_of ( [:D1, D2:], [:L, L:]) by WAYBEL_0: 75;

      reconsider D1, D2 as non empty Subset of L;

      D9 c= [:D1, D2:] by YELLOW_3: 1;

      then ( sup D) <= ( sup [:D1, D2:]) by A5, A10, YELLOW_0: 34;

      then ( sup D) <= [( sup ( proj1 D)), ( sup ( proj2 D))] by A1, A4, YELLOW_3: 43;

      hence thesis by A9, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_2:13



     Th13: for S1,S2 be RelStr, D be Subset of S1 holds for f be Function of S1, S2 st f is monotone holds (f .: ( downarrow D)) c= ( downarrow (f .: D))

    proof

      let S1,S2 be RelStr, D be Subset of S1, f be Function of S1, S2 such that

       A1: f is monotone;

      let q be object;

      assume

       A2: q in (f .: ( downarrow D));

      then

      consider x be object such that

       A3: x in ( dom f) and

       A4: x in ( downarrow D) and

       A5: q = (f . x) by FUNCT_1:def 6;

      reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;

      reconsider x as Element of s1 by A3;

      consider y be Element of s1 such that

       A6: x <= y and

       A7: y in D by A4, WAYBEL_0:def 15;

      reconsider f1 = f as Function of s1, s2;

      (f1 . x) is Element of s2;

      then

      reconsider q1 = q, fy = (f1 . y) as Element of s2 by A5;

      the carrier of s2 <> {} ;

      then ( dom f) = the carrier of s1 by FUNCT_2:def 1;

      then

       A8: (f . y) in (f .: D) by A7, FUNCT_1:def 6;

      q1 <= fy by A1, A5, A6;

      hence thesis by A8, WAYBEL_0:def 15;

    end;

    theorem :: WAYBEL_2:14



     Th14: for S1,S2 be RelStr, D be Subset of S1 holds for f be Function of S1, S2 st f is monotone holds (f .: ( uparrow D)) c= ( uparrow (f .: D))

    proof

      let S1,S2 be RelStr, D be Subset of S1, f be Function of S1, S2 such that

       A1: f is monotone;

      let q be object;

      assume

       A2: q in (f .: ( uparrow D));

      then

      consider x be object such that

       A3: x in ( dom f) and

       A4: x in ( uparrow D) and

       A5: q = (f . x) by FUNCT_1:def 6;

      reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;

      reconsider x as Element of s1 by A3;

      consider y be Element of s1 such that

       A6: y <= x and

       A7: y in D by A4, WAYBEL_0:def 16;

      reconsider f1 = f as Function of s1, s2;

      (f1 . x) is Element of s2;

      then

      reconsider q1 = q, fy = (f1 . y) as Element of s2 by A5;

      the carrier of s2 <> {} ;

      then ( dom f) = the carrier of s1 by FUNCT_2:def 1;

      then

       A8: (f . y) in (f .: D) by A7, FUNCT_1:def 6;

      fy <= q1 by A1, A5, A6;

      hence thesis by A8, WAYBEL_0:def 16;

    end;

    registration

      cluster -> distributive complemented for 1 -element reflexive RelStr;

      coherence

      proof

        let L be 1 -element reflexive RelStr;

        thus L is distributive by STRUCT_0:def 10;

        let x be Element of L;

        take y = x;

        thus (x "\/" y) = ( Top L) by STRUCT_0:def 10;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      cluster strict1 -element for LATTICE;

      existence

      proof

        set B = the strict1 -element reflexive RelStr;

        take B;

        thus thesis;

      end;

    end

    theorem :: WAYBEL_2:15



     Th15: for H be distributive complete LATTICE holds for a be Element of H, X be finite Subset of H holds ( sup ( {a} "/\" X)) = (a "/\" ( sup X))

    proof

      let H be distributive complete LATTICE, a be Element of H, X be finite Subset of H;

      defpred P[ set] means ex A be Subset of H st A = $1 & (a "/\" ( sup A)) = ( sup ( {a} "/\" A));



       A1: P[ {} ]

      proof

        reconsider A = {} as Subset of H by XBOOLE_1: 2;

        take A;

        thus A = {} ;

        ( Bottom H) <= a & ( {a} "/\" ( {} H)) = {} by YELLOW_0: 44, YELLOW_4: 36;

        hence thesis by YELLOW_0: 25;

      end;



       A2: for x,B be set st x in X & B c= X & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A3: x in X and

         A4: B c= X and

         A5: P[B];

        reconsider x1 = x as Element of H by A3;



         A6: {x1} c= the carrier of H;

        B c= the carrier of H by A4, XBOOLE_1: 1;

        then

        reconsider C = (B \/ {x}) as Subset of H by A6, XBOOLE_1: 8;

        take C;

        thus C = (B \/ {x});

        consider A be Subset of H such that

         A7: A = B and

         A8: (a "/\" ( sup A)) = ( sup ( {a} "/\" A)) by A5;



         A9: ( {a} "/\" C) = (( {a} "/\" A) \/ ( {a} "/\" {x1})) by A7, YELLOW_4: 43

        .= (( {a} "/\" A) \/ {(a "/\" x1)}) by YELLOW_4: 46;



         A10: ex_sup_of (( {a} "/\" A),H) & ex_sup_of ( {(a "/\" x1)},H) by YELLOW_0: 17;

         ex_sup_of (B,H) & ex_sup_of ( {x},H) by YELLOW_0: 17;



        hence (a "/\" ( sup C)) = (a "/\" (( "\/" (B,H)) "\/" ( "\/" ( {x},H)))) by YELLOW_2: 3

        .= (( sup ( {a} "/\" A)) "\/" (a "/\" ( "\/" ( {x},H)))) by A7, A8, WAYBEL_1:def 3

        .= (( sup ( {a} "/\" A)) "\/" (a "/\" x1)) by YELLOW_0: 39

        .= (( sup ( {a} "/\" A)) "\/" ( sup {(a "/\" x1)})) by YELLOW_0: 39

        .= ( sup ( {a} "/\" C)) by A10, A9, YELLOW_2: 3;

      end;



       A11: X is finite;

       P[X] from FINSET_1:sch 2( A11, A1, A2);

      hence thesis;

    end;

    theorem :: WAYBEL_2:16

    for H be distributive complete LATTICE holds for a be Element of H, X be finite Subset of H holds ( inf ( {a} "\/" X)) = (a "\/" ( inf X))

    proof

      let H be distributive complete LATTICE, a be Element of H, X be finite Subset of H;

      defpred P[ set] means ex A be Subset of H st A = $1 & (a "\/" ( inf A)) = ( inf ( {a} "\/" A));



       A1: P[ {} ]

      proof

        reconsider A = {} as Subset of H by XBOOLE_1: 2;

        take A;

        thus A = {} ;

        a <= ( Top H) & ( {a} "\/" ( {} H)) = {} by YELLOW_0: 45, YELLOW_4: 9;

        hence thesis by YELLOW_0: 24;

      end;



       A2: for x,B be set st x in X & B c= X & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A3: x in X and

         A4: B c= X and

         A5: P[B];

        reconsider x1 = x as Element of H by A3;



         A6: {x1} c= the carrier of H;

        B c= the carrier of H by A4, XBOOLE_1: 1;

        then

        reconsider C = (B \/ {x}) as Subset of H by A6, XBOOLE_1: 8;

        take C;

        thus C = (B \/ {x});

        consider A be Subset of H such that

         A7: A = B and

         A8: (a "\/" ( inf A)) = ( inf ( {a} "\/" A)) by A5;



         A9: ( {a} "\/" C) = (( {a} "\/" A) \/ ( {a} "\/" {x1})) by A7, YELLOW_4: 16

        .= (( {a} "\/" A) \/ {(a "\/" x1)}) by YELLOW_4: 19;



         A10: ex_inf_of (( {a} "\/" A),H) & ex_inf_of ( {(a "\/" x1)},H) by YELLOW_0: 17;

         ex_inf_of (B,H) & ex_inf_of ( {x},H) by YELLOW_0: 17;



        hence (a "\/" ( inf C)) = (a "\/" (( "/\" (B,H)) "/\" ( "/\" ( {x},H)))) by YELLOW_2: 4

        .= (( inf ( {a} "\/" A)) "/\" (a "\/" ( "/\" ( {x},H)))) by A7, A8, WAYBEL_1: 5

        .= (( inf ( {a} "\/" A)) "/\" (a "\/" x1)) by YELLOW_0: 39

        .= (( inf ( {a} "\/" A)) "/\" ( inf {(a "\/" x1)})) by YELLOW_0: 39

        .= ( inf ( {a} "\/" C)) by A10, A9, YELLOW_2: 4;

      end;



       A11: X is finite;

       P[X] from FINSET_1:sch 2( A11, A1, A2);

      hence thesis;

    end;

    theorem :: WAYBEL_2:17



     Th17: for H be complete distributive LATTICE, a be Element of H holds for X be finite Subset of H holds (a "/\" ) preserves_sup_of X

    proof

      let H be complete distributive LATTICE, a be Element of H, X be finite Subset of H;

      assume ex_sup_of (X,H);

      thus ex_sup_of (((a "/\" ) .: X),H) by YELLOW_0: 17;



      thus ( sup ((a "/\" ) .: X)) = ( "\/" ({ (a "/\" y) where y be Element of H : y in X },H)) by WAYBEL_1: 61

      .= ( sup ( {a} "/\" X)) by YELLOW_4: 42

      .= (a "/\" ( sup X)) by Th15

      .= ((a "/\" ) . ( sup X)) by WAYBEL_1:def 18;

    end;

    begin

    scheme :: WAYBEL_2:sch1

    ExNet { L() -> non empty RelStr , N() -> prenet of L() , F( set) -> Element of L() } :

ex M be prenet of L() st the RelStr of M = the RelStr of N() & for i be Element of M holds (the mapping of M . i) = F(.);

      deffunc G( Element of N()) = F(.);



       A1: for i be Element of N() holds G(i) in the carrier of L();

      consider f be Function of the carrier of N(), the carrier of L() such that

       A2: for i be Element of N() holds (f . i) = G(i) from FUNCT_2:sch 8( A1);

      set M = NetStr (# the carrier of N(), the InternalRel of N(), f #);

       the RelStr of M = the RelStr of N() & ( [#] N()) is directed by WAYBEL_0:def 6;

      then ( [#] M) is directed by WAYBEL_0: 3;

      then

      reconsider M as prenet of L() by WAYBEL_0:def 6;

      take M;

      thus thesis by A2;

    end;

    theorem :: WAYBEL_2:18



     Th18: for L be non empty RelStr holds for N be prenet of L st N is eventually-directed holds ( rng ( netmap (N,L))) is directed

    proof

      let L be non empty RelStr, N be prenet of L such that

       A1: N is eventually-directed;

      set f = ( netmap (N,L));

      let x,y be Element of L such that

       A2: x in ( rng f) and

       A3: y in ( rng f);

      consider a be object such that

       A4: a in ( dom f) and

       A5: (f . a) = x by A2, FUNCT_1:def 3;

      consider b be object such that

       A6: b in ( dom f) and

       A7: (f . b) = y by A3, FUNCT_1:def 3;

      reconsider a, b as Element of N by A4, A6;

      consider ja be Element of N such that

       A8: for k be Element of N st ja <= k holds (N . a) <= (N . k) by A1, WAYBEL_0: 11;

      consider jb be Element of N such that

       A9: for k be Element of N st jb <= k holds (N . b) <= (N . k) by A1, WAYBEL_0: 11;

      ( [#] N) is directed by WAYBEL_0:def 6;

      then

      consider c be Element of N such that c in ( [#] N) and

       A10: ja <= c & jb <= c;

      take z = (f . c);

      ( dom f) = the carrier of N by FUNCT_2:def 1;

      hence z in ( rng f) by FUNCT_1:def 3;

      (N . c) = (f . c);

      hence thesis by A5, A7, A8, A9, A10;

    end;

    theorem :: WAYBEL_2:19



     Th19: for L be non empty reflexive RelStr, D be non empty directed Subset of L holds for n be Function of D, the carrier of L holds NetStr (# D, (the InternalRel of L |_2 D), n #) is prenet of L

    proof

      let L be non empty reflexive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L;

      set N = NetStr (# D, (the InternalRel of L |_2 D), n #);

      N is directed

      proof

        let x,y be Element of N;

        assume that x in ( [#] N) and y in ( [#] N);

        reconsider x1 = x, y1 = y as Element of D;

        consider z1 be Element of L such that

         A1: z1 in D and

         A2: x1 <= z1 & y1 <= z1 by WAYBEL_0:def 1;

        reconsider z = z1 as Element of N by A1;

        take z;

        thus z in ( [#] N);

        the InternalRel of N c= the InternalRel of L by XBOOLE_1: 17;

        then

        reconsider N as SubRelStr of L by YELLOW_0:def 13;

        N is full;

        hence thesis by A2, YELLOW_0: 60;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_2:20



     Th20: for L be non empty reflexive RelStr, D be non empty directed Subset of L holds for n be Function of D, the carrier of L, N be prenet of L st n = ( id D) & N = NetStr (# D, (the InternalRel of L |_2 D), n #) holds N is eventually-directed

    proof

      let L be non empty reflexive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L, N be prenet of L such that

       A1: n = ( id D) and

       A2: N = NetStr (# D, (the InternalRel of L |_2 D), n #);

      for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) <= (N . k)

      proof

        let i be Element of N;

        take j = i;

        let k be Element of N such that

         A3: j <= k;

        the InternalRel of N c= the InternalRel of L by A2, XBOOLE_1: 17;

        then

         A4: N is SubRelStr of L by A2, YELLOW_0:def 13;

        reconsider nj = (n . j), nk = (n . k) as Element of L by A2, FUNCT_2: 5;

        nj = j & nk = k by A1, A2;

        hence thesis by A2, A3, A4, YELLOW_0: 59;

      end;

      hence thesis by WAYBEL_0: 11;

    end;

    definition

      let L be non empty RelStr, N be NetStr over L;

      :: WAYBEL_2:def1

      func sup N -> Element of L equals ( Sup the mapping of N);

      coherence ;

    end

    definition

      let L be non empty RelStr, J be set, f be Function of J, the carrier of L;

      :: WAYBEL_2:def2

      func FinSups f -> prenet of L means

      : Def2: ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & it = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #);

      existence

      proof

        deffunc F( Element of ( Fin J)) = ( sup (f .: $1));



         A1: for x be Element of ( Fin J) holds F(x) in the carrier of L;

        consider g be Function of ( Fin J), the carrier of L such that

         A2: for x be Element of ( Fin J) holds (g . x) = F(x) from FUNCT_2:sch 8( A1);

        set M = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #);

        M is directed

        proof

          let x,y be Element of M such that x in ( [#] M) and y in ( [#] M);

          reconsider x1 = x, y1 = y as Element of ( Fin J);

          reconsider z = (x1 \/ y1) as Element of M;

          take z;

          thus z in ( [#] M);



           A3: ( InclPoset ( Fin J)) = RelStr (# ( Fin J), ( RelIncl ( Fin J)) #) by YELLOW_1:def 1;

          then

          reconsider x2 = x, y2 = y, z1 = z as Element of ( InclPoset ( Fin J));

          y c= z by XBOOLE_1: 7;

          then

           A4: y2 <= z1 by YELLOW_1: 3;

          x c= z by XBOOLE_1: 7;

          then x2 <= z1 by YELLOW_1: 3;

          hence thesis by A3, A4, YELLOW_0: 1;

        end;

        then

        reconsider M as prenet of L;

        take M;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let A,B be prenet of L such that

         A5: ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & A = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #) and

         A6: ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & B = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #);

        consider g1 be Function of ( Fin J), the carrier of L such that

         A7: for x be Element of ( Fin J) holds (g1 . x) = ( sup (f .: x)) & A = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g1 #) by A5;

        consider g2 be Function of ( Fin J), the carrier of L such that

         A8: for x be Element of ( Fin J) holds (g2 . x) = ( sup (f .: x)) & B = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g2 #) by A6;

        for x be object st x in ( Fin J) holds (g1 . x) = (g2 . x)

        proof

          let x be object;

          assume

           A9: x in ( Fin J);

          reconsider xx = x as set by TARSKI: 1;



          thus (g1 . x) = ( sup (f .: xx)) by A7, A9

          .= (g2 . x) by A8, A9;

        end;

        hence thesis by A7, A8, FUNCT_2: 12;

      end;

    end

    theorem :: WAYBEL_2:21

    for L be non empty RelStr, J,x be set holds for f be Function of J, the carrier of L holds x is Element of ( FinSups f) iff x is Element of ( Fin J)

    proof

      let L be non empty RelStr, J,x be set, f be Function of J, the carrier of L;

      ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & ( FinSups f) = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #) by Def2;

      hence thesis;

    end;

    registration

      let L be complete antisymmetric non empty reflexive RelStr, J be set, f be Function of J, the carrier of L;

      cluster ( FinSups f) -> monotone;

      coherence

      proof

        let x,y be Element of ( FinSups f) such that

         A1: x <= y;

        consider g be Function of ( Fin J), the carrier of L such that

         A2: for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & ( FinSups f) = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #) by Def2;

        (g . x) = ( sup (f .: x)) by A2;

        then

        reconsider fx = (g . x) as Element of L;



         A3: ( InclPoset ( Fin J)) = RelStr (# ( Fin J), ( RelIncl ( Fin J)) #) by YELLOW_1:def 1;

        then

        reconsider x1 = x, y1 = y as Element of ( InclPoset ( Fin J)) by A2;



         A4: ex_sup_of ((f .: x),L) & ex_sup_of ((f .: y),L) by YELLOW_0: 17;

        x1 <= y1 by A1, A2, A3, YELLOW_0: 1;

        then x c= y by YELLOW_1: 3;

        then ( sup (f .: x)) <= ( sup (f .: y)) by A4, RELAT_1: 123, YELLOW_0: 34;

        then

         A5: fx <= ( sup (f .: y)) by A2;

        let a,b be Element of L;

        assume a = (( netmap (( FinSups f),L)) . x) & b = (( netmap (( FinSups f),L)) . y);

        hence a <= b by A2, A5;

      end;

    end

    definition

      let L be non empty RelStr, x be Element of L, N be non empty NetStr over L;

      :: WAYBEL_2:def3

      func x "/\" N -> strict NetStr over L means

      : Def3: the RelStr of it = the RelStr of N & for i be Element of it holds ex y be Element of L st y = (the mapping of N . i) & (the mapping of it . i) = (x "/\" y);

      existence

      proof

        defpred P[ set, set] means ex y be Element of L st y = (the mapping of N . $1) & $2 = (x "/\" y);



         A1: for e be Element of N holds ex u be Element of L st P[e, u]

        proof

          let e be Element of N;

          take (x "/\" (the mapping of N . e)), (the mapping of N . e);

          thus thesis;

        end;

        ex g be Function of the carrier of N, the carrier of L st for i be Element of N holds P[i, (g . i)] from FUNCT_2:sch 3( A1);

        then

        consider g be Function of the carrier of N, the carrier of L such that

         A2: for i be Element of N holds ex y be Element of L st y = (the mapping of N . i) & (g . i) = (x "/\" y);

        take NetStr (# the carrier of N, the InternalRel of N, g #);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let A,B be strict NetStr over L such that

         A3: the RelStr of A = the RelStr of N and

         A4: for i be Element of A holds ex y be Element of L st y = (the mapping of N . i) & (the mapping of A . i) = (x "/\" y) and

         A5: the RelStr of B = the RelStr of N and

         A6: for i be Element of B holds ex y be Element of L st y = (the mapping of N . i) & (the mapping of B . i) = (x "/\" y);

        reconsider C = the carrier of A as non empty set by A3;

        reconsider f1 = the mapping of A, f2 = the mapping of B as Function of C, the carrier of L by A3, A5;

        for c be Element of C holds (f1 . c) = (f2 . c)

        proof

          let c be Element of C;

          (ex ya be Element of L st ya = (the mapping of N . c) & (f1 . c) = (x "/\" ya)) & ex yb be Element of L st yb = (the mapping of N . c) & (f2 . c) = (x "/\" yb) by A3, A4, A5, A6;

          hence thesis;

        end;

        hence thesis by A3, A5, FUNCT_2: 63;

      end;

    end

    theorem :: WAYBEL_2:22



     Th22: for L be non empty RelStr, N be non empty NetStr over L holds for x be Element of L, y be set holds y is Element of N iff y is Element of (x "/\" N)

    proof

      let L be non empty RelStr, N be non empty NetStr over L, x be Element of L, y be set;

       the RelStr of (x "/\" N) = the RelStr of N by Def3;

      hence thesis;

    end;

    registration

      let L be non empty RelStr, x be Element of L, N be non empty NetStr over L;

      cluster (x "/\" N) -> non empty;

      coherence

      proof

         the RelStr of (x "/\" N) = the RelStr of N by Def3;

        hence thesis;

      end;

    end

    registration

      let L be non empty RelStr, x be Element of L, N be prenet of L;

      cluster (x "/\" N) -> directed;

      coherence

      proof

         the RelStr of (x "/\" N) = the RelStr of N & ( [#] N) is directed by Def3, WAYBEL_0:def 6;

        hence ( [#] (x "/\" N)) is directed by WAYBEL_0: 3;

      end;

    end

    theorem :: WAYBEL_2:23



     Th23: for L be non empty RelStr, x be Element of L holds for F be non empty NetStr over L holds ( rng the mapping of (x "/\" F)) = ( {x} "/\" ( rng the mapping of F))

    proof

      let L be non empty RelStr, x be Element of L, F be non empty NetStr over L;

      set f = the mapping of F, h = the mapping of (x "/\" F), A = ( rng the mapping of F);



       A1: ( {x} "/\" A) = { (x "/\" y) where y be Element of L : y in A } by YELLOW_4: 42;



       A2: the RelStr of (x "/\" F) = the RelStr of F by Def3;

      then

       A3: ( dom h) = the carrier of F by FUNCT_2:def 1;



       A4: ( dom f) = the carrier of F by FUNCT_2:def 1;

      thus ( rng the mapping of (x "/\" F)) c= ( {x} "/\" A)

      proof

        let q be object;

        assume q in ( rng h);

        then

        consider a be object such that

         A5: a in ( dom h) and

         A6: q = (h . a) by FUNCT_1:def 3;

        reconsider a as Element of (x "/\" F) by A5;

        consider y be Element of L such that

         A7: y = (f . a) and

         A8: (h . a) = (x "/\" y) by Def3;

        y in A by A2, A4, A7, FUNCT_1:def 3;

        hence thesis by A1, A6, A8;

      end;

      let q be object;

      assume q in ( {x} "/\" A);

      then

      consider y be Element of L such that

       A9: q = (x "/\" y) and

       A10: y in A by A1;

      consider z be object such that

       A11: z in ( dom f) and

       A12: y = (f . z) by A10, FUNCT_1:def 3;

      reconsider z as Element of (x "/\" F) by A2, A11;

      ex w be Element of L st w = (f . z) & (h . z) = (x "/\" w) by Def3;

      hence thesis by A3, A9, A11, A12, FUNCT_1:def 3;

    end;

    theorem :: WAYBEL_2:24



     Th24: for L be non empty RelStr, J be set holds for f be Function of J, the carrier of L st for x be set holds ex_sup_of ((f .: x),L) holds ( rng ( netmap (( FinSups f),L))) c= ( finsups ( rng f))

    proof

      let L be non empty RelStr, J be set, f be Function of J, the carrier of L such that

       A1: for x be set holds ex_sup_of ((f .: x),L);

      let q be object;

      set h = ( netmap (( FinSups f),L));

      assume q in ( rng h);

      then

      consider x be object such that

       A2: x in ( dom h) and

       A3: (h . x) = q by FUNCT_1:def 3;



       A4: ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & ( FinSups f) = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #) by Def2;

      then

      reconsider x as Element of ( Fin J) by A2;



       A5: (f .: x) is finite Subset of ( rng f) & ex_sup_of ((f .: x),L) by A1, RELAT_1: 111;

      (h . x) = ( sup (f .: x)) by A4;

      hence thesis by A3, A5;

    end;

    theorem :: WAYBEL_2:25



     Th25: for L be non empty reflexive antisymmetric RelStr, J be set holds for f be Function of J, the carrier of L holds ( rng f) c= ( rng ( netmap (( FinSups f),L)))

    proof

      let L be non empty reflexive antisymmetric RelStr, J be set, f be Function of J, the carrier of L;

      per cases ;

        suppose

         A1: J is non empty;

        let a be object;

        assume a in ( rng f);

        then

        consider b be object such that

         A2: b in ( dom f) and

         A3: a = (f . b) by FUNCT_1:def 3;

        reconsider b as Element of J by A2;

        (f . b) in ( rng f) by A2, FUNCT_1:def 3;

        then

        reconsider fb = (f . b) as Element of L;



         A4: ( Im (f,b)) = {fb} by A2, FUNCT_1: 59;

         {b} c= J by A1, ZFMISC_1: 31;

        then

        reconsider x = {b} as Element of ( Fin J) by FINSUB_1:def 5;

        consider g be Function of ( Fin J), the carrier of L such that

         A5: for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & ( FinSups f) = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #) by Def2;

        ( dom g) = ( Fin J) by FUNCT_2:def 1;

        then

         A6: x in ( dom g);

        (g . {b}) = ( sup (f .: x)) by A5

        .= a by A3, A4, YELLOW_0: 39;

        hence thesis by A5, A6, FUNCT_1:def 3;

      end;

        suppose

         A7: J is empty;

        ( rng f) = {} by A7;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL_2:26



     Th26: for L be non empty reflexive antisymmetric RelStr, J be set holds for f be Function of J, the carrier of L st ex_sup_of (( rng f),L) & ex_sup_of (( rng ( netmap (( FinSups f),L))),L) & for x be Element of ( Fin J) holds ex_sup_of ((f .: x),L) holds ( Sup f) = ( sup ( FinSups f))

    proof

      let L be non empty reflexive antisymmetric RelStr, J be set, f be Function of J, the carrier of L such that

       A1: ex_sup_of (( rng f),L) and

       A2: ex_sup_of (( rng ( netmap (( FinSups f),L))),L) and

       A3: for x be Element of ( Fin J) holds ex_sup_of ((f .: x),L);

      set h = ( netmap (( FinSups f),L));



       A4: ( "\/" (( rng f),L)) <= ( sup ( rng h)) by A1, A2, Th25, YELLOW_0: 34;

      ( rng h) is_<=_than ( "\/" (( rng f),L))

      proof

        let a be Element of L;

        assume a in ( rng h);

        then

        consider x be object such that

         A5: x in ( dom h) and

         A6: a = (h . x) by FUNCT_1:def 3;



         A7: ex g be Function of ( Fin J), the carrier of L st for x be Element of ( Fin J) holds (g . x) = ( sup (f .: x)) & ( FinSups f) = NetStr (# ( Fin J), ( RelIncl ( Fin J)), g #) by Def2;

        then

        reconsider x as Element of ( Fin J) by A5;

         ex_sup_of ((f .: x),L) by A3;

        then ( sup (f .: x)) <= ( "\/" (( rng f),L)) by A1, RELAT_1: 111, YELLOW_0: 34;

        hence a <= ( "\/" (( rng f),L)) by A6, A7;

      end;

      then

       A8: ( sup ( rng h)) <= ( "\/" (( rng f),L)) by A2, YELLOW_0:def 9;



      thus ( Sup f) = ( "\/" (( rng f),L)) by YELLOW_2:def 5

      .= ( sup ( rng ( netmap (( FinSups f),L)))) by A4, A8, ORDERS_2: 2

      .= ( sup ( FinSups f)) by YELLOW_2:def 5;

    end;

    theorem :: WAYBEL_2:27



     Th27: for L be with_infima antisymmetric transitive RelStr, N be prenet of L holds for x be Element of L st N is eventually-directed holds (x "/\" N) is eventually-directed

    proof

      let L be with_infima antisymmetric transitive RelStr, N be prenet of L, x be Element of L such that

       A1: N is eventually-directed;



       A2: the RelStr of (x "/\" N) = the RelStr of N by Def3;

      for i be Element of (x "/\" N) holds ex j be Element of (x "/\" N) st for k be Element of (x "/\" N) st j <= k holds ((x "/\" N) . i) <= ((x "/\" N) . k)

      proof

        let i1 be Element of (x "/\" N);

        reconsider i = i1 as Element of N by Th22;

        consider j be Element of N such that

         A3: for k be Element of N st j <= k holds (N . i) <= (N . k) by A1, WAYBEL_0: 11;

        reconsider j1 = j as Element of (x "/\" N) by Th22;

        take j1;

        let k1 be Element of (x "/\" N);

        reconsider k = k1 as Element of N by Th22;

        assume j1 <= k1;

        then j <= k by A2, YELLOW_0: 1;

        then

         A4: (N . i) <= (N . k) by A3;

        (ex yi be Element of L st yi = (the mapping of N . i1) & (the mapping of (x "/\" N) . i1) = (x "/\" yi)) & ex yk be Element of L st yk = (the mapping of N . k1) & (the mapping of (x "/\" N) . k1) = (x "/\" yk) by Def3;

        hence thesis by A4, WAYBEL_1: 1;

      end;

      hence thesis by WAYBEL_0: 11;

    end;

    theorem :: WAYBEL_2:28



     Th28: for L be up-complete Semilattice st for x be Element of L, E be non empty directed Subset of L st x <= ( sup E) holds x <= ( sup ( {x} "/\" E)) holds for D be non empty directed Subset of L, x be Element of L holds (x "/\" ( sup D)) = ( sup ( {x} "/\" D))

    proof

      let L be up-complete Semilattice such that

       A1: for x be Element of L, E be non empty directed Subset of L st x <= ( sup E) holds x <= ( sup ( {x} "/\" E));

      let D be non empty directed Subset of L, x be Element of L;

      ex w be Element of L st x >= w & ( sup D) >= w & for c be Element of L st x >= c & ( sup D) >= c holds w >= c by LATTICE3:def 11;

      then (x "/\" ( sup D)) <= ( sup D) by LATTICE3:def 14;

      then

       A2: (x "/\" ( sup D)) <= ( sup ( {(x "/\" ( sup D))} "/\" D)) by A1;

      reconsider T = {(x "/\" ( sup D))} as non empty directed Subset of L by WAYBEL_0: 5;

       ex_sup_of (D,L) by WAYBEL_0: 75;

      then

       A3: ( sup D) is_>=_than D by YELLOW_0: 30;

       ex_sup_of ((T "/\" D),L) & ( {(x "/\" ( sup D))} "/\" D) is_<=_than (x "/\" ( sup D)) by WAYBEL_0: 75, YELLOW_4: 52;

      then ( sup ( {(x "/\" ( sup D))} "/\" D)) <= (x "/\" ( sup D)) by YELLOW_0: 30;



      hence (x "/\" ( sup D)) = ( sup ( {(x "/\" ( sup D))} "/\" D)) by A2, ORDERS_2: 2

      .= ( sup (( {x} "/\" {( sup D)}) "/\" D)) by YELLOW_4: 46

      .= ( sup ( {x} "/\" ( {( sup D)} "/\" D))) by YELLOW_4: 41

      .= ( sup ( {x} "/\" D)) by A3, YELLOW_4: 51;

    end;

    theorem :: WAYBEL_2:29

    for L be with_suprema Poset st for X be directed Subset of L, x be Element of L holds (x "/\" ( sup X)) = ( sup ( {x} "/\" X)) holds for X be Subset of L, x be Element of L st ex_sup_of (X,L) holds (x "/\" ( sup X)) = ( sup ( {x} "/\" ( finsups X)))

    proof

      let L be with_suprema Poset such that

       A1: for X be directed Subset of L, x be Element of L holds (x "/\" ( sup X)) = ( sup ( {x} "/\" X));

      let X be Subset of L, x be Element of L;

      assume ex_sup_of (X,L);



      hence (x "/\" ( sup X)) = (x "/\" ( sup ( finsups X))) by WAYBEL_0: 55

      .= ( sup ( {x} "/\" ( finsups X))) by A1;

    end;

    theorem :: WAYBEL_2:30

    for L be up-complete LATTICE st for X be Subset of L, x be Element of L holds (x "/\" ( sup X)) = ( sup ( {x} "/\" ( finsups X))) holds for X be non empty directed Subset of L, x be Element of L holds (x "/\" ( sup X)) = ( sup ( {x} "/\" X))

    proof

      let L be up-complete LATTICE such that

       A1: for X be Subset of L, x be Element of L holds (x "/\" ( sup X)) = ( sup ( {x} "/\" ( finsups X)));

      let X be non empty directed Subset of L, x be Element of L;

      reconsider T = {x} as non empty directed Subset of L by WAYBEL_0: 5;



       A2: ex_sup_of ((T "/\" X),L) by WAYBEL_0: 75;



       A3: ( {x} "/\" ( finsups X)) = { (x "/\" y) where y be Element of L : y in ( finsups X) } by YELLOW_4: 42;



       A4: ( {x} "/\" ( finsups X)) is_<=_than ( sup ( {x} "/\" X))

      proof

        let q be Element of L;



         A5: x <= x;

        assume q in ( {x} "/\" ( finsups X));

        then

        consider y be Element of L such that

         A6: q = (x "/\" y) and

         A7: y in ( finsups X) by A3;

        consider Y be finite Subset of X such that

         A8: y = ( "\/" (Y,L)) and

         A9: ex_sup_of (Y,L) by A7;

        consider z be Element of L such that

         A10: z in X and

         A11: z is_>=_than Y by WAYBEL_0: 1;

        ( "\/" (Y,L)) <= z by A9, A11, YELLOW_0: 30;

        then

         A12: (x "/\" y) <= (x "/\" z) by A8, A5, YELLOW_3: 2;

        x in {x} by TARSKI:def 1;

        then (x "/\" z) <= ( sup ( {x} "/\" X)) by A2, A10, YELLOW_4: 1, YELLOW_4: 37;

        hence q <= ( sup ( {x} "/\" X)) by A6, A12, YELLOW_0:def 2;

      end;

       ex_sup_of ((T "/\" ( finsups X)),L) by WAYBEL_0: 75;

      then ( sup ( {x} "/\" ( finsups X))) <= ( sup ( {x} "/\" X)) by A4, YELLOW_0: 30;

      then

       A13: (x "/\" ( sup X)) <= ( sup ( {x} "/\" X)) by A1;

       ex_sup_of (X,L) by WAYBEL_0: 75;

      then ( sup ( {x} "/\" X)) <= (x "/\" ( sup X)) by A2, YELLOW_4: 53;

      hence thesis by A13, ORDERS_2: 2;

    end;

    begin

    definition

      let L be non empty RelStr;

      :: WAYBEL_2:def4

      func inf_op L -> Function of [:L, L:], L means

      : Def4: for x,y be Element of L holds (it . (x,y)) = (x "/\" y);

      existence

      proof

        deffunc F( Element of L, Element of L) = ($1 "/\" $2);



         A1: for x,y be Element of L holds F(x,y) is Element of L;

        consider f be Function of [:L, L:], L such that

         A2: for x,y be Element of L holds (f . (x,y)) = F(x,y) from YELLOW_3:sch 6( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of [:L, L:], L such that

         A3: for x,y be Element of L holds (f . (x,y)) = (x "/\" y) and

         A4: for x,y be Element of L holds (g . (x,y)) = (x "/\" y);

        now

          let x,y be Element of L;



          thus (f . (x,y)) = (x "/\" y) by A3

          .= (g . (x,y)) by A4;

        end;

        hence f = g by YELLOW_3: 13;

      end;

    end

    theorem :: WAYBEL_2:31



     Th31: for L be non empty RelStr, x be Element of [:L, L:] holds (( inf_op L) . x) = ((x `1 ) "/\" (x `2 ))

    proof

      let L be non empty RelStr, x be Element of [:L, L:];

      the carrier of [:L, L:] = [:the carrier of L, the carrier of L:] by YELLOW_3:def 2;

      then ex a,b be object st a in the carrier of L & b in the carrier of L & x = [a, b] by ZFMISC_1:def 2;



      hence (( inf_op L) . x) = (( inf_op L) . ((x `1 ),(x `2 )))

      .= ((x `1 ) "/\" (x `2 )) by Def4;

    end;

    registration

      let L be with_infima transitive antisymmetric RelStr;

      cluster ( inf_op L) -> monotone;

      coherence

      proof

        let x,y be Element of [:L, L:];

        set f = ( inf_op L);

        assume x <= y;

        then

         A1: (x `1 ) <= (y `1 ) & (x `2 ) <= (y `2 ) by YELLOW_3: 12;



         A2: (f . x) = ((x `1 ) "/\" (x `2 )) & (f . y) = ((y `1 ) "/\" (y `2 )) by Th31;

        let a,b be Element of L;

        assume a = (f . x) & b = (f . y);

        hence thesis by A1, A2, YELLOW_3: 2;

      end;

    end

    theorem :: WAYBEL_2:32



     Th32: for S be non empty RelStr, D1,D2 be Subset of S holds (( inf_op S) .: [:D1, D2:]) = (D1 "/\" D2)

    proof

      let S be non empty RelStr, D1,D2 be Subset of S;

      set f = ( inf_op S);

      reconsider X = [:D1, D2:] as set;

      thus (f .: [:D1, D2:]) c= (D1 "/\" D2)

      proof

        let q be object;

        assume

         A1: q in (f .: [:D1, D2:]);

        then

        reconsider q1 = q as Element of S;

        consider c be Element of [:S, S:] such that

         A2: c in [:D1, D2:] and

         A3: q1 = (f . c) by A1, FUNCT_2: 65;

        consider x,y be object such that

         A4: x in D1 & y in D2 and

         A5: c = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x, y as Element of S by A4;

        q = (f . (x,y)) by A3, A5

        .= (x "/\" y) by Def4;

        then q in { (a "/\" b) where a,b be Element of S : a in D1 & b in D2 } by A4;

        hence thesis by YELLOW_4:def 4;

      end;

      let q be object;

      assume q in (D1 "/\" D2);

      then q in { (x "/\" y) where x,y be Element of S : x in D1 & y in D2 } by YELLOW_4:def 4;

      then

      consider x,y be Element of S such that

       A6: q = (x "/\" y) & x in D1 & y in D2;

      q = (f . (x,y)) & [x, y] in X by A6, Def4, ZFMISC_1: 87;

      hence thesis by FUNCT_2: 35;

    end;

    theorem :: WAYBEL_2:33



     Th33: for L be up-complete Semilattice holds for D be non empty directed Subset of [:L, L:] holds ( sup (( inf_op L) .: D)) = ( sup (( proj1 D) "/\" ( proj2 D)))

    proof

      let L be up-complete Semilattice, D be non empty directed Subset of [:L, L:];

      reconsider C = the carrier of L as non empty set;

      reconsider D9 = D as non empty Subset of [:C, C:] by YELLOW_3:def 2;

      reconsider D1 = ( proj1 D), D2 = ( proj2 D) as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;

      set f = ( inf_op L);



       A1: ex_sup_of ((D1 "/\" D2),L) by WAYBEL_0: 75;



       A2: (f .: [:D1, D2:]) = (D1 "/\" D2) by Th32;



       A3: (f .: [:D1, D2:]) c= (f .: ( downarrow D)) & (f .: ( downarrow D)) c= ( downarrow (f .: D)) by Th13, RELAT_1: 123, YELLOW_3: 48;



       A4: (f .: D) is directed by YELLOW_2: 15;

      then

       A5: ex_sup_of ((f .: D),L) by WAYBEL_0: 75;

       ex_sup_of (( downarrow (f .: D)),L) by A4, WAYBEL_0: 75;

      then ( sup (D1 "/\" D2)) <= ( sup ( downarrow (f .: D))) by A1, A3, A2, XBOOLE_1: 1, YELLOW_0: 34;

      then

       A6: ( sup (D1 "/\" D2)) <= ( sup (f .: D)) by A5, WAYBEL_0: 33;

      (f .: D9) c= (f .: [:D1, D2:]) by RELAT_1: 123, YELLOW_3: 1;

      then (f .: D9) c= (D1 "/\" D2) by Th32;

      then ( sup (f .: D)) <= ( sup (D1 "/\" D2)) by A5, A1, YELLOW_0: 34;

      hence thesis by A6, ORDERS_2: 2;

    end;

    definition

      let L be non empty RelStr;

      :: WAYBEL_2:def5

      func sup_op L -> Function of [:L, L:], L means

      : Def5: for x,y be Element of L holds (it . (x,y)) = (x "\/" y);

      existence

      proof

        deffunc F( Element of L, Element of L) = ($1 "\/" $2);



         A1: for x,y be Element of L holds F(x,y) is Element of L;

        consider f be Function of [:L, L:], L such that

         A2: for x,y be Element of L holds (f . (x,y)) = F(x,y) from YELLOW_3:sch 6( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of [:L, L:], L such that

         A3: for x,y be Element of L holds (f . (x,y)) = (x "\/" y) and

         A4: for x,y be Element of L holds (g . (x,y)) = (x "\/" y);

        now

          let x,y be Element of L;



          thus (f . (x,y)) = (x "\/" y) by A3

          .= (g . (x,y)) by A4;

        end;

        hence f = g by YELLOW_3: 13;

      end;

    end

    theorem :: WAYBEL_2:34



     Th34: for L be non empty RelStr, x be Element of [:L, L:] holds (( sup_op L) . x) = ((x `1 ) "\/" (x `2 ))

    proof

      let L be non empty RelStr, x be Element of [:L, L:];

      the carrier of [:L, L:] = [:the carrier of L, the carrier of L:] by YELLOW_3:def 2;

      then ex a,b be object st a in the carrier of L & b in the carrier of L & x = [a, b] by ZFMISC_1:def 2;



      hence (( sup_op L) . x) = (( sup_op L) . ((x `1 ),(x `2 )))

      .= ((x `1 ) "\/" (x `2 )) by Def5;

    end;

    registration

      let L be with_suprema transitive antisymmetric RelStr;

      cluster ( sup_op L) -> monotone;

      coherence

      proof

        let x,y be Element of [:L, L:];

        set f = ( sup_op L);

        assume x <= y;

        then

         A1: (x `1 ) <= (y `1 ) & (x `2 ) <= (y `2 ) by YELLOW_3: 12;



         A2: (f . x) = ((x `1 ) "\/" (x `2 )) & (f . y) = ((y `1 ) "\/" (y `2 )) by Th34;

        let a,b be Element of L;

        assume a = (f . x) & b = (f . y);

        hence thesis by A1, A2, YELLOW_3: 3;

      end;

    end

    theorem :: WAYBEL_2:35



     Th35: for S be non empty RelStr, D1,D2 be Subset of S holds (( sup_op S) .: [:D1, D2:]) = (D1 "\/" D2)

    proof

      let S be non empty RelStr, D1,D2 be Subset of S;

      set f = ( sup_op S);

      reconsider X = [:D1, D2:] as set;

      thus (f .: [:D1, D2:]) c= (D1 "\/" D2)

      proof

        let q be object;

        assume

         A1: q in (f .: [:D1, D2:]);

        then

        reconsider q1 = q as Element of S;

        consider c be Element of [:S, S:] such that

         A2: c in [:D1, D2:] and

         A3: q1 = (f . c) by A1, FUNCT_2: 65;

        consider x,y be object such that

         A4: x in D1 & y in D2 and

         A5: c = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x, y as Element of S by A4;

        q = (f . (x,y)) by A3, A5

        .= (x "\/" y) by Def5;

        then q in { (a "\/" b) where a,b be Element of S : a in D1 & b in D2 } by A4;

        hence thesis by YELLOW_4:def 3;

      end;

      let q be object;

      assume q in (D1 "\/" D2);

      then q in { (x "\/" y) where x,y be Element of S : x in D1 & y in D2 } by YELLOW_4:def 3;

      then

      consider x,y be Element of S such that

       A6: q = (x "\/" y) & x in D1 & y in D2;

      q = (f . (x,y)) & [x, y] in X by A6, Def5, ZFMISC_1: 87;

      hence thesis by FUNCT_2: 35;

    end;

    theorem :: WAYBEL_2:36

    for L be complete non empty Poset holds for D be non empty filtered Subset of [:L, L:] holds ( inf (( sup_op L) .: D)) = ( inf (( proj1 D) "\/" ( proj2 D)))

    proof

      let L be complete non empty Poset, D be non empty filtered Subset of [:L, L:];

      reconsider C = the carrier of L as non empty set;

      reconsider D9 = D as non empty Subset of [:C, C:] by YELLOW_3:def 2;

      set D1 = ( proj1 D), D2 = ( proj2 D), f = ( sup_op L);



       A1: ex_inf_of ((D1 "\/" D2),L) by YELLOW_0: 17;



       A2: ex_inf_of (( uparrow (f .: D)),L) & (f .: [:D1, D2:]) c= (f .: ( uparrow D)) by RELAT_1: 123, YELLOW_0: 17, YELLOW_3: 49;

      (f .: ( uparrow D)) c= ( uparrow (f .: D)) & (f .: [:D1, D2:]) = (D1 "\/" D2) by Th14, Th35;

      then ( inf (D1 "\/" D2)) >= ( inf ( uparrow (f .: D))) by A1, A2, XBOOLE_1: 1, YELLOW_0: 35;

      then

       A3: ( inf (D1 "\/" D2)) >= ( inf (f .: D)) by WAYBEL_0: 38, YELLOW_0: 17;

      (f .: D9) c= (f .: [:D1, D2:]) by RELAT_1: 123, YELLOW_3: 1;

      then ex_inf_of ((f .: D9),L) & (f .: D9) c= (D1 "\/" D2) by Th35, YELLOW_0: 17;

      then ( inf (f .: D)) >= ( inf (D1 "\/" D2)) by A1, YELLOW_0: 35;

      hence thesis by A3, ORDERS_2: 2;

    end;

    begin

    definition

      let R be non empty reflexive RelStr;

      :: WAYBEL_2:def6

      attr R is satisfying_MC means

      : Def6: for x be Element of R, D be non empty directed Subset of R holds (x "/\" ( sup D)) = ( sup ( {x} "/\" D));

    end

    definition

      let R be non empty reflexive RelStr;

      :: WAYBEL_2:def7

      attr R is meet-continuous means R is up-complete satisfying_MC;

    end

    registration

      cluster -> satisfying_MC for 1 -element reflexive RelStr;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster meet-continuous -> up-complete satisfying_MC for non empty reflexive RelStr;

      coherence ;

      cluster up-complete satisfying_MC -> meet-continuous for non empty reflexive RelStr;

      coherence ;

    end

    theorem :: WAYBEL_2:37



     Th37: for S be non empty reflexive RelStr st for X be Subset of S, x be Element of S holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S)) holds S is satisfying_MC

    proof

      let S be non empty reflexive RelStr such that

       A1: for X be Subset of S, x be Element of S holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of S : y in X },S));

      let y be Element of S, D be non empty directed Subset of S;



      thus ( sup ( {y} "/\" D)) = ( "\/" ({ (y "/\" z) where z be Element of S : z in D },S)) by YELLOW_4: 42

      .= (y "/\" ( sup D)) by A1;

    end;

    theorem :: WAYBEL_2:38



     Th38: for L be up-complete Semilattice st ( SupMap L) is meet-preserving holds for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2))

    proof

      let L be up-complete Semilattice such that

       A1: ( SupMap L) is meet-preserving;

      set f = ( SupMap L);

      let I1,I2 be Ideal of L;

      reconsider x = I1, y = I2 as Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;



       A2: f preserves_inf_of {x, y} by A1;

      reconsider fx = (f . x) as Element of L;



      thus (( sup I1) "/\" ( sup I2)) = (fx "/\" ( sup I2)) by YELLOW_2:def 3

      .= ((f . x) "/\" (f . y)) by YELLOW_2:def 3

      .= (f . (x "/\" y)) by A2, YELLOW_3: 8

      .= (f . (I1 "/\" I2)) by YELLOW_4: 58

      .= ( sup (I1 "/\" I2)) by YELLOW_2:def 3;

    end;

    registration

      let L be up-complete sup-Semilattice;

      cluster ( SupMap L) -> join-preserving;

      coherence

      proof

        let x,y be Element of ( InclPoset ( Ids L));

        set f = ( SupMap L);

        assume ex_sup_of ( {x, y},( InclPoset ( Ids L)));

        reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2: 41;



         A1: ex_sup_of ((x1 "\/" y1),L) by WAYBEL_0: 75;



         A2: ( dom f) = the carrier of ( InclPoset ( Ids L)) by FUNCT_2:def 1;

        then (f .: {x, y}) = {(f . x), (f . y)} by FUNCT_1: 60;

        hence ex_sup_of ((f .: {x, y}),L) by YELLOW_0: 20;



        thus ( sup (f .: {x, y})) = ( sup {(f . x), (f . y)}) by A2, FUNCT_1: 60

        .= ((f . x) "\/" (f . y)) by YELLOW_0: 41

        .= ((f . x) "\/" ( sup y1)) by YELLOW_2:def 3

        .= (( sup x1) "\/" ( sup y1)) by YELLOW_2:def 3

        .= ( sup (x1 "\/" y1)) by Th4

        .= ( sup ( downarrow (x1 "\/" y1))) by A1, WAYBEL_0: 33

        .= (f . ( downarrow (x1 "\/" y1))) by YELLOW_2:def 3

        .= (f . (x "\/" y)) by YELLOW_4: 30

        .= (f . ( sup {x, y})) by YELLOW_0: 41;

      end;

    end

    theorem :: WAYBEL_2:39



     Th39: for L be up-complete Semilattice st for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2)) holds ( SupMap L) is meet-preserving

    proof

      let L be up-complete Semilattice such that

       A1: for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2));

      let x,y be Element of ( InclPoset ( Ids L));

      set f = ( SupMap L);

      assume ex_inf_of ( {x, y},( InclPoset ( Ids L)));

      reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2: 41;



       A2: ( dom f) = the carrier of ( InclPoset ( Ids L)) by FUNCT_2:def 1;

      then (f .: {x, y}) = {(f . x), (f . y)} by FUNCT_1: 60;

      hence ex_inf_of ((f .: {x, y}),L) by YELLOW_0: 21;



      thus ( inf (f .: {x, y})) = ( inf {(f . x), (f . y)}) by A2, FUNCT_1: 60

      .= ((f . x) "/\" (f . y)) by YELLOW_0: 40

      .= ((f . x) "/\" ( sup y1)) by YELLOW_2:def 3

      .= (( sup x1) "/\" ( sup y1)) by YELLOW_2:def 3

      .= ( sup (x1 "/\" y1)) by A1

      .= (f . (x1 "/\" y1)) by YELLOW_2:def 3

      .= (f . (x "/\" y)) by YELLOW_4: 58

      .= (f . ( inf {x, y})) by YELLOW_0: 40;

    end;

    theorem :: WAYBEL_2:40



     Th40: for L be up-complete Semilattice st for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2)) holds for D1,D2 be directed non empty Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2))

    proof

      let L be up-complete Semilattice such that

       A1: for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2));

      let D1,D2 be directed non empty Subset of L;



       A2: ex_sup_of (D2,L) by WAYBEL_0: 75;



       A3: ex_sup_of ((( downarrow D1) "/\" ( downarrow D2)),L) by WAYBEL_0: 75;



       A4: ex_sup_of ((D1 "/\" D2),L) by WAYBEL_0: 75;

       ex_sup_of (D1,L) by WAYBEL_0: 75;



      hence (( sup D1) "/\" ( sup D2)) = (( sup ( downarrow D1)) "/\" ( sup D2)) by WAYBEL_0: 33

      .= (( sup ( downarrow D1)) "/\" ( sup ( downarrow D2))) by A2, WAYBEL_0: 33

      .= ( sup (( downarrow D1) "/\" ( downarrow D2))) by A1

      .= ( sup ( downarrow (( downarrow D1) "/\" ( downarrow D2)))) by A3, WAYBEL_0: 33

      .= ( sup ( downarrow (D1 "/\" D2))) by YELLOW_4: 62

      .= ( sup (D1 "/\" D2)) by A4, WAYBEL_0: 33;

    end;

    theorem :: WAYBEL_2:41



     Th41: for L be non empty reflexive RelStr st L is satisfying_MC holds for x be Element of L, N be non empty prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L)))))

    proof

      let L be non empty reflexive RelStr such that

       A1: L is satisfying_MC;

      let x be Element of L, N be non empty prenet of L;

      assume N is eventually-directed;

      then

       A2: ( rng ( netmap (N,L))) is directed by Th18;



      thus (x "/\" ( sup N)) = (x "/\" ( sup ( rng ( netmap (N,L))))) by YELLOW_2:def 5

      .= ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by A1, A2;

    end;

    theorem :: WAYBEL_2:42



     Th42: for L be non empty reflexive RelStr st for x be Element of L, N be prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L))))) holds L is satisfying_MC

    proof

      let L be non empty reflexive RelStr such that

       A1: for x be Element of L, N be prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L)))));

      let x be Element of L, D be non empty directed Subset of L;

      reconsider n = ( id D) as Function of D, the carrier of L by FUNCT_2: 7;

      reconsider N = NetStr (# D, (the InternalRel of L |_2 D), n #) as prenet of L by Th19;



       A2: ( Sup ( netmap (N,L))) = ( sup N);

      D c= D;



      then

       A3: D = (n .: D) by FUNCT_1: 92

      .= ( rng ( netmap (N,L))) by RELSET_1: 22;



      hence (x "/\" ( sup D)) = (x "/\" ( Sup ( netmap (N,L)))) by YELLOW_2:def 5

      .= ( sup ( {x} "/\" D)) by A1, A3, A2, Th20;

    end;

    theorem :: WAYBEL_2:43



     Th43: for L be up-complete antisymmetric non empty reflexive RelStr st ( inf_op L) is directed-sups-preserving holds for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2))

    proof

      let L be up-complete antisymmetric non empty reflexive RelStr such that

       A1: ( inf_op L) is directed-sups-preserving;

      let D1,D2 be non empty directed Subset of L;

      set X = [:D1, D2:], f = ( inf_op L);



       A2: f preserves_sup_of X by A1;



       A3: ex_sup_of (X, [:L, L:]) by WAYBEL_0: 75;



       A4: ex_sup_of (D1,L) & ex_sup_of (D2,L) by WAYBEL_0: 75;



      thus (( sup D1) "/\" ( sup D2)) = (f . (( sup D1),( sup D2))) by Def4

      .= (f . ( sup X)) by A4, YELLOW_3: 43

      .= ( sup (f .: X)) by A2, A3

      .= ( sup (D1 "/\" D2)) by Th32;

    end;

    theorem :: WAYBEL_2:44



     Th44: for L be non empty reflexive antisymmetric RelStr st for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2)) holds L is satisfying_MC

    proof

      let L be non empty reflexive antisymmetric RelStr such that

       A1: for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2));

      let x be Element of L, D be non empty directed Subset of L;



       A2: {x} is directed by WAYBEL_0: 5;



      thus (x "/\" ( sup D)) = (( sup {x}) "/\" ( sup D)) by YELLOW_0: 39

      .= ( sup ( {x} "/\" D)) by A1, A2;

    end;

    theorem :: WAYBEL_2:45



     Th45: for L be satisfying_MC with_infima antisymmetric non empty reflexive RelStr holds for x be Element of L, D be non empty directed Subset of L st x <= ( sup D) holds x = ( sup ( {x} "/\" D))

    proof

      let L be satisfying_MC with_infima antisymmetric non empty reflexive RelStr;

      let x be Element of L, D be non empty directed Subset of L;

      assume x <= ( sup D);



      hence x = (x "/\" ( sup D)) by YELLOW_0: 25

      .= ( sup ( {x} "/\" D)) by Def6;

    end;

    theorem :: WAYBEL_2:46



     Th46: for L be up-complete Semilattice st for x be Element of L, E be non empty directed Subset of L st x <= ( sup E) holds x <= ( sup ( {x} "/\" E)) holds ( inf_op L) is directed-sups-preserving

    proof

      let L be up-complete Semilattice such that

       A1: for x be Element of L, E be non empty directed Subset of L st x <= ( sup E) holds x <= ( sup ( {x} "/\" E));

      let D be Subset of [:L, L:];

      assume D is non empty directed;

      then

      reconsider DD = D as non empty directed Subset of [:L, L:];

      thus ( inf_op L) preserves_sup_of D

      proof

        reconsider D1 = ( proj1 DD), D2 = ( proj2 DD) as non empty directed Subset of L by YELLOW_3: 21, YELLOW_3: 22;

        reconsider C = the carrier of L as non empty set;

        set f = ( inf_op L);

        assume ex_sup_of (D, [:L, L:]);

        set d2 = ( sup D2);

        defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" D2) & x in D1;

        (f .: DD) is directed by YELLOW_2: 15;

        hence ex_sup_of ((f .: D),L) by WAYBEL_0: 75;

        { (x "/\" y) where x,y be Element of L : x in D1 & y in {d2} } c= C

        proof

          let q be object;

          assume q in { (x "/\" y) where x,y be Element of L : x in D1 & y in {d2} };

          then ex x,y be Element of L st q = (x "/\" y) & x in D1 & y in {d2};

          hence thesis;

        end;

        then

        reconsider F = { (x "/\" y) where x,y be Element of L : x in D1 & y in {d2} } as Subset of L;



         A2: ( "\/" ({ ( sup X) where X be non empty directed Subset of L : P[X] },L)) = ( "\/" (( union { X where X be non empty directed Subset of L : P[X] }),L)) by Th10;



         A3: F = { ( sup ( {z} "/\" D2)) where z be Element of L : z in D1 }

        proof

          thus F c= { ( sup ( {z} "/\" D2)) where z be Element of L : z in D1 }

          proof

            let q be object;

            assume q in F;

            then

            consider x,y be Element of L such that

             A4: q = (x "/\" y) and

             A5: x in D1 and

             A6: y in {d2};

            q = (x "/\" d2) by A4, A6, TARSKI:def 1

            .= ( sup ( {x} "/\" D2)) by A1, Th28;

            hence thesis by A5;

          end;

          let q be object;



           A7: d2 in {d2} by TARSKI:def 1;

          assume q in { ( sup ( {z} "/\" D2)) where z be Element of L : z in D1 };

          then

          consider z be Element of L such that

           A8: q = ( sup ( {z} "/\" D2)) and

           A9: z in D1;

          q = (z "/\" d2) by A1, A8, Th28;

          hence thesis by A9, A7;

        end;



        thus ( sup (f .: D)) = ( sup (D1 "/\" D2)) by Th33

        .= ( "\/" ({ ( "\/" (X,L)) where X be non empty directed Subset of L : P[X] },L)) by A2, Th6

        .= ( "\/" ({ ( sup ( {x} "/\" D2)) where x be Element of L : x in D1 },L)) by Th5

        .= ( sup ( {d2} "/\" D1)) by A3, YELLOW_4:def 4

        .= (( sup D1) "/\" d2) by A1, Th28

        .= (f . (( sup D1),( sup D2))) by Def4

        .= (f . ( sup D)) by Th12;

      end;

    end;

    theorem :: WAYBEL_2:47



     Th47: for L be complete antisymmetric non empty reflexive RelStr st for x be Element of L, N be prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L))))) holds for x be Element of L, J be set, f be Function of J, the carrier of L holds (x "/\" ( Sup f)) = ( sup (x "/\" ( FinSups f)))

    proof

      let L be complete antisymmetric non empty reflexive RelStr such that

       A1: for x be Element of L, N be prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L)))));

      let x be Element of L, J be set, f be Function of J, the carrier of L;

      set F = ( FinSups f);



       A2: for x be Element of ( Fin J) holds ex_sup_of ((f .: x),L) by YELLOW_0: 17;

       ex_sup_of (( rng f),L) & ex_sup_of (( rng ( netmap (( FinSups f),L))),L) by YELLOW_0: 17;



      hence (x "/\" ( Sup f)) = (x "/\" ( sup F)) by A2, Th26

      .= ( sup ( {x} "/\" ( rng ( netmap (F,L))))) by A1

      .= ( "\/" (( rng the mapping of (x "/\" F)),L)) by Th23

      .= ( sup (x "/\" F)) by YELLOW_2:def 5;

    end;

    theorem :: WAYBEL_2:48



     Th48: for L be complete Semilattice st for x be Element of L, J be set, f be Function of J, the carrier of L holds (x "/\" ( Sup f)) = ( sup (x "/\" ( FinSups f))) holds for x be Element of L, N be prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L)))))

    proof

      let L be complete Semilattice such that

       A1: for x be Element of L, J be set holds for f be Function of J, the carrier of L holds (x "/\" ( Sup f)) = ( sup (x "/\" ( FinSups f)));

      let x be Element of L, N be prenet of L such that

       A2: N is eventually-directed;

      reconsider R = ( rng ( netmap (N,L))) as non empty directed Subset of L by A2, Th18;

      reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0: 5;

      set f = the mapping of N;

      set h = the mapping of ( FinSups f);



       A3: ex_sup_of ((xx "/\" R),L) by WAYBEL_0: 75;



       A4: ( rng the mapping of (x "/\" ( FinSups f))) is_<=_than ( sup ( {x} "/\" ( rng ( netmap (N,L)))))

      proof

        let a be Element of L;



         A5: ( {x} "/\" ( rng h)) = { (x "/\" y) where y be Element of L : y in ( rng h) } by YELLOW_4: 42;

        assume a in ( rng the mapping of (x "/\" ( FinSups f)));

        then a in ( {x} "/\" ( rng h)) by Th23;

        then

        consider y be Element of L such that

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

         A7: y in ( rng h) by A5;

        for x be set holds ex_sup_of ((f .: x),L) by YELLOW_0: 17;

        then ( rng ( netmap (( FinSups f),L))) c= ( finsups ( rng f)) by Th24;

        then y in ( finsups ( rng f)) by A7;

        then

        consider Y be finite Subset of ( rng f) such that

         A8: y = ( "\/" (Y,L)) and

         A9: ex_sup_of (Y,L);

        ( rng ( netmap (N,L))) is directed by A2, Th18;

        then

        consider z be Element of L such that

         A10: z in ( rng f) and

         A11: z is_>=_than Y by WAYBEL_0: 1;



         A12: x <= x;

        ( "\/" (Y,L)) <= z by A9, A11, YELLOW_0: 30;

        then

         A13: (x "/\" y) <= (x "/\" z) by A8, A12, YELLOW_3: 2;

        x in {x} by TARSKI:def 1;

        then (x "/\" z) <= ( sup (xx "/\" ( rng f))) by A3, A10, YELLOW_4: 1, YELLOW_4: 37;

        hence a <= ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by A6, A13, YELLOW_0:def 2;

      end;

      (x "/\" ( FinSups f)) is eventually-directed by Th27;

      then ( rng ( netmap ((x "/\" ( FinSups f)),L))) is directed by Th18;

      then ex_sup_of (( rng the mapping of (x "/\" ( FinSups f))),L) by WAYBEL_0: 75;

      then ( sup (x "/\" ( FinSups f))) = ( "\/" (( rng the mapping of (x "/\" ( FinSups f))),L)) & ( "\/" (( rng the mapping of (x "/\" ( FinSups f))),L)) <= ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by A4, YELLOW_0:def 9, YELLOW_2:def 5;

      then

       A14: (x "/\" ( Sup ( netmap (N,L)))) <= ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by A1;

       ex_sup_of (R,L) & ( Sup ( netmap (N,L))) = ( "\/" (( rng ( netmap (N,L))),L)) by WAYBEL_0: 75, YELLOW_2:def 5;

      then ( sup ( {x} "/\" ( rng ( netmap (N,L))))) <= (x "/\" ( Sup ( netmap (N,L)))) by A3, YELLOW_4: 53;

      hence thesis by A14, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_2:49



     Th49: for L be up-complete LATTICE holds L is meet-continuous iff ( SupMap L) is meet-preserving join-preserving

    proof

      let L be up-complete LATTICE;

      hereby

        assume

         A1: L is meet-continuous;

        for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2))

        proof

          let D1,D2 be non empty directed Subset of L;

          for x be Element of L, E be non empty directed Subset of L st x <= ( sup E) holds x <= ( sup ( {x} "/\" E)) by A1, Th45;

          then ( inf_op L) is directed-sups-preserving by Th46;

          hence thesis by Th43;

        end;

        then for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2));

        hence ( SupMap L) is meet-preserving join-preserving by Th39;

      end;

      assume

       A2: ( SupMap L) is meet-preserving join-preserving;

      thus L is up-complete;

      for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2)) by A2, Th38;

      then for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2)) by Th40;

      hence thesis by Th44;

    end;

    registration

      let L be meet-continuous LATTICE;

      cluster ( SupMap L) -> meet-preserving join-preserving;

      coherence by Th49;

    end

    theorem :: WAYBEL_2:50



     Th50: for L be up-complete LATTICE holds L is meet-continuous iff for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2))

    proof

      let L be up-complete LATTICE;

      hereby

        assume L is meet-continuous;

        then ( SupMap L) is meet-preserving join-preserving;

        hence for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2)) by Th38;

      end;

      assume for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2));

      then for D1,D2 be directed non empty Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2)) by Th40;

      hence L is up-complete & L is satisfying_MC by Th44;

    end;

    theorem :: WAYBEL_2:51



     Th51: for L be up-complete LATTICE holds L is meet-continuous iff for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2))

    proof

      let L be up-complete LATTICE;

      hereby

        assume L is meet-continuous;

        then for I1,I2 be Ideal of L holds (( sup I1) "/\" ( sup I2)) = ( sup (I1 "/\" I2)) by Th50;

        hence for D1,D2 be directed non empty Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2)) by Th40;

      end;

      assume for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2));

      hence L is up-complete & L is satisfying_MC by Th44;

    end;

    theorem :: WAYBEL_2:52

    for L be up-complete LATTICE holds L is meet-continuous iff for x be Element of L, D be non empty directed Subset of L st x <= ( sup D) holds x = ( sup ( {x} "/\" D))

    proof

      let L be up-complete LATTICE;

      thus L is meet-continuous implies for x be Element of L, D be non empty directed Subset of L st x <= ( sup D) holds x = ( sup ( {x} "/\" D)) by Th45;

      assume for x be Element of L, D be non empty directed Subset of L st x <= ( sup D) holds x = ( sup ( {x} "/\" D));

      then for x be Element of L, D be non empty directed Subset of L st x <= ( sup D) holds x <= ( sup ( {x} "/\" D));

      then ( inf_op L) is directed-sups-preserving by Th46;

      then for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2)) by Th43;

      hence thesis by Th51;

    end;

    theorem :: WAYBEL_2:53



     Th53: for L be up-complete Semilattice holds L is meet-continuous iff ( inf_op L) is directed-sups-preserving

    proof

      let L be up-complete Semilattice;

      hereby

        assume L is meet-continuous;

        then for x be Element of L, D be non empty directed Subset of L st x <= ( sup D) holds x <= ( sup ( {x} "/\" D)) by Th45;

        hence ( inf_op L) is directed-sups-preserving by Th46;

      end;

      assume ( inf_op L) is directed-sups-preserving;

      then for D1,D2 be non empty directed Subset of L holds (( sup D1) "/\" ( sup D2)) = ( sup (D1 "/\" D2)) by Th43;

      hence L is up-complete & L is satisfying_MC by Th44;

    end;

    registration

      let L be meet-continuous Semilattice;

      cluster ( inf_op L) -> directed-sups-preserving;

      coherence by Th53;

    end

    theorem :: WAYBEL_2:54



     Th54: for L be up-complete Semilattice holds L is meet-continuous iff for x be Element of L, N be non empty prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by Th41, Th42;

    theorem :: WAYBEL_2:55

    for L be complete Semilattice holds L is meet-continuous iff for x be Element of L, J be set holds for f be Function of J, the carrier of L holds (x "/\" ( Sup f)) = ( sup (x "/\" ( FinSups f)))

    proof

      let L be complete Semilattice;

      hereby

        assume L is meet-continuous;

        then for x be Element of L, N be non empty prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by Th54;

        hence for x be Element of L, J be set holds for f be Function of J, the carrier of L holds (x "/\" ( Sup f)) = ( sup (x "/\" ( FinSups f))) by Th47;

      end;

      assume for x be Element of L, J be set holds for f be Function of J, the carrier of L holds (x "/\" ( Sup f)) = ( sup (x "/\" ( FinSups f)));

      then for x be Element of L, N be prenet of L st N is eventually-directed holds (x "/\" ( sup N)) = ( sup ( {x} "/\" ( rng ( netmap (N,L))))) by Th48;

      hence L is up-complete & L is satisfying_MC by Th42;

    end;



     Lm1: for L be meet-continuous Semilattice, x be Element of L holds (x "/\" ) is directed-sups-preserving

    proof

      let L be meet-continuous Semilattice, x be Element of L;

      let X be Subset of L such that

       A1: X is non empty directed;

      reconsider X1 = X as non empty Subset of L by A1;

      assume ex_sup_of (X,L);



       A2: ((x "/\" ) .: X1) is non empty;

      ((x "/\" ) .: X) is directed by A1, YELLOW_2: 15;

      hence ex_sup_of (((x "/\" ) .: X),L) by A2, WAYBEL_0: 75;



       A3: for x be Element of L, E be non empty directed Subset of L st x <= ( sup E) holds x <= ( sup ( {x} "/\" E)) by Th45;



      thus ( sup ((x "/\" ) .: X)) = ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L)) by WAYBEL_1: 61

      .= ( sup ( {x} "/\" X)) by YELLOW_4: 42

      .= (x "/\" ( sup X)) by A1, A3, Th28

      .= ((x "/\" ) . ( sup X)) by WAYBEL_1:def 18;

    end;

    registration

      let L be meet-continuous Semilattice, x be Element of L;

      cluster (x "/\" ) -> directed-sups-preserving;

      coherence by Lm1;

    end

    theorem :: WAYBEL_2:56



     Th56: for H be complete non empty Poset holds H is Heyting iff H is meet-continuous distributive

    proof

      let H be complete non empty Poset;

      hereby

        assume

         A1: H is Heyting;

        then for x be Element of H holds (x "/\" ) is lower_adjoint;

        then for X be Subset of H, x be Element of H holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of H : y in X },H)) by WAYBEL_1: 64;

        then H is up-complete satisfying_MC by Th37;

        hence H is meet-continuous;

        thus H is distributive by A1;

      end;

      assume

       A2: H is meet-continuous distributive;

      thus H is LATTICE;

      let a be Element of H;

      (for X be finite Subset of H holds (a "/\" ) preserves_sup_of X) & for X be non empty directed Subset of H holds (a "/\" ) preserves_sup_of X by A2, Th17, WAYBEL_0:def 37;

      then (a "/\" ) is sups-preserving by WAYBEL_0: 74;

      hence thesis by WAYBEL_1: 17;

    end;

    registration

      cluster complete Heyting -> meet-continuous distributive for non empty Poset;

      coherence by Th56;

      cluster complete meet-continuous distributive -> Heyting for non empty Poset;

      coherence by Th56;

    end