waybel23.miz



    begin

    theorem :: WAYBEL23:1

    

     Th1: for L be non empty Poset holds for x be Element of L holds ( compactbelow x) = (( waybelow x) /\ the carrier of ( CompactSublatt L))

    proof

      let L be non empty Poset;

      let x be Element of L;

      

       A1: ( compactbelow x) c= (( waybelow x) /\ the carrier of ( CompactSublatt L))

      proof

        let y be object;

        assume

         A2: y in ( compactbelow x);

        then

        reconsider y1 = y as Element of L;

        

         A3: y in (( downarrow x) /\ the carrier of ( CompactSublatt L)) by A2, WAYBEL_8: 5;

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

        then

         A4: y1 <= x by WAYBEL_0: 17;

        

         A5: y in the carrier of ( CompactSublatt L) by A3, XBOOLE_0:def 4;

        then y1 is compact by WAYBEL_8:def 1;

        then y1 << y1 by WAYBEL_3:def 2;

        then y1 << x by A4, WAYBEL_3: 2;

        then y1 in ( waybelow x) by WAYBEL_3: 7;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      (( waybelow x) /\ the carrier of ( CompactSublatt L)) c= ( compactbelow x)

      proof

        let y be object;

        assume

         A6: y in (( waybelow x) /\ the carrier of ( CompactSublatt L));

        then

        reconsider y1 = y as Element of L;

        y in ( waybelow x) by A6, XBOOLE_0:def 4;

        then y1 << x by WAYBEL_3: 7;

        then y1 <= x by WAYBEL_3: 1;

        then

         A7: y in ( downarrow x) by WAYBEL_0: 17;

        y in the carrier of ( CompactSublatt L) by A6, XBOOLE_0:def 4;

        then y in (( downarrow x) /\ the carrier of ( CompactSublatt L)) by A7, XBOOLE_0:def 4;

        hence thesis by WAYBEL_8: 5;

      end;

      hence thesis by A1;

    end;

    definition

      let L be non empty reflexive transitive RelStr;

      let X be Subset of ( InclPoset ( Ids L));

      :: original: union

      redefine

      func union X -> Subset of L ;

      coherence

      proof

        ( union X) c= the carrier of L

        proof

          let x be object;

          assume x in ( union X);

          then

          consider Y be set such that

           A1: x in Y and

           A2: Y in X by TARSKI:def 4;

          reconsider Y as Ideal of L by A2, YELLOW_2: 41;

          x in Y by A1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    

     Lm1: for X be non empty set holds for Y be 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 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;

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

      end;

      hence thesis by ZFMISC_1: 76;

    end;

    theorem :: WAYBEL23:2

    

     Th2: for L be non empty RelStr holds for X,Y be Subset of L st X c= Y holds ( finsups X) c= ( finsups Y)

    proof

      let L be non empty RelStr;

      let X,Y be Subset of L;

      assume

       A1: X c= Y;

      let x be object;

      assume x in ( finsups X);

      then x in { ( "\/" (V,L)) where V be finite Subset of X : ex_sup_of (V,L) } by WAYBEL_0:def 27;

      then

      consider Z be finite Subset of X such that

       A2: x = ( "\/" (Z,L)) and

       A3: ex_sup_of (Z,L);

      reconsider Z as finite Subset of Y by A1, XBOOLE_1: 1;

       ex_sup_of (Z,L) by A3;

      then x in { ( "\/" (V,L)) where V be finite Subset of Y : ex_sup_of (V,L) } by A2;

      hence thesis by WAYBEL_0:def 27;

    end;

    theorem :: WAYBEL23:3

    

     Th3: for L be non empty transitive RelStr holds for S be sups-inheriting non empty full SubRelStr of L holds for X be Subset of L holds for Y be Subset of S st X = Y holds ( finsups X) c= ( finsups Y)

    proof

      let L be non empty transitive RelStr;

      let S be sups-inheriting non empty full SubRelStr of L;

      let X be Subset of L;

      let Y be Subset of S;

      assume

       A1: X = Y;

      let x be object;

      assume x in ( finsups X);

      then x in { ( "\/" (V,L)) where V be finite Subset of X : ex_sup_of (V,L) } by WAYBEL_0:def 27;

      then

      consider Z be finite Subset of X such that

       A2: x = ( "\/" (Z,L)) and

       A3: ex_sup_of (Z,L);

      reconsider Z as finite Subset of Y by A1;

      reconsider Z1 = Z as Subset of S by XBOOLE_1: 1;

      

       A4: ( "\/" (Z1,L)) in the carrier of S by A3, YELLOW_0:def 19;

      then

       A5: ex_sup_of (Z1,S) by A3, YELLOW_0: 64;

      x = ( "\/" (Z1,S)) by A2, A3, A4, YELLOW_0: 64;

      then x in { ( "\/" (V,S)) where V be finite Subset of Y : ex_sup_of (V,S) } by A5;

      hence thesis by WAYBEL_0:def 27;

    end;

    theorem :: WAYBEL23:4

    for L be complete transitive antisymmetric non empty RelStr holds for S be sups-inheriting non empty full SubRelStr of L holds for X be Subset of L holds for Y be Subset of S st X = Y holds ( finsups X) = ( finsups Y)

    proof

      let L be complete transitive antisymmetric non empty RelStr;

      let S be sups-inheriting non empty full SubRelStr of L;

      let X be Subset of L;

      let Y be Subset of S;

      assume

       A1: X = Y;

      hence ( finsups X) c= ( finsups Y) by Th3;

      let x be object;

      assume x in ( finsups Y);

      then x in { ( "\/" (V,S)) where V be finite Subset of Y : ex_sup_of (V,S) } by WAYBEL_0:def 27;

      then

      consider Z be finite Subset of Y such that

       A2: x = ( "\/" (Z,S)) and ex_sup_of (Z,S);

      reconsider Z as finite Subset of X by A1;

      reconsider Z1 = Z as Subset of S by XBOOLE_1: 1;

      

       A3: ex_sup_of (Z1,L) by YELLOW_0: 17;

      then ( "\/" (Z1,L)) in the carrier of S by YELLOW_0:def 19;

      then x = ( "\/" (Z1,L)) by A2, A3, YELLOW_0: 64;

      then x in { ( "\/" (V,L)) where V be finite Subset of X : ex_sup_of (V,L) } by A3;

      hence thesis by WAYBEL_0:def 27;

    end;

    theorem :: WAYBEL23:5

    

     Th5: for L be complete sup-Semilattice holds for S be join-inheriting non empty full SubRelStr of L st ( Bottom L) in the carrier of S holds for X be Subset of L holds for Y be Subset of S st X = Y holds ( finsups Y) c= ( finsups X)

    proof

      let L be complete sup-Semilattice;

      let S be join-inheriting non empty full SubRelStr of L;

      assume

       A1: ( Bottom L) in the carrier of S;

      let X be Subset of L;

      let Y be Subset of S;

      assume

       A2: X = Y;

      let x be object;

      assume x in ( finsups Y);

      then x in { ( "\/" (V,S)) where V be finite Subset of Y : ex_sup_of (V,S) } by WAYBEL_0:def 27;

      then

      consider Z be finite Subset of Y such that

       A3: x = ( "\/" (Z,S)) and

       A4: ex_sup_of (Z,S);

      reconsider Z as finite Subset of X by A2;

      now

        per cases ;

          suppose Z is non empty;

          then

          reconsider Z1 = Z as finite non empty Subset of S by XBOOLE_1: 1;

          reconsider xl = ( "\/" (Z1,L)) as Element of S by WAYBEL21: 15;

          

           A5: ex_sup_of (Z1,L) by YELLOW_0: 17;

           A6:

          now

            let b be Element of S;

            reconsider b1 = b as Element of L by YELLOW_0: 58;

            assume

             A7: b is_>=_than Z1;

            b1 is_>=_than Z1 by A7, YELLOW_0: 59;

            then ( "\/" (Z1,L)) <= b1 by A5, YELLOW_0: 30;

            hence xl <= b by YELLOW_0: 60;

          end;

          

           A8: ( "\/" (Z1,L)) is_>=_than Z1 by A5, YELLOW_0: 30;

          xl is_>=_than Z1

          proof

            let b be Element of S;

            reconsider b1 = b as Element of L by YELLOW_0: 58;

            assume b in Z1;

            then b1 <= ( "\/" (Z1,L)) by A8;

            hence b <= xl by YELLOW_0: 60;

          end;

          then ( "\/" (Z1,S)) = ( "\/" (Z1,L)) by A6, YELLOW_0: 30;

          then x in { ( "\/" (V,L)) where V be finite Subset of X : ex_sup_of (V,L) } by A3, A5;

          hence thesis by WAYBEL_0:def 27;

        end;

          suppose

           A9: Z is empty;

          reconsider dL = ( Bottom L) as Element of S by A1;

          reconsider dS = ( Bottom S) as Element of L by YELLOW_0: 58;

          S is lower-bounded by A4, A9, WAYBEL20: 6;

          then ( Bottom S) <= dL by YELLOW_0: 44;

          then

           A10: dS <= ( Bottom L) by YELLOW_0: 59;

          

           A11: ex_sup_of (Z,L) by YELLOW_0: 17;

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

          then dS = ( Bottom L) by A10, YELLOW_0:def 3;

          then x in { ( "\/" (V,L)) where V be finite Subset of X : ex_sup_of (V,L) } by A3, A9, A11;

          hence thesis by WAYBEL_0:def 27;

        end;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL23:6

    

     Th6: for L be lower-bounded sup-Semilattice holds for X be Subset of ( InclPoset ( Ids L)) holds ( sup X) = ( downarrow ( finsups ( union X)))

    proof

      let L be lower-bounded sup-Semilattice;

      let X be Subset of ( InclPoset ( Ids L));

      reconsider a = ( downarrow ( finsups ( union X))) as Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;

      

       A1: ( union X) c= ( sup X) by Lm1, YELLOW_0: 17;

       A2:

      now

        let b be Element of ( InclPoset ( Ids L));

        reconsider b1 = b as Ideal of L by YELLOW_2: 41;

        assume b is_>=_than X;

        then b >= ( sup X) by YELLOW_0: 32;

        then ( sup X) c= b1 by YELLOW_1: 3;

        then ( union X) c= b1 by A1;

        then ( downarrow ( finsups ( union X))) c= b1 by WAYBEL_0: 61;

        hence a <= b by YELLOW_1: 3;

      end;

      

       A3: ( union X) c= ( downarrow ( finsups ( union X))) by WAYBEL_0: 61;

      now

        let b be Element of ( InclPoset ( Ids L));

        assume b in X;

        then b c= ( union X) by ZFMISC_1: 74;

        then b c= ( downarrow ( finsups ( union X))) by A3;

        hence b <= a by YELLOW_1: 3;

      end;

      then a is_>=_than X;

      hence thesis by A2, YELLOW_0: 32;

    end;

    theorem :: WAYBEL23:7

    

     Th7: for L be reflexive transitive RelStr holds for X be Subset of L holds ( downarrow ( downarrow X)) = ( downarrow X)

    proof

      let L be reflexive transitive RelStr;

      let X be Subset of L;

      

       A1: ( downarrow ( downarrow X)) c= ( downarrow X)

      proof

        let x be object;

        assume

         A2: x in ( downarrow ( downarrow X));

        then

        reconsider x1 = x as Element of L;

        consider y be Element of L such that

         A3: y >= x1 and

         A4: y in ( downarrow X) by A2, WAYBEL_0:def 15;

        consider z be Element of L such that

         A5: z >= y and

         A6: z in X by A4, WAYBEL_0:def 15;

        z >= x1 by A3, A5, YELLOW_0:def 2;

        hence thesis by A6, WAYBEL_0:def 15;

      end;

      ( downarrow X) c= ( downarrow ( downarrow X)) by WAYBEL_0: 16;

      hence thesis by A1;

    end;

    theorem :: WAYBEL23:8

    for L be reflexive transitive RelStr holds for X be Subset of L holds ( uparrow ( uparrow X)) = ( uparrow X)

    proof

      let L be reflexive transitive RelStr;

      let X be Subset of L;

      

       A1: ( uparrow ( uparrow X)) c= ( uparrow X)

      proof

        let x be object;

        assume

         A2: x in ( uparrow ( uparrow X));

        then

        reconsider x1 = x as Element of L;

        consider y be Element of L such that

         A3: y <= x1 and

         A4: y in ( uparrow X) by A2, WAYBEL_0:def 16;

        consider z be Element of L such that

         A5: z <= y and

         A6: z in X by A4, WAYBEL_0:def 16;

        z <= x1 by A3, A5, YELLOW_0:def 2;

        hence thesis by A6, WAYBEL_0:def 16;

      end;

      ( uparrow X) c= ( uparrow ( uparrow X)) by WAYBEL_0: 16;

      hence thesis by A1;

    end;

    theorem :: WAYBEL23:9

    for L be non empty reflexive transitive RelStr holds for x be Element of L holds ( downarrow ( downarrow x)) = ( downarrow x)

    proof

      let L be non empty reflexive transitive RelStr;

      let x be Element of L;

      

       A1: ( downarrow ( downarrow x)) c= ( downarrow x)

      proof

        let v be object;

        assume

         A2: v in ( downarrow ( downarrow x));

        then

        reconsider v1 = v as Element of L;

        consider y be Element of L such that

         A3: y >= v1 and

         A4: y in ( downarrow x) by A2, WAYBEL_0:def 15;

        x >= y by A4, WAYBEL_0: 17;

        then x >= v1 by A3, YELLOW_0:def 2;

        hence thesis by WAYBEL_0: 17;

      end;

      ( downarrow x) c= ( downarrow ( downarrow x)) by WAYBEL_0: 16;

      hence thesis by A1;

    end;

    theorem :: WAYBEL23:10

    for L be non empty reflexive transitive RelStr holds for x be Element of L holds ( uparrow ( uparrow x)) = ( uparrow x)

    proof

      let L be non empty reflexive transitive RelStr;

      let x be Element of L;

      

       A1: ( uparrow ( uparrow x)) c= ( uparrow x)

      proof

        let v be object;

        assume

         A2: v in ( uparrow ( uparrow x));

        then

        reconsider v1 = v as Element of L;

        consider y be Element of L such that

         A3: y <= v1 and

         A4: y in ( uparrow x) by A2, WAYBEL_0:def 16;

        x <= y by A4, WAYBEL_0: 18;

        then x <= v1 by A3, YELLOW_0:def 2;

        hence thesis by WAYBEL_0: 18;

      end;

      ( uparrow x) c= ( uparrow ( uparrow x)) by WAYBEL_0: 16;

      hence thesis by A1;

    end;

    theorem :: WAYBEL23:11

    

     Th11: for L be non empty RelStr holds for S be non empty SubRelStr of L holds for X be Subset of L holds for Y be Subset of S st X = Y holds ( downarrow Y) c= ( downarrow X)

    proof

      let L be non empty RelStr;

      let S be non empty SubRelStr of L;

      let X be Subset of L;

      let Y be Subset of S;

      assume

       A1: X = Y;

      let x be object;

      assume

       A2: x in ( downarrow Y);

      then

      reconsider x1 = x as Element of S;

      consider y1 be Element of S such that

       A3: y1 >= x1 and

       A4: y1 in Y by A2, WAYBEL_0:def 15;

      reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0: 58;

      y2 >= x2 by A3, YELLOW_0: 59;

      hence thesis by A1, A4, WAYBEL_0:def 15;

    end;

    theorem :: WAYBEL23:12

    

     Th12: for L be non empty RelStr holds for S be non empty SubRelStr of L holds for X be Subset of L holds for Y be Subset of S st X = Y holds ( uparrow Y) c= ( uparrow X)

    proof

      let L be non empty RelStr;

      let S be non empty SubRelStr of L;

      let X be Subset of L;

      let Y be Subset of S;

      assume

       A1: X = Y;

      let x be object;

      assume

       A2: x in ( uparrow Y);

      then

      reconsider x1 = x as Element of S;

      consider y1 be Element of S such that

       A3: y1 <= x1 and

       A4: y1 in Y by A2, WAYBEL_0:def 16;

      reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0: 58;

      y2 <= x2 by A3, YELLOW_0: 59;

      hence thesis by A1, A4, WAYBEL_0:def 16;

    end;

    theorem :: WAYBEL23:13

    for L be non empty RelStr holds for S be non empty SubRelStr of L holds for x be Element of L holds for y be Element of S st x = y holds ( downarrow y) c= ( downarrow x)

    proof

      let L be non empty RelStr;

      let S be non empty SubRelStr of L;

      let x be Element of L;

      let y be Element of S;

      

       A1: ( downarrow x) = ( downarrow {x}) by WAYBEL_0:def 17;

      

       A2: ( downarrow y) = ( downarrow {y}) by WAYBEL_0:def 17;

      assume x = y;

      hence thesis by A1, A2, Th11;

    end;

    theorem :: WAYBEL23:14

    for L be non empty RelStr holds for S be non empty SubRelStr of L holds for x be Element of L holds for y be Element of S st x = y holds ( uparrow y) c= ( uparrow x)

    proof

      let L be non empty RelStr;

      let S be non empty SubRelStr of L;

      let x be Element of L;

      let y be Element of S;

      

       A1: ( uparrow x) = ( uparrow {x}) by WAYBEL_0:def 18;

      

       A2: ( uparrow y) = ( uparrow {y}) by WAYBEL_0:def 18;

      assume x = y;

      hence thesis by A1, A2, Th12;

    end;

    begin

    definition

      let L be non empty RelStr;

      let S be Subset of L;

      :: WAYBEL23:def1

      attr S is meet-closed means

      : Def1: ( subrelstr S) is meet-inheriting;

    end

    definition

      let L be non empty RelStr;

      let S be Subset of L;

      :: WAYBEL23:def2

      attr S is join-closed means

      : Def2: ( subrelstr S) is join-inheriting;

    end

    definition

      let L be non empty RelStr;

      let S be Subset of L;

      :: WAYBEL23:def3

      attr S is infs-closed means

      : Def3: ( subrelstr S) is infs-inheriting;

    end

    definition

      let L be non empty RelStr;

      let S be Subset of L;

      :: WAYBEL23:def4

      attr S is sups-closed means

      : Def4: ( subrelstr S) is sups-inheriting;

    end

    registration

      let L be non empty RelStr;

      cluster infs-closed -> meet-closed for Subset of L;

      coherence ;

      cluster sups-closed -> join-closed for Subset of L;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster infs-closed sups-closed non empty for Subset of L;

      existence

      proof

        the carrier of L c= the carrier of L;

        then

        reconsider S = the carrier of L as Subset of L;

        take S;

        the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

        then for X be Subset of ( subrelstr S) st ex_inf_of (X,L) holds ( "/\" (X,L)) in the carrier of ( subrelstr S);

        hence ( subrelstr S) is infs-inheriting;

        the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

        then for X be Subset of ( subrelstr S) st ex_sup_of (X,L) holds ( "\/" (X,L)) in the carrier of ( subrelstr S);

        hence ( subrelstr S) is sups-inheriting;

        thus thesis;

      end;

    end

    theorem :: WAYBEL23:15

    

     Th15: for L be non empty RelStr holds for S be Subset of L holds S is meet-closed iff for x,y be Element of L st x in S & y in S & ex_inf_of ( {x, y},L) holds ( inf {x, y}) in S

    proof

      let L be non empty RelStr;

      let S be Subset of L;

      thus S is meet-closed implies for x,y be Element of L st x in S & y in S & ex_inf_of ( {x, y},L) holds ( inf {x, y}) in S

      proof

        assume S is meet-closed;

        then

         A1: ( subrelstr S) is meet-inheriting;

        let x,y be Element of L;

        assume that

         A2: x in S and

         A3: y in S and

         A4: ex_inf_of ( {x, y},L);

        the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

        hence thesis by A1, A2, A3, A4;

      end;

      assume

       A5: for x,y be Element of L st x in S & y in S & ex_inf_of ( {x, y},L) holds ( inf {x, y}) in S;

      now

        let x,y be Element of L;

        assume that

         A6: x in the carrier of ( subrelstr S) and

         A7: y in the carrier of ( subrelstr S) and

         A8: ex_inf_of ( {x, y},L);

        the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

        hence ( inf {x, y}) in the carrier of ( subrelstr S) by A5, A6, A7, A8;

      end;

      then ( subrelstr S) is meet-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:16

    

     Th16: for L be non empty RelStr holds for S be Subset of L holds S is join-closed iff for x,y be Element of L st x in S & y in S & ex_sup_of ( {x, y},L) holds ( sup {x, y}) in S

    proof

      let L be non empty RelStr;

      let S be Subset of L;

      thus S is join-closed implies for x,y be Element of L st x in S & y in S & ex_sup_of ( {x, y},L) holds ( sup {x, y}) in S

      proof

        assume S is join-closed;

        then

         A1: ( subrelstr S) is join-inheriting;

        let x,y be Element of L;

        assume that

         A2: x in S and

         A3: y in S and

         A4: ex_sup_of ( {x, y},L);

        the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

        hence thesis by A1, A2, A3, A4;

      end;

      assume

       A5: for x,y be Element of L st x in S & y in S & ex_sup_of ( {x, y},L) holds ( sup {x, y}) in S;

      now

        let x,y be Element of L;

        assume that

         A6: x in the carrier of ( subrelstr S) and

         A7: y in the carrier of ( subrelstr S) and

         A8: ex_sup_of ( {x, y},L);

        the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

        hence ( sup {x, y}) in the carrier of ( subrelstr S) by A5, A6, A7, A8;

      end;

      then ( subrelstr S) is join-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:17

    for L be antisymmetric with_infima RelStr holds for S be Subset of L holds S is meet-closed iff for x,y be Element of L st x in S & y in S holds ( inf {x, y}) in S

    proof

      let L be antisymmetric with_infima RelStr;

      let S be Subset of L;

      thus S is meet-closed implies for x,y be Element of L st x in S & y in S holds ( inf {x, y}) in S by YELLOW_0: 21, Th15;

      assume for x,y be Element of L st x in S & y in S holds ( inf {x, y}) in S;

      then for x,y be Element of L st x in S & y in S & ex_inf_of ( {x, y},L) holds ( inf {x, y}) in S;

      hence thesis by Th15;

    end;

    theorem :: WAYBEL23:18

    

     Th18: for L be antisymmetric with_suprema RelStr holds for S be Subset of L holds S is join-closed iff for x,y be Element of L st x in S & y in S holds ( sup {x, y}) in S

    proof

      let L be antisymmetric with_suprema RelStr;

      let S be Subset of L;

      thus S is join-closed implies for x,y be Element of L st x in S & y in S holds ( sup {x, y}) in S by YELLOW_0: 20, Th16;

      assume for x,y be Element of L st x in S & y in S holds ( sup {x, y}) in S;

      then for x,y be Element of L st x in S & y in S & ex_sup_of ( {x, y},L) holds ( sup {x, y}) in S;

      hence thesis by Th16;

    end;

    theorem :: WAYBEL23:19

    for L be non empty RelStr holds for S be Subset of L holds S is infs-closed iff for X be Subset of S st ex_inf_of (X,L) holds ( "/\" (X,L)) in S

    proof

      let L be non empty RelStr;

      let S be Subset of L;

      thus S is infs-closed implies for X be Subset of S st ex_inf_of (X,L) holds ( "/\" (X,L)) in S

      proof

        assume S is infs-closed;

        then

         A1: ( subrelstr S) is infs-inheriting;

        let X be Subset of S;

        assume

         A2: ex_inf_of (X,L);

        X is Subset of ( subrelstr S) by YELLOW_0:def 15;

        then ( "/\" (X,L)) in the carrier of ( subrelstr S) by A1, A2;

        hence thesis by YELLOW_0:def 15;

      end;

      assume

       A3: for X be Subset of S st ex_inf_of (X,L) holds ( "/\" (X,L)) in S;

      now

        let X be Subset of ( subrelstr S);

        assume

         A4: ex_inf_of (X,L);

        X is Subset of S by YELLOW_0:def 15;

        then ( "/\" (X,L)) in S by A3, A4;

        hence ( "/\" (X,L)) in the carrier of ( subrelstr S) by YELLOW_0:def 15;

      end;

      then ( subrelstr S) is infs-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:20

    for L be non empty RelStr holds for S be Subset of L holds S is sups-closed iff for X be Subset of S st ex_sup_of (X,L) holds ( "\/" (X,L)) in S

    proof

      let L be non empty RelStr;

      let S be Subset of L;

      thus S is sups-closed implies for X be Subset of S st ex_sup_of (X,L) holds ( "\/" (X,L)) in S

      proof

        assume S is sups-closed;

        then

         A1: ( subrelstr S) is sups-inheriting;

        let X be Subset of S;

        assume

         A2: ex_sup_of (X,L);

        X is Subset of ( subrelstr S) by YELLOW_0:def 15;

        then ( "\/" (X,L)) in the carrier of ( subrelstr S) by A1, A2;

        hence thesis by YELLOW_0:def 15;

      end;

      assume

       A3: for X be Subset of S st ex_sup_of (X,L) holds ( "\/" (X,L)) in S;

      now

        let X be Subset of ( subrelstr S);

        assume

         A4: ex_sup_of (X,L);

        X is Subset of S by YELLOW_0:def 15;

        then ( "\/" (X,L)) in S by A3, A4;

        hence ( "\/" (X,L)) in the carrier of ( subrelstr S) by YELLOW_0:def 15;

      end;

      then ( subrelstr S) is sups-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:21

    

     Th21: for L be non empty transitive RelStr holds for S be infs-closed non empty Subset of L holds for X be Subset of S st ex_inf_of (X,L) holds ex_inf_of (X,( subrelstr S)) & ( "/\" (X,( subrelstr S))) = ( "/\" (X,L))

    proof

      let L be non empty transitive RelStr;

      let S be infs-closed non empty Subset of L;

      let X be Subset of S;

      

       A1: X is Subset of ( subrelstr S) by YELLOW_0:def 15;

      assume

       A2: ex_inf_of (X,L);

      ( subrelstr S) is infs-inheriting non empty full SubRelStr of L by Def3;

      then ( "/\" (X,L)) in the carrier of ( subrelstr S) by A1, A2, YELLOW_0:def 18;

      hence thesis by A1, A2, YELLOW_0: 63;

    end;

    theorem :: WAYBEL23:22

    

     Th22: for L be non empty transitive RelStr holds for S be sups-closed non empty Subset of L holds for X be Subset of S st ex_sup_of (X,L) holds ex_sup_of (X,( subrelstr S)) & ( "\/" (X,( subrelstr S))) = ( "\/" (X,L))

    proof

      let L be non empty transitive RelStr;

      let S be sups-closed non empty Subset of L;

      let X be Subset of S;

      

       A1: X is Subset of ( subrelstr S) by YELLOW_0:def 15;

      assume

       A2: ex_sup_of (X,L);

      ( subrelstr S) is sups-inheriting non empty full SubRelStr of L by Def4;

      then ( "\/" (X,L)) in the carrier of ( subrelstr S) by A1, A2, YELLOW_0:def 19;

      hence thesis by A1, A2, YELLOW_0: 64;

    end;

    theorem :: WAYBEL23:23

    for L be non empty transitive RelStr holds for S be meet-closed non empty Subset of L holds for x,y be Element of S st ex_inf_of ( {x, y},L) holds ex_inf_of ( {x, y},( subrelstr S)) & ( "/\" ( {x, y},( subrelstr S))) = ( "/\" ( {x, y},L))

    proof

      let L be non empty transitive RelStr;

      let S be meet-closed non empty Subset of L;

      let x,y be Element of S;

      

       A1: x is Element of ( subrelstr S) by YELLOW_0:def 15;

      

       A2: y is Element of ( subrelstr S) by YELLOW_0:def 15;

      assume

       A3: ex_inf_of ( {x, y},L);

      ( subrelstr S) is meet-inheriting non empty full SubRelStr of L by Def1;

      then ( "/\" ( {x, y},L)) in the carrier of ( subrelstr S) by A1, A2, A3, YELLOW_0:def 16;

      hence thesis by A1, A2, A3, YELLOW_0: 65;

    end;

    theorem :: WAYBEL23:24

    for L be non empty transitive RelStr holds for S be join-closed non empty Subset of L holds for x,y be Element of S st ex_sup_of ( {x, y},L) holds ex_sup_of ( {x, y},( subrelstr S)) & ( "\/" ( {x, y},( subrelstr S))) = ( "\/" ( {x, y},L))

    proof

      let L be non empty transitive RelStr;

      let S be join-closed non empty Subset of L;

      let x,y be Element of S;

      

       A1: x is Element of ( subrelstr S) by YELLOW_0:def 15;

      

       A2: y is Element of ( subrelstr S) by YELLOW_0:def 15;

      assume

       A3: ex_sup_of ( {x, y},L);

      ( subrelstr S) is join-inheriting non empty full SubRelStr of L by Def2;

      then ( "\/" ( {x, y},L)) in the carrier of ( subrelstr S) by A1, A2, A3, YELLOW_0:def 17;

      hence thesis by A1, A2, A3, YELLOW_0: 66;

    end;

    theorem :: WAYBEL23:25

    

     Th25: for L be with_infima antisymmetric transitive RelStr holds for S be non empty meet-closed Subset of L holds ( subrelstr S) is with_infima

    proof

      let L be with_infima antisymmetric transitive RelStr;

      let S be non empty meet-closed Subset of L;

      ( subrelstr S) is non empty meet-inheriting full SubRelStr of L by Def1;

      hence thesis;

    end;

    theorem :: WAYBEL23:26

    

     Th26: for L be with_suprema antisymmetric transitive RelStr holds for S be non empty join-closed Subset of L holds ( subrelstr S) is with_suprema

    proof

      let L be with_suprema antisymmetric transitive RelStr;

      let S be non empty join-closed Subset of L;

      ( subrelstr S) is non empty join-inheriting full SubRelStr of L by Def2;

      hence thesis;

    end;

    registration

      let L be with_infima antisymmetric transitive RelStr;

      let S be non empty meet-closed Subset of L;

      cluster ( subrelstr S) -> with_infima;

      coherence by Th25;

    end

    registration

      let L be with_suprema antisymmetric transitive RelStr;

      let S be non empty join-closed Subset of L;

      cluster ( subrelstr S) -> with_suprema;

      coherence by Th26;

    end

    theorem :: WAYBEL23:27

    for L be complete transitive antisymmetric non empty RelStr holds for S be infs-closed non empty Subset of L holds for X be Subset of S holds ( "/\" (X,( subrelstr S))) = ( "/\" (X,L))

    proof

      let L be complete transitive antisymmetric non empty RelStr;

      let S be infs-closed non empty Subset of L;

      let X be Subset of S;

       ex_inf_of (X,L) by YELLOW_0: 17;

      hence thesis by Th21;

    end;

    theorem :: WAYBEL23:28

    for L be complete transitive antisymmetric non empty RelStr holds for S be sups-closed non empty Subset of L holds for X be Subset of S holds ( "\/" (X,( subrelstr S))) = ( "\/" (X,L))

    proof

      let L be complete transitive antisymmetric non empty RelStr;

      let S be sups-closed non empty Subset of L;

      let X be Subset of S;

       ex_sup_of (X,L) by YELLOW_0: 17;

      hence thesis by Th22;

    end;

    theorem :: WAYBEL23:29

    

     Th29: for L be Semilattice holds for S be meet-closed Subset of L holds S is filtered

    proof

      let L be Semilattice;

      let S be meet-closed Subset of L;

      ( subrelstr S) is meet-inheriting by Def1;

      hence thesis by YELLOW12: 26;

    end;

    theorem :: WAYBEL23:30

    

     Th30: for L be sup-Semilattice holds for S be join-closed Subset of L holds S is directed

    proof

      let L be sup-Semilattice;

      let S be join-closed Subset of L;

      ( subrelstr S) is join-inheriting by Def2;

      hence thesis by YELLOW12: 27;

    end;

    registration

      let L be Semilattice;

      cluster meet-closed -> filtered for Subset of L;

      coherence by Th29;

    end

    registration

      let L be sup-Semilattice;

      cluster join-closed -> directed for Subset of L;

      coherence by Th30;

    end

    theorem :: WAYBEL23:31

    for L be Semilattice holds for S be upper non empty Subset of L holds S is Filter of L iff S is meet-closed by WAYBEL_0: 63;

    theorem :: WAYBEL23:32

    for L be sup-Semilattice holds for S be lower non empty Subset of L holds S is Ideal of L iff S is join-closed by WAYBEL_0: 64;

    theorem :: WAYBEL23:33

    

     Th33: for L be non empty RelStr holds for S1,S2 be join-closed Subset of L holds (S1 /\ S2) is join-closed

    proof

      let L be non empty RelStr;

      let S1,S2 be join-closed Subset of L;

      

       A1: ( subrelstr S2) is join-inheriting by Def2;

      

       A2: ( subrelstr S1) is join-inheriting by Def2;

      now

        let x,y be Element of L;

        assume that

         A3: x in the carrier of ( subrelstr (S1 /\ S2)) and

         A4: y in the carrier of ( subrelstr (S1 /\ S2)) and

         A5: ex_sup_of ( {x, y},L);

        

         A6: y in (S1 /\ S2) by A4, YELLOW_0:def 15;

        then y in S2 by XBOOLE_0:def 4;

        then

         A7: y in the carrier of ( subrelstr S2) by YELLOW_0:def 15;

        

         A8: x in (S1 /\ S2) by A3, YELLOW_0:def 15;

        then x in S2 by XBOOLE_0:def 4;

        then x in the carrier of ( subrelstr S2) by YELLOW_0:def 15;

        then ( sup {x, y}) in the carrier of ( subrelstr S2) by A1, A5, A7;

        then

         A9: ( sup {x, y}) in S2 by YELLOW_0:def 15;

        y in S1 by A6, XBOOLE_0:def 4;

        then

         A10: y in the carrier of ( subrelstr S1) by YELLOW_0:def 15;

        x in S1 by A8, XBOOLE_0:def 4;

        then x in the carrier of ( subrelstr S1) by YELLOW_0:def 15;

        then ( sup {x, y}) in the carrier of ( subrelstr S1) by A2, A5, A10;

        then ( sup {x, y}) in S1 by YELLOW_0:def 15;

        then ( sup {x, y}) in (S1 /\ S2) by A9, XBOOLE_0:def 4;

        hence ( sup {x, y}) in the carrier of ( subrelstr (S1 /\ S2)) by YELLOW_0:def 15;

      end;

      then ( subrelstr (S1 /\ S2)) is join-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:34

    for L be non empty RelStr holds for S1,S2 be meet-closed Subset of L holds (S1 /\ S2) is meet-closed

    proof

      let L be non empty RelStr;

      let S1,S2 be meet-closed Subset of L;

      

       A1: ( subrelstr S2) is meet-inheriting by Def1;

      

       A2: ( subrelstr S1) is meet-inheriting by Def1;

      now

        let x,y be Element of L;

        assume that

         A3: x in the carrier of ( subrelstr (S1 /\ S2)) and

         A4: y in the carrier of ( subrelstr (S1 /\ S2)) and

         A5: ex_inf_of ( {x, y},L);

        

         A6: y in (S1 /\ S2) by A4, YELLOW_0:def 15;

        then y in S2 by XBOOLE_0:def 4;

        then

         A7: y in the carrier of ( subrelstr S2) by YELLOW_0:def 15;

        

         A8: x in (S1 /\ S2) by A3, YELLOW_0:def 15;

        then x in S2 by XBOOLE_0:def 4;

        then x in the carrier of ( subrelstr S2) by YELLOW_0:def 15;

        then ( inf {x, y}) in the carrier of ( subrelstr S2) by A1, A5, A7;

        then

         A9: ( inf {x, y}) in S2 by YELLOW_0:def 15;

        y in S1 by A6, XBOOLE_0:def 4;

        then

         A10: y in the carrier of ( subrelstr S1) by YELLOW_0:def 15;

        x in S1 by A8, XBOOLE_0:def 4;

        then x in the carrier of ( subrelstr S1) by YELLOW_0:def 15;

        then ( inf {x, y}) in the carrier of ( subrelstr S1) by A2, A5, A10;

        then ( inf {x, y}) in S1 by YELLOW_0:def 15;

        then ( inf {x, y}) in (S1 /\ S2) by A9, XBOOLE_0:def 4;

        hence ( inf {x, y}) in the carrier of ( subrelstr (S1 /\ S2)) by YELLOW_0:def 15;

      end;

      then ( subrelstr (S1 /\ S2)) is meet-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:35

    

     Th35: for L be sup-Semilattice holds for x be Element of L holds ( downarrow x) is join-closed

    proof

      let L be sup-Semilattice;

      let x be Element of L;

      reconsider x1 = x as Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( downarrow x)) and

         A2: z in the carrier of ( subrelstr ( downarrow x)) and ex_sup_of ( {y, z},L);

        z in ( downarrow x) by A2, YELLOW_0:def 15;

        then

         A3: z <= x1 by WAYBEL_0: 17;

        y in ( downarrow x) by A1, YELLOW_0:def 15;

        then y <= x1 by WAYBEL_0: 17;

        then (y "\/" z) <= x1 by A3, YELLOW_5: 9;

        then (y "\/" z) in ( downarrow x) by WAYBEL_0: 17;

        then ( sup {y, z}) in ( downarrow x) by YELLOW_0: 41;

        hence ( sup {y, z}) in the carrier of ( subrelstr ( downarrow x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( downarrow x)) is join-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:36

    

     Th36: for L be Semilattice holds for x be Element of L holds ( downarrow x) is meet-closed

    proof

      let L be Semilattice;

      let x be Element of L;

      reconsider x1 = x as Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( downarrow x)) and z in the carrier of ( subrelstr ( downarrow x)) and ex_inf_of ( {y, z},L);

        y in ( downarrow x) by A1, YELLOW_0:def 15;

        then

         A2: y <= x1 by WAYBEL_0: 17;

        (y "/\" z) <= y by YELLOW_0: 23;

        then (y "/\" z) <= x1 by A2, YELLOW_0:def 2;

        then (y "/\" z) in ( downarrow x) by WAYBEL_0: 17;

        then ( inf {y, z}) in ( downarrow x) by YELLOW_0: 40;

        hence ( inf {y, z}) in the carrier of ( subrelstr ( downarrow x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( downarrow x)) is meet-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:37

    

     Th37: for L be sup-Semilattice holds for x be Element of L holds ( uparrow x) is join-closed

    proof

      let L be sup-Semilattice;

      let x be Element of L;

      reconsider x1 = x as Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( uparrow x)) and z in the carrier of ( subrelstr ( uparrow x)) and ex_sup_of ( {y, z},L);

        y in ( uparrow x) by A1, YELLOW_0:def 15;

        then

         A2: y >= x1 by WAYBEL_0: 18;

        (y "\/" z) >= y by YELLOW_0: 22;

        then (y "\/" z) >= x1 by A2, YELLOW_0:def 2;

        then (y "\/" z) in ( uparrow x) by WAYBEL_0: 18;

        then ( sup {y, z}) in ( uparrow x) by YELLOW_0: 41;

        hence ( sup {y, z}) in the carrier of ( subrelstr ( uparrow x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( uparrow x)) is join-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:38

    

     Th38: for L be Semilattice holds for x be Element of L holds ( uparrow x) is meet-closed

    proof

      let L be Semilattice;

      let x be Element of L;

      reconsider x1 = x as Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( uparrow x)) and

         A2: z in the carrier of ( subrelstr ( uparrow x)) and ex_inf_of ( {y, z},L);

        z in ( uparrow x) by A2, YELLOW_0:def 15;

        then

         A3: z >= x1 by WAYBEL_0: 18;

        y in ( uparrow x) by A1, YELLOW_0:def 15;

        then y >= x1 by WAYBEL_0: 18;

        then (y "/\" z) >= (x1 "/\" x1) by A3, YELLOW_3: 2;

        then (y "/\" z) >= x1 by YELLOW_5: 2;

        then (y "/\" z) in ( uparrow x) by WAYBEL_0: 18;

        then ( inf {y, z}) in ( uparrow x) by YELLOW_0: 40;

        hence ( inf {y, z}) in the carrier of ( subrelstr ( uparrow x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( uparrow x)) is meet-inheriting;

      hence thesis;

    end;

    registration

      let L be sup-Semilattice;

      let x be Element of L;

      cluster ( downarrow x) -> join-closed;

      coherence by Th35;

      cluster ( uparrow x) -> join-closed;

      coherence by Th37;

    end

    registration

      let L be Semilattice;

      let x be Element of L;

      cluster ( downarrow x) -> meet-closed;

      coherence by Th36;

      cluster ( uparrow x) -> meet-closed;

      coherence by Th38;

    end

    theorem :: WAYBEL23:39

    

     Th39: for L be sup-Semilattice holds for x be Element of L holds ( waybelow x) is join-closed

    proof

      let L be sup-Semilattice;

      let x be Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( waybelow x)) and

         A2: z in the carrier of ( subrelstr ( waybelow x)) and ex_sup_of ( {y, z},L);

        z in ( waybelow x) by A2, YELLOW_0:def 15;

        then

         A3: z << x by WAYBEL_3: 7;

        y in ( waybelow x) by A1, YELLOW_0:def 15;

        then y << x by WAYBEL_3: 7;

        then (y "\/" z) << x by A3, WAYBEL_3: 3;

        then (y "\/" z) in ( waybelow x) by WAYBEL_3: 7;

        then ( sup {y, z}) in ( waybelow x) by YELLOW_0: 41;

        hence ( sup {y, z}) in the carrier of ( subrelstr ( waybelow x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( waybelow x)) is join-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:40

    

     Th40: for L be Semilattice holds for x be Element of L holds ( waybelow x) is meet-closed

    proof

      let L be Semilattice;

      let x be Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( waybelow x)) and z in the carrier of ( subrelstr ( waybelow x)) and ex_inf_of ( {y, z},L);

        y in ( waybelow x) by A1, YELLOW_0:def 15;

        then

         A2: y << x by WAYBEL_3: 7;

        (y "/\" z) <= y by YELLOW_0: 23;

        then (y "/\" z) << x by A2, WAYBEL_3: 2;

        then (y "/\" z) in ( waybelow x) by WAYBEL_3: 7;

        then ( inf {y, z}) in ( waybelow x) by YELLOW_0: 40;

        hence ( inf {y, z}) in the carrier of ( subrelstr ( waybelow x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( waybelow x)) is meet-inheriting;

      hence thesis;

    end;

    theorem :: WAYBEL23:41

    

     Th41: for L be sup-Semilattice holds for x be Element of L holds ( wayabove x) is join-closed

    proof

      let L be sup-Semilattice;

      let x be Element of L;

      now

        let y,z be Element of L;

        assume that

         A1: y in the carrier of ( subrelstr ( wayabove x)) and z in the carrier of ( subrelstr ( wayabove x)) and ex_sup_of ( {y, z},L);

        y in ( wayabove x) by A1, YELLOW_0:def 15;

        then

         A2: y >> x by WAYBEL_3: 8;

        (y "\/" z) >= y by YELLOW_0: 22;

        then (y "\/" z) >> x by A2, WAYBEL_3: 2;

        then (y "\/" z) in ( wayabove x) by WAYBEL_3: 8;

        then ( sup {y, z}) in ( wayabove x) by YELLOW_0: 41;

        hence ( sup {y, z}) in the carrier of ( subrelstr ( wayabove x)) by YELLOW_0:def 15;

      end;

      then ( subrelstr ( wayabove x)) is join-inheriting;

      hence thesis;

    end;

    registration

      let L be sup-Semilattice;

      let x be Element of L;

      cluster ( waybelow x) -> join-closed;

      coherence by Th39;

      cluster ( wayabove x) -> join-closed;

      coherence by Th41;

    end

    registration

      let L be Semilattice;

      let x be Element of L;

      cluster ( waybelow x) -> meet-closed;

      coherence by Th40;

    end

    begin

    definition

      let T be TopStruct;

      :: WAYBEL23:def5

      func weight T -> Cardinal equals ( meet the set of all ( card B) where B be Basis of T);

      coherence

      proof

        set X = the set of all ( card B1) where B1 be Basis of T;

        defpred P[ Ordinal] means $1 in the set of all ( card B) where B be Basis of T;

        

         A1: ex A be Ordinal st P[A]

        proof

          take ( card the topology of T);

          the topology of T is Basis of T by CANTOR_1: 2;

          hence thesis;

        end;

        consider A be Ordinal such that

         A2: P[A] and

         A3: for C be Ordinal st P[C] holds A c= C from ORDINAL1:sch 1( A1);

        ex B be Basis of T st A = ( card B) by A2;

        then

        reconsider A as Cardinal;

         A4:

        now

          let x be object;

          thus (for y be set holds y in X implies x in y) implies x in A by A2;

          assume

           A5: x in A;

          let y be set;

          assume

           A6: y in X;

          then ex B1 be Basis of T st y = ( card B1);

          then

          reconsider y1 = y as Cardinal;

          A c= y1 by A3, A6;

          hence x in y by A5;

        end;

        the topology of T is Basis of T by CANTOR_1: 2;

        then ( card the topology of T) in X;

        hence thesis by A4, SETFAM_1:def 1;

      end;

    end

    definition

      let T be TopStruct;

      :: WAYBEL23:def6

      attr T is second-countable means ( weight T) c= omega ;

    end

    definition

      let L be continuous sup-Semilattice;

      :: WAYBEL23:def7

      mode CLbasis of L -> Subset of L means

      : Def7: it is join-closed & for x be Element of L holds x = ( sup (( waybelow x) /\ it ));

      existence

      proof

        take S = ( [#] L);

        ( subrelstr S) is join-inheriting by WAYBEL_0: 64;

        hence S is join-closed;

        let x be Element of L;

        

        thus x = ( sup ( waybelow x)) by WAYBEL_3:def 5

        .= ( sup (( waybelow x) /\ S)) by XBOOLE_1: 28;

      end;

    end

    definition

      let L be non empty RelStr;

      let S be Subset of L;

      :: WAYBEL23:def8

      attr S is with_bottom means

      : Def8: ( Bottom L) in S;

    end

    definition

      let L be non empty RelStr;

      let S be Subset of L;

      :: WAYBEL23:def9

      attr S is with_top means ( Top L) in S;

    end

    registration

      let L be non empty RelStr;

      cluster with_bottom -> non empty for Subset of L;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster with_top -> non empty for Subset of L;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster with_bottom for Subset of L;

      existence

      proof

        take ( [#] L);

        thus ( Bottom L) in ( [#] L);

      end;

      cluster with_top for Subset of L;

      existence

      proof

        take ( [#] L);

        thus ( Top L) in ( [#] L);

      end;

    end

    registration

      let L be continuous sup-Semilattice;

      cluster with_bottom for CLbasis of L;

      existence

      proof

         A1:

        now

          let x be Element of L;

          (( waybelow x) /\ ( [#] L)) = ( waybelow x) by XBOOLE_1: 28;

          hence x = ( sup (( waybelow x) /\ ( [#] L))) by WAYBEL_3:def 5;

        end;

        for x,y be Element of L st x in ( [#] L) & y in ( [#] L) holds ( sup {x, y}) in ( [#] L);

        then ( [#] L) is join-closed by Th18;

        then

        reconsider S = ( [#] L) as CLbasis of L by A1, Def7;

        take S;

        thus thesis;

      end;

      cluster with_top for CLbasis of L;

      existence

      proof

         A2:

        now

          let x be Element of L;

          (( waybelow x) /\ ( [#] L)) = ( waybelow x) by XBOOLE_1: 28;

          hence x = ( sup (( waybelow x) /\ ( [#] L))) by WAYBEL_3:def 5;

        end;

        for x,y be Element of L st x in ( [#] L) & y in ( [#] L) holds ( sup {x, y}) in ( [#] L);

        then ( [#] L) is join-closed by Th18;

        then

        reconsider S = ( [#] L) as CLbasis of L by A2, Def7;

        take S;

        thus thesis;

      end;

    end

    theorem :: WAYBEL23:42

    

     Th42: for L be lower-bounded antisymmetric non empty RelStr holds for S be with_bottom Subset of L holds ( subrelstr S) is lower-bounded

    proof

      let L be lower-bounded antisymmetric non empty RelStr;

      let S be with_bottom Subset of L;

      ( Bottom L) in S by Def8;

      then

      reconsider dL = ( Bottom L) as Element of ( subrelstr S) by YELLOW_0:def 15;

      take dL;

      now

        let x be Element of ( subrelstr S);

        assume x in the carrier of ( subrelstr S);

        reconsider x1 = x as Element of L by YELLOW_0: 58;

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

        hence dL <= x by YELLOW_0: 60;

      end;

      hence thesis;

    end;

    registration

      let L be lower-bounded antisymmetric non empty RelStr;

      let S be with_bottom Subset of L;

      cluster ( subrelstr S) -> lower-bounded;

      coherence by Th42;

    end

    registration

      let L be continuous sup-Semilattice;

      cluster -> join-closed for CLbasis of L;

      coherence by Def7;

    end

    registration

      cluster bounded non trivial for continuous LATTICE;

      existence

      proof

        set X = the non empty set;

        take ( BoolePoset X);

        thus thesis;

      end;

    end

    registration

      let L be lower-bounded non trivial continuous sup-Semilattice;

      cluster -> non empty for CLbasis of L;

      coherence

      proof

        let B be CLbasis of L;

        assume

         A1: B is empty;

        ( Top L) = ( "\/" ((( waybelow ( Top L)) /\ B),L)) by Def7

        .= ( Bottom L) by A1;

        hence contradiction by WAYBEL_7: 3;

      end;

    end

    theorem :: WAYBEL23:43

    

     Th43: for L be sup-Semilattice holds the carrier of ( CompactSublatt L) is join-closed Subset of L

    proof

      let L be sup-Semilattice;

      reconsider C = the carrier of ( CompactSublatt L) as Subset of L by YELLOW_0:def 13;

      ( subrelstr C) = ( CompactSublatt L) by YELLOW_0:def 15;

      hence thesis by Def2;

    end;

    theorem :: WAYBEL23:44

    

     Th44: for L be algebraic lower-bounded LATTICE holds the carrier of ( CompactSublatt L) is with_bottom CLbasis of L

    proof

      let L be algebraic lower-bounded LATTICE;

      reconsider C = the carrier of ( CompactSublatt L) as join-closed Subset of L by Th43;

      now

        let x be Element of L;

        x = ( sup ( compactbelow x)) by WAYBEL_8:def 3;

        hence x = ( sup (( waybelow x) /\ C)) by Th1;

      end;

      then

      reconsider C as CLbasis of L by Def7;

      ( Bottom L) in C by WAYBEL_8: 3;

      hence thesis by Def8;

    end;

    theorem :: WAYBEL23:45

    for L be continuous lower-bounded sup-Semilattice st the carrier of ( CompactSublatt L) is CLbasis of L holds L is algebraic

    proof

      let L be continuous lower-bounded sup-Semilattice;

      reconsider C = the carrier of ( CompactSublatt L) as Subset of L by Th43;

      assume

       A1: the carrier of ( CompactSublatt L) is CLbasis of L;

      now

        let x be Element of L;

        x = ( sup (( waybelow x) /\ C)) by A1, Def7;

        hence x = ( sup ( compactbelow x)) by Th1;

      end;

      then

       A2: L is satisfying_axiom_K by WAYBEL_8:def 3;

      for x be Element of L holds ( compactbelow x) is non empty directed;

      hence thesis by A2, WAYBEL_8:def 4;

    end;

    theorem :: WAYBEL23:46

    

     Th46: for L be continuous lower-bounded LATTICE holds for B be join-closed Subset of L holds B is CLbasis of L iff for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b << y

    proof

      let L be continuous lower-bounded LATTICE;

      let B be join-closed Subset of L;

      thus B is CLbasis of L implies for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b << y

      proof

        assume

         A1: B is CLbasis of L;

        let x,y be Element of L such that

         A2: not y <= x;

        thus ex b be Element of L st b in B & not b <= x & b << y

        proof

          assume

           A3: for b1 be Element of L holds not b1 in B or b1 <= x or not b1 << y;

          

           A4: (( waybelow y) /\ B) c= ( downarrow x)

          proof

            let z be object;

            assume

             A5: z in (( waybelow y) /\ B);

            then

            reconsider z1 = z as Element of L;

            z in ( waybelow y) by A5, XBOOLE_0:def 4;

            then

             A6: z1 << y by WAYBEL_3: 7;

            z in B by A5, XBOOLE_0:def 4;

            then z1 <= x by A3, A6;

            hence thesis by WAYBEL_0: 17;

          end;

          

           A7: ex_sup_of (( downarrow x),L) by YELLOW_0: 17;

           ex_sup_of ((( waybelow y) /\ B),L) by YELLOW_0: 17;

          then ( sup (( waybelow y) /\ B)) <= ( sup ( downarrow x)) by A7, A4, YELLOW_0: 34;

          then y <= ( sup ( downarrow x)) by A1, Def7;

          hence contradiction by A2, WAYBEL_0: 34;

        end;

      end;

      assume

       A8: for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b << y;

      now

        let x be Element of L;

        

         A9: ex_sup_of (( waybelow x),L) by YELLOW_0: 17;

         ex_sup_of ((( waybelow x) /\ B),L) by YELLOW_0: 17;

        then

         A10: ( sup (( waybelow x) /\ B)) <= ( sup ( waybelow x)) by A9, XBOOLE_1: 17, YELLOW_0: 34;

        

         A11: x <= ( sup (( waybelow x) /\ B))

        proof

          assume not x <= ( sup (( waybelow x) /\ B));

          then

          consider b be Element of L such that

           A12: b in B and

           A13: not b <= ( sup (( waybelow x) /\ B)) and

           A14: b << x by A8;

          b in ( waybelow x) by A14, WAYBEL_3: 7;

          then b in (( waybelow x) /\ B) by A12, XBOOLE_0:def 4;

          hence contradiction by A13, YELLOW_2: 22;

        end;

        x = ( sup ( waybelow x)) by WAYBEL_3:def 5;

        hence x = ( sup (( waybelow x) /\ B)) by A10, A11, YELLOW_0:def 3;

      end;

      hence thesis by Def7;

    end;

    theorem :: WAYBEL23:47

    

     Th47: for L be continuous lower-bounded LATTICE holds for B be join-closed Subset of L st ( Bottom L) in B holds B is CLbasis of L iff for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y

    proof

      let L be continuous lower-bounded LATTICE;

      let B be join-closed Subset of L;

      assume

       A1: ( Bottom L) in B;

      thus B is CLbasis of L implies for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y

      proof

        assume

         A2: B is CLbasis of L;

        let x,y be Element of L;

        assume

         A3: x << y;

        ( Bottom L) << y by WAYBEL_3: 4;

        then

         A4: ( Bottom L) in ( waybelow y) by WAYBEL_3: 7;

        (( waybelow y) /\ B) is join-closed by Th33;

        then

        reconsider D = (( waybelow y) /\ B) as non empty directed Subset of L by A1, A4, XBOOLE_0:def 4;

        y = ( sup D) by A2, Def7;

        then

        consider b be Element of L such that

         A5: b in D and

         A6: x <= b by A3, WAYBEL_3:def 1;

        take b;

        b in ( waybelow y) by A5, XBOOLE_0:def 4;

        hence thesis by A5, A6, WAYBEL_3: 7, XBOOLE_0:def 4;

      end;

      assume

       A7: for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y;

      now

        let x be Element of L;

        

         A8: x <= ( sup (( waybelow x) /\ B))

        proof

          

           A9: for x be Element of L holds ( waybelow x) is non empty directed;

          assume not x <= ( sup (( waybelow x) /\ B));

          then

          consider u be Element of L such that

           A10: u << x and

           A11: not u <= ( sup (( waybelow x) /\ B)) by A9, WAYBEL_3: 24;

          consider b be Element of L such that

           A12: b in B and

           A13: u <= b and

           A14: b << x by A7, A10;

          b in ( waybelow x) by A14, WAYBEL_3: 7;

          then

           A15: b in (( waybelow x) /\ B) by A12, XBOOLE_0:def 4;

          

           A16: ( sup (( waybelow x) /\ B)) is_>=_than (( waybelow x) /\ B) by YELLOW_0: 32;

           not b <= ( sup (( waybelow x) /\ B)) by A11, A13, YELLOW_0:def 2;

          hence contradiction by A15, A16;

        end;

        (( waybelow x) /\ B) c= ( waybelow x) by XBOOLE_1: 17;

        then ( sup (( waybelow x) /\ B)) <= ( sup ( waybelow x)) by WAYBEL_7: 1;

        then ( sup (( waybelow x) /\ B)) <= x by WAYBEL_3:def 5;

        hence x = ( sup (( waybelow x) /\ B)) by A8, YELLOW_0:def 3;

      end;

      hence thesis by Def7;

    end;

    

     Lm2: for L be continuous lower-bounded LATTICE holds for B be join-closed Subset of L st ( Bottom L) in B holds (for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y) implies (the carrier of ( CompactSublatt L) c= B & for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y)

    proof

      let L be continuous lower-bounded LATTICE;

      let B be join-closed Subset of L;

      assume

       A1: ( Bottom L) in B;

      assume

       A2: for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y;

      thus the carrier of ( CompactSublatt L) c= B

      proof

        let z be object;

        assume

         A3: z in the carrier of ( CompactSublatt L);

        the carrier of ( CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;

        then

        reconsider z1 = z as Element of L by A3;

        z1 is compact by A3, WAYBEL_8:def 1;

        then z1 << z1 by WAYBEL_3:def 2;

        then

        consider b be Element of L such that

         A4: b in B and

         A5: z1 <= b and

         A6: b << z1 by A2;

        b <= z1 by A6, WAYBEL_3: 1;

        hence thesis by A4, A5, YELLOW_0:def 3;

      end;

      let x,y be Element of L;

      assume

       A7: not y <= x;

      B is CLbasis of L by A1, A2, Th47;

      then

      consider b be Element of L such that

       A8: b in B and

       A9: not b <= x and

       A10: b << y by A7, Th46;

      take b;

      thus thesis by A8, A9, A10, WAYBEL_3: 1;

    end;

    

     Lm3: for L be continuous lower-bounded LATTICE holds for B be Subset of L holds (for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y) implies for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b << y

    proof

      let L be continuous lower-bounded LATTICE;

      let B be Subset of L;

      assume

       A1: for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y;

      let x,y be Element of L;

      

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

      assume not y <= x;

      then

      consider y1 be Element of L such that

       A3: y1 << y and

       A4: not y1 <= x by A2, WAYBEL_3: 24;

      consider b be Element of L such that

       A5: b in B and

       A6: not b <= x and

       A7: b <= y1 by A1, A4;

      take b;

      thus thesis by A3, A5, A6, A7, WAYBEL_3: 2;

    end;

    theorem :: WAYBEL23:48

    

     Th48: for L be continuous lower-bounded LATTICE holds for B be join-closed Subset of L st ( Bottom L) in B holds B is CLbasis of L iff (the carrier of ( CompactSublatt L) c= B & for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y)

    proof

      let L be continuous lower-bounded LATTICE;

      let B be join-closed Subset of L;

      assume

       A1: ( Bottom L) in B;

      thus B is CLbasis of L implies (the carrier of ( CompactSublatt L) c= B & for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y)

      proof

        assume B is CLbasis of L;

        then for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y by A1, Th47;

        hence thesis by A1, Lm2;

      end;

      assume that the carrier of ( CompactSublatt L) c= B and

       A2: for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y;

      for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b << y by A2, Lm3;

      hence thesis by Th46;

    end;

    theorem :: WAYBEL23:49

    for L be continuous lower-bounded LATTICE holds for B be join-closed Subset of L st ( Bottom L) in B holds B is CLbasis of L iff for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y

    proof

      let L be continuous lower-bounded LATTICE;

      let B be join-closed Subset of L;

      assume

       A1: ( Bottom L) in B;

      thus B is CLbasis of L implies for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y

      proof

        assume B is CLbasis of L;

        then for x,y be Element of L st x << y holds ex b be Element of L st b in B & x <= b & b << y by A1, Th47;

        hence thesis by A1, Lm2;

      end;

      assume for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b <= y;

      then for x,y be Element of L st not y <= x holds ex b be Element of L st b in B & not b <= x & b << y by Lm3;

      hence thesis by Th46;

    end;

    theorem :: WAYBEL23:50

    

     Th50: for L be lower-bounded sup-Semilattice holds for S be non empty full SubRelStr of L st ( Bottom L) in the carrier of S & the carrier of S is join-closed Subset of L holds for x be Element of L holds (( waybelow x) /\ the carrier of S) is Ideal of S

    proof

      let L be lower-bounded sup-Semilattice;

      let S be non empty full SubRelStr of L;

      assume that

       A1: ( Bottom L) in the carrier of S and

       A2: the carrier of S is join-closed Subset of L;

      let x be Element of L;

      ( Bottom L) << x by WAYBEL_3: 4;

      then ( Bottom L) in ( waybelow x) by WAYBEL_3: 7;

      then

      reconsider X = (( waybelow x) /\ the carrier of S) as non empty Subset of S by A1, XBOOLE_0:def 4, XBOOLE_1: 17;

      reconsider S1 = the carrier of S as join-closed Subset of L by A2;

       A3:

      now

        let a,b be Element of S;

        reconsider a1 = a, b1 = b as Element of L by YELLOW_0: 58;

        assume that

         A4: a in X and

         A5: b <= a;

        a in ( waybelow x) by A4, XBOOLE_0:def 4;

        then

         A6: a1 << x by WAYBEL_3: 7;

        b1 <= a1 by A5, YELLOW_0: 59;

        then b1 << x by A6, WAYBEL_3: 2;

        then b in ( waybelow x) by WAYBEL_3: 7;

        hence b in X by XBOOLE_0:def 4;

      end;

      (( waybelow x) /\ S1) is join-closed by Th33;

      hence thesis by A3, WAYBEL10: 23, WAYBEL_0:def 19;

    end;

    definition

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      :: WAYBEL23:def10

      func supMap S -> Function of ( InclPoset ( Ids S)), L means

      : Def10: for I be Ideal of S holds (it . I) = ( "\/" (I,L));

      existence

      proof

        deffunc F( set) = ( "\/" ($1,L));

        set P = ( InclPoset ( Ids S));

        

         A1: for I be set st I in the carrier of P holds F(I) in the carrier of L;

        ex f be Function of the carrier of P, the carrier of L st for I be set st I in the carrier of P holds (f . I) = F(I) from FUNCT_2:sch 11( A1);

        then

        consider f be Function of the carrier of P, the carrier of L such that

         A2: for I be set st I in the carrier of P holds (f . I) = ( "\/" (I,L));

        reconsider f as Function of P, L;

        take f;

        for I be Ideal of S holds (f . I) = ( "\/" (I,L))

        proof

          let I be Ideal of S;

          I in the set of all X where X be Ideal of S;

          then I in the carrier of RelStr (# ( Ids S), ( RelIncl ( Ids S)) #) by WAYBEL_0:def 23;

          then I in the carrier of P by YELLOW_1:def 1;

          hence thesis by A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set P = ( InclPoset ( Ids S));

        let f,g be Function of ( InclPoset ( Ids S)), L;

        assume that

         A3: for I be Ideal of S holds (f . I) = ( "\/" (I,L)) and

         A4: for I be Ideal of S holds (g . I) = ( "\/" (I,L));

        

         A5: the carrier of P = the carrier of RelStr (# ( Ids S), ( RelIncl ( Ids S)) #) by YELLOW_1:def 1

        .= ( Ids S);

         A6:

        now

          let x be object;

          assume x in the carrier of P;

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

          then ex I be Ideal of S st x = I;

          then

          reconsider I = x as Ideal of S;

          (f . I) = ( "\/" (I,L)) by A3;

          hence (f . x) = (g . x) by A4;

        end;

        

         A7: ( dom g) = the carrier of P by FUNCT_2:def 1;

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

        hence f = g by A7, A6, FUNCT_1: 2;

      end;

    end

    definition

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      :: WAYBEL23:def11

      func idsMap S -> Function of ( InclPoset ( Ids S)), ( InclPoset ( Ids L)) means

      : Def11: for I be Ideal of S holds ex J be Subset of L st I = J & (it . I) = ( downarrow J);

      existence

      proof

        defpred P[ set, set] means ex J be Subset of L st $1 = J & $2 = ( downarrow J);

        set R = ( InclPoset ( Ids L));

        set P = ( InclPoset ( Ids S));

        

         A1: for I be Element of P holds ex K be Element of R st P[I, K]

        proof

          let I be Element of P;

          I in the carrier of P;

          then I in ( Ids S) by YELLOW_1: 1;

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

          then

          consider J be Ideal of S such that

           A2: J = I;

          reconsider J as non empty directed Subset of L by YELLOW_2: 7;

          ( downarrow J) in the set of all X where X be Ideal of L;

          then ( downarrow J) in ( Ids L) by WAYBEL_0:def 23;

          then

          reconsider K = ( downarrow J) as Element of R by YELLOW_1: 1;

          take K, J;

          thus thesis by A2;

        end;

        ex f be Function of the carrier of P, the carrier of R st for I be Element of P holds P[I, (f . I)] from FUNCT_2:sch 3( A1);

        then

        consider f be Function of the carrier of P, the carrier of R such that

         A3: for I be Element of P holds ex J be Subset of L st I = J & (f . I) = ( downarrow J);

        reconsider f as Function of P, R;

        take f;

        for I be Ideal of S holds ex J be Subset of L st I = J & (f . I) = ( downarrow J)

        proof

          let I be Ideal of S;

          I in the set of all X where X be Ideal of S;

          then I in the carrier of RelStr (# ( Ids S), ( RelIncl ( Ids S)) #) by WAYBEL_0:def 23;

          then I in the carrier of P by YELLOW_1:def 1;

          then

          consider J be Subset of L such that

           A4: I = J and

           A5: (f . I) = ( downarrow J) by A3;

          reconsider J as Subset of L;

          take J;

          thus thesis by A4, A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set P = ( InclPoset ( Ids S));

        let f,g be Function of ( InclPoset ( Ids S)), ( InclPoset ( Ids L));

        assume that

         A6: for I be Ideal of S holds ex J be Subset of L st I = J & (f . I) = ( downarrow J) and

         A7: for I be Ideal of S holds ex J be Subset of L st I = J & (g . I) = ( downarrow J);

        

         A8: the carrier of P = the carrier of RelStr (# ( Ids S), ( RelIncl ( Ids S)) #) by YELLOW_1:def 1

        .= ( Ids S);

         A9:

        now

          let x be object;

          assume x in the carrier of P;

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

          then ex I be Ideal of S st x = I;

          then

          reconsider I = x as Ideal of S;

          

           A10: ex J2 be Subset of L st I = J2 & (g . I) = ( downarrow J2) by A7;

          ex J1 be Subset of L st I = J1 & (f . I) = ( downarrow J1) by A6;

          hence (f . x) = (g . x) by A10;

        end;

        

         A11: ( dom g) = the carrier of P by FUNCT_2:def 1;

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

        hence f = g by A11, A9, FUNCT_1: 2;

      end;

    end

    registration

      let L be reflexive RelStr;

      let B be Subset of L;

      cluster ( subrelstr B) -> reflexive;

      coherence ;

    end

    registration

      let L be transitive RelStr;

      let B be Subset of L;

      cluster ( subrelstr B) -> transitive;

      coherence ;

    end

    registration

      let L be antisymmetric RelStr;

      let B be Subset of L;

      cluster ( subrelstr B) -> antisymmetric;

      coherence ;

    end

    definition

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      :: WAYBEL23:def12

      func baseMap B -> Function of L, ( InclPoset ( Ids ( subrelstr B))) means

      : Def12: for x be Element of L holds (it . x) = (( waybelow x) /\ B);

      existence

      proof

        defpred P[ set, set] means ex y be Element of L st $1 = y & $2 = (( waybelow y) /\ B);

        set P = ( InclPoset ( Ids ( subrelstr B)));

        

         A1: for x be Element of L holds ex z be Element of P st P[x, z]

        proof

          let x be Element of L;

          reconsider y = x as Element of L;

          

           A2: the carrier of ( subrelstr B) = B by YELLOW_0:def 15;

          ( Bottom L) in B by Def8;

          then (( waybelow y) /\ B) is Ideal of ( subrelstr B) by A2, Th50;

          then

          reconsider z = (( waybelow y) /\ B) as Element of P by YELLOW_2: 41;

          take z, y;

          thus thesis;

        end;

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

        then

        consider f be Function of the carrier of L, the carrier of P such that

         A3: for x be Element of L holds ex y be Element of L st x = y & (f . x) = (( waybelow y) /\ B);

        reconsider f as Function of L, P;

        take f;

        now

          let x be Element of L;

          ex y be Element of L st x = y & (f . x) = (( waybelow y) /\ B) by A3;

          hence (f . x) = (( waybelow x) /\ B);

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of L, ( InclPoset ( Ids ( subrelstr B)));

        assume that

         A4: for x be Element of L holds (f . x) = (( waybelow x) /\ B) and

         A5: for x be Element of L holds (g . x) = (( waybelow x) /\ B);

         A6:

        now

          let z be object;

          assume z in the carrier of L;

          then

          reconsider z1 = z as Element of L;

          (f . z) = (( waybelow z1) /\ B) by A4;

          hence (f . z) = (g . z) by A5;

        end;

        

         A7: ( dom g) = the carrier of L by FUNCT_2:def 1;

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

        hence f = g by A7, A6, FUNCT_1: 2;

      end;

    end

    theorem :: WAYBEL23:51

    

     Th51: for L be non empty reflexive transitive RelStr holds for S be non empty full SubRelStr of L holds ( dom ( supMap S)) = ( Ids S) & ( rng ( supMap S)) is Subset of L

    proof

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      set P = ( InclPoset ( Ids S));

      

      thus ( dom ( supMap S)) = the carrier of P by FUNCT_2:def 1

      .= the carrier of RelStr (# ( Ids S), ( RelIncl ( Ids S)) #) by YELLOW_1:def 1

      .= ( Ids S);

      thus thesis;

    end;

    theorem :: WAYBEL23:52

    

     Th52: for L be non empty reflexive transitive RelStr holds for S be non empty full SubRelStr of L holds for x be set holds x in ( dom ( supMap S)) iff x is Ideal of S

    proof

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      let x be set;

      hereby

        assume x in ( dom ( supMap S));

        then x in ( Ids S) by Th51;

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

        then ex I be Ideal of S st x = I;

        hence x is Ideal of S;

      end;

      assume x is Ideal of S;

      then x in the set of all X where X be Ideal of S;

      then x in ( Ids S) by WAYBEL_0:def 23;

      hence thesis by Th51;

    end;

    theorem :: WAYBEL23:53

    

     Th53: for L be non empty reflexive transitive RelStr holds for S be non empty full SubRelStr of L holds ( dom ( idsMap S)) = ( Ids S) & ( rng ( idsMap S)) is Subset of ( Ids L)

    proof

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      set P = ( InclPoset ( Ids S));

      

      thus ( dom ( idsMap S)) = the carrier of P by FUNCT_2:def 1

      .= the carrier of RelStr (# ( Ids S), ( RelIncl ( Ids S)) #) by YELLOW_1:def 1

      .= ( Ids S);

      thus thesis by YELLOW_1: 1;

    end;

    theorem :: WAYBEL23:54

    

     Th54: for L be non empty reflexive transitive RelStr holds for S be non empty full SubRelStr of L holds for x be set holds x in ( dom ( idsMap S)) iff x is Ideal of S

    proof

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      let x be set;

      hereby

        assume x in ( dom ( idsMap S));

        then x in ( Ids S) by Th53;

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

        then ex I be Ideal of S st x = I;

        hence x is Ideal of S;

      end;

      assume x is Ideal of S;

      then x in the set of all X where X be Ideal of S;

      then x in ( Ids S) by WAYBEL_0:def 23;

      hence thesis by Th53;

    end;

    theorem :: WAYBEL23:55

    

     Th55: for L be non empty reflexive transitive RelStr holds for S be non empty full SubRelStr of L holds for x be set holds x in ( rng ( idsMap S)) implies x is Ideal of L

    proof

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      let x be set;

      assume

       A1: x in ( rng ( idsMap S));

      ( rng ( idsMap S)) is Subset of ( Ids L) by Th53;

      then x in ( Ids L) by A1;

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

      then ex I be Ideal of L st x = I;

      hence thesis;

    end;

    theorem :: WAYBEL23:56

    for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( dom ( baseMap B)) = the carrier of L & ( rng ( baseMap B)) is Subset of ( Ids ( subrelstr B)) by FUNCT_2:def 1, YELLOW_1: 1;

    theorem :: WAYBEL23:57

    for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds for x be set holds x in ( rng ( baseMap B)) implies x is Ideal of ( subrelstr B)

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      let x be set;

      

       A1: ( rng ( baseMap B)) is Subset of ( Ids ( subrelstr B)) by YELLOW_1: 1;

      assume x in ( rng ( baseMap B));

      then x in ( Ids ( subrelstr B)) by A1;

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

      then ex I be Ideal of ( subrelstr B) st x = I;

      hence thesis;

    end;

    theorem :: WAYBEL23:58

    

     Th58: for L be up-complete non empty Poset holds for S be non empty full SubRelStr of L holds ( supMap S) is monotone

    proof

      let L be up-complete non empty Poset;

      let S be non empty full SubRelStr of L;

      set f = ( supMap S);

      now

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

        reconsider I = x, J = y as Ideal of S by YELLOW_2: 41;

        assume x <= y;

        then

         A1: I c= J by YELLOW_1: 3;

        I is non empty directed Subset of L by YELLOW_2: 7;

        then

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

        J is non empty directed Subset of L by YELLOW_2: 7;

        then

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

        

         A4: (f . y) = ( "\/" (J,L)) by Def10;

        (f . x) = ( "\/" (I,L)) by Def10;

        hence (f . x) <= (f . y) by A2, A3, A1, A4, YELLOW_0: 34;

      end;

      hence thesis by WAYBEL_1:def 2;

    end;

    theorem :: WAYBEL23:59

    

     Th59: for L be non empty reflexive transitive RelStr holds for S be non empty full SubRelStr of L holds ( idsMap S) is monotone

    proof

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      set f = ( idsMap S);

      now

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

        reconsider I = x, J = y as Ideal of S by YELLOW_2: 41;

        consider K1 be Subset of L such that

         A1: I = K1 and

         A2: (f . x) = ( downarrow K1) by Def11;

        consider K2 be Subset of L such that

         A3: J = K2 and

         A4: (f . y) = ( downarrow K2) by Def11;

        assume x <= y;

        then I c= J by YELLOW_1: 3;

        then ( downarrow K1) c= ( downarrow K2) by A1, A3, YELLOW_3: 6;

        hence (f . x) <= (f . y) by A2, A4, YELLOW_1: 3;

      end;

      hence thesis by WAYBEL_1:def 2;

    end;

    theorem :: WAYBEL23:60

    

     Th60: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( baseMap B) is monotone

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      set f = ( baseMap B);

      now

        let x,y be Element of L;

        assume

         A1: x <= y;

        

         A2: (f . y) = (( waybelow y) /\ B) by Def12;

        (f . x) = (( waybelow x) /\ B) by Def12;

        then (f . x) c= (f . y) by A1, A2, WAYBEL_3: 12, XBOOLE_1: 26;

        hence (f . x) <= (f . y) by YELLOW_1: 3;

      end;

      hence thesis by WAYBEL_1:def 2;

    end;

    registration

      let L be up-complete non empty Poset;

      let S be non empty full SubRelStr of L;

      cluster ( supMap S) -> monotone;

      coherence by Th58;

    end

    registration

      let L be non empty reflexive transitive RelStr;

      let S be non empty full SubRelStr of L;

      cluster ( idsMap S) -> monotone;

      coherence by Th59;

    end

    registration

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      cluster ( baseMap B) -> monotone;

      coherence by Th60;

    end

    theorem :: WAYBEL23:61

    

     Th61: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( idsMap ( subrelstr B)) is sups-preserving

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      set f = ( idsMap ( subrelstr B));

      

       A1: ( subrelstr B) is join-inheriting by Def2;

      

       A2: ( Bottom L) in B by Def8;

      then

       A3: ( Bottom L) in the carrier of ( subrelstr B) by YELLOW_0:def 15;

      now

        let X be Subset of ( InclPoset ( Ids ( subrelstr B)));

        reconsider supX = ( sup X) as Ideal of ( subrelstr B) by YELLOW_2: 41;

        reconsider unionX = ( union X) as Subset of L by WAYBEL13: 3;

        reconsider dfuX = ( downarrow ( finsups ( union X))) as Subset of L by WAYBEL13: 3;

        reconsider fuX = ( finsups ( union X)) as Subset of L by WAYBEL13: 3;

        

         A4: ex J be Subset of L st supX = J & (f . supX) = ( downarrow J) by Def11;

        now

          assume ex_sup_of (X,( InclPoset ( Ids ( subrelstr B))));

          thus ex_sup_of ((f .: X),( InclPoset ( Ids L))) by YELLOW_0: 17;

          

           A5: ( downarrow ( finsups ( union (f .: X)))) c= ( downarrow dfuX)

          proof

            defpred P[ object, object] means ex I be Element of ( InclPoset ( Ids ( subrelstr B))), z1,z2 be Element of L st z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2;

            let x be object;

            assume

             A6: x in ( downarrow ( finsups ( union (f .: X))));

            then

            reconsider x1 = x as Element of L;

            consider y1 be Element of L such that

             A7: y1 >= x1 and

             A8: y1 in ( finsups ( union (f .: X))) by A6, WAYBEL_0:def 15;

            y1 in { ( "\/" (V,L)) where V be finite Subset of ( union (f .: X)) : ex_sup_of (V,L) } by A8, WAYBEL_0:def 27;

            then

            consider Y be finite Subset of ( union (f .: X)) such that

             A9: y1 = ( "\/" (Y,L)) and ex_sup_of (Y,L);

            

             A10: for z be object st z in Y holds ex v be Element of B st P[z, v]

            proof

              let z be object;

              assume z in Y;

              then

              consider J be set such that

               A11: z in J and

               A12: J in (f .: X) by TARSKI:def 4;

              consider I be object such that I in ( dom f) and

               A13: I in X and

               A14: J = (f . I) by A12, FUNCT_1:def 6;

              reconsider I as Element of ( InclPoset ( Ids ( subrelstr B))) by A13;

              (f . I) is Element of ( InclPoset ( Ids L));

              then

              reconsider J as Element of ( InclPoset ( Ids L)) by A14;

              J is Ideal of L by YELLOW_2: 41;

              then

              reconsider z1 = z as Element of L by A11;

              reconsider I1 = I as Ideal of ( subrelstr B) by YELLOW_2: 41;

              consider I2 be Subset of L such that

               A15: I1 = I2 and

               A16: (f . I1) = ( downarrow I2) by Def11;

              consider z2 be Element of L such that

               A17: z2 >= z1 and

               A18: z2 in I2 by A11, A14, A16, WAYBEL_0:def 15;

              reconsider v = z2 as Element of B by A15, A18, YELLOW_0:def 15;

              take v, I, z1, z2;

              thus thesis by A13, A15, A17, A18;

            end;

            consider g be Function of Y, B such that

             A19: for z be object st z in Y holds P[z, (g . z)] from MONOID_1:sch 1( A10);

            reconsider Z = ( rng g) as finite Subset of ( subrelstr B) by YELLOW_0:def 15;

            

             A20: ( dom g) = Y by FUNCT_2:def 1;

            

             A21: ( "\/" (( rng g),L)) is_>=_than Y

            proof

              let a be Element of L;

              

               A22: ( "\/" (( rng g),L)) is_>=_than ( rng g) by YELLOW_0: 32;

              assume

               A23: a in Y;

              then

              consider I be Element of ( InclPoset ( Ids ( subrelstr B))), a1,a2 be Element of L such that

               A24: a1 = a and

               A25: a2 = (g . a) and I in X and (g . a) in I and

               A26: a1 <= a2 by A19;

              (g . a) in ( rng g) by A20, A23, FUNCT_1:def 3;

              then a2 <= ( "\/" (( rng g),L)) by A25, A22;

              hence a <= ( "\/" (( rng g),L)) by A24, A26, YELLOW_0:def 2;

            end;

            

             A27: ex_sup_of (Z,( subrelstr B))

            proof

              per cases ;

                suppose Z is non empty;

                hence thesis by YELLOW_0: 54;

              end;

                suppose Z is empty;

                hence thesis by YELLOW_0: 42;

              end;

            end;

            ( rng g) c= ( union X)

            proof

              let a be object;

              assume a in ( rng g);

              then

              consider b be object such that

               A28: b in ( dom g) and

               A29: a = (g . b) by FUNCT_1:def 3;

              ex I be Element of ( InclPoset ( Ids ( subrelstr B))), b1,b2 be Element of L st b1 = b & b2 = (g . b) & I in X & (g . b) in I & b1 <= b2 by A19, A28;

              hence thesis by A29, TARSKI:def 4;

            end;

            then ( "\/" (Z,( subrelstr B))) in { ( "\/" (V,( subrelstr B))) where V be finite Subset of ( union X) : ex_sup_of (V,( subrelstr B)) } by A27;

            then

             A30: ( "\/" (( rng g),( subrelstr B))) in ( finsups ( union X)) by WAYBEL_0:def 27;

            ( "\/" (Z,L)) in the carrier of ( subrelstr B)

            proof

              per cases ;

                suppose Z is non empty;

                hence thesis by A1, WAYBEL21: 15;

              end;

                suppose Z is empty;

                hence thesis by A2, YELLOW_0:def 15;

              end;

            end;

            then

            reconsider xl = ( "\/" (Z,L)) as Element of ( subrelstr B);

            reconsider srg = ( "\/" (( rng g),( subrelstr B))) as Element of L by YELLOW_0: 58;

            

             A31: ex_sup_of (Z,L) by YELLOW_0: 17;

             A32:

            now

              let b be Element of ( subrelstr B);

              reconsider b1 = b as Element of L by YELLOW_0: 58;

              assume

               A33: b is_>=_than Z;

              b1 is_>=_than Z by A33, YELLOW_0: 59;

              then ( "\/" (Z,L)) <= b1 by A31, YELLOW_0: 30;

              hence xl <= b by YELLOW_0: 60;

            end;

            

             A34: ( "\/" (Z,L)) is_>=_than Z by A31, YELLOW_0: 30;

            xl is_>=_than Z

            proof

              let b be Element of ( subrelstr B);

              reconsider b1 = b as Element of L by YELLOW_0: 58;

              assume b in Z;

              then b1 <= ( "\/" (Z,L)) by A34;

              hence b <= xl by YELLOW_0: 60;

            end;

            then ( "\/" (Z,( subrelstr B))) = ( "\/" (Z,L)) by A32, YELLOW_0: 30;

            then ( "\/" (Y,L)) <= srg by A21, YELLOW_0: 32;

            then

             A35: x1 <= srg by A7, A9, YELLOW_0:def 2;

            ( finsups ( union X)) c= ( downarrow ( finsups ( union X))) by WAYBEL_0: 16;

            hence thesis by A35, A30, WAYBEL_0:def 15;

          end;

          now

            let x be set;

            assume

             A36: x in X;

            then

            reconsider x1 = x as Ideal of ( subrelstr B) by YELLOW_2: 41;

            consider x2 be Subset of L such that

             A37: x1 = x2 and

             A38: (f . x1) = ( downarrow x2) by Def11;

            x in the carrier of ( InclPoset ( Ids ( subrelstr B))) by A36;

            then x1 in ( dom f) by FUNCT_2:def 1;

            then

             A39: (f . x1) in (f .: X) by A36, FUNCT_1:def 6;

            thus x c= ( union (f .: X))

            proof

              let y be object;

              assume

               A40: y in x;

              x c= ( downarrow x2) by A37, WAYBEL_0: 16;

              hence thesis by A38, A39, A40, TARSKI:def 4;

            end;

          end;

          then ( union X) c= ( union (f .: X)) by ZFMISC_1: 76;

          then

           A41: ( finsups unionX) c= ( finsups ( union (f .: X))) by Th2;

          ( finsups ( union X)) c= ( finsups unionX) by A3, A1, Th5;

          then ( finsups ( union X)) c= ( finsups ( union (f .: X))) by A41;

          then

           A42: ( downarrow fuX) c= ( downarrow ( finsups ( union (f .: X)))) by YELLOW_3: 6;

          ( downarrow ( finsups ( union X))) c= ( downarrow fuX) by Th11;

          then dfuX c= ( downarrow ( finsups ( union (f .: X)))) by A42;

          then ( downarrow dfuX) c= ( downarrow ( downarrow ( finsups ( union (f .: X))))) by YELLOW_3: 6;

          then

           A43: ( downarrow dfuX) c= ( downarrow ( finsups ( union (f .: X)))) by Th7;

          

          thus ( sup (f .: X)) = ( downarrow ( finsups ( union (f .: X)))) by Th6

          .= ( downarrow dfuX) by A5, A43

          .= (f . ( sup X)) by A4, Th6;

        end;

        hence f preserves_sup_of X by WAYBEL_0:def 31;

      end;

      hence thesis by WAYBEL_0:def 33;

    end;

    theorem :: WAYBEL23:62

    

     Th62: for L be up-complete non empty Poset holds for S be non empty full SubRelStr of L holds ( supMap S) = (( SupMap L) * ( idsMap S))

    proof

      let L be up-complete non empty Poset;

      let S be non empty full SubRelStr of L;

       A1:

      now

        let x be object;

        thus x in ( dom ( supMap S)) implies x in ( dom ( idsMap S)) & (( idsMap S) . x) in ( dom ( SupMap L))

        proof

          assume x in ( dom ( supMap S));

          then x is Ideal of S by Th52;

          hence x in ( dom ( idsMap S)) by Th54;

          then (( idsMap S) . x) in ( rng ( idsMap S)) by FUNCT_1:def 3;

          then (( idsMap S) . x) is Ideal of L by Th55;

          hence thesis by YELLOW_2: 50;

        end;

        thus x in ( dom ( idsMap S)) & (( idsMap S) . x) in ( dom ( SupMap L)) implies x in ( dom ( supMap S))

        proof

          assume that

           A2: x in ( dom ( idsMap S)) and (( idsMap S) . x) in ( dom ( SupMap L));

          x is Ideal of S by A2, Th54;

          hence thesis by Th52;

        end;

      end;

      now

        let x be object;

        assume x in ( dom ( supMap S));

        then

        reconsider I = x as Ideal of S by Th52;

        consider J be Subset of L such that

         A3: I = J and

         A4: (( idsMap S) . I) = ( downarrow J) by Def11;

        reconsider J as non empty directed Subset of L by A3, YELLOW_2: 7;

        

         A5: ex_sup_of (J,L) by WAYBEL_0: 75;

        

        thus (( supMap S) . x) = ( "\/" (I,L)) by Def10

        .= ( sup ( downarrow J)) by A3, A5, WAYBEL_0: 33

        .= (( SupMap L) . (( idsMap S) . x)) by A4, YELLOW_2:def 3;

      end;

      hence thesis by A1, FUNCT_1: 10;

    end;

    theorem :: WAYBEL23:63

    

     Th63: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds [( supMap ( subrelstr B)), ( baseMap B)] is Galois

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      now

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

        reconsider I = y as Ideal of ( subrelstr B) by YELLOW_2: 41;

        reconsider J = I as non empty directed Subset of L by YELLOW_2: 7;

        

         A1: ex_sup_of ((( waybelow x) /\ B),L) by YELLOW_0: 17;

        thus x <= (( supMap ( subrelstr B)) . y) implies (( baseMap B) . x) <= y

        proof

          

           A2: (( downarrow J) /\ B) c= J

          proof

            let z be object;

            assume

             A3: z in (( downarrow J) /\ B);

            then

            reconsider z1 = z as Element of L;

            z in B by A3, XBOOLE_0:def 4;

            then

            reconsider z2 = z as Element of ( subrelstr B) by YELLOW_0:def 15;

            z in ( downarrow J) by A3, XBOOLE_0:def 4;

            then

            consider v1 be Element of L such that

             A4: v1 >= z1 and

             A5: v1 in J by WAYBEL_0:def 15;

            reconsider v2 = v1 as Element of ( subrelstr B) by A5;

            z2 <= v2 by A4, YELLOW_0: 60;

            hence thesis by A5, WAYBEL_0:def 19;

          end;

          assume x <= (( supMap ( subrelstr B)) . y);

          then x <= ( "\/" (I,L)) by Def10;

          then

           A6: x <= ( sup ( downarrow J)) by WAYBEL_0: 33, YELLOW_0: 17;

          ( waybelow x) c= ( downarrow J)

          proof

            let z be object;

            assume

             A7: z in ( waybelow x);

            then

            reconsider z1 = z as Element of L;

            z1 << x by A7, WAYBEL_3: 7;

            hence thesis by A6, WAYBEL_3: 20;

          end;

          then (( waybelow x) /\ B) c= (( downarrow J) /\ B) by XBOOLE_1: 26;

          then (( waybelow x) /\ B) c= y by A2;

          then (( baseMap B) . x) c= y by Def12;

          hence thesis by YELLOW_1: 3;

        end;

        

         A8: ex_sup_of (J,L) by YELLOW_0: 17;

        thus (( baseMap B) . x) <= y implies x <= (( supMap ( subrelstr B)) . y)

        proof

          assume (( baseMap B) . x) <= y;

          then (( baseMap B) . x) c= y by YELLOW_1: 3;

          then (( waybelow x) /\ B) c= y by Def12;

          then ( sup (( waybelow x) /\ B)) <= ( sup J) by A8, A1, YELLOW_0: 34;

          then x <= ( "\/" (I,L)) by Def7;

          hence thesis by Def10;

        end;

      end;

      hence thesis by WAYBEL_1: 8;

    end;

    theorem :: WAYBEL23:64

    

     Th64: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( supMap ( subrelstr B)) is upper_adjoint & ( baseMap B) is lower_adjoint

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

       [( supMap ( subrelstr B)), ( baseMap B)] is Galois by Th63;

      hence thesis by WAYBEL_1: 9;

    end;

    theorem :: WAYBEL23:65

    

     Th65: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( rng ( supMap ( subrelstr B))) = the carrier of L

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      

       A1: ( Bottom L) in B by Def8;

      thus ( rng ( supMap ( subrelstr B))) = the carrier of L

      proof

        thus ( rng ( supMap ( subrelstr B))) c= the carrier of L;

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x1 = x as Element of L;

        set z = (( waybelow x1) /\ B);

        z is Subset of B by XBOOLE_1: 17;

        then

        reconsider z as Subset of ( subrelstr B) by YELLOW_0:def 15;

         A2:

        now

          let a,b be Element of ( subrelstr B);

          reconsider a1 = a, b1 = b as Element of L by YELLOW_0: 58;

          assume that

           A3: a in z and

           A4: b <= a;

          a in ( waybelow x1) by A3, XBOOLE_0:def 4;

          then

           A5: a1 << x1 by WAYBEL_3: 7;

          b1 <= a1 by A4, YELLOW_0: 59;

          then b1 << x1 by A5, WAYBEL_3: 2;

          then

           A6: b in ( waybelow x1) by WAYBEL_3: 7;

          b in the carrier of ( subrelstr B);

          then b in B by YELLOW_0:def 15;

          hence b in z by A6, XBOOLE_0:def 4;

        end;

        ( Bottom L) << x1 by WAYBEL_3: 4;

        then

         A7: ( Bottom L) in ( waybelow x1) by WAYBEL_3: 7;

        (( waybelow x1) /\ B) is join-closed by Th33;

        then

        reconsider z as Ideal of ( subrelstr B) by A1, A7, A2, WAYBEL10: 23, WAYBEL_0:def 19, XBOOLE_0:def 4;

        z in the set of all X where X be Ideal of ( subrelstr B);

        then z in ( Ids ( subrelstr B)) by WAYBEL_0:def 23;

        then

         A8: z in ( dom ( supMap ( subrelstr B))) by Th51;

        x = ( "\/" (z,L)) by Def7

        .= (( supMap ( subrelstr B)) . z) by Def10;

        hence thesis by A8, FUNCT_1:def 3;

      end;

    end;

    theorem :: WAYBEL23:66

    

     Th66: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( supMap ( subrelstr B)) is infs-preserving sups-preserving

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      

       A1: ( SupMap L) is sups-preserving by WAYBEL13: 33;

      thus ( supMap ( subrelstr B)) is infs-preserving by Th64, WAYBEL_1: 12;

      

       A2: ( supMap ( subrelstr B)) = (( SupMap L) * ( idsMap ( subrelstr B))) by Th62;

      ( idsMap ( subrelstr B)) is sups-preserving by Th61;

      hence thesis by A2, A1, WAYBEL20: 27;

    end;

    theorem :: WAYBEL23:67

    for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds ( baseMap B) is sups-preserving by Th64, WAYBEL_1: 13;

    registration

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      cluster ( supMap ( subrelstr B)) -> infs-preserving sups-preserving;

      coherence by Th66;

      cluster ( baseMap B) -> sups-preserving;

      coherence by Th64, WAYBEL_1: 13;

    end

    theorem :: WAYBEL23:68

    

     Th68: for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B)))) = the set of all ( downarrow b) where b be Element of ( subrelstr B)

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      thus the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B)))) c= the set of all ( downarrow b) where b be Element of ( subrelstr B)

      proof

        let x be object;

        assume

         A1: x in the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B))));

        the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B)))) c= the carrier of ( InclPoset ( Ids ( subrelstr B))) by YELLOW_0:def 13;

        then

        reconsider x1 = x as Element of ( InclPoset ( Ids ( subrelstr B))) by A1;

        x1 is compact by A1, WAYBEL_8:def 1;

        then ex b be Element of ( subrelstr B) st x1 = ( downarrow b) by WAYBEL13: 12;

        hence thesis;

      end;

      thus the set of all ( downarrow b) where b be Element of ( subrelstr B) c= the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B))))

      proof

        let x be object;

        assume x in the set of all ( downarrow b) where b be Element of ( subrelstr B);

        then

         A2: ex b be Element of ( subrelstr B) st x = ( downarrow b);

        then

        reconsider x1 = x as Element of ( InclPoset ( Ids ( subrelstr B))) by YELLOW_2: 41;

        x1 is compact by A2, WAYBEL13: 12;

        hence thesis by WAYBEL_8:def 1;

      end;

    end;

    theorem :: WAYBEL23:69

    for L be lower-bounded continuous sup-Semilattice holds for B be with_bottom CLbasis of L holds (( CompactSublatt ( InclPoset ( Ids ( subrelstr B)))),( subrelstr B)) are_isomorphic

    proof

      let L be lower-bounded continuous sup-Semilattice;

      let B be with_bottom CLbasis of L;

      deffunc F( Element of ( subrelstr B)) = ( downarrow $1);

      

       A1: for x be Element of ( subrelstr B) holds F(x) is Element of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B))))

      proof

        let x be Element of ( subrelstr B);

        ( downarrow x) in the set of all ( downarrow b) where b be Element of ( subrelstr B);

        hence thesis by Th68;

      end;

      consider f be Function of ( subrelstr B), ( CompactSublatt ( InclPoset ( Ids ( subrelstr B)))) such that

       A2: for x be Element of ( subrelstr B) holds (f . x) = F(x) from FUNCT_2:sch 9( A1);

      f is isomorphic by A2, WAYBEL13: 13;

      then (( subrelstr B),( CompactSublatt ( InclPoset ( Ids ( subrelstr B))))) are_isomorphic by WAYBEL_1:def 8;

      hence thesis by WAYBEL_1: 6;

    end;

    

     Lm4: for L be continuous lower-bounded LATTICE holds L is algebraic implies the carrier of ( CompactSublatt L) is with_bottom CLbasis of L & for B be with_bottom CLbasis of L holds the carrier of ( CompactSublatt L) c= B

    proof

      let L be continuous lower-bounded LATTICE;

      assume L is algebraic;

      hence the carrier of ( CompactSublatt L) is with_bottom CLbasis of L by Th44;

      let B be with_bottom CLbasis of L;

      ( Bottom L) in B by Def8;

      hence thesis by Th48;

    end;

    theorem :: WAYBEL23:70

    

     Th70: for L be continuous lower-bounded LATTICE holds for B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1 holds for J be Element of ( InclPoset ( Ids ( subrelstr B))) holds J = (( waybelow ( "\/" (J,L))) /\ B)

    proof

      let L be continuous lower-bounded LATTICE;

      let B be with_bottom CLbasis of L;

      assume

       A1: for B1 be with_bottom CLbasis of L holds B c= B1;

      let J be Element of ( InclPoset ( Ids ( subrelstr B)));

      reconsider J1 = J as Ideal of ( subrelstr B) by YELLOW_2: 41;

      reconsider J2 = J1 as non empty directed Subset of L by YELLOW_2: 7;

      set x = ( "\/" (J,L));

      set C = ((B \ J2) \/ (( waybelow x) /\ B));

      

       A2: (( waybelow x) /\ B) c= B by XBOOLE_1: 17;

      (B \ J2) c= B by XBOOLE_1: 36;

      then

       A3: C c= B by A2, XBOOLE_1: 8;

       A4:

      now

        let y be Element of L;

        per cases ;

          suppose not y <= x;

          then

          consider u be Element of L such that

           A5: u in B and

           A6: not u <= x and

           A7: u << y by Th46;

           A8:

          now

            let b be Element of L;

            assume

             A9: b is_>=_than (( waybelow y) /\ C);

            b is_>=_than (( waybelow y) /\ B)

            proof

              let c be Element of L;

              u <= (c "\/" u) by YELLOW_0: 22;

              then

               A10: not (c "\/" u) <= x by A6, YELLOW_0:def 2;

              assume

               A11: c in (( waybelow y) /\ B);

              then c in B by XBOOLE_0:def 4;

              then ( sup {c, u}) in B by A5, Th18;

              then

               A12: (c "\/" u) in B by YELLOW_0: 41;

              J is_<=_than x by YELLOW_0: 32;

              then not (c "\/" u) in J by A10;

              then (c "\/" u) in (B \ J) by A12, XBOOLE_0:def 5;

              then

               A13: (c "\/" u) in C by XBOOLE_0:def 3;

              c in ( waybelow y) by A11, XBOOLE_0:def 4;

              then c << y by WAYBEL_3: 7;

              then (c "\/" u) << y by A7, WAYBEL_3: 3;

              then (c "\/" u) in ( waybelow y) by WAYBEL_3: 7;

              then (c "\/" u) in (( waybelow y) /\ C) by A13, XBOOLE_0:def 4;

              then

               A14: (c "\/" u) <= b by A9;

              c <= (c "\/" u) by YELLOW_0: 22;

              hence c <= b by A14, YELLOW_0:def 2;

            end;

            hence ( sup (( waybelow y) /\ B)) <= b by YELLOW_0: 32;

          end;

          

           A15: (( waybelow y) /\ B) is_<=_than ( sup (( waybelow y) /\ B)) by YELLOW_0: 32;

          ( sup (( waybelow y) /\ B)) is_>=_than (( waybelow y) /\ C)

          proof

            let b be Element of L;

            assume

             A16: b in (( waybelow y) /\ C);

            then

             A17: b in C by XBOOLE_0:def 4;

            b in ( waybelow y) by A16, XBOOLE_0:def 4;

            then b in (( waybelow y) /\ B) by A3, A17, XBOOLE_0:def 4;

            hence b <= ( sup (( waybelow y) /\ B)) by A15;

          end;

          then ( sup (( waybelow y) /\ B)) = ( sup (( waybelow y) /\ C)) by A8, YELLOW_0: 32;

          hence y = ( sup (( waybelow y) /\ C)) by Def7;

        end;

          suppose

           A18: y <= x;

          

           A19: (( waybelow y) /\ B) c= (( waybelow y) /\ C)

          proof

            let a be object;

            assume

             A20: a in (( waybelow y) /\ B);

            then

            reconsider a1 = a as Element of L;

            

             A21: a in ( waybelow y) by A20, XBOOLE_0:def 4;

            then a1 << y by WAYBEL_3: 7;

            then a1 << x by A18, WAYBEL_3: 2;

            then

             A22: a1 in ( waybelow x) by WAYBEL_3: 7;

            a in B by A20, XBOOLE_0:def 4;

            then a in (( waybelow x) /\ B) by A22, XBOOLE_0:def 4;

            then a in C by XBOOLE_0:def 3;

            hence thesis by A21, XBOOLE_0:def 4;

          end;

          (( waybelow y) /\ C) c= (( waybelow y) /\ B) by A3, XBOOLE_1: 26;

          then (( waybelow y) /\ B) = (( waybelow y) /\ C) by A19;

          hence y = ( sup (( waybelow y) /\ C)) by Def7;

        end;

      end;

      

       A23: ( subrelstr B) is join-inheriting by Def2;

      ( subrelstr C) is join-inheriting

      proof

        let a,b be Element of L;

        assume that

         A24: a in the carrier of ( subrelstr C) and

         A25: b in the carrier of ( subrelstr C) and

         A26: ex_sup_of ( {a, b},L);

        

         A27: b in C by A25, YELLOW_0:def 15;

        

         A28: a in C by A24, YELLOW_0:def 15;

        then

         A29: ( sup {a, b}) in B by A3, A26, A27, Th16;

        reconsider a1 = a, b1 = b as Element of ( subrelstr B) by A3, A28, A27, YELLOW_0:def 15;

        

         A30: a1 <= (a1 "\/" b1) by YELLOW_0: 22;

        

         A31: b1 <= (a1 "\/" b1) by YELLOW_0: 22;

        now

          per cases by A28, A27, XBOOLE_0:def 3;

            suppose a in (B \ J) & b in (B \ J);

            then

             A32: not a in J by XBOOLE_0:def 5;

             not (a "\/" b) in J

            proof

              assume (a "\/" b) in J;

              then (a1 "\/" b1) in J1 by A23, YELLOW_0: 70;

              hence contradiction by A30, A32, WAYBEL_0:def 19;

            end;

            then not ( sup {a, b}) in J by YELLOW_0: 41;

            then ( sup {a, b}) in (B \ J) by A29, XBOOLE_0:def 5;

            hence ( sup {a, b}) in C by XBOOLE_0:def 3;

          end;

            suppose a in (B \ J) & b in (( waybelow x) /\ B);

            then

             A33: not a in J by XBOOLE_0:def 5;

             not (a "\/" b) in J

            proof

              assume (a "\/" b) in J;

              then (a1 "\/" b1) in J1 by A23, YELLOW_0: 70;

              hence contradiction by A30, A33, WAYBEL_0:def 19;

            end;

            then not ( sup {a, b}) in J by YELLOW_0: 41;

            then ( sup {a, b}) in (B \ J) by A29, XBOOLE_0:def 5;

            hence ( sup {a, b}) in C by XBOOLE_0:def 3;

          end;

            suppose a in (( waybelow x) /\ B) & b in (B \ J);

            then

             A34: not b in J by XBOOLE_0:def 5;

             not (a "\/" b) in J

            proof

              assume (a "\/" b) in J;

              then (a1 "\/" b1) in J1 by A23, YELLOW_0: 70;

              hence contradiction by A31, A34, WAYBEL_0:def 19;

            end;

            then not ( sup {a, b}) in J by YELLOW_0: 41;

            then ( sup {a, b}) in (B \ J) by A29, XBOOLE_0:def 5;

            hence ( sup {a, b}) in C by XBOOLE_0:def 3;

          end;

            suppose

             A35: a in (( waybelow x) /\ B) & b in (( waybelow x) /\ B);

            then b in ( waybelow x) by XBOOLE_0:def 4;

            then

             A36: b << x by WAYBEL_3: 7;

            a in ( waybelow x) by A35, XBOOLE_0:def 4;

            then a << x by WAYBEL_3: 7;

            then (a "\/" b) << x by A36, WAYBEL_3: 3;

            then (a "\/" b) in ( waybelow x) by WAYBEL_3: 7;

            then ( sup {a, b}) in ( waybelow x) by YELLOW_0: 41;

            then ( sup {a, b}) in (( waybelow x) /\ B) by A29, XBOOLE_0:def 4;

            hence ( sup {a, b}) in C by XBOOLE_0:def 3;

          end;

        end;

        hence thesis by YELLOW_0:def 15;

      end;

      then

       A37: C is join-closed;

      ( Bottom L) << x by WAYBEL_3: 4;

      then

       A38: ( Bottom L) in ( waybelow x) by WAYBEL_3: 7;

      reconsider C as CLbasis of L by A37, A4, Def7;

      ( Bottom L) in B by Def8;

      then ( Bottom L) in (( waybelow x) /\ B) by A38, XBOOLE_0:def 4;

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

      then C is with_bottom;

      then B c= C by A1;

      then

       A39: B = C by A3;

      

       A40: J c= (( waybelow x) /\ B)

      proof

        let a be object;

        assume

         A41: a in J;

        then a in J1;

        then a in the carrier of ( subrelstr B);

        then

         A42: a in C by A39, YELLOW_0:def 15;

         not a in (B \ J2) by A41, XBOOLE_0:def 5;

        hence thesis by A42, XBOOLE_0:def 3;

      end;

      (( waybelow x) /\ B) c= J

      proof

        let a be object;

        assume

         A43: a in (( waybelow x) /\ B);

        then

        reconsider a1 = a as Element of L;

        a in B by A43, XBOOLE_0:def 4;

        then

        reconsider a2 = a as Element of ( subrelstr B) by YELLOW_0:def 15;

        a in ( waybelow x) by A43, XBOOLE_0:def 4;

        then a1 << x by WAYBEL_3: 7;

        then

        consider d1 be Element of L such that

         A44: d1 in J2 and

         A45: a1 <= d1 by WAYBEL_3:def 1;

        reconsider d2 = d1 as Element of ( subrelstr B) by A44;

        a2 <= d2 by A45, YELLOW_0: 60;

        hence thesis by A44, WAYBEL_0:def 19;

      end;

      hence thesis by A40;

    end;

    

     Lm5: for L be continuous lower-bounded LATTICE holds (ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1) implies L is algebraic

    proof

      let L be continuous lower-bounded LATTICE;

      given B be with_bottom CLbasis of L such that

       A1: for B1 be with_bottom CLbasis of L holds B c= B1;

      

       A2: for x,y be Element of ( InclPoset ( Ids ( subrelstr B))) holds x <= y iff (( supMap ( subrelstr B)) . x) <= (( supMap ( subrelstr B)) . y)

      proof

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

        thus x <= y implies (( supMap ( subrelstr B)) . x) <= (( supMap ( subrelstr B)) . y) by WAYBEL_1:def 2;

        reconsider x1 = x, y1 = y as Ideal of ( subrelstr B) by YELLOW_2: 41;

        assume

         A3: (( supMap ( subrelstr B)) . x) <= (( supMap ( subrelstr B)) . y);

        

         A4: (( supMap ( subrelstr B)) . y1) = ( "\/" (y1,L)) by Def10;

        (( supMap ( subrelstr B)) . x1) = ( "\/" (x1,L)) by Def10;

        then ( waybelow ( "\/" (x1,L))) c= ( waybelow ( "\/" (y1,L))) by A4, A3, WAYBEL_3: 25;

        then

         A5: (( waybelow ( "\/" (x1,L))) /\ B) c= (( waybelow ( "\/" (y1,L))) /\ B) by XBOOLE_1: 26;

        

         A6: y = (( waybelow ( "\/" (y,L))) /\ B) by A1, Th70;

        x = (( waybelow ( "\/" (x,L))) /\ B) by A1, Th70;

        hence thesis by A6, A5, YELLOW_1: 3;

      end;

      the carrier of ( InclPoset ( Ids ( subrelstr B))) c= ( rng ( baseMap B))

      proof

        let J be object;

        reconsider JJ = J as set by TARSKI: 1;

        set x = ( "\/" (JJ,L));

        assume J in the carrier of ( InclPoset ( Ids ( subrelstr B)));

        then J = (( waybelow x) /\ B) by A1, Th70;

        then

         A7: J = (( baseMap B) . x) by Def12;

        ( dom ( baseMap B)) = the carrier of L by FUNCT_2:def 1;

        hence thesis by A7, FUNCT_1:def 3;

      end;

      then ( rng ( baseMap B)) = the carrier of ( InclPoset ( Ids ( subrelstr B)));

      then

       A8: ( baseMap B) is onto by FUNCT_2:def 3;

       [( supMap ( subrelstr B)), ( baseMap B)] is Galois by Th63;

      then

       A9: ( supMap ( subrelstr B)) is one-to-one by A8, WAYBEL_1: 27;

      ( rng ( supMap ( subrelstr B))) = the carrier of L by Th65;

      then ( supMap ( subrelstr B)) is isomorphic by A9, A2, WAYBEL_0: 66;

      then

       A10: (( InclPoset ( Ids ( subrelstr B))),L) are_isomorphic by WAYBEL_1:def 8;

      ( InclPoset ( Ids ( subrelstr B))) is lower-bounded algebraic by WAYBEL13: 10;

      hence thesis by A10, WAYBEL13: 32;

    end;

    theorem :: WAYBEL23:71

    for L be continuous lower-bounded LATTICE holds L is algebraic iff the carrier of ( CompactSublatt L) is with_bottom CLbasis of L & for B be with_bottom CLbasis of L holds the carrier of ( CompactSublatt L) c= B by Lm4, Lm5;

    theorem :: WAYBEL23:72

    for L be continuous lower-bounded LATTICE holds L is algebraic iff ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1

    proof

      let L be continuous lower-bounded LATTICE;

      thus L is algebraic implies ex B be with_bottom CLbasis of L st for B1 be with_bottom CLbasis of L holds B c= B1

      proof

        assume

         A1: L is algebraic;

        then

         A2: for B be with_bottom CLbasis of L holds the carrier of ( CompactSublatt L) c= B by Lm4;

        the carrier of ( CompactSublatt L) is with_bottom CLbasis of L by A1, Lm4;

        hence thesis by A2;

      end;

      thus thesis by Lm5;

    end;

    theorem :: WAYBEL23:73

    for T be TopStruct holds for b be Basis of T holds ( weight T) c= ( card b)

    proof

      let T be TopStruct;

      let b be Basis of T;

      ( card b) in the set of all ( card B1) where B1 be Basis of T;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: WAYBEL23:74

    for T be TopStruct holds ex b be Basis of T st ( card b) = ( weight T)

    proof

      let T be TopStruct;

      defpred P[ Ordinal] means $1 in the set of all ( card b) where b be Basis of T;

      set X = the set of all ( card b1) where b1 be Basis of T;

      

       A1: ex A be Ordinal st P[A]

      proof

        take ( card the topology of T);

        the topology of T is Basis of T by CANTOR_1: 2;

        hence thesis;

      end;

      consider A be Ordinal such that

       A2: P[A] and

       A3: for C be Ordinal st P[C] holds A c= C from ORDINAL1:sch 1( A1);

      consider b be Basis of T such that

       A4: A = ( card b) by A2;

       A5:

      now

        let x be object;

        thus (for y be set holds y in X implies x in y) implies x in A by A2;

        assume

         A6: x in A;

        let y be set;

        assume

         A7: y in X;

        then ex B2 be Basis of T st y = ( card B2);

        then

        reconsider y1 = y as Cardinal;

        A c= y1 by A3, A7;

        hence x in y by A6;

      end;

      take b;

      the topology of T is Basis of T by CANTOR_1: 2;

      then ( card the topology of T) in X;

      hence thesis by A4, A5, SETFAM_1:def 1;

    end;