waybel16.miz



    begin

    theorem :: WAYBEL16:1

    

     Th1: for L be sup-Semilattice holds for x,y be Element of L holds ( "/\" ((( uparrow x) /\ ( uparrow y)),L)) = (x "\/" y)

    proof

      let L be sup-Semilattice;

      let x,y be Element of L;

      (( uparrow x) /\ ( uparrow y)) = ( uparrow (x "\/" y)) by WAYBEL14: 4;

      hence thesis by WAYBEL_0: 39;

    end;

    theorem :: WAYBEL16:2

    for L be Semilattice holds for x,y be Element of L holds ( "\/" ((( downarrow x) /\ ( downarrow y)),L)) = (x "/\" y)

    proof

      let L be Semilattice;

      let x,y be Element of L;

      (( downarrow x) /\ ( downarrow y)) = ( downarrow (x "/\" y)) by WAYBEL14: 3;

      hence thesis by WAYBEL_0: 34;

    end;

    theorem :: WAYBEL16:3

    

     Th3: for L be non empty RelStr holds for x,y be Element of L st x is_maximal_in (the carrier of L \ ( uparrow y)) holds (( uparrow x) \ {x}) = (( uparrow x) /\ ( uparrow y))

    proof

      let L be non empty RelStr;

      let x,y be Element of L;

      assume

       A1: x is_maximal_in (the carrier of L \ ( uparrow y));

      then x in (the carrier of L \ ( uparrow y)) by WAYBEL_4: 55;

      then not x in ( uparrow y) by XBOOLE_0:def 5;

      then

       A2: not y <= x by WAYBEL_0: 18;

      thus (( uparrow x) \ {x}) c= (( uparrow x) /\ ( uparrow y))

      proof

        let a be object;

        assume

         A3: a in (( uparrow x) \ {x});

        then

        reconsider a1 = a as Element of L;

         not a in {x} by A3, XBOOLE_0:def 5;

        then

         A4: a1 <> x by TARSKI:def 1;

        

         A5: a in ( uparrow x) by A3, XBOOLE_0:def 5;

        then x <= a1 by WAYBEL_0: 18;

        then x < a1 by A4, ORDERS_2:def 6;

        then not a1 in (the carrier of L \ ( uparrow y)) by A1, WAYBEL_4: 55;

        then a in ( uparrow y) by XBOOLE_0:def 5;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      let a be object;

      assume

       A6: a in (( uparrow x) /\ ( uparrow y));

      then

       A7: a in ( uparrow x) by XBOOLE_0:def 4;

      reconsider a1 = a as Element of L by A6;

      a in ( uparrow y) by A6, XBOOLE_0:def 4;

      then y <= a1 by WAYBEL_0: 18;

      then not a in {x} by A2, TARSKI:def 1;

      hence thesis by A7, XBOOLE_0:def 5;

    end;

    theorem :: WAYBEL16:4

    for L be non empty RelStr holds for x,y be Element of L st x is_minimal_in (the carrier of L \ ( downarrow y)) holds (( downarrow x) \ {x}) = (( downarrow x) /\ ( downarrow y))

    proof

      let L be non empty RelStr;

      let x,y be Element of L;

      assume

       A1: x is_minimal_in (the carrier of L \ ( downarrow y));

      then x in (the carrier of L \ ( downarrow y)) by WAYBEL_4: 56;

      then not x in ( downarrow y) by XBOOLE_0:def 5;

      then

       A2: not x <= y by WAYBEL_0: 17;

      thus (( downarrow x) \ {x}) c= (( downarrow x) /\ ( downarrow y))

      proof

        let a be object;

        assume

         A3: a in (( downarrow x) \ {x});

        then

        reconsider a1 = a as Element of L;

         not a in {x} by A3, XBOOLE_0:def 5;

        then

         A4: a1 <> x by TARSKI:def 1;

        

         A5: a in ( downarrow x) by A3, XBOOLE_0:def 5;

        then a1 <= x by WAYBEL_0: 17;

        then a1 < x by A4, ORDERS_2:def 6;

        then not a1 in (the carrier of L \ ( downarrow y)) by A1, WAYBEL_4: 56;

        then a in ( downarrow y) by XBOOLE_0:def 5;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      let a be object;

      assume

       A6: a in (( downarrow x) /\ ( downarrow y));

      then

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

      reconsider a1 = a as Element of L by A6;

      a in ( downarrow y) by A6, XBOOLE_0:def 4;

      then a1 <= y by WAYBEL_0: 17;

      then not a in {x} by A2, TARSKI:def 1;

      hence thesis by A7, XBOOLE_0:def 5;

    end;

    theorem :: WAYBEL16:5

    

     Th5: for L be with_suprema Poset holds for X,Y be Subset of L holds for X9,Y9 be Subset of (L opp ) st X = X9 & Y = Y9 holds (X "\/" Y) = (X9 "/\" Y9)

    proof

      let L be with_suprema Poset;

      let X,Y be Subset of L;

      let X9,Y9 be Subset of (L opp );

      assume

       A1: X = X9 & Y = Y9;

      thus (X "\/" Y) c= (X9 "/\" Y9)

      proof

        let a be object;

        assume a in (X "\/" Y);

        then a in { (p "\/" q) where p,q be Element of L : p in X & q in Y } by YELLOW_4:def 3;

        then

        consider x,y be Element of L such that

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

         A3: x in X & y in Y;

        

         A4: a = ((x ~ ) "/\" (y ~ )) by A2, YELLOW_7: 23;

        (x ~ ) in X9 & (y ~ ) in Y9 by A1, A3, LATTICE3:def 6;

        then a in { (p "/\" q) where p,q be Element of (L opp ) : p in X9 & q in Y9 } by A4;

        hence thesis by YELLOW_4:def 4;

      end;

      let a be object;

      assume a in (X9 "/\" Y9);

      then a in { (p "/\" q) where p,q be Element of (L opp ) : p in X9 & q in Y9 } by YELLOW_4:def 4;

      then

      consider x,y be Element of (L opp ) such that

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

       A6: x in X9 & y in Y9;

      

       A7: a = (( ~ x) "\/" ( ~ y)) by A5, YELLOW_7: 24;

      ( ~ x) in X & ( ~ y) in Y by A1, A6, LATTICE3:def 7;

      then a in { (p "\/" q) where p,q be Element of L : p in X & q in Y } by A7;

      hence thesis by YELLOW_4:def 3;

    end;

    theorem :: WAYBEL16:6

    for L be with_infima Poset holds for X,Y be Subset of L holds for X9,Y9 be Subset of (L opp ) st X = X9 & Y = Y9 holds (X "/\" Y) = (X9 "\/" Y9)

    proof

      let L be with_infima Poset;

      let X,Y be Subset of L;

      let X9,Y9 be Subset of (L opp );

      assume

       A1: X = X9 & Y = Y9;

      thus (X "/\" Y) c= (X9 "\/" Y9)

      proof

        let a be object;

        assume a in (X "/\" Y);

        then a in { (p "/\" q) where p,q be Element of L : p in X & q in Y } by YELLOW_4:def 4;

        then

        consider x,y be Element of L such that

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

         A3: x in X & y in Y;

        

         A4: a = ((x ~ ) "\/" (y ~ )) by A2, YELLOW_7: 21;

        (x ~ ) in X9 & (y ~ ) in Y9 by A1, A3, LATTICE3:def 6;

        then a in { (p "\/" q) where p,q be Element of (L opp ) : p in X9 & q in Y9 } by A4;

        hence thesis by YELLOW_4:def 3;

      end;

      let a be object;

      assume a in (X9 "\/" Y9);

      then a in { (p "\/" q) where p,q be Element of (L opp ) : p in X9 & q in Y9 } by YELLOW_4:def 3;

      then

      consider x,y be Element of (L opp ) such that

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

       A6: x in X9 & y in Y9;

      

       A7: a = (( ~ x) "/\" ( ~ y)) by A5, YELLOW_7: 22;

      ( ~ x) in X & ( ~ y) in Y by A1, A6, LATTICE3:def 7;

      then a in { (p "/\" q) where p,q be Element of L : p in X & q in Y } by A7;

      hence thesis by YELLOW_4:def 4;

    end;

    theorem :: WAYBEL16:7

    

     Th7: for L be non empty reflexive transitive RelStr holds ( Filt L) = ( Ids (L opp ))

    proof

      let L be non empty reflexive transitive RelStr;

      

       A1: ( Ids (L opp )) c= ( Filt L)

      proof

        let x be object;

        assume x in ( Ids (L opp ));

        then x in the set of all X where X be Ideal of (L opp ) by WAYBEL_0:def 23;

        then

        consider x1 be Ideal of (L opp ) such that

         A2: x1 = x;

        x1 is upper Subset of L & x1 is filtered Subset of L by YELLOW_7: 27, YELLOW_7: 29;

        then x in the set of all X where X be Filter of L by A2;

        hence thesis by WAYBEL_0:def 24;

      end;

      ( Filt L) c= ( Ids (L opp ))

      proof

        let x be object;

        assume x in ( Filt L);

        then x in the set of all X where X be Filter of L by WAYBEL_0:def 24;

        then

        consider x1 be Filter of L such that

         A3: x1 = x;

        x1 is lower Subset of (L opp ) & x1 is directed Subset of (L opp ) by YELLOW_7: 27, YELLOW_7: 29;

        then x in the set of all X where X be Ideal of (L opp ) by A3;

        hence thesis by WAYBEL_0:def 23;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL16:8

    for L be non empty reflexive transitive RelStr holds ( Ids L) = ( Filt (L opp ))

    proof

      let L be non empty reflexive transitive RelStr;

      

       A1: ( Filt (L opp )) c= ( Ids L)

      proof

        let x be object;

        assume x in ( Filt (L opp ));

        then x in the set of all X where X be Filter of (L opp ) by WAYBEL_0:def 24;

        then

        consider x1 be Filter of (L opp ) such that

         A2: x1 = x;

        x1 is lower Subset of L & x1 is directed Subset of L by YELLOW_7: 26, YELLOW_7: 28;

        then x in the set of all X where X be Ideal of L by A2;

        hence thesis by WAYBEL_0:def 23;

      end;

      ( Ids L) c= ( Filt (L opp ))

      proof

        let x be object;

        assume x in ( Ids L);

        then x in the set of all X where X be Ideal of L by WAYBEL_0:def 23;

        then

        consider x1 be Ideal of L such that

         A3: x1 = x;

        x1 is upper Subset of (L opp ) & x1 is filtered Subset of (L opp ) by YELLOW_7: 26, YELLOW_7: 28;

        then x in the set of all X where X be Filter of (L opp ) by A3;

        hence thesis by WAYBEL_0:def 24;

      end;

      hence thesis by A1;

    end;

    begin

    definition

      let S,T be complete non empty Poset;

      :: WAYBEL16:def1

      mode CLHomomorphism of S,T -> Function of S, T means it is directed-sups-preserving infs-preserving;

      existence

      proof

        reconsider f = (the carrier of S --> ( Top T)) as Function of the carrier of S, the carrier of T;

        reconsider f as Function of S, T;

        take f;

        now

          let X be Subset of S;

          assume

           A1: X is non empty directed;

          now

            assume ex_sup_of (X,S);

            ( rng f) = {( Top T)} by FUNCOP_1: 8;

            then

             A2: (f .: X) c= {( Top T)} by RELAT_1: 111;

            now

              let x,y be Element of S;

              assume x <= y;

              (f . x) = ( Top T) by FUNCOP_1: 7

              .= (f . y) by FUNCOP_1: 7;

              hence (f . x) <= (f . y);

            end;

            then f is monotone by WAYBEL_1:def 2;

            then

             A3: (f .: X) is non empty finite directed Subset of T by A1, A2, YELLOW_2: 15;

            hence ex_sup_of ((f .: X),T) by WAYBEL_0: 75;

            ( sup (f .: X)) in (f .: X) by A3, WAYBEL_3: 16;

            then ( sup (f .: X)) = ( Top T) by A2, TARSKI:def 1;

            hence ( sup (f .: X)) = (f . ( sup X)) by FUNCOP_1: 7;

          end;

          hence f preserves_sup_of X by WAYBEL_0:def 31;

        end;

        hence f is directed-sups-preserving by WAYBEL_0:def 37;

        now

          let X be Subset of S;

          now

            assume ex_inf_of (X,S);

            thus ex_inf_of ((f .: X),T) by YELLOW_0: 17;

            ( rng f) = {( Top T)} by FUNCOP_1: 8;

            then

             A4: (f .: X) is Subset of {( Top T)} by RELAT_1: 111;

            now

              per cases ;

                suppose (f .: X) = {} ;

                

                hence ( inf (f .: X)) = ( Top T) by YELLOW_0:def 12

                .= (f . ( inf X)) by FUNCOP_1: 7;

              end;

                suppose (f .: X) <> {} ;

                then (f .: X) = {( Top T)} by A4, ZFMISC_1: 33;

                

                hence ( inf (f .: X)) = ( Top T) by YELLOW_0: 39

                .= (f . ( inf X)) by FUNCOP_1: 7;

              end;

            end;

            hence ( inf (f .: X)) = (f . ( inf X));

          end;

          hence f preserves_inf_of X by WAYBEL_0:def 30;

        end;

        hence thesis by WAYBEL_0:def 32;

      end;

    end

    definition

      let S be continuous complete non empty Poset;

      let A be Subset of S;

      :: WAYBEL16:def2

      pred A is_FG_set means for T be continuous complete non empty Poset holds for f be Function of A, the carrier of T holds ex h be CLHomomorphism of S, T st (h | A) = f & for h9 be CLHomomorphism of S, T st (h9 | A) = f holds h9 = h;

    end

    registration

      let L be upper-bounded non empty Poset;

      cluster ( Filt L) -> non empty;

      coherence

      proof

        now

          let x,y be Element of L;

          assume that

           A1: x in {( Top L)} and

           A2: x <= y;

          x = ( Top L) by A1, TARSKI:def 1;

          then y = ( Top L) by A2, WAYBEL15: 3;

          hence y in {( Top L)} by TARSKI:def 1;

        end;

        then {( Top L)} is Filter of L by WAYBEL_0: 5, WAYBEL_0:def 20;

        then {( Top L)} in the set of all Y where Y be Filter of L;

        hence thesis by WAYBEL_0:def 24;

      end;

    end

    theorem :: WAYBEL16:9

    

     Th9: for X be set holds for Y be non empty Subset of ( InclPoset ( Filt ( BoolePoset X))) holds ( meet Y) is Filter of ( BoolePoset X)

    proof

      let X be set;

      set L = ( BoolePoset X);

      let Y be non empty Subset of ( InclPoset ( Filt L));

       A1:

      now

        let Z be set;

        assume Z in Y;

        then Z in the carrier of ( InclPoset ( Filt L));

        then Z in the carrier of RelStr (# ( Filt L), ( RelIncl ( Filt L)) #) by YELLOW_1:def 1;

        then Z in the set of all V where V be Filter of L by WAYBEL_0:def 24;

        then ex Z1 be Filter of L st Z1 = Z;

        hence ( Top L) in Z by WAYBEL_4: 22;

      end;

      Y c= the carrier of ( InclPoset ( Filt L));

      then

       A2: Y c= the carrier of RelStr (# ( Filt L), ( RelIncl ( Filt L)) #) by YELLOW_1:def 1;

      

       A3: for Z be Subset of L st Z in Y holds Z is upper

      proof

        let Z be Subset of L;

        assume Z in Y;

        then Z in ( Filt L) by A2;

        then Z in the set of all V where V be Filter of L by WAYBEL_0:def 24;

        then ex Z1 be Filter of L st Z1 = Z;

        hence thesis;

      end;

       A4:

      now

        let V be Subset of L;

        assume V in Y;

        then V in ( Filt L) by A2;

        then V in the set of all Z where Z be Filter of L by WAYBEL_0:def 24;

        then

         A5: ex V1 be Filter of L st V1 = V;

        hence V is upper;

        thus V is filtered by A5;

      end;

      Y c= ( bool the carrier of L)

      proof

        let v be object;

        assume v in Y;

        then v in ( Filt L) by A2;

        then v in the set of all V where V be Filter of L by WAYBEL_0:def 24;

        then ex v1 be Filter of L st v1 = v;

        hence thesis;

      end;

      hence thesis by A1, A3, A4, SETFAM_1:def 1, YELLOW_2: 37, YELLOW_2: 39;

    end;

    theorem :: WAYBEL16:10

    for X be set holds for Y be non empty Subset of ( InclPoset ( Filt ( BoolePoset X))) holds ex_inf_of (Y,( InclPoset ( Filt ( BoolePoset X)))) & ( "/\" (Y,( InclPoset ( Filt ( BoolePoset X))))) = ( meet Y)

    proof

      let X be set;

      set L = ( InclPoset ( Filt ( BoolePoset X)));

      let Y be non empty Subset of L;

      ( meet Y) is Filter of ( BoolePoset X) by Th9;

      then ( meet Y) in the set of all Z where Z be Filter of ( BoolePoset X);

      then ( meet Y) in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by WAYBEL_0:def 24;

      then

      reconsider a = ( meet Y) as Element of L by YELLOW_1:def 1;

      

       A1: for b be Element of L st b is_<=_than Y holds b <= a

      proof

        let b be Element of L;

        assume

         A2: b is_<=_than Y;

        for x be set st x in Y holds b c= x by YELLOW_1: 3, A2, LATTICE3:def 8;

        then b c= ( meet Y) by SETFAM_1: 5;

        hence thesis by YELLOW_1: 3;

      end;

      for b be Element of L st b in Y holds a <= b by YELLOW_1: 3, SETFAM_1: 3;

      then a is_<=_than Y by LATTICE3:def 8;

      hence thesis by A1, YELLOW_0: 31;

    end;

    theorem :: WAYBEL16:11

    

     Th11: for X be set holds ( bool X) is Filter of ( BoolePoset X)

    proof

      let X be set;

      ( bool X) c= the carrier of ( BoolePoset X) by WAYBEL_7: 2;

      then

      reconsider A = ( bool X) as non empty Subset of ( BoolePoset X);

       A1:

      now

        let x,y be set;

        assume x in A & y in A;

        then (x /\ y) c= (X /\ X) by XBOOLE_1: 27;

        hence (x /\ y) in A;

      end;

      for x,y be set st x c= y & y c= X & x in A holds y in A;

      then A is upper by WAYBEL_7: 7;

      hence thesis by A1, WAYBEL_7: 9;

    end;

    theorem :: WAYBEL16:12

    

     Th12: for X be set holds {X} is Filter of ( BoolePoset X)

    proof

      let X be set;

      now

        let c be object;

        assume c in {X};

        then c = X by TARSKI:def 1;

        then c is Element of ( BoolePoset X) by WAYBEL_8: 26;

        hence c in the carrier of ( BoolePoset X);

      end;

      then

      reconsider A = {X} as non empty Subset of ( BoolePoset X) by TARSKI:def 3;

      for x,y be set st x c= y & y c= X & x in A holds y in A

      proof

        let x,y be set;

        assume that

         A1: x c= y & y c= X and

         A2: x in A;

        x = X by A2, TARSKI:def 1;

        then y = X by A1;

        hence thesis by TARSKI:def 1;

      end;

      then

       A3: A is upper by WAYBEL_7: 7;

      now

        let x,y be set;

        assume x in A & y in A;

        then x = X & y = X by TARSKI:def 1;

        hence (x /\ y) in A by TARSKI:def 1;

      end;

      hence thesis by A3, WAYBEL_7: 9;

    end;

    theorem :: WAYBEL16:13

    for X be set holds ( InclPoset ( Filt ( BoolePoset X))) is upper-bounded

    proof

      let X be set;

      set L = ( InclPoset ( Filt ( BoolePoset X)));

      ( bool X) is Filter of ( BoolePoset X) by Th11;

      then ( bool X) in the set of all Z where Z be Filter of ( BoolePoset X);

      then ( bool X) in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by WAYBEL_0:def 24;

      then

      reconsider x = ( bool X) as Element of L by YELLOW_1:def 1;

      now

        let b be Element of L;

        assume b in the carrier of L;

        then b in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by YELLOW_1:def 1;

        then b in the set of all V where V be Filter of ( BoolePoset X) by WAYBEL_0:def 24;

        then ex b1 be Filter of ( BoolePoset X) st b1 = b;

        then b c= the carrier of ( BoolePoset X);

        then b c= ( bool X) by WAYBEL_7: 2;

        hence b <= x by YELLOW_1: 3;

      end;

      then x is_>=_than the carrier of L by LATTICE3:def 9;

      hence thesis by YELLOW_0:def 5;

    end;

    theorem :: WAYBEL16:14

    for X be set holds ( InclPoset ( Filt ( BoolePoset X))) is lower-bounded

    proof

      let X be set;

      set L = ( InclPoset ( Filt ( BoolePoset X)));

       {X} is Filter of ( BoolePoset X) by Th12;

      then {X} in the set of all Z where Z be Filter of ( BoolePoset X);

      then {X} in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by WAYBEL_0:def 24;

      then

      reconsider x = {X} as Element of L by YELLOW_1:def 1;

      now

        let b be Element of L;

        assume b in the carrier of L;

        then b in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by YELLOW_1:def 1;

        then b in the set of all V where V be Filter of ( BoolePoset X) by WAYBEL_0:def 24;

        then

        consider b1 be Filter of ( BoolePoset X) such that

         A1: b1 = b;

        consider d be object such that

         A2: d in b1 by XBOOLE_0:def 1;

        reconsider d as set by TARSKI: 1;

        

         A3: d c= X by A2, WAYBEL_8: 26;

        now

          let c be object;

          assume c in {X};

          then c = X by TARSKI:def 1;

          hence c in b by A1, A2, A3, WAYBEL_7: 7;

        end;

        then {X} c= b;

        hence x <= b by YELLOW_1: 3;

      end;

      then x is_<=_than the carrier of L by LATTICE3:def 8;

      hence thesis by YELLOW_0:def 4;

    end;

    theorem :: WAYBEL16:15

    for X be set holds ( Top ( InclPoset ( Filt ( BoolePoset X)))) = ( bool X)

    proof

      let X be set;

      set L = ( InclPoset ( Filt ( BoolePoset X)));

      ( bool X) is Filter of ( BoolePoset X) by Th11;

      then ( bool X) in the set of all Z where Z be Filter of ( BoolePoset X);

      then ( bool X) in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by WAYBEL_0:def 24;

      then

      reconsider bX = ( bool X) as Element of L by YELLOW_1:def 1;

      

       A1: for b be Element of L st b is_<=_than {} holds bX >= b

      proof

        let b be Element of L;

        assume b is_<=_than {} ;

        b in the carrier of L;

        then b in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by YELLOW_1:def 1;

        then b in the set of all V where V be Filter of ( BoolePoset X) by WAYBEL_0:def 24;

        then ex b1 be Filter of ( BoolePoset X) st b1 = b;

        then b c= the carrier of ( BoolePoset X);

        then b c= ( bool X) by WAYBEL_7: 2;

        hence thesis by YELLOW_1: 3;

      end;

      bX is_<=_than {} by YELLOW_0: 6;

      then ( "/\" ( {} ,L)) = ( bool X) by A1, YELLOW_0: 31;

      hence thesis by YELLOW_0:def 12;

    end;

    theorem :: WAYBEL16:16

    for X be set holds ( Bottom ( InclPoset ( Filt ( BoolePoset X)))) = {X}

    proof

      let X be set;

      set L = ( InclPoset ( Filt ( BoolePoset X)));

       {X} is Filter of ( BoolePoset X) by Th12;

      then {X} in the set of all Z where Z be Filter of ( BoolePoset X);

      then {X} in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by WAYBEL_0:def 24;

      then

      reconsider bX = {X} as Element of L by YELLOW_1:def 1;

      

       A1: for b be Element of L st b is_>=_than {} holds bX <= b

      proof

        let b be Element of L;

        assume b is_>=_than {} ;

        b in the carrier of L;

        then b in the carrier of RelStr (# ( Filt ( BoolePoset X)), ( RelIncl ( Filt ( BoolePoset X))) #) by YELLOW_1:def 1;

        then b in the set of all V where V be Filter of ( BoolePoset X) by WAYBEL_0:def 24;

        then

        consider b1 be Filter of ( BoolePoset X) such that

         A2: b1 = b;

        consider d be object such that

         A3: d in b1 by XBOOLE_0:def 1;

        reconsider d as set by TARSKI: 1;

        

         A4: d c= X by A3, WAYBEL_8: 26;

        now

          let c be object;

          assume c in {X};

          then c = X by TARSKI:def 1;

          hence c in b by A2, A3, A4, WAYBEL_7: 7;

        end;

        then {X} c= b;

        hence thesis by YELLOW_1: 3;

      end;

      bX is_>=_than {} by YELLOW_0: 6;

      then ( "\/" ( {} ,L)) = {X} by A1, YELLOW_0: 30;

      hence thesis by YELLOW_0:def 11;

    end;

    theorem :: WAYBEL16:17

    for X be non empty set holds for Y be non empty Subset of ( InclPoset X) st ex_sup_of (Y,( InclPoset X)) holds ( union Y) c= ( sup Y)

    proof

      let X be non empty set;

      let Y be non empty Subset of ( InclPoset X);

      assume

       A1: ex_sup_of (Y,( InclPoset X));

      now

        let x be set;

        assume

         A2: x in Y;

        then

        reconsider x1 = x as Element of ( InclPoset X);

        ( sup Y) is_>=_than Y by A1, YELLOW_0: 30;

        then ( sup Y) >= x1 by A2, LATTICE3:def 9;

        hence x c= ( sup Y) by YELLOW_1: 3;

      end;

      hence thesis by ZFMISC_1: 76;

    end;

    theorem :: WAYBEL16:18

    

     Th18: for L be upper-bounded Semilattice holds ( InclPoset ( Filt L)) is complete

    proof

      let L be upper-bounded Semilattice;

      ( InclPoset ( Ids (L opp ))) is complete;

      hence thesis by Th7;

    end;

    registration

      let L be upper-bounded Semilattice;

      cluster ( InclPoset ( Filt L)) -> complete;

      coherence by Th18;

    end

    begin

    definition

      let L be non empty RelStr;

      let p be Element of L;

      :: WAYBEL16:def3

      attr p is completely-irreducible means ex_min_of ((( uparrow p) \ {p}),L);

    end

    theorem :: WAYBEL16:19

    

     Th19: for L be non empty RelStr holds for p be Element of L st p is completely-irreducible holds ( "/\" ((( uparrow p) \ {p}),L)) <> p

    proof

      let L be non empty RelStr;

      let p be Element of L;

      assume p is completely-irreducible;

      then ex_min_of ((( uparrow p) \ {p}),L);

      then ( "/\" ((( uparrow p) \ {p}),L)) in (( uparrow p) \ {p}) by WAYBEL_1:def 4;

      then not ( "/\" ((( uparrow p) \ {p}),L)) in {p} by XBOOLE_0:def 5;

      hence thesis by TARSKI:def 1;

    end;

    definition

      let L be non empty RelStr;

      :: WAYBEL16:def4

      func Irr L -> Subset of L means

      : Def4: for x be Element of L holds x in it iff x is completely-irreducible;

      existence

      proof

        defpred P[ Element of L] means $1 is completely-irreducible;

        consider X be Subset of L such that

         A1: for x be Element of L holds x in X iff P[x] from SUBSET_1:sch 3;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be Subset of L such that

         A2: for x be Element of L holds x in S1 iff x is completely-irreducible and

         A3: for x be Element of L holds x in S2 iff x is completely-irreducible;

        for x1 be object holds x1 in S1 iff x1 in S2 by A2, A3;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: WAYBEL16:20

    

     Th20: for L be non empty Poset holds for p be Element of L holds p is completely-irreducible iff ex q be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & ( uparrow p) = ( {p} \/ ( uparrow q))

    proof

      let L be non empty Poset;

      let p be Element of L;

      thus p is completely-irreducible implies ex q be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & ( uparrow p) = ( {p} \/ ( uparrow q))

      proof

        assume

         A1: p is completely-irreducible;

        then ex_min_of ((( uparrow p) \ {p}),L);

        then

         A2: ex_inf_of ((( uparrow p) \ {p}),L) by WAYBEL_1:def 4;

        take q = ( "/\" ((( uparrow p) \ {p}),L));

        now

          let s be Element of L;

          assume s in (( uparrow p) \ {p});

          then s in ( uparrow p) by XBOOLE_0:def 5;

          hence p <= s by WAYBEL_0: 18;

        end;

        then p is_<=_than (( uparrow p) \ {p}) by LATTICE3:def 8;

        then

         A3: p <= q by A2, YELLOW_0:def 10;

        

         A4: ( {p} \/ ( uparrow q)) c= ( uparrow p)

        proof

          let x be object;

          assume

           A5: x in ( {p} \/ ( uparrow q));

          now

            per cases by A5, XBOOLE_0:def 3;

              suppose

               A6: x in {p};

              

               A7: p <= p;

              x = p by A6, TARSKI:def 1;

              hence thesis by A7, WAYBEL_0: 18;

            end;

              suppose

               A8: x in ( uparrow q);

              then

              reconsider x1 = x as Element of L;

              q <= x1 by A8, WAYBEL_0: 18;

              then p <= x1 by A3, ORDERS_2: 3;

              hence thesis by WAYBEL_0: 18;

            end;

          end;

          hence thesis;

        end;

        ( "/\" ((( uparrow p) \ {p}),L)) <> p by A1, Th19;

        hence p < q by A3, ORDERS_2:def 6;

        

         A9: q is_<=_than (( uparrow p) \ {p}) by A2, YELLOW_0:def 10;

        thus for s be Element of L st p < s holds q <= s

        proof

          let s be Element of L;

          assume

           A10: p < s;

          then p <= s by ORDERS_2:def 6;

          then

           A11: s in ( uparrow p) by WAYBEL_0: 18;

           not s in {p} by A10, TARSKI:def 1;

          then s in (( uparrow p) \ {p}) by A11, XBOOLE_0:def 5;

          hence thesis by A9, LATTICE3:def 8;

        end;

        ( uparrow p) c= ( {p} \/ ( uparrow q))

        proof

          let x be object;

          assume

           A12: x in ( uparrow p);

          then

          reconsider x1 = x as Element of L;

          p = x1 or x1 in ( uparrow p) & not x1 in {p} by A12, TARSKI:def 1;

          then p = x1 or x1 in (( uparrow p) \ {p}) by XBOOLE_0:def 5;

          then p = x1 or ( "/\" ((( uparrow p) \ {p}),L)) <= x1 by A9, LATTICE3:def 8;

          then x in {p} or x in ( uparrow q) by TARSKI:def 1, WAYBEL_0: 18;

          hence thesis by XBOOLE_0:def 3;

        end;

        hence ( uparrow p) = ( {p} \/ ( uparrow q)) by A4;

      end;

      thus (ex q be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & ( uparrow p) = ( {p} \/ ( uparrow q))) implies p is completely-irreducible

      proof

        given q be Element of L such that

         A13: p < q and

         A14: for s be Element of L st p < s holds q <= s and

         A15: ( uparrow p) = ( {p} \/ ( uparrow q));

        

         A16: not q in {p} by A13, TARSKI:def 1;

        ex q be Element of L st (( uparrow p) \ {p}) is_>=_than q & for b be Element of L st (( uparrow p) \ {p}) is_>=_than b holds q >= b

        proof

          take q;

          now

            let a be Element of L;

            assume

             A17: a in (( uparrow p) \ {p});

            then not a in {p} by XBOOLE_0:def 5;

            then

             A18: a <> p by TARSKI:def 1;

            a in ( uparrow p) by A17, XBOOLE_0:def 5;

            then p <= a by WAYBEL_0: 18;

            then p < a by A18, ORDERS_2:def 6;

            hence q <= a by A14;

          end;

          hence (( uparrow p) \ {p}) is_>=_than q by LATTICE3:def 8;

          let b be Element of L;

          assume

           A19: (( uparrow p) \ {p}) is_>=_than b;

          q <= q;

          then q in ( uparrow q) by WAYBEL_0: 18;

          then

           A20: q in ( {p} \/ ( uparrow q)) by XBOOLE_0:def 3;

           not q in {p} by A13, TARSKI:def 1;

          then q in (( uparrow p) \ {p}) by A15, A20, XBOOLE_0:def 5;

          hence thesis by A19, LATTICE3:def 8;

        end;

        then

         A21: ex_inf_of ((( uparrow p) \ {p}),L) by YELLOW_0: 16;

         A22:

        now

          let b be Element of L;

          assume

           A23: b is_<=_than (( uparrow p) \ {p});

          p <= q by A13, ORDERS_2:def 6;

          then

           A24: q in ( uparrow p) by WAYBEL_0: 18;

           not q in {p} by A13, TARSKI:def 1;

          then q in (( uparrow p) \ {p}) by A24, XBOOLE_0:def 5;

          hence q >= b by A23, LATTICE3:def 8;

        end;

        p <= q by A13, ORDERS_2:def 6;

        then

         A25: q in ( uparrow p) by WAYBEL_0: 18;

        now

          let c be Element of L;

          assume c in (( uparrow p) \ {p});

          then c in ( uparrow p) & not c in {p} by XBOOLE_0:def 5;

          then c in ( uparrow q) by A15, XBOOLE_0:def 3;

          hence q <= c by WAYBEL_0: 18;

        end;

        then q is_<=_than (( uparrow p) \ {p}) by LATTICE3:def 8;

        then q = ( "/\" ((( uparrow p) \ {p}),L)) by A22, YELLOW_0: 31;

        then ( "/\" ((( uparrow p) \ {p}),L)) in (( uparrow p) \ {p}) by A25, A16, XBOOLE_0:def 5;

        then ex_min_of ((( uparrow p) \ {p}),L) by A21, WAYBEL_1:def 4;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL16:21

    

     Th21: for L be upper-bounded non empty Poset holds not ( Top L) in ( Irr L)

    proof

      let L be upper-bounded non empty Poset;

      assume ( Top L) in ( Irr L);

      then ( Top L) is completely-irreducible by Def4;

      then ( "/\" ((( uparrow ( Top L)) \ {( Top L)}),L)) <> ( Top L) by Th19;

      then ( "/\" (( {( Top L)} \ {( Top L)}),L)) <> ( Top L) by WAYBEL_4: 24;

      then ( "/\" ( {} ,L)) <> ( Top L) by XBOOLE_1: 37;

      hence contradiction by YELLOW_0:def 12;

    end;

    theorem :: WAYBEL16:22

    

     Th22: for L be Semilattice holds ( Irr L) c= ( IRR L)

    proof

      let L be Semilattice;

      let x be object;

      assume

       A1: x in ( Irr L);

      then

      reconsider x1 = x as Element of L;

      x1 is completely-irreducible by A1, Def4;

      then

      consider q be Element of L such that

       A2: x1 < q and

       A3: for s be Element of L st x1 < s holds q <= s and ( uparrow x1) = ( {x1} \/ ( uparrow q)) by Th20;

      now

        let a,b be Element of L;

        assume that

         A4: x1 = (a "/\" b) and

         A5: a <> x1 and

         A6: b <> x1;

        x1 <= b by A4, YELLOW_0: 23;

        then x1 < b by A6, ORDERS_2:def 6;

        then

         A7: q <= b by A3;

        

         A8: x1 <= q by A2, ORDERS_2:def 6;

        x1 <= a by A4, YELLOW_0: 23;

        then x1 < a by A5, ORDERS_2:def 6;

        then q <= a by A3;

        then q <= x1 by A4, A7, YELLOW_0: 23;

        hence contradiction by A2, A8, ORDERS_2: 2;

      end;

      then x1 is irreducible by WAYBEL_6:def 2;

      hence thesis by WAYBEL_6:def 4;

    end;

    theorem :: WAYBEL16:23

    

     Th23: for L be Semilattice holds for x be Element of L holds x is completely-irreducible implies x is irreducible

    proof

      let L be Semilattice;

      let x be Element of L;

      assume x is completely-irreducible;

      then

       A1: x in ( Irr L) by Def4;

      ( Irr L) c= ( IRR L) by Th22;

      hence thesis by A1, WAYBEL_6:def 4;

    end;

    theorem :: WAYBEL16:24

    

     Th24: for L be non empty Poset holds for x be Element of L holds x is completely-irreducible implies for X be Subset of L st ex_inf_of (X,L) & x = ( inf X) holds x in X

    proof

      let L be non empty Poset;

      let x be Element of L;

      assume x is completely-irreducible;

      then

      consider q be Element of L such that

       A1: x < q and

       A2: for s be Element of L st x < s holds q <= s and ( uparrow x) = ( {x} \/ ( uparrow q)) by Th20;

      let X be Subset of L;

      assume that

       A3: ex_inf_of (X,L) and

       A4: x = ( inf X) and

       A5: not x in X;

      

       A6: X c= ( uparrow q)

      proof

        let y be object;

        assume

         A7: y in X;

        then

        reconsider y1 = y as Element of L;

        ( inf X) is_<=_than X by A3, YELLOW_0: 31;

        then x <= y1 by A4, A7, LATTICE3:def 8;

        then x < y1 by A5, A7, ORDERS_2:def 6;

        then q <= y1 by A2;

        hence thesis by WAYBEL_0: 18;

      end;

       ex_inf_of (( uparrow q),L) by WAYBEL_0: 39;

      then ( inf ( uparrow q)) <= ( inf X) by A3, A6, YELLOW_0: 35;

      then q <= x by A4, WAYBEL_0: 39;

      hence contradiction by A1, ORDERS_2: 6;

    end;

    theorem :: WAYBEL16:25

    

     Th25: for L be non empty Poset holds for X be Subset of L st X is order-generating holds ( Irr L) c= X

    proof

      let L be non empty Poset;

      let X be Subset of L;

      assume

       A1: X is order-generating;

      let x be object;

      assume

       A2: x in ( Irr L);

      then

      reconsider x1 = x as Element of L;

      

       A3: x1 = ( "/\" ((( uparrow x1) /\ X),L)) & ex_inf_of ((( uparrow x1) /\ X),L) by A1, WAYBEL_6:def 5;

      x1 is completely-irreducible by A2, Def4;

      then x1 in (( uparrow x1) /\ X) by A3, Th24;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: WAYBEL16:26

    

     Th26: for L be complete LATTICE holds for p be Element of L holds (ex k be Element of L st p is_maximal_in (the carrier of L \ ( uparrow k))) implies p is completely-irreducible

    proof

      let L be complete LATTICE;

      let p be Element of L;

      given k be Element of L such that

       A1: p is_maximal_in (the carrier of L \ ( uparrow k));

      k <= (p "\/" k) by YELLOW_0: 22;

      then

       A2: (p "\/" k) in ( uparrow k) by WAYBEL_0: 18;

      p <= (p "\/" k) by YELLOW_0: 22;

      then (p "\/" k) in ( uparrow p) by WAYBEL_0: 18;

      then

       A3: ex_inf_of ((( uparrow p) \ {p}),L) & (p "\/" k) in (( uparrow p) /\ ( uparrow k)) by A2, XBOOLE_0:def 4, YELLOW_0: 17;

      

       A4: (( uparrow p) \ {p}) = (( uparrow p) /\ ( uparrow k)) by A1, Th3;

      then ( "/\" ((( uparrow p) \ {p}),L)) = (p "\/" k) by Th1;

      then ex_min_of ((( uparrow p) \ {p}),L) by A4, A3, WAYBEL_1:def 4;

      hence thesis;

    end;

    theorem :: WAYBEL16:27

    

     Th27: for L be transitive antisymmetric with_suprema RelStr holds for p,q,u be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & not u <= p holds (p "\/" u) = (q "\/" u)

    proof

      let L be transitive antisymmetric with_suprema RelStr;

      let p,q,u be Element of L;

      assume that

       A1: p < q and

       A2: for s be Element of L st p < s holds q <= s and

       A3: not u <= p;

      

       A4: (q "\/" u) >= q by YELLOW_0: 22;

       A5:

      now

        let v be Element of L;

        assume that

         A6: v >= p and

         A7: v >= u;

        v > p by A3, A6, A7, ORDERS_2:def 6;

        then v >= q by A2;

        hence (q "\/" u) <= v by A7, YELLOW_0: 22;

      end;

      p <= q by A1, ORDERS_2:def 6;

      then

       A8: (q "\/" u) >= p by A4, ORDERS_2: 3;

      (q "\/" u) >= u by YELLOW_0: 22;

      hence thesis by A8, A5, YELLOW_0: 22;

    end;

    theorem :: WAYBEL16:28

    

     Th28: for L be distributive LATTICE holds for p,q,u be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & not u <= p holds not (u "/\" q) <= p

    proof

      let L be distributive LATTICE;

      let p,q,u be Element of L;

      assume that

       A1: p < q and

       A2: (for s be Element of L st p < s holds q <= s) & not u <= p and

       A3: (u "/\" q) <= p;

      

       A4: p <= q by A1, ORDERS_2:def 6;

      p = (p "\/" (u "/\" q)) by A3, YELLOW_0: 24

      .= ((p "\/" u) "/\" (q "\/" p)) by WAYBEL_1: 5

      .= ((p "\/" u) "/\" q) by A4, YELLOW_0: 24

      .= (q "/\" (q "\/" u)) by A1, A2, Th27

      .= q by LATTICE3: 18;

      hence contradiction by A1;

    end;

    theorem :: WAYBEL16:29

    

     Th29: for L be distributive complete LATTICE st (L opp ) is meet-continuous holds for p be Element of L st p is completely-irreducible holds (the carrier of L \ ( downarrow p)) is Open Filter of L

    proof

      let L be distributive complete LATTICE;

      assume

       A1: (L opp ) is meet-continuous;

      let p be Element of L;

      assume

       A2: p is completely-irreducible;

      then

      consider q be Element of L such that

       A3: p < q and

       A4: for s be Element of L st p < s holds q <= s and ( uparrow p) = ( {p} \/ ( uparrow q)) by Th20;

      defpred P[ Element of L] means $1 <= q & not $1 <= p;

      reconsider F = { t where t be Element of L : P[t] } as Subset of L from DOMAIN_1:sch 7;

       not q <= p by A3, ORDERS_2: 6;

      then

       A5: q in F;

       A6:

      now

        let x,y be Element of L;

        assume that

         A7: x in F and

         A8: y in F;

        

         A9: ex x1 be Element of L st x1 = x & x1 <= q & not x1 <= p by A7;

        take z = (x "/\" y);

        

         A10: z <= x by YELLOW_0: 23;

        

         A11: ex y1 be Element of L st y1 = y & y1 <= q & not y1 <= p by A8;

        

         A12: not z <= p

        proof

           A13:

          now

            let d be Element of L;

            assume d >= y & d >= p;

            then d > p by A11, ORDERS_2:def 6;

            hence q <= d by A4;

          end;

          assume

           A14: z <= p;

          

           A15: q >= p by A3, ORDERS_2:def 6;

          x = (x "/\" q) by A9, YELLOW_0: 25

          .= (x "/\" (y "\/" p)) by A11, A15, A13, YELLOW_0: 22

          .= (z "\/" (x "/\" p)) by WAYBEL_1:def 3

          .= ((x "\/" z) "/\" (z "\/" p)) by WAYBEL_1: 5

          .= (x "/\" (p "\/" z)) by A10, YELLOW_0: 24

          .= (x "/\" p) by A14, YELLOW_0: 24;

          hence contradiction by A9, YELLOW_0: 25;

        end;

        z <= q by A9, A10, ORDERS_2: 3;

        hence z in F by A12;

        thus z <= x by YELLOW_0: 23;

        thus z <= y by YELLOW_0: 23;

      end;

      p is irreducible by A2, Th23;

      then

       A16: p is prime by WAYBEL_6: 27;

       not ( Top L) in ( Irr L) by Th21;

      then p <> ( Top L) by A2, Def4;

      then (( downarrow p) ` ) is Filter of L by A16, WAYBEL_6: 26;

      then

      reconsider V = (the carrier of L \ ( downarrow p)) as Filter of L by SUBSET_1:def 4;

      reconsider F as non empty filtered Subset of L by A5, A6, WAYBEL_0:def 2;

      reconsider F1 = F as non empty directed Subset of (L opp ) by YELLOW_7: 27;

      now

        let x be Element of L;

        assume

         A17: x in V;

        take y = ( inf F);

        thus y in V

        proof

          now

            let r be Element of L;

            assume r in ( {p} "\/" F);

            then r in { (p "\/" v) where v be Element of L : v in F } by YELLOW_4: 15;

            then

            consider v be Element of L such that

             A18: r = (p "\/" v) and

             A19: v in F;

            ex v1 be Element of L st v = v1 & v1 <= q & not v1 <= p by A19;

            then

             A20: p <> r by A18, YELLOW_0: 24;

            p <= r by A18, YELLOW_0: 22;

            then p < r by A20, ORDERS_2:def 6;

            hence q <= r by A4;

          end;

          then

           A21: q is_<=_than ( {p} "\/" F) by LATTICE3:def 8;

          

           A22: ex_inf_of (( {(p ~ )} "/\" F1),L) by YELLOW_0: 17;

           ex_inf_of (F,L) by YELLOW_0: 17;

          then

           A23: ( inf F) = ( sup F1) by YELLOW_7: 13;

          

           A24: {(p ~ )} = {p} by LATTICE3:def 6;

          assume not y in V;

          then y in ( downarrow p) by XBOOLE_0:def 5;

          then y <= p by WAYBEL_0: 17;

          

          then p = (p "\/" y) by YELLOW_0: 24

          .= ((p ~ ) "/\" (( inf F) ~ )) by YELLOW_7: 23

          .= ((p ~ ) "/\" ( sup F1)) by A23, LATTICE3:def 6

          .= ( sup ( {(p ~ )} "/\" F1)) by A1, WAYBEL_2:def 6

          .= ( "/\" (( {(p ~ )} "/\" F1),L)) by A22, YELLOW_7: 13

          .= ( "/\" (( {p} "\/" F),L)) by A24, Th5;

          then q <= p by A21, YELLOW_0: 33;

          hence contradiction by A3, ORDERS_2: 6;

        end;

        then not y in ( downarrow p) by XBOOLE_0:def 5;

        then

         A25: not y <= p by WAYBEL_0: 17;

        now

          let D be non empty directed Subset of L;

          assume

           A26: y <= ( sup D);

          (D \ ( downarrow p)) is non empty

          proof

            assume (D \ ( downarrow p)) is empty;

            then D c= ( downarrow p) by XBOOLE_1: 37;

            then ( sup D) <= ( sup ( downarrow p)) by WAYBEL_7: 1;

            then y <= ( sup ( downarrow p)) by A26, ORDERS_2: 3;

            hence contradiction by A25, WAYBEL_0: 34;

          end;

          then

          consider d be object such that

           A27: d in (D \ ( downarrow p));

          reconsider d as Element of L by A27;

          take d;

          thus d in D by A27, XBOOLE_0:def 5;

           not d in ( downarrow p) by A27, XBOOLE_0:def 5;

          then not d <= p by WAYBEL_0: 17;

          then (d "/\" q) <= q & not (d "/\" q) <= p by A3, A4, Th28, YELLOW_0: 23;

          then y is_<=_than F & (d "/\" q) in F by YELLOW_0: 33;

          then (d "/\" q) <= d & y <= (d "/\" q) by LATTICE3:def 8, YELLOW_0: 23;

          hence y <= d by ORDERS_2: 3;

        end;

        then

         A28: y << y by WAYBEL_3:def 1;

         not x in ( downarrow p) by A17, XBOOLE_0:def 5;

        then not x <= p by WAYBEL_0: 17;

        then (x "/\" q) <= q & not (x "/\" q) <= p by A3, A4, Th28, YELLOW_0: 23;

        then y is_<=_than F & (x "/\" q) in F by YELLOW_0: 33;

        then (x "/\" q) <= x & y <= (x "/\" q) by LATTICE3:def 8, YELLOW_0: 23;

        then y <= x by ORDERS_2: 3;

        hence y << x by A28, WAYBEL_3: 2;

      end;

      hence thesis by WAYBEL_6:def 1;

    end;

    theorem :: WAYBEL16:30

    for L be distributive complete LATTICE st (L opp ) is meet-continuous holds for p be Element of L holds p is completely-irreducible implies ex k be Element of L st k in the carrier of ( CompactSublatt L) & p is_maximal_in (the carrier of L \ ( uparrow k))

    proof

      let L be distributive complete LATTICE;

      assume

       A1: (L opp ) is meet-continuous;

      let p be Element of L;

      assume

       A2: p is completely-irreducible;

      then

      reconsider V = (the carrier of L \ ( downarrow p)) as Open Filter of L by A1, Th29;

      now

        let b be Element of L;

        assume b in (( uparrow p) \ {p});

        then b in ( uparrow p) by XBOOLE_0:def 5;

        hence p <= b by WAYBEL_0: 18;

      end;

      then p is_<=_than (( uparrow p) \ {p}) by LATTICE3:def 8;

      then

       A3: p <= ( "/\" ((( uparrow p) \ {p}),L)) by YELLOW_0: 33;

      ( "/\" ((( uparrow p) \ {p}),L)) <> p by A2, Th19;

      then

       A4: p < ( "/\" ((( uparrow p) \ {p}),L)) by A3, ORDERS_2:def 6;

      

       A5: ex_inf_of (V,L) & (( inf V) ~ ) = ( inf V) by LATTICE3:def 6, YELLOW_0: 17;

      take k = ( inf V);

      reconsider V9 = V as non empty directed Subset of (L opp ) by YELLOW_7: 27;

      

       A6: ex_inf_of (( {(p ~ )} "/\" V9),L) by YELLOW_0: 17;

      

       A7: ex_inf_of (( {p} "\/" V),L) & ex_inf_of ((( uparrow p) \ {p}),L) by YELLOW_0: 17;

      

       A8: ( {p} "\/" V) c= (( uparrow p) \ {p})

      proof

        let x be object;

        assume x in ( {p} "\/" V);

        then x in { (p "\/" v) where v be Element of L : v in V } by YELLOW_4: 15;

        then

        consider v be Element of L such that

         A9: x = (p "\/" v) and

         A10: v in V;

         not v in ( downarrow p) by A10, XBOOLE_0:def 5;

        then not v <= p by WAYBEL_0: 17;

        then (p "\/" v) <> p by YELLOW_0: 22;

        then

         A11: not (p "\/" v) in {p} by TARSKI:def 1;

        p <= (p "\/" v) by YELLOW_0: 22;

        then (p "\/" v) in ( uparrow p) by WAYBEL_0: 18;

        hence thesis by A9, A11, XBOOLE_0:def 5;

      end;

      

       A12: p = (p ~ ) by LATTICE3:def 6;

      (p "\/" k) = ((p ~ ) "/\" (( inf V) ~ )) by YELLOW_7: 23

      .= ((p ~ ) "/\" ( "\/" (V,(L opp )))) by A5, YELLOW_7: 13

      .= ( "\/" (( {(p ~ )} "/\" V9),(L opp ))) by A1, WAYBEL_2:def 6

      .= ( "/\" (( {(p ~ )} "/\" V9),L)) by A6, YELLOW_7: 13

      .= ( inf ( {p} "\/" V)) by A12, Th5;

      then

       A13: ( "/\" ((( uparrow p) \ {p}),L)) <= (p "\/" k) by A7, A8, YELLOW_0: 35;

      

       A14: not k <= p

      proof

        assume k <= p;

        then (p "\/" k) = p by YELLOW_0: 24;

        hence contradiction by A13, A4, ORDERS_2: 7;

      end;

      ( uparrow k) = V

      proof

        thus ( uparrow k) c= V

        proof

          let x be object;

          assume

           A15: x in ( uparrow k);

          then

          reconsider x1 = x as Element of L;

          k <= x1 by A15, WAYBEL_0: 18;

          then not x1 <= p by A14, ORDERS_2: 3;

          then not x1 in ( downarrow p) by WAYBEL_0: 17;

          hence thesis by XBOOLE_0:def 5;

        end;

        let x be object;

        assume

         A16: x in V;

        then

        reconsider x1 = x as Element of L;

        k is_<=_than V by YELLOW_0: 33;

        then k <= x1 by A16, LATTICE3:def 8;

        hence thesis by WAYBEL_0: 18;

      end;

      then k is compact by WAYBEL_8: 2;

      hence k in the carrier of ( CompactSublatt L) by WAYBEL_8:def 1;

      

       A17: not ex y be Element of L st y in (the carrier of L \ ( uparrow k)) & p < y

      proof

        given y be Element of L such that

         A18: y in (the carrier of L \ ( uparrow k)) and

         A19: p < y;

         not y in ( uparrow k) by A18, XBOOLE_0:def 5;

        then k is_<=_than V & not k <= y by WAYBEL_0: 18, YELLOW_0: 33;

        then not y in V by LATTICE3:def 8;

        then y in ( downarrow p) by XBOOLE_0:def 5;

        then y <= p by WAYBEL_0: 17;

        hence contradiction by A19, ORDERS_2: 6;

      end;

       not p in ( uparrow k) by A14, WAYBEL_0: 18;

      then p in (the carrier of L \ ( uparrow k)) by XBOOLE_0:def 5;

      hence thesis by A17, WAYBEL_4: 55;

    end;

    theorem :: WAYBEL16:31

    

     Th31: for L be lower-bounded algebraic LATTICE holds for x,y be Element of L holds not y <= x implies ex p be Element of L st p is completely-irreducible & x <= p & not y <= p

    proof

      let L be lower-bounded algebraic LATTICE;

      let x,y be Element of L;

      assume

       A1: not y <= x;

      for z be Element of L holds ( waybelow z) is non empty directed;

      then

      consider k1 be Element of L such that

       A2: k1 << y and

       A3: not k1 <= x by A1, WAYBEL_3: 24;

      consider k be Element of L such that

       A4: k in the carrier of ( CompactSublatt L) and

       A5: k1 <= k and

       A6: k <= y by A2, WAYBEL_8: 7;

       not k <= x by A3, A5, ORDERS_2: 3;

      then not x in ( uparrow k) by WAYBEL_0: 18;

      then x in (the carrier of L \ ( uparrow k)) by XBOOLE_0:def 5;

      then

       A7: x in (( uparrow k) ` ) by SUBSET_1:def 4;

      k is compact by A4, WAYBEL_8:def 1;

      then ( uparrow k) is Open Filter of L by WAYBEL_8: 2;

      then

      consider p be Element of L such that

       A8: x <= p and

       A9: p is_maximal_in (( uparrow k) ` ) by A7, WAYBEL_6: 9;

      take p;

      (the carrier of L \ ( uparrow k)) = (( uparrow k) ` ) by SUBSET_1:def 4;

      hence p is completely-irreducible by A9, Th26;

      thus x <= p by A8;

      thus not y <= p

      proof

        p in (( uparrow k) ` ) by A9, WAYBEL_4: 55;

        then p in (the carrier of L \ ( uparrow k)) by SUBSET_1:def 4;

        then

         A10: not p in ( uparrow k) by XBOOLE_0:def 5;

        assume y <= p;

        then k <= p by A6, ORDERS_2: 3;

        hence contradiction by A10, WAYBEL_0: 18;

      end;

    end;

    theorem :: WAYBEL16:32

    

     Th32: for L be lower-bounded algebraic LATTICE holds ( Irr L) is order-generating & for X be Subset of L st X is order-generating holds ( Irr L) c= X

    proof

      let L be lower-bounded algebraic LATTICE;

      now

        let x,y be Element of L;

        assume not y <= x;

        then

        consider p be Element of L such that

         A1: p is completely-irreducible and

         A2: x <= p and

         A3: not y <= p by Th31;

        take p;

        thus p in ( Irr L) by A1, Def4;

        thus x <= p by A2;

        thus not y <= p by A3;

      end;

      hence ( Irr L) is order-generating by WAYBEL_6: 17;

      let X be Subset of L;

      assume X is order-generating;

      hence thesis by Th25;

    end;

    theorem :: WAYBEL16:33

    for L be lower-bounded algebraic LATTICE holds for s be Element of L holds s = ( "/\" ((( uparrow s) /\ ( Irr L)),L))

    proof

      let L be lower-bounded algebraic LATTICE;

      let s be Element of L;

      ( Irr L) is order-generating by Th32;

      hence thesis by WAYBEL_6:def 5;

    end;

    theorem :: WAYBEL16:34

    

     Th34: for L be complete non empty Poset holds for X be Subset of L holds for p be Element of L st p is completely-irreducible & p = ( inf X) holds p in X

    proof

      let L be complete non empty Poset;

      let X be Subset of L;

      let p be Element of L;

      assume that

       A1: p is completely-irreducible and

       A2: p = ( inf X);

      assume

       A3: not p in X;

      consider q be Element of L such that

       A4: p < q and

       A5: for s be Element of L st p < s holds q <= s and ( uparrow p) = ( {p} \/ ( uparrow q)) by A1, Th20;

      

       A6: p is_<=_than X by A2, YELLOW_0: 33;

      now

        let b be Element of L;

        assume

         A7: b in X;

        then p <= b by A6, LATTICE3:def 8;

        then p < b by A3, A7, ORDERS_2:def 6;

        hence q <= b by A5;

      end;

      then

       A8: q is_<=_than X by LATTICE3:def 8;

      

       A9: p <= q by A4, ORDERS_2:def 6;

      now

        let b be Element of L;

        assume b is_<=_than X;

        then p >= b by A2, YELLOW_0: 33;

        hence q >= b by A9, ORDERS_2: 3;

      end;

      hence contradiction by A2, A4, A8, YELLOW_0: 33;

    end;

    theorem :: WAYBEL16:35

    

     Th35: for L be complete algebraic LATTICE holds for p be Element of L st p is completely-irreducible holds p = ( "/\" ({ x where x be Element of L : x in ( uparrow p) & ex k be Element of L st k in the carrier of ( CompactSublatt L) & x is_maximal_in (the carrier of L \ ( uparrow k)) },L))

    proof

      let L be complete algebraic LATTICE;

      let p be Element of L;

      set A = { x where x be Element of L : x in ( uparrow p) & ex k be Element of L st k in the carrier of ( CompactSublatt L) & x is_maximal_in (the carrier of L \ ( uparrow k)) };

      p <= p;

      then

       A1: p in ( uparrow p) by WAYBEL_0: 18;

      now

        let a be Element of L;

        assume a in A;

        then ex a1 be Element of L st a1 = a & a1 in ( uparrow p) & ex k be Element of L st k in the carrier of ( CompactSublatt L) & a1 is_maximal_in (the carrier of L \ ( uparrow k));

        hence p <= a by WAYBEL_0: 18;

      end;

      then

       A2: p is_<=_than A by LATTICE3:def 8;

      assume p is completely-irreducible;

      then

      consider q be Element of L such that

       A3: p < q and

       A4: for s be Element of L st p < s holds q <= s and ( uparrow p) = ( {p} \/ ( uparrow q)) by Th20;

      

       A5: ( compactbelow p) <> ( compactbelow q)

      proof

        assume ( compactbelow p) = ( compactbelow q);

        

        then p = ( sup ( compactbelow q)) by WAYBEL_8:def 3

        .= q by WAYBEL_8:def 3;

        hence contradiction by A3;

      end;

      p <= q by A3, ORDERS_2:def 6;

      then ( compactbelow p) c= ( compactbelow q) by WAYBEL13: 1;

      then not ( compactbelow q) c= ( compactbelow p) by A5;

      then

      consider k1 be object such that

       A6: k1 in ( compactbelow q) and

       A7: not k1 in ( compactbelow p);

      k1 in { y where y be Element of L : q >= y & y is compact } by A6, WAYBEL_8:def 2;

      then

      consider k be Element of L such that

       A8: k = k1 and

       A9: q >= k and

       A10: k is compact;

      

       A11: not ex y be Element of L st y in (the carrier of L \ ( uparrow k)) & p < y

      proof

        given y be Element of L such that

         A12: y in (the carrier of L \ ( uparrow k)) and

         A13: p < y;

        q <= y by A4, A13;

        then k <= y by A9, ORDERS_2: 3;

        then y in ( uparrow k) by WAYBEL_0: 18;

        hence contradiction by A12, XBOOLE_0:def 5;

      end;

       not k <= p by A7, A8, A10, WAYBEL_8: 4;

      then not p in ( uparrow k) by WAYBEL_0: 18;

      then p in (the carrier of L \ ( uparrow k)) by XBOOLE_0:def 5;

      then

       A14: p is_maximal_in (the carrier of L \ ( uparrow k)) by A11, WAYBEL_4: 55;

      k in the carrier of ( CompactSublatt L) by A10, WAYBEL_8:def 1;

      then p in A by A1, A14;

      then for u be Element of L st u is_<=_than A holds p >= u by LATTICE3:def 8;

      hence thesis by A2, YELLOW_0: 33;

    end;

    theorem :: WAYBEL16:36

    for L be complete algebraic LATTICE holds for p be Element of L holds (ex k be Element of L st k in the carrier of ( CompactSublatt L) & p is_maximal_in (the carrier of L \ ( uparrow k))) iff p is completely-irreducible

    proof

      let L be complete algebraic LATTICE;

      let p be Element of L;

      thus (ex k be Element of L st k in the carrier of ( CompactSublatt L) & p is_maximal_in (the carrier of L \ ( uparrow k))) implies p is completely-irreducible by Th26;

      thus p is completely-irreducible implies ex k be Element of L st k in the carrier of ( CompactSublatt L) & p is_maximal_in (the carrier of L \ ( uparrow k))

      proof

        defpred P[ Element of L] means $1 in ( uparrow p) & ex k be Element of L st k in the carrier of ( CompactSublatt L) & $1 is_maximal_in (the carrier of L \ ( uparrow k));

        reconsider A = { x where x be Element of L : P[x] } as Subset of L from DOMAIN_1:sch 7;

        assume

         A1: p is completely-irreducible;

        then p = ( inf A) by Th35;

        then p in A by A1, Th34;

        then

        consider x be Element of L such that

         A2: x = p and x in ( uparrow p) and

         A3: ex k be Element of L st k in the carrier of ( CompactSublatt L) & x is_maximal_in (the carrier of L \ ( uparrow k));

        consider k be Element of L such that

         A4: k in the carrier of ( CompactSublatt L) and

         A5: x is_maximal_in (the carrier of L \ ( uparrow k)) by A3;

        take k;

        thus k in the carrier of ( CompactSublatt L) by A4;

        thus thesis by A2, A5;

      end;

    end;