waybel31.miz



    begin

    scheme :: WAYBEL31:sch1

    UparrowUnion { L1() -> RelStr , P[ set] } :

for S be Subset-Family of L1() st S = { X where X be Subset of L1() : P[X] } holds ( uparrow ( union S)) = ( union { ( uparrow X) where X be Subset of L1() : P[X] });

      let S be Subset-Family of L1();

      assume

       A1: S = { X where X be Subset of L1() : P[X] };

      

       A2: ( union { ( uparrow X) where X be Subset of L1() : P[X] }) c= ( uparrow ( union S))

      proof

        let z be object;

        assume z in ( union { ( uparrow X) where X be Subset of L1() : P[X] });

        then

        consider Z be set such that

         A3: z in Z and

         A4: Z in { ( uparrow X) where X be Subset of L1() : P[X] } by TARSKI:def 4;

        consider X1 be Subset of L1() such that

         A5: Z = ( uparrow X1) and

         A6: P[X1] by A4;

        reconsider z1 = z as Element of L1() by A3, A5;

        consider y1 be Element of L1() such that

         A7: y1 <= z1 and

         A8: y1 in X1 by A3, A5, WAYBEL_0:def 16;

        X1 in S by A1, A6;

        then y1 in ( union S) by A8, TARSKI:def 4;

        hence thesis by A7, WAYBEL_0:def 16;

      end;

      ( uparrow ( union S)) c= ( union { ( uparrow X) where X be Subset of L1() : P[X] })

      proof

        let z be object;

        assume

         A9: z in ( uparrow ( union S));

        then

        reconsider z1 = z as Element of L1();

        consider y1 be Element of L1() such that

         A10: y1 <= z1 and

         A11: y1 in ( union S) by A9, WAYBEL_0:def 16;

        consider Z be set such that

         A12: y1 in Z and

         A13: Z in S by A11, TARSKI:def 4;

        consider X1 be Subset of L1() such that

         A14: Z = X1 and

         A15: P[X1] by A1, A13;

        

         A16: ( uparrow X1) in { ( uparrow X) where X be Subset of L1() : P[X] } by A15;

        z in ( uparrow X1) by A10, A12, A14, WAYBEL_0:def 16;

        hence thesis by A16, TARSKI:def 4;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    scheme :: WAYBEL31:sch2

    DownarrowUnion { L1() -> RelStr , P[ set] } :

for S be Subset-Family of L1() st S = { X where X be Subset of L1() : P[X] } holds ( downarrow ( union S)) = ( union { ( downarrow X) where X be Subset of L1() : P[X] });

      let S be Subset-Family of L1();

      assume

       A1: S = { X where X be Subset of L1() : P[X] };

      

       A2: ( union { ( downarrow X) where X be Subset of L1() : P[X] }) c= ( downarrow ( union S))

      proof

        let z be object;

        assume z in ( union { ( downarrow X) where X be Subset of L1() : P[X] });

        then

        consider Z be set such that

         A3: z in Z and

         A4: Z in { ( downarrow X) where X be Subset of L1() : P[X] } by TARSKI:def 4;

        consider X1 be Subset of L1() such that

         A5: Z = ( downarrow X1) and

         A6: P[X1] by A4;

        reconsider z1 = z as Element of L1() by A3, A5;

        consider y1 be Element of L1() such that

         A7: y1 >= z1 and

         A8: y1 in X1 by A3, A5, WAYBEL_0:def 15;

        X1 in S by A1, A6;

        then y1 in ( union S) by A8, TARSKI:def 4;

        hence thesis by A7, WAYBEL_0:def 15;

      end;

      ( downarrow ( union S)) c= ( union { ( downarrow X) where X be Subset of L1() : P[X] })

      proof

        let z be object;

        assume

         A9: z in ( downarrow ( union S));

        then

        reconsider z1 = z as Element of L1();

        consider y1 be Element of L1() such that

         A10: y1 >= z1 and

         A11: y1 in ( union S) by A9, WAYBEL_0:def 15;

        consider Z be set such that

         A12: y1 in Z and

         A13: Z in S by A11, TARSKI:def 4;

        consider X1 be Subset of L1() such that

         A14: Z = X1 and

         A15: P[X1] by A1, A13;

        

         A16: ( downarrow X1) in { ( downarrow X) where X be Subset of L1() : P[X] } by A15;

        z in ( downarrow X1) by A10, A12, A14, WAYBEL_0:def 15;

        hence thesis by A16, TARSKI:def 4;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    registration

      let L1 be lower-bounded continuous sup-Semilattice;

      let B1 be with_bottom CLbasis of L1;

      cluster ( InclPoset ( Ids ( subrelstr B1))) -> algebraic;

      coherence by WAYBEL13: 10;

    end

    definition

      let L1 be continuous sup-Semilattice;

      :: WAYBEL31:def1

      func CLweight L1 -> Cardinal equals ( meet the set of all ( card B1) where B1 be with_bottom CLbasis of L1);

      coherence

      proof

        set X = the set of all ( card B2) where B2 be with_bottom CLbasis of L1;

        defpred P[ Ordinal] means $1 in the set of all ( card B1) where B1 be with_bottom CLbasis of L1;

        

         A1: ex A be Ordinal st P[A]

        proof

          take ( card ( [#] L1));

          ( [#] L1) is CLbasis of L1 by YELLOW15: 25;

          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 B1 be with_bottom CLbasis of L1 st A = ( card B1) 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 B2 be with_bottom CLbasis of L1 st y = ( card B2);

          then

          reconsider y1 = y as Cardinal;

          A c= y1 by A3, A6;

          hence x in y by A5;

        end;

        ( [#] L1) is CLbasis of L1 by YELLOW15: 25;

        then ( card ( [#] L1)) in X;

        hence thesis by A4, SETFAM_1:def 1;

      end;

    end

    theorem :: WAYBEL31:1

    

     Th1: for L1 be continuous sup-Semilattice holds for B1 be with_bottom CLbasis of L1 holds ( CLweight L1) c= ( card B1)

    proof

      let L1 be continuous sup-Semilattice;

      let B1 be with_bottom CLbasis of L1;

      ( card B1) in the set of all ( card B2) where B2 be with_bottom CLbasis of L1;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: WAYBEL31:2

    

     Th2: for L1 be continuous sup-Semilattice holds ex B1 be with_bottom CLbasis of L1 st ( card B1) = ( CLweight L1)

    proof

      let L1 be continuous sup-Semilattice;

      defpred P[ Ordinal] means $1 in the set of all ( card B1) where B1 be with_bottom CLbasis of L1;

      set X = the set of all ( card B2) where B2 be with_bottom CLbasis of L1;

      

       A1: ex A be Ordinal st P[A]

      proof

        take ( card ( [#] L1));

        ( [#] L1) is CLbasis of L1 by YELLOW15: 25;

        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 B1 be with_bottom CLbasis of L1 such that

       A4: A = ( card B1) 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 with_bottom CLbasis of L1 st y = ( card B2);

        then

        reconsider y1 = y as Cardinal;

        A c= y1 by A3, A7;

        hence x in y by A6;

      end;

      take B1;

      ( [#] L1) is CLbasis of L1 by YELLOW15: 25;

      then ( card ( [#] L1)) in X;

      hence thesis by A4, A5, SETFAM_1:def 1;

    end;

    theorem :: WAYBEL31:3

    

     Th3: for L1 be algebraic lower-bounded LATTICE holds ( CLweight L1) = ( card the carrier of ( CompactSublatt L1))

    proof

      let L1 be algebraic lower-bounded LATTICE;

      set CB = the set of all ( card B1) where B1 be with_bottom CLbasis of L1;

      the carrier of ( CompactSublatt L1) is with_bottom CLbasis of L1 by WAYBEL23: 71;

      then

       A1: ( card the carrier of ( CompactSublatt L1)) in CB;

      then

       A2: ( meet CB) c= ( card the carrier of ( CompactSublatt L1)) by SETFAM_1: 3;

      now

        let X be set;

        assume X in CB;

        then

        consider B1 be with_bottom CLbasis of L1 such that

         A3: X = ( card B1);

        the carrier of ( CompactSublatt L1) c= B1 by WAYBEL23: 71;

        hence ( card the carrier of ( CompactSublatt L1)) c= X by A3, CARD_1: 11;

      end;

      then ( card the carrier of ( CompactSublatt L1)) c= ( meet CB) by A1, SETFAM_1: 5;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL31:4

    

     Th4: for T be non empty TopSpace holds for L1 be continuous sup-Semilattice st ( InclPoset the topology of T) = L1 holds for B1 be with_bottom CLbasis of L1 holds B1 is Basis of T

    proof

      let T be non empty TopSpace;

      let L1 be continuous sup-Semilattice;

      assume

       A1: ( InclPoset the topology of T) = L1;

      let B1 be with_bottom CLbasis of L1;

      B1 c= the carrier of L1;

      then B1 c= the topology of T by A1, YELLOW_1: 1;

      then

      reconsider B2 = B1 as Subset-Family of T by XBOOLE_1: 1;

      

       A2: for A be Subset of T st A is open holds for p be Point of T st p in A holds ex a be Subset of T st a in B2 & p in a & a c= A

      proof

        let A be Subset of T;

        assume A is open;

        then A in the topology of T by PRE_TOPC:def 2;

        then

        reconsider A1 = A as Element of L1 by A1, YELLOW_1: 1;

        let p be Point of T;

        assume

         A3: p in A;

        A1 = ( sup (( waybelow A1) /\ B1)) by WAYBEL23:def 7

        .= ( union (( waybelow A1) /\ B1)) by A1, YELLOW_1: 22;

        then

        consider a be set such that

         A4: p in a and

         A5: a in (( waybelow A1) /\ B1) by A3, TARSKI:def 4;

        a in the carrier of L1 by A5;

        then a in the topology of T by A1, YELLOW_1: 1;

        then

        reconsider a as Subset of T;

        take a;

        thus a in B2 by A5, XBOOLE_0:def 4;

        thus p in a by A4;

        reconsider a1 = a as Element of L1 by A5;

        a1 in ( waybelow A1) by A5, XBOOLE_0:def 4;

        then a1 << A1 by WAYBEL_3: 7;

        then a1 <= A1 by WAYBEL_3: 1;

        hence thesis by A1, YELLOW_1: 3;

      end;

      B2 c= the topology of T

      proof

        let x be object;

        assume x in B2;

        then

        reconsider x1 = x as Element of L1;

        x1 in the carrier of L1;

        hence thesis by A1, YELLOW_1: 1;

      end;

      hence thesis by A2, YELLOW_9: 32;

    end;

    theorem :: WAYBEL31:5

    

     Th5: for T be non empty TopSpace holds for L1 be continuous lower-bounded LATTICE st ( InclPoset the topology of T) = L1 holds for B1 be Basis of T holds for B2 be Subset of L1 st B1 = B2 holds ( finsups B2) is with_bottom CLbasis of L1

    proof

      let T be non empty TopSpace;

      let L1 be continuous lower-bounded LATTICE;

      assume

       A1: ( InclPoset the topology of T) = L1;

      let B1 be Basis of T;

      let B2 be Subset of L1;

      assume

       A2: B1 = B2;

      

       A3: for x,y be Element of L1 st not y <= x holds ex b be Element of L1 st b in ( finsups B2) & not b <= x & b <= y

      proof

        let x,y be Element of L1;

        y in the carrier of L1;

        then

         A4: y in the topology of T by A1, YELLOW_1: 1;

        then

        reconsider y1 = y as Subset of T;

        assume not y <= x;

        then not y c= x by A1, YELLOW_1: 3;

        then

        consider v be object such that

         A5: v in y and

         A6: not v in x;

        v in y1 by A5;

        then

        reconsider v as Point of T;

        y1 is open by A4, PRE_TOPC:def 2;

        then

        consider b be Subset of T such that

         A7: b in B1 and

         A8: v in b and

         A9: b c= y1 by A5, YELLOW_9: 31;

        reconsider b as Element of L1 by A2, A7;

        for z be object st z in {b} holds z in B2 by A2, A7, TARSKI:def 1;

        then

         A10: {b} is finite Subset of B2 by TARSKI:def 3;

        take b;

         ex_sup_of ( {b},L1) & b = ( "\/" ( {b},L1)) by YELLOW_0: 38, YELLOW_0: 39;

        then b in { ( "\/" (Y,L1)) where Y be finite Subset of B2 : ex_sup_of (Y,L1) } by A10;

        hence b in ( finsups B2) by WAYBEL_0:def 27;

         not b c= x by A6, A8;

        hence not b <= x by A1, YELLOW_1: 3;

        thus thesis by A1, A9, YELLOW_1: 3;

      end;

      now

        let x,y be Element of L1;

        assume that

         A11: x in ( finsups B2) and

         A12: y in ( finsups B2);

        y in { ( "\/" (Y,L1)) where Y be finite Subset of B2 : ex_sup_of (Y,L1) } by A12, WAYBEL_0:def 27;

        then

        consider Y2 be finite Subset of B2 such that

         A13: y = ( "\/" (Y2,L1)) and

         A14: ex_sup_of (Y2,L1);

        x in { ( "\/" (Y,L1)) where Y be finite Subset of B2 : ex_sup_of (Y,L1) } by A11, WAYBEL_0:def 27;

        then

        consider Y1 be finite Subset of B2 such that

         A15: x = ( "\/" (Y1,L1)) and

         A16: ex_sup_of (Y1,L1);

         ex_sup_of ((Y1 \/ Y2),L1) & ( "\/" ((Y1 \/ Y2),L1)) = (( "\/" (Y1,L1)) "\/" ( "\/" (Y2,L1))) by A16, A14, YELLOW_2: 3;

        then (x "\/" y) in { ( "\/" (Y,L1)) where Y be finite Subset of B2 : ex_sup_of (Y,L1) } by A15, A13;

        then (x "\/" y) in ( finsups B2) by WAYBEL_0:def 27;

        hence ( sup {x, y}) in ( finsups B2) by YELLOW_0: 41;

      end;

      then

       A17: ( finsups B2) is join-closed by WAYBEL23: 18;

       {} c= B2 & ex_sup_of ( {} ,L1) by YELLOW_0: 42;

      then ( "\/" ( {} ,L1)) in { ( "\/" (Y,L1)) where Y be finite Subset of B2 : ex_sup_of (Y,L1) };

      then ( Bottom L1) in ( finsups B2) by WAYBEL_0:def 27;

      hence thesis by A17, A3, WAYBEL23: 49, WAYBEL23:def 8;

    end;

    theorem :: WAYBEL31:6

    

     Th6: for T be T_0 non empty TopSpace holds for L1 be continuous lower-bounded sup-Semilattice st ( InclPoset the topology of T) = L1 holds T is infinite implies ( weight T) = ( CLweight L1)

    proof

      let T be T_0 non empty TopSpace;

      let L1 be continuous lower-bounded sup-Semilattice;

      assume that

       A1: ( InclPoset the topology of T) = L1 and

       A2: T is infinite;

      

       A3: the set of all ( card B1) where B1 be Basis of T c= the set of all ( card B1) where B1 be with_bottom CLbasis of L1

      proof

        let b be object;

        assume b in the set of all ( card B1) where B1 be Basis of T;

        then

        consider B2 be Basis of T such that

         A4: b = ( card B2);

        B2 c= the topology of T by TOPS_2: 64;

        then

        reconsider B3 = B2 as Subset of L1 by A1, YELLOW_1: 1;

        B2 is infinite by A2, YELLOW15: 30;

        then

         A5: ( card B2) = ( card ( finsups B3)) by YELLOW15: 27;

        ( finsups B3) is with_bottom CLbasis of L1 by A1, Th5;

        hence thesis by A4, A5;

      end;

       the set of all ( card B1) where B1 be with_bottom CLbasis of L1 c= the set of all ( card B1) where B1 be Basis of T

      proof

        let b be object;

        assume b in the set of all ( card B1) where B1 be with_bottom CLbasis of L1;

        then

        consider B2 be with_bottom CLbasis of L1 such that

         A6: b = ( card B2);

        B2 is Basis of T by A1, Th4;

        hence thesis by A6;

      end;

      then the set of all ( card B1) where B1 be Basis of T = the set of all ( card B1) where B1 be with_bottom CLbasis of L1 by A3, XBOOLE_0:def 10;

      hence thesis by WAYBEL23:def 5;

    end;

    theorem :: WAYBEL31:7

    

     Th7: for T be T_0 non empty TopSpace holds for L1 be continuous sup-Semilattice st ( InclPoset the topology of T) = L1 holds ( card the carrier of T) c= ( card the carrier of L1)

    proof

      let T be T_0 non empty TopSpace;

      let L1 be continuous sup-Semilattice;

      

       A1: ( card the carrier of T) c= ( card the topology of T) by YELLOW15: 28;

      assume ( InclPoset the topology of T) = L1;

      hence thesis by A1, YELLOW_1: 1;

    end;

    theorem :: WAYBEL31:8

    

     Th8: for T be T_0 non empty TopSpace st T is finite holds ( weight T) = ( card the carrier of T)

    proof

      let T be T_0 non empty TopSpace;

      deffunc F( object) = ( meet { A where A be Element of the topology of T : $1 in A });

      

       A1: for x be object st x in the carrier of T holds F(x) in the carrier of ( BoolePoset the carrier of T)

      proof

        let x be object;

        assume

         A2: x in the carrier of T;

        the carrier of T in the topology of T by PRE_TOPC:def 1;

        then the carrier of T in { A where A be Element of the topology of T : x in A } by A2;

        then ( meet { A where A be Element of the topology of T : x in A }) c= the carrier of T by SETFAM_1: 3;

        then ( meet { A where A be Element of the topology of T : x in A }) in ( bool the carrier of T);

        hence thesis by WAYBEL_7: 2;

      end;

      consider f be Function of the carrier of T, the carrier of ( BoolePoset the carrier of T) such that

       A3: for x be object st x in the carrier of T holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

      reconsider rf = ( rng f) as Subset-Family of T by WAYBEL_7: 2;

      

       A4: for A be Subset of T st A is open holds for p be Point of T st p in A holds ex a be Subset of T st a in rf & p in a & a c= A

      proof

        let A be Subset of T;

        assume A is open;

        then

         A5: A in the topology of T by PRE_TOPC:def 2;

        let p be Point of T;

        assume p in A;

        then

         A6: A in { C where C be Element of the topology of T : p in C } by A5;

        ( meet { C where C be Element of the topology of T : p in C }) c= the carrier of T

        proof

          let z be object;

          assume z in ( meet { C where C be Element of the topology of T : p in C });

          then z in A by A6, SETFAM_1:def 1;

          hence thesis;

        end;

        then

        reconsider a = ( meet { C where C be Element of the topology of T : p in C }) as Subset of T;

        take a;

        p in the carrier of T;

        then

         A7: p in ( dom f) by FUNCT_2:def 1;

        a = (f . p) by A3;

        hence a in rf by A7, FUNCT_1:def 3;

        now

          let Y be set;

          assume Y in { C where C be Element of the topology of T : p in C };

          then ex C be Element of the topology of T st Y = C & p in C;

          hence p in Y;

        end;

        hence p in a by A6, SETFAM_1:def 1;

        thus a c= A by A6, SETFAM_1:def 1;

      end;

      assume

       A8: T is finite;

      rf c= the topology of T

      proof

        reconsider tT = the topology of T as finite non empty set by A8;

        let z be object;

        deffunc F( set) = $1;

        assume z in rf;

        then

        consider y be object such that

         A9: y in ( dom f) & z = (f . y) by FUNCT_1:def 3;

        { A where A be Element of the topology of T : y in A } c= ( bool the carrier of T)

        proof

          let z be object;

          assume z in { A where A be Element of the topology of T : y in A };

          then ex A be Element of the topology of T st z = A & y in A;

          hence thesis;

        end;

        then

        reconsider sfA = { A where A be Element of the topology of T : y in A } as Subset-Family of T;

        defpred P[ set] means y in $1;

        reconsider sfA as Subset-Family of T;

        now

          let P be Subset of T;

          assume P in sfA;

          then ex A be Element of the topology of T st P = A & y in A;

          hence P is open by PRE_TOPC:def 2;

        end;

        then

         A10: sfA is open by TOPS_2:def 1;

        { F(A) where A be Element of tT : P[A] } is finite from PRE_CIRC:sch 1;

        then

         A11: ( meet sfA) is open by A10, TOPS_2: 20;

        z = ( meet { A where A be Element of the topology of T : y in A }) by A3, A9;

        hence thesis by A11, PRE_TOPC:def 2;

      end;

      then ( rng f) is Basis of T by A4, YELLOW_9: 32;

      then

       A12: ( card ( rng f)) in the set of all ( card B1) where B1 be Basis of T;

      then

       A13: ( meet the set of all ( card B1) where B1 be Basis of T) c= ( card ( rng f)) by SETFAM_1: 3;

      now

        let x1,x2 be object;

        assume that

         A14: x1 in ( dom f) & x2 in ( dom f) and

         A15: (f . x1) = (f . x2);

        reconsider x3 = x1, x4 = x2 as Point of T by A14;

        assume x1 <> x2;

        then

        consider V be Subset of T such that

         A16: V is open and

         A17: x3 in V & not x4 in V or x4 in V & not x3 in V by T_0TOPSP:def 7;

        

         A18: (f . x3) = ( meet { A where A be Element of the topology of T : x3 in A }) & (f . x4) = ( meet { A where A be Element of the topology of T : x4 in A }) by A3;

        now

          per cases by A17;

            suppose

             A19: x3 in V & not x4 in V;

            V in the topology of T by A16, PRE_TOPC:def 2;

            then

             A20: V in { A where A be Element of the topology of T : x3 in A } by A19;

            

             A21: ( meet { A where A be Element of the topology of T : x3 in A }) c= V by A20, SETFAM_1:def 1;

             A22:

            now

              let Y be set;

              assume Y in { A where A be Element of the topology of T : x4 in A };

              then ex A be Element of the topology of T st Y = A & x4 in A;

              hence x4 in Y;

            end;

            the carrier of T in the topology of T by PRE_TOPC:def 1;

            then the carrier of T in { A where A be Element of the topology of T : x4 in A };

            then x4 in ( meet { A where A be Element of the topology of T : x3 in A }) by A15, A18, A22, SETFAM_1:def 1;

            hence contradiction by A19, A21;

          end;

            suppose

             A23: x4 in V & not x3 in V;

            V in the topology of T by A16, PRE_TOPC:def 2;

            then

             A24: V in { A where A be Element of the topology of T : x4 in A } by A23;

            

             A25: ( meet { A where A be Element of the topology of T : x4 in A }) c= V by A24, SETFAM_1:def 1;

             A26:

            now

              let Y be set;

              assume Y in { A where A be Element of the topology of T : x3 in A };

              then ex A be Element of the topology of T st Y = A & x3 in A;

              hence x3 in Y;

            end;

            the carrier of T in the topology of T by PRE_TOPC:def 1;

            then the carrier of T in { A where A be Element of the topology of T : x3 in A };

            then x3 in ( meet { A where A be Element of the topology of T : x4 in A }) by A15, A18, A26, SETFAM_1:def 1;

            hence contradiction by A23, A25;

          end;

        end;

        hence contradiction;

      end;

      then ( dom f) = the carrier of T & f is one-to-one by FUNCT_1:def 4, FUNCT_2:def 1;

      then

       A27: (the carrier of T,( rng f)) are_equipotent by WELLORD2:def 4;

      for X be set st X in the set of all ( card B1) where B1 be Basis of T holds ( card ( rng f)) c= X

      proof

        let X be set;

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

        then

        consider B2 be Basis of T such that

         A28: X = ( card B2);

        ( rng f) c= B2

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A29: x in ( dom f) and

           A30: y = (f . x) by FUNCT_1:def 3;

          reconsider x1 = x as Element of T by A29;

          y = ( meet { A where A be Element of the topology of T : x1 in A }) by A3, A30;

          hence thesis by A8, YELLOW15: 31;

        end;

        hence thesis by A28, CARD_1: 11;

      end;

      then ( card ( rng f)) c= ( meet the set of all ( card B1) where B1 be Basis of T) by A12, SETFAM_1: 5;

      

      then ( card ( rng f)) = ( meet the set of all ( card B1) where B1 be Basis of T) by A13, XBOOLE_0:def 10

      .= ( weight T) by WAYBEL23:def 5;

      hence thesis by A27, CARD_1: 5;

    end;

    theorem :: WAYBEL31:9

    

     Th9: for T be TopStruct holds for L1 be continuous lower-bounded LATTICE st ( InclPoset the topology of T) = L1 & T is finite holds ( CLweight L1) = ( card the carrier of L1)

    proof

      let T be TopStruct;

      let L1 be continuous lower-bounded LATTICE;

      assume

       A1: ( InclPoset the topology of T) = L1;

      ( [#] L1) is with_bottom CLbasis of L1 by YELLOW15: 25;

      then

       A2: ( card the carrier of L1) in the set of all ( card B1) where B1 be with_bottom CLbasis of L1;

      

       A3: ( CLweight L1) c= ( card the carrier of L1) by A2, SETFAM_1:def 1;

      assume

       A4: T is finite;

      now

        let Z be set;

        assume Z in the set of all ( card B1) where B1 be with_bottom CLbasis of L1;

        then

        consider B1 be with_bottom CLbasis of L1 such that

         A5: Z = ( card B1);

        ( Bottom L1) in B1 by WAYBEL23:def 8;

        then the carrier of ( CompactSublatt L1) c= B1 by WAYBEL23: 48;

        then

         A6: ( card the carrier of ( CompactSublatt L1)) c= ( card B1) by CARD_1: 11;

        L1 is finite by A1, A4, YELLOW_1: 1;

        hence ( card the carrier of L1) c= Z by A5, A6, YELLOW15: 26;

      end;

      then ( card the carrier of L1) c= ( meet the set of all ( card B1) where B1 be with_bottom CLbasis of L1) by A2, SETFAM_1: 5;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL31:10

    

     Th10: for L1 be continuous lower-bounded sup-Semilattice holds for T1 be Scott TopAugmentation of L1 holds for T2 be Lawson correct TopAugmentation of L1 holds for B2 be Basis of T2 holds { ( uparrow V) where V be Subset of T2 : V in B2 } is Basis of T1

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T1 be Scott TopAugmentation of L1;

      let T2 be Lawson correct TopAugmentation of L1;

      let B2 be Basis of T2;

      

       A1: the RelStr of T1 = the RelStr of L1 & the RelStr of T2 = the RelStr of L1 by YELLOW_9:def 4;

      { ( uparrow V) where V be Subset of T2 : V in B2 } c= ( bool the carrier of T1)

      proof

        let z be object;

        assume z in { ( uparrow V) where V be Subset of T2 : V in B2 };

        then ex V be Subset of T2 st z = ( uparrow V) & V in B2;

        hence thesis by A1;

      end;

      then

      reconsider upV = { ( uparrow V) where V be Subset of T2 : V in B2 } as Subset-Family of T1;

      reconsider upV as Subset-Family of T1;

      

       A2: the topology of T1 c= ( UniCl upV)

      proof

        let z be object;

        assume

         A3: z in the topology of T1;

        then

        reconsider z2 = z as Subset of T1;

        z2 is open by A3, PRE_TOPC:def 2;

        then z2 is upper by WAYBEL11:def 4;

        then

         A4: ( uparrow z2) c= z2 by WAYBEL_0: 24;

        reconsider z1 = z as Subset of T2 by A1, A3;

        z in ( sigma T1) by A3, WAYBEL14: 23;

        then ( sigma T2) c= ( lambda T2) & z in ( sigma T2) by A1, WAYBEL30: 10, YELLOW_9: 52;

        then z in ( lambda T2);

        then z in the topology of T2 by WAYBEL30: 9;

        then

         A5: z1 is open by PRE_TOPC:def 2;

        { ( uparrow G) where G be Subset of T2 : G in B2 & G c= z1 } c= ( bool the carrier of T1)

        proof

          let v be object;

          assume v in { ( uparrow G) where G be Subset of T2 : G in B2 & G c= z1 };

          then ex G be Subset of T2 st v = ( uparrow G) & G in B2 & G c= z1;

          hence thesis by A1;

        end;

        then

        reconsider Y = { ( uparrow G) where G be Subset of T2 : G in B2 & G c= z1 } as Subset-Family of T1;

        { G where G be Subset of T2 : G in B2 & G c= z1 } c= ( bool the carrier of T1)

        proof

          let v be object;

          assume v in { G where G be Subset of T2 : G in B2 & G c= z1 };

          then ex G be Subset of T2 st v = G & G in B2 & G c= z1;

          hence thesis by A1;

        end;

        then

        reconsider Y1 = { G where G be Subset of T2 : G in B2 & G c= z1 } as Subset-Family of T1;

        defpred P[ set] means $1 in B2 & $1 c= z1;

        reconsider Y as Subset-Family of T1;

        reconsider Y1 as Subset-Family of T1;

        reconsider Y3 = Y1 as Subset-Family of T2 by A1;

        

         A6: Y c= upV

        proof

          let v be object;

          assume v in Y;

          then ex G be Subset of T2 st v = ( uparrow G) & G in B2 & G c= z1;

          hence thesis;

        end;

        

         A7: for S be Subset-Family of T2 st S = { X where X be Subset of T2 : P[X] } holds ( uparrow ( union S)) = ( union { ( uparrow X) where X be Subset of T2 : P[X] }) from UparrowUnion;

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

        

        then z1 = ( uparrow z2) by A4, XBOOLE_0:def 10

        .= ( uparrow ( union Y1)) by A5, YELLOW_8: 9

        .= ( uparrow ( union Y3)) by A1, WAYBEL_0: 13

        .= ( union Y) by A7;

        hence thesis by A6, CANTOR_1:def 1;

      end;

      upV c= the topology of T1

      proof

        let z be object;

        assume z in upV;

        then

        consider V be Subset of T2 such that

         A8: z = ( uparrow V) and

         A9: V in B2;

        

         A10: T1 is Scott TopAugmentation of T2 by A1, YELLOW_9:def 4;

        B2 c= the topology of T2 by TOPS_2: 64;

        then V in the topology of T2 by A9;

        then V in ( lambda T2) by WAYBEL30: 9;

        then ( uparrow V) in ( sigma T1) by A10, WAYBEL30: 14;

        hence thesis by A8, WAYBEL14: 23;

      end;

      hence thesis by A2, CANTOR_1:def 2, TOPS_2: 64;

    end;

    

     Lm1: for L1 be continuous lower-bounded sup-Semilattice holds for T1 be Scott TopAugmentation of L1 holds for T2 be Lawson correct TopAugmentation of L1 holds ( weight T1) c= ( weight T2)

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T1 be Scott TopAugmentation of L1;

      let T2 be Lawson correct TopAugmentation of L1;

      consider B1 be Basis of T2 such that

       A1: ( card B1) = ( weight T2) by WAYBEL23: 74;

      defpred P[ object, object] means ex y be Subset of T2 st y = $1 & $2 = ( uparrow y);

      

       A2: for x be object st x in B1 holds ex z be object st P[x, z]

      proof

        let x be object;

        assume x in B1;

        then

        reconsider y = x as Subset of T2;

        take ( uparrow y);

        take y;

        thus thesis;

      end;

      consider f be Function such that

       A3: ( dom f) = B1 and

       A4: for x be object st x in B1 holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      { ( uparrow V) where V be Subset of T2 : V in B1 } c= ( rng f)

      proof

        let z be object;

        assume z in { ( uparrow V) where V be Subset of T2 : V in B1 };

        then

        consider V be Subset of T2 such that

         A5: z = ( uparrow V) and

         A6: V in B1;

        ex V1 be Subset of T2 st V1 = V & (f . V) = ( uparrow V1) by A4, A6;

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

      end;

      then

       A7: ( card { ( uparrow V) where V be Subset of T2 : V in B1 }) c= ( card B1) by A3, CARD_1: 12;

      { ( uparrow V) where V be Subset of T2 : V in B1 } is Basis of T1 by Th10;

      then ( card { ( uparrow V) where V be Subset of T2 : V in B1 }) in the set of all ( card B2) where B2 be Basis of T1;

      then ( meet the set of all ( card B2) where B2 be Basis of T1) c= ( card { ( uparrow V) where V be Subset of T2 : V in B1 }) by SETFAM_1: 3;

      then ( meet the set of all ( card B2) where B2 be Basis of T1) c= ( card B1) by A7;

      hence thesis by A1, WAYBEL23:def 5;

    end;

    theorem :: WAYBEL31:11

    

     Th11: for L1 be up-complete non empty Poset st L1 is finite holds for x be Element of L1 holds x in ( compactbelow x)

    proof

      let L1 be up-complete non empty Poset;

      assume

       A1: L1 is finite;

      let x be Element of L1;

      

       A2: x <= x;

      x is compact by A1, WAYBEL_3: 17;

      hence thesis by A2;

    end;

    theorem :: WAYBEL31:12

    

     Th12: for L1 be finite LATTICE holds L1 is arithmetic

    proof

      let L1 be finite LATTICE;

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

      thus L1 is up-complete;

      thus L1 is satisfying_axiom_K

      proof

        let x be Element of L1;

        

         A1: for y be Element of L1 st y is_>=_than ( compactbelow x) holds x <= y by Th11, LATTICE3:def 9;

        for y be Element of L1 st y in ( compactbelow x) holds y <= x by WAYBEL_8: 4;

        then x is_>=_than ( compactbelow x) by LATTICE3:def 9;

        hence thesis by A1, YELLOW_0: 30;

      end;

      thus ( CompactSublatt L1) is meet-inheriting

      proof

        let x,y be Element of L1;

        assume that x in the carrier of ( CompactSublatt L1) and y in the carrier of ( CompactSublatt L1) and ex_inf_of ( {x, y},L1);

        (x "/\" y) is compact by WAYBEL_3: 17;

        then (x "/\" y) in the carrier of ( CompactSublatt L1) by WAYBEL_8:def 1;

        hence thesis by YELLOW_0: 40;

      end;

    end;

    registration

      cluster finite -> arithmetic for LATTICE;

      coherence by Th12;

    end

    registration

      cluster reflexive transitive antisymmetric with_suprema with_infima lower-bounded1 -element finite strict for RelStr;

      existence

      proof

         0 in { 0 } by TARSKI:def 1;

        then

        reconsider r = { [ 0 , 0 ]} as Relation of { 0 } by RELSET_1: 3;

        reconsider T = RelStr (# { 0 }, r #) as non empty RelStr;

        take T;

        thus T is reflexive

        proof

          let x be Element of T;

          x = 0 by TARSKI:def 1;

          then [x, x] in { [ 0 , 0 ]} by TARSKI:def 1;

          hence thesis by ORDERS_2:def 5;

        end;

        then

        reconsider T9 = T as 1 -element reflexive RelStr;

        reconsider T99 = T9 as LATTICE;

        T9 is transitive;

        hence T is transitive;

        T9 is antisymmetric;

        hence T is antisymmetric;

        T9 is with_suprema;

        hence T is with_suprema;

        T9 is with_infima;

        hence T is with_infima;

        T99 is lower-bounded;

        hence T is lower-bounded;

        thus T is 1 -element;

        thus T is finite;

        thus thesis;

      end;

    end

    theorem :: WAYBEL31:13

    

     Th13: for L1 be finite LATTICE holds for B1 be with_bottom CLbasis of L1 holds ( card B1) = ( CLweight L1) iff B1 = the carrier of ( CompactSublatt L1)

    proof

      let L1 be finite LATTICE;

      let B1 be with_bottom CLbasis of L1;

      thus ( card B1) = ( CLweight L1) implies B1 = the carrier of ( CompactSublatt L1)

      proof

        assume ( card B1) = ( CLweight L1);

        then

         A1: ( card the carrier of ( CompactSublatt L1)) = ( card B1) by Th3;

        the carrier of ( CompactSublatt L1) c= B1 by WAYBEL23: 71;

        hence thesis by A1, CARD_2: 102;

      end;

      assume B1 = the carrier of ( CompactSublatt L1);

      hence thesis by Th3;

    end;

    definition

      let L1 be non empty reflexive RelStr;

      let A be Subset of L1;

      let a be Element of L1;

      :: WAYBEL31:def2

      func Way_Up (a,A) -> Subset of L1 equals (( wayabove a) \ ( uparrow A));

      coherence ;

    end

    theorem :: WAYBEL31:14

    for L1 be non empty reflexive RelStr holds for a be Element of L1 holds ( Way_Up (a,( {} L1))) = ( wayabove a);

    theorem :: WAYBEL31:15

    for L1 be non empty Poset holds for A be Subset of L1 holds for a be Element of L1 st a in ( uparrow A) holds ( Way_Up (a,A)) = {}

    proof

      let L1 be non empty Poset;

      let A be Subset of L1;

      let a be Element of L1;

      assume

       A1: a in ( uparrow A);

      ( wayabove a) c= ( uparrow A)

      proof

        let z be object;

        assume

         A2: z in ( wayabove a);

        then

        reconsider z1 = z as Element of L1;

        a << z1 by A2, WAYBEL_3: 8;

        then a <= z1 by WAYBEL_3: 1;

        hence thesis by A1, WAYBEL_0:def 20;

      end;

      hence thesis by XBOOLE_1: 37;

    end;

    theorem :: WAYBEL31:16

    

     Th16: for L1 be non empty finite reflexive transitive RelStr holds ( Ids L1) is finite

    proof

      deffunc F( set) = $1;

      let L1 be non empty finite reflexive transitive RelStr;

      reconsider Y = ( bool the carrier of L1) as finite non empty set;

      

       A1: the set of all X where X be Ideal of L1 c= { X where X be Element of Y : X is Ideal of L1 }

      proof

        let z be object;

        assume z in the set of all X where X be Ideal of L1;

        then ex X1 be Ideal of L1 st z = X1;

        hence thesis;

      end;

      defpred P[ set] means $1 is Ideal of L1;

      

       A2: { X where X be Element of Y : X is Ideal of L1 } c= the set of all X where X be Ideal of L1

      proof

        let z be object;

        assume z in { X where X be Element of Y : X is Ideal of L1 };

        then ex X1 be Element of Y st z = X1 & X1 is Ideal of L1;

        hence thesis;

      end;

      

       A3: { F(X) where X be Element of Y : P[X] } is finite from PRE_CIRC:sch 1;

      ( Ids L1) = the set of all X where X be Ideal of L1 by WAYBEL_0:def 23

      .= { X where X be Element of Y : X is Ideal of L1 } by A1, A2, XBOOLE_0:def 10;

      hence thesis by A3;

    end;

    theorem :: WAYBEL31:17

    

     Th17: for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds for B1 be with_bottom CLbasis of L1 holds B1 is infinite

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      assume

       A1: L1 is infinite;

      let B1 be with_bottom CLbasis of L1;

      ( dom ( supMap ( subrelstr B1))) = ( Ids ( subrelstr B1)) & ( rng ( supMap ( subrelstr B1))) = the carrier of L1 by WAYBEL23: 51, WAYBEL23: 65;

      then ( card the carrier of L1) c= ( card ( Ids ( subrelstr B1))) by CARD_1: 12;

      then ( Ids ( subrelstr B1)) is infinite by A1;

      then ( subrelstr B1) is infinite by Th16;

      hence thesis by YELLOW_0:def 15;

    end;

    theorem :: WAYBEL31:18

    for L1 be complete non empty Poset holds for x be Element of L1 holds x is compact implies x = ( inf ( wayabove x))

    proof

      let L1 be complete non empty Poset;

      let x be Element of L1;

      assume x is compact;

      then x << x by WAYBEL_3:def 2;

      then x in ( wayabove x) by WAYBEL_3: 8;

      then

       A1: ( inf ( wayabove x)) <= x by YELLOW_2: 22;

      x <= ( inf ( wayabove x)) by WAYBEL14: 9;

      hence thesis by A1, YELLOW_0:def 3;

    end;

    theorem :: WAYBEL31:19

    

     Th19: for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds for B1 be with_bottom CLbasis of L1 holds ( card { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 }) c= ( card B1)

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      assume

       A1: L1 is infinite;

      let B1 be with_bottom CLbasis of L1;

      consider a1 be object such that

       A2: a1 in B1 by XBOOLE_0:def 1;

      reconsider a1 as Element of L1 by A2;

      ( {} L1) c= B1;

      then ( Way_Up (a1,( {} L1))) in { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 } by A2;

      then

      reconsider WU = { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 } as non empty set;

      defpred P[ Element of (B1 * ), set] means ex y be Element of L1, z be Subset of L1 st y = ($1 /. 1) & z = ( rng ( Del ($1,1))) & $2 = ( Way_Up (y,z));

      

       A3: for x be Element of (B1 * ) holds ex u be Element of WU st P[x, u]

      proof

        let x be Element of (B1 * );

        reconsider y = (x /. 1) as Element of L1 by TARSKI:def 3;

        ( rng ( Del (x,1))) c= ( rng x) by FINSEQ_3: 106;

        then

         A4: ( rng ( Del (x,1))) c= B1 by XBOOLE_1: 1;

        then

        reconsider z = ( rng ( Del (x,1))) as Subset of L1 by XBOOLE_1: 1;

        ( Way_Up (y,z)) in { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 } by A4;

        then

        reconsider u = ( Way_Up (y,z)) as Element of WU;

        take u, y, z;

        thus thesis;

      end;

      consider f be Function of (B1 * ), WU such that

       A5: for x be Element of (B1 * ) holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

      

       A6: ( dom f) = (B1 * ) by FUNCT_2:def 1;

      

       A7: WU c= ( rng f)

      proof

        let z be object;

        assume z in WU;

        then

        consider a be Element of L1, A be finite Subset of L1 such that

         A8: z = ( Way_Up (a,A)) and

         A9: a in B1 and

         A10: A c= B1;

        reconsider a1 = a as Element of B1 by A9;

        consider p be FinSequence such that

         A11: A = ( rng p) by FINSEQ_1: 52;

        reconsider p as FinSequence of B1 by A10, A11, FINSEQ_1:def 4;

        set q = ( <*a1*> ^ p);

        

         A12: q in (B1 * ) by FINSEQ_1:def 11;

        then

        consider y be Element of L1, v be Subset of L1 such that

         A13: y = (q /. 1) and

         A14: v = ( rng ( Del (q,1))) and

         A15: (f . q) = ( Way_Up (y,v)) by A5;

        

         A16: a = y by A13, FINSEQ_5: 15;

        A = v by A11, A14, WSIERP_1: 40;

        hence thesis by A6, A8, A12, A15, A16, FUNCT_1:def 3;

      end;

      B1 is infinite by A1, Th17;

      then ( card B1) = ( card (B1 * )) by CARD_4: 24;

      hence thesis by A6, A7, CARD_1: 12;

    end;

    theorem :: WAYBEL31:20

    

     Th20: for T be Lawson complete TopLattice holds for X be finite Subset of T holds (( uparrow X) ` ) is open & (( downarrow X) ` ) is open

    proof

      let T be Lawson complete TopLattice;

      let X be finite Subset of T;

      deffunc F( Element of T) = ( uparrow $1);

      { ( uparrow x) where x be Element of T : x in X } c= ( bool the carrier of T)

      proof

        let z be object;

        assume z in { ( uparrow x) where x be Element of T : x in X };

        then ex x be Element of T st z = ( uparrow x) & x in X;

        hence thesis;

      end;

      then

      reconsider upx = { ( uparrow x) where x be Element of T : x in X } as Subset-Family of T;

      { ( downarrow x) where x be Element of T : x in X } c= ( bool the carrier of T)

      proof

        let z be object;

        assume z in { ( downarrow x) where x be Element of T : x in X };

        then ex x be Element of T st z = ( downarrow x) & x in X;

        hence thesis;

      end;

      then

      reconsider dox = { ( downarrow x) where x be Element of T : x in X } as Subset-Family of T;

      reconsider dox as Subset-Family of T;

      reconsider upx as Subset-Family of T;

      

       A1: ( uparrow X) = ( union upx) by YELLOW_9: 4;

      now

        let P be Subset of T;

        assume P in upx;

        then ex x be Element of T st P = ( uparrow x) & x in X;

        hence P is closed by WAYBEL19: 38;

      end;

      then

       A2: upx is closed by TOPS_2:def 2;

      

       A3: X is finite;

      { F(x) where x be Element of T : x in X } is finite from FRAENKEL:sch 21( A3);

      then ( uparrow X) is closed by A2, A1, TOPS_2: 21;

      hence (( uparrow X) ` ) is open by TOPS_1: 3;

      deffunc F( Element of T) = ( downarrow $1);

      

       A4: ( downarrow X) = ( union dox) by YELLOW_9: 4;

      now

        let P be Subset of T;

        assume P in dox;

        then ex x be Element of T st P = ( downarrow x) & x in X;

        hence P is closed by WAYBEL19: 38;

      end;

      then

       A5: dox is closed by TOPS_2:def 2;

      { F(x) where x be Element of T : x in X } is finite from FRAENKEL:sch 21( A3);

      then ( downarrow X) is closed by A5, A4, TOPS_2: 21;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: WAYBEL31:21

    

     Th21: for L1 be continuous lower-bounded sup-Semilattice holds for T be Lawson correct TopAugmentation of L1 holds for B1 be with_bottom CLbasis of L1 holds { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 } is Basis of T

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Lawson correct TopAugmentation of L1;

      let B1 be with_bottom CLbasis of L1;

      

       A1: the RelStr of L1 = the RelStr of T by YELLOW_9:def 4;

      { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 } c= ( bool the carrier of T)

      proof

        let z be object;

        assume z in { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 };

        then ex a be Element of L1, A be finite Subset of L1 st z = ( Way_Up (a,A)) & a in B1 & A c= B1;

        hence thesis by A1;

      end;

      then

      reconsider WU = { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 } as Subset-Family of T;

      reconsider WU as Subset-Family of T;

       A2:

      now

        reconsider BL = { (W \ ( uparrow F)) where W,F be Subset of T : W in ( sigma T) & F is finite } as Basis of T by WAYBEL19: 32;

        set S = the Scott TopAugmentation of T;

        let A be Subset of T;

        assume

         A3: A is open;

        let pT be Point of T;

        assume pT in A;

        then

        consider a be Subset of T such that

         A4: a in BL and

         A5: pT in a and

         A6: a c= A by A3, YELLOW_9: 31;

        consider W,FT be Subset of T such that

         A7: a = (W \ ( uparrow FT)) and

         A8: W in ( sigma T) and

         A9: FT is finite by A4;

        

         A10: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

        then

        reconsider pS = pT as Element of S;

        reconsider W1 = W as Subset of S by A10;

        ( sigma S) = ( sigma T) by A10, YELLOW_9: 52;

        then

         A11: W = ( union { ( wayabove x) where x be Element of S : x in W1 }) by A8, WAYBEL14: 33;

        reconsider pL = pS as Element of L1 by A1;

        defpred P[ object, object] means ex b1,y1 be Element of L1 st y1 = $1 & b1 = $2 & b1 in B1 & not b1 <= pL & b1 << y1;

        

         A12: ( Bottom L1) in B1 by WAYBEL23:def 8;

        pT in W by A5, A7, XBOOLE_0:def 5;

        then

        consider k be set such that

         A13: pT in k and

         A14: k in { ( wayabove x) where x be Element of S : x in W1 } by A11, TARSKI:def 4;

        consider xS be Element of S such that

         A15: k = ( wayabove xS) and

         A16: xS in W1 by A14;

        reconsider xL = xS as Element of L1 by A1, A10;

        xS << pS by A13, A15, WAYBEL_3: 8;

        then xL << pL by A1, A10, WAYBEL_8: 8;

        then

        consider bL be Element of L1 such that

         A17: bL in B1 and

         A18: xL <= bL and

         A19: bL << pL by A12, WAYBEL23: 47;

        reconsider FL = FT as Subset of L1 by A1;

        

         A20: ( uparrow FT) = ( uparrow FL) by A1, WAYBEL_0: 13;

        

         A21: not pT in ( uparrow FT) by A5, A7, XBOOLE_0:def 5;

        

         A22: for y be object st y in FL holds ex b be object st P[y, b]

        proof

          let y be object;

          assume

           A23: y in FL;

          then

          reconsider y1 = y as Element of L1;

           not y1 <= pL by A21, A20, A23, WAYBEL_0:def 16;

          then

          consider b1 be Element of L1 such that

           A24: b1 in B1 & not b1 <= pL & b1 << y1 by WAYBEL23: 46;

          reconsider b = b1 as set;

          take b, b1, y1;

          thus thesis by A24;

        end;

        consider f be Function such that

         A25: ( dom f) = FL and

         A26: for y be object st y in FL holds P[y, (f . y)] from CLASSES1:sch 1( A22);

        ( rng f) c= the carrier of L1

        proof

          let z be object;

          assume z in ( rng f);

          then

          consider v be object such that

           A27: v in ( dom f) and

           A28: z = (f . v) by FUNCT_1:def 3;

          ex b1,y1 be Element of L1 st y1 = v & b1 = (f . v) & b1 in B1 & ( not b1 <= pL) & b1 << y1 by A25, A26, A27;

          hence thesis by A28;

        end;

        then

        reconsider FFL = ( rng f) as Subset of L1;

        

         A29: FFL c= B1

        proof

          let z be object;

          assume z in FFL;

          then

          consider v be object such that

           A30: v in ( dom f) and

           A31: z = (f . v) by FUNCT_1:def 3;

          ex b1,y1 be Element of L1 st y1 = v & b1 = (f . v) & b1 in B1 & ( not b1 <= pL) & b1 << y1 by A25, A26, A30;

          hence thesis by A31;

        end;

        

         A32: ( uparrow FL) c= ( uparrow FFL)

        proof

          let z be object;

          assume

           A33: z in ( uparrow FL);

          then

          reconsider z1 = z as Element of L1;

          consider v1 be Element of L1 such that

           A34: v1 <= z1 and

           A35: v1 in FL by A33, WAYBEL_0:def 16;

          consider b1,y1 be Element of L1 such that

           A36: y1 = v1 and

           A37: b1 = (f . v1) and b1 in B1 and not b1 <= pL and

           A38: b1 << y1 by A26, A35;

          b1 << z1 by A34, A36, A38, WAYBEL_3: 2;

          then

           A39: b1 <= z1 by WAYBEL_3: 1;

          b1 in FFL by A25, A35, A37, FUNCT_1:def 3;

          hence thesis by A39, WAYBEL_0:def 16;

        end;

        reconsider cT = (( wayabove bL) \ ( uparrow FFL)) as Subset of T by A1;

        take cT;

        cT = ( Way_Up (bL,FFL)) & FFL is finite by A9, A25, FINSET_1: 8;

        hence cT in WU by A17, A29;

        ( wayabove bL) c= ( wayabove xL) by A18, WAYBEL_3: 12;

        then

         A40: (( wayabove bL) \ ( uparrow FFL)) c= (( wayabove xL) \ ( uparrow FL)) by A32, XBOOLE_1: 35;

        for z be Element of L1 holds not z in FFL or not z <= pL

        proof

          let z be Element of L1;

          assume z in FFL;

          then

          consider v be object such that

           A41: v in ( dom f) and

           A42: z = (f . v) by FUNCT_1:def 3;

          ex b1,y1 be Element of L1 st y1 = v & b1 = (f . v) & b1 in B1 & ( not b1 <= pL) & b1 << y1 by A25, A26, A41;

          hence thesis by A42;

        end;

        then for z be Element of L1 holds not z <= pL or not z in FFL;

        then

         A43: not pL in ( uparrow FFL) by WAYBEL_0:def 16;

        pL in ( wayabove bL) by A19, WAYBEL_3: 8;

        hence pT in cT by A43, XBOOLE_0:def 5;

        ( wayabove xL) c= W

        proof

          let z be object;

          ( wayabove xL) = ( wayabove xS) by A1, A10, YELLOW12: 13;

          then

           A44: ( wayabove xL) in { ( wayabove x) where x be Element of S : x in W1 } by A16;

          assume z in ( wayabove xL);

          hence thesis by A11, A44, TARSKI:def 4;

        end;

        then (( wayabove xL) \ ( uparrow FL)) c= a by A7, A20, XBOOLE_1: 33;

        then (( wayabove bL) \ ( uparrow FFL)) c= a by A40;

        hence cT c= A by A6;

      end;

      WU c= the topology of T

      proof

        let z be object;

        assume z in WU;

        then

        consider a be Element of L1, A be finite Subset of L1 such that

         A45: z = ( Way_Up (a,A)) and a in B1 and A c= B1;

        reconsider A1 = A as finite Subset of T by A1;

        reconsider a1 = a as Element of T by A1;

        ( wayabove a1) is open & (( uparrow A1) ` ) is open by Th20, WAYBEL19: 40;

        then

         A46: (( wayabove a1) /\ (( uparrow A1) ` )) is open by TOPS_1: 11;

        z = (( wayabove a1) \ ( uparrow A)) by A1, A45, YELLOW12: 13

        .= (( wayabove a1) \ ( uparrow A1)) by A1, WAYBEL_0: 13

        .= (( wayabove a1) /\ (( uparrow A1) ` )) by SUBSET_1: 13;

        hence thesis by A46, PRE_TOPC:def 2;

      end;

      hence thesis by A2, YELLOW_9: 32;

    end;

    

     Lm2: for L1 be continuous lower-bounded sup-Semilattice holds for T be Lawson correct TopAugmentation of L1 holds ( weight T) c= ( CLweight L1)

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Lawson correct TopAugmentation of L1;

      consider B1 be with_bottom CLbasis of L1 such that

       A1: ( card B1) = ( CLweight L1) by Th2;

      

       A2: the RelStr of T = the RelStr of L1 by YELLOW_9:def 4;

      now

        per cases ;

          suppose

           A3: L1 is finite;

          then

           A4: T is finite by A2;

          B1 = the carrier of ( CompactSublatt L1) by A1, A3, Th13

          .= the carrier of L1 by A3, YELLOW15: 26;

          hence thesis by A2, A1, A4, Th8;

        end;

          suppose

           A5: L1 is infinite;

          set WU = { ( Way_Up (a,A)) where a be Element of L1, A be finite Subset of L1 : a in B1 & A c= B1 };

          WU is Basis of T by Th21;

          then

           A6: ( weight T) c= ( card WU) by WAYBEL23: 73;

          ( card WU) c= ( CLweight L1) by A1, A5, Th19;

          hence thesis by A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL31:22

    

     Th22: for L1 be continuous lower-bounded sup-Semilattice holds for T be Scott TopAugmentation of L1 holds for b be Basis of T holds { ( wayabove ( inf u)) where u be Subset of T : u in b } is Basis of T

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Scott TopAugmentation of L1;

      let b be Basis of T;

      set b2 = { ( wayabove ( inf u)) where u be Subset of T : u in b };

      b2 c= ( bool the carrier of T)

      proof

        let z be object;

        assume z in b2;

        then ex u be Subset of T st z = ( wayabove ( inf u)) & u in b;

        hence thesis;

      end;

      then

      reconsider b2 as Subset-Family of T;

      reconsider b1 = the set of all ( wayabove x) where x be Element of T as Basis of T by WAYBEL11: 45;

       A1:

      now

        let A be Subset of T;

        assume

         A2: A is open;

        let a be Point of T;

        assume a in A;

        then

        consider C be Subset of T such that

         A3: C in b1 and

         A4: a in C and

         A5: C c= A by A2, YELLOW_9: 31;

        C is open by A3, YELLOW_8: 10;

        then

        consider D be Subset of T such that

         A6: D in b and

         A7: a in D and

         A8: D c= C by A4, YELLOW_9: 31;

        D is open by A6, YELLOW_8: 10;

        then

        consider E be Subset of T such that

         A9: E in b1 and

         A10: a in E and

         A11: E c= D by A7, YELLOW_9: 31;

        consider z be Element of T such that

         A12: E = ( wayabove z) by A9;

        take u = ( wayabove ( inf D));

        thus u in b2 by A6;

        reconsider a1 = a as Element of T;

        consider x be Element of T such that

         A13: C = ( wayabove x) by A3;

        z << a1 by A10, A12, WAYBEL_3: 8;

        then

        consider y be Element of T such that

         A14: z << y and

         A15: y << a1 by WAYBEL_4: 52;

        ( inf D) is_<=_than D & y in ( wayabove z) by A14, WAYBEL_3: 8, YELLOW_0: 33;

        then ( inf D) <= y by A11, A12, LATTICE3:def 8;

        then ( inf D) << a1 by A15, WAYBEL_3: 2;

        hence a in u by WAYBEL_3: 8;

        

         A16: ( wayabove x) c= ( uparrow x) by WAYBEL_3: 11;

         ex_inf_of (( uparrow x),T) & ex_inf_of (D,T) by YELLOW_0: 17;

        then ( inf ( uparrow x)) <= ( inf D) by A13, A8, A16, XBOOLE_1: 1, YELLOW_0: 35;

        then x <= ( inf D) by WAYBEL_0: 39;

        then ( wayabove ( inf D)) c= C by A13, WAYBEL_3: 12;

        hence u c= A by A5;

      end;

      b2 c= the topology of T

      proof

        let z be object;

        assume z in b2;

        then

        consider u be Subset of T such that

         A17: z = ( wayabove ( inf u)) and u in b;

        ( wayabove ( inf u)) is open by WAYBEL11: 36;

        hence thesis by A17, PRE_TOPC:def 2;

      end;

      hence thesis by A1, YELLOW_9: 32;

    end;

    theorem :: WAYBEL31:23

    

     Th23: for L1 be continuous lower-bounded sup-Semilattice holds for T be Scott TopAugmentation of L1 holds for B1 be Basis of T st B1 is infinite holds { ( inf u) where u be Subset of T : u in B1 } is infinite

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Scott TopAugmentation of L1;

      let B1 be Basis of T;

      reconsider B2 = { ( inf u) where u be Subset of T : u in B1 } as set;

      defpred P[ object, object] means ex y be Element of T st $1 = y & $2 = ( wayabove y);

      reconsider B3 = { ( wayabove ( inf u)) where u be Subset of T : u in B1 } as Basis of T by Th22;

      assume that

       A1: B1 is infinite and

       A2: { ( inf u) where u be Subset of T : u in B1 } is finite;

      

       A3: for x be object st x in B2 holds ex y be object st y in B3 & P[x, y]

      proof

        let x be object;

        assume x in B2;

        then

         A4: ex u1 be Subset of T st x = ( inf u1) & u1 in B1;

        then

        reconsider z = x as Element of T;

        take y = ( wayabove z);

        thus y in B3 by A4;

        take z;

        thus thesis;

      end;

      consider f be Function such that

       A5: ( dom f) = B2 and

       A6: ( rng f) c= B3 and

       A7: for x be object st x in B2 holds P[x, (f . x)] from FUNCT_1:sch 6( A3);

      B3 c= ( rng f)

      proof

        let z be object;

        assume z in B3;

        then

        consider u1 be Subset of T such that

         A8: z = ( wayabove ( inf u1)) and

         A9: u1 in B1;

        ( inf u1) in B2 by A9;

        then

         A10: ex y be Element of T st ( inf u1) = y & (f . ( inf u1)) = ( wayabove y) by A7;

        ( inf u1) in B2 by A9;

        hence thesis by A5, A8, A10, FUNCT_1:def 3;

      end;

      then ( rng f) = B3 by A6, XBOOLE_0:def 10;

      then B3 is finite by A2, A5, FINSET_1: 8;

      then T is finite by YELLOW15: 30;

      hence contradiction by A1;

    end;

    

     Lm3: for L1 be continuous lower-bounded sup-Semilattice holds for T be Scott TopAugmentation of L1 holds ( CLweight L1) c= ( weight T)

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Scott TopAugmentation of L1;

      consider B1 be Basis of T such that

       A1: ( card B1) = ( weight T) by WAYBEL23: 74;

      { ( inf u) where u be Subset of T : u in B1 } c= the carrier of T

      proof

        let z be object;

        assume z in { ( inf u) where u be Subset of T : u in B1 };

        then ex u be Subset of T st z = ( inf u) & u in B1;

        hence thesis;

      end;

      then

      reconsider B0 = { ( inf u) where u be Subset of T : u in B1 } as Subset of T;

      set B2 = ( finsups B0);

      defpred P[ object, object] means ex y be Subset of T st $1 = y & $2 = ( inf y);

      

       A2: for x be object st x in B1 holds ex y be object st y in B0 & P[x, y]

      proof

        let x be object;

        assume

         A3: x in B1;

        then

        reconsider z = x as Subset of T;

        take y = ( inf z);

        thus y in B0 by A3;

        take z;

        thus thesis;

      end;

      consider f be Function such that

       A4: ( dom f) = B1 and ( rng f) c= B0 and

       A5: for x be object st x in B1 holds P[x, (f . x)] from FUNCT_1:sch 6( A2);

      B0 c= ( rng f)

      proof

        let z be object;

        assume z in B0;

        then

        consider u be Subset of T such that

         A6: z = ( inf u) and

         A7: u in B1;

        ex y be Subset of T st u = y & (f . u) = ( inf y) by A5, A7;

        hence thesis by A4, A6, A7, FUNCT_1:def 3;

      end;

      then

       A8: ( card B0) c= ( card B1) by A4, CARD_1: 12;

      

       A9: the RelStr of L1 = the RelStr of T by YELLOW_9:def 4;

       A10:

      now

        per cases ;

          suppose

           A11: L1 is finite;

          the carrier of L1 c= B0

          proof

            let z be object;

            assume z in the carrier of L1;

            then

            reconsider z1 = z as Element of T by A9;

            z1 <= z1;

            then

             A12: z1 in ( uparrow z1) by WAYBEL_0: 18;

            T is finite by A9, A11;

            then ( uparrow z1) is open by WAYBEL11:def 5;

            then

            consider A be Subset of T such that

             A13: A in B1 and

             A14: z1 in A and

             A15: A c= ( uparrow z1) by A12, YELLOW_9: 31;

             ex_inf_of (( uparrow z1),T) & ex_inf_of (A,T) by YELLOW_0: 17;

            then ( inf ( uparrow z1)) <= ( inf A) by A15, YELLOW_0: 35;

            then

             A16: z1 <= ( inf A) by WAYBEL_0: 39;

            ( inf A) <= z1 by A14, YELLOW_2: 22;

            then z = ( inf A) by A16, YELLOW_0:def 3;

            hence thesis by A13;

          end;

          then B0 c= B2 & B2 c= B0 by A9, WAYBEL_0: 50;

          hence ( card B2) = ( card B0) by XBOOLE_0:def 10;

        end;

          suppose L1 is infinite;

          then T is infinite by A9;

          then B0 is infinite by Th23, YELLOW15: 30;

          hence ( card B2) = ( card B0) by YELLOW15: 27;

        end;

      end;

       ex_sup_of ( {} ,T) & {} is finite Subset of B0 by XBOOLE_1: 2, YELLOW_0: 42;

      then ( "\/" ( {} ,T)) in { ( "\/" (Y,T)) where Y be finite Subset of B0 : ex_sup_of (Y,T) };

      then ( "\/" ( {} ,T)) in ( finsups B0) by WAYBEL_0:def 27;

      then

       A17: ( Bottom L1) in B2 by A9, YELLOW_0: 26, YELLOW_0: 42;

      reconsider B2 as Subset of L1 by A9;

      now

        let x,y be Element of L1;

        assume that

         A18: x in B2 and

         A19: y in B2;

        y in { ( "\/" (Y,T)) where Y be finite Subset of B0 : ex_sup_of (Y,T) } by A19, WAYBEL_0:def 27;

        then

        consider Y2 be finite Subset of B0 such that

         A20: y = ( "\/" (Y2,T)) and

         A21: ex_sup_of (Y2,T);

        x in { ( "\/" (Y,T)) where Y be finite Subset of B0 : ex_sup_of (Y,T) } by A18, WAYBEL_0:def 27;

        then

        consider Y1 be finite Subset of B0 such that

         A22: x = ( "\/" (Y1,T)) and

         A23: ex_sup_of (Y1,T);

        

         A24: ex_sup_of ((Y1 \/ Y2),T) by YELLOW_0: 17;

        ( sup {x, y}) = (x "\/" y) by YELLOW_0: 41

        .= (( "\/" (Y1,T)) "\/" ( "\/" (Y2,T))) by A9, A22, A20, YELLOW12: 10

        .= ( "\/" ((Y1 \/ Y2),T)) by A23, A21, YELLOW_2: 3;

        then ( sup {x, y}) in { ( "\/" (Y,T)) where Y be finite Subset of B0 : ex_sup_of (Y,T) } by A24;

        hence ( sup {x, y}) in B2 by WAYBEL_0:def 27;

      end;

      then

      reconsider B2 as join-closed Subset of L1 by WAYBEL23: 18;

      for x,y be Element of L1 st x << y holds ex b be Element of L1 st b in B2 & x <= b & b << y

      proof

        let x,y be Element of L1;

        reconsider x1 = x, y1 = y as Element of T by A9;

        

         A25: B0 c= B2 by WAYBEL_0: 50;

        assume x << y;

        then y in ( wayabove x) by WAYBEL_3: 8;

        then

         A26: y1 in ( wayabove x1) by A9, YELLOW12: 13;

        ( wayabove x1) is open by WAYBEL11: 36;

        then

        consider u be Subset of T such that

         A27: u in B1 and

         A28: y1 in u and

         A29: u c= ( wayabove x1) by A26, YELLOW_9: 31;

        reconsider b = ( inf u) as Element of L1 by A9;

        take b;

        b in B0 by A27;

        hence b in B2 by A25;

        

         A30: ( wayabove x1) c= ( uparrow x1) by WAYBEL_3: 11;

         ex_inf_of (( uparrow x1),T) & ex_inf_of (u,T) by YELLOW_0: 17;

        then ( inf ( uparrow x1)) <= ( inf u) by A29, A30, XBOOLE_1: 1, YELLOW_0: 35;

        then x1 <= ( inf u) by WAYBEL_0: 39;

        hence x <= b by A9, YELLOW_0: 1;

        u is open by A27, YELLOW_8: 10;

        hence thesis by A9, A28, WAYBEL14: 26, WAYBEL_8: 8;

      end;

      then

       A31: B2 is CLbasis of L1 by A17, WAYBEL23: 47;

      B2 is with_bottom by A17, WAYBEL23:def 8;

      then ( CLweight L1) c= ( card B0) by A10, A31, Th1;

      hence thesis by A1, A8;

    end;

    theorem :: WAYBEL31:24

    

     Th24: for L1 be continuous lower-bounded sup-Semilattice holds for T be Scott TopAugmentation of L1 holds ( CLweight L1) = ( weight T)

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Scott TopAugmentation of L1;

      set T1 = the Lawson correct TopAugmentation of L1;

      ( weight T) c= ( weight T1) & ( weight T1) c= ( CLweight L1) by Lm1, Lm2;

      then

       A1: ( weight T) c= ( CLweight L1);

      ( CLweight L1) c= ( weight T) by Lm3;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL31:25

    for L1 be continuous lower-bounded sup-Semilattice holds for T be Lawson correct TopAugmentation of L1 holds ( CLweight L1) = ( weight T)

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let T be Lawson correct TopAugmentation of L1;

      set T1 = the Scott TopAugmentation of L1;

      ( CLweight L1) c= ( weight T1) & ( weight T1) c= ( weight T) by Lm1, Lm3;

      then

       A1: ( CLweight L1) c= ( weight T);

      ( weight T) c= ( CLweight L1) by Lm2;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL31:26

    

     Th26: for L1,L2 be non empty RelStr st (L1,L2) are_isomorphic holds ( card the carrier of L1) = ( card the carrier of L2)

    proof

      let L1,L2 be non empty RelStr;

      assume (L1,L2) are_isomorphic ;

      then

      consider f be Function of L1, L2 such that

       A1: f is isomorphic by WAYBEL_1:def 8;

      

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

      f is one-to-one & ( rng f) = the carrier of L2 by A1, WAYBEL_0: 66;

      then (the carrier of L1,the carrier of L2) are_equipotent by A2, WELLORD2:def 4;

      hence thesis by CARD_1: 5;

    end;

    theorem :: WAYBEL31:27

    for L1 be continuous lower-bounded sup-Semilattice holds for B1 be with_bottom CLbasis of L1 st ( card B1) = ( CLweight L1) holds ( CLweight L1) = ( CLweight ( InclPoset ( Ids ( subrelstr B1))))

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      let B1 be with_bottom CLbasis of L1;

      assume

       A1: ( card B1) = ( CLweight L1);

      

       A2: ( card the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B1))))) = ( card the carrier of ( subrelstr B1)) by Th26, WAYBEL23: 69;

      

      thus ( CLweight ( InclPoset ( Ids ( subrelstr B1)))) = ( card the carrier of ( CompactSublatt ( InclPoset ( Ids ( subrelstr B1))))) by Th3

      .= ( CLweight L1) by A1, A2, YELLOW_0:def 15;

    end;

    registration

      let L1 be continuous lower-bounded sup-Semilattice;

      cluster ( InclPoset ( sigma L1)) -> with_suprema continuous;

      coherence

      proof

        set S = the Scott TopAugmentation of L1;

        

         A1: the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;

        ( InclPoset ( sigma S)) is complete;

        hence ( InclPoset ( sigma L1)) is with_suprema by A1, YELLOW_9: 52;

        ( InclPoset ( sigma S)) is continuous by WAYBEL14: 36;

        hence thesis by A1, YELLOW_9: 52;

      end;

    end

    theorem :: WAYBEL31:28

    for L1 be continuous lower-bounded sup-Semilattice holds ( CLweight L1) c= ( CLweight ( InclPoset ( sigma L1)))

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      set S = the Scott TopAugmentation of L1;

      

       A1: the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;

      

       A2: ( InclPoset the topology of S) = ( InclPoset ( sigma L1)) by YELLOW_9: 51;

      

       A3: ( CLweight L1) = ( weight S) by Th24;

      now

        per cases ;

          suppose L1 is infinite;

          then S is infinite by A1;

          hence thesis by A3, A2, Th6;

        end;

          suppose

           A4: L1 is finite;

          

           A5: ( card the carrier of S) c= ( card the carrier of ( InclPoset ( sigma L1))) by A2, Th7;

          

           A6: S is finite by A1, A4;

          then ( weight S) = ( card the carrier of S) by Th8;

          hence thesis by A3, A2, A6, A5, Th9;

        end;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL31:29

    for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds ( CLweight L1) = ( CLweight ( InclPoset ( sigma L1)))

    proof

      let L1 be continuous lower-bounded sup-Semilattice;

      set S = the Scott TopAugmentation of L1;

      assume

       A1: L1 is infinite;

      

       A2: ( CLweight L1) = ( weight S) & ( InclPoset the topology of S) = ( InclPoset ( sigma L1)) by Th24, YELLOW_9: 51;

       the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;

      then S is infinite by A1;

      hence thesis by A2, Th6;

    end;