:: WAYBEL31 semantic presentation begin scheme :: WAYBEL31:sch 1 UparrowUnion{ F1() -> RelStr , P1[ set ] } : for S being Subset-Family of F1() st S = { X where X is Subset of F1() : P1[X] } holds uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } proof let S be Subset-Family of F1(); ::_thesis: ( S = { X where X is Subset of F1() : P1[X] } implies uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } ) assume A1: S = { X where X is Subset of F1() : P1[X] } ; ::_thesis: uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } A2: union { (uparrow X) where X is Subset of F1() : P1[X] } c= uparrow (union S) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (uparrow X) where X is Subset of F1() : P1[X] } or z in uparrow (union S) ) assume z in union { (uparrow X) where X is Subset of F1() : P1[X] } ; ::_thesis: z in uparrow (union S) then consider Z being set such that A3: z in Z and A4: Z in { (uparrow X) where X is Subset of F1() : P1[X] } by TARSKI:def_4; consider X1 being Subset of F1() such that A5: Z = uparrow X1 and A6: P1[X1] by A4; reconsider z1 = z as Element of F1() by A3, A5; consider y1 being Element of F1() 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 z in uparrow (union S) by A7, WAYBEL_0:def_16; ::_thesis: verum end; uparrow (union S) c= union { (uparrow X) where X is Subset of F1() : P1[X] } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow (union S) or z in union { (uparrow X) where X is Subset of F1() : P1[X] } ) assume A9: z in uparrow (union S) ; ::_thesis: z in union { (uparrow X) where X is Subset of F1() : P1[X] } then reconsider z1 = z as Element of F1() ; consider y1 being Element of F1() such that A10: y1 <= z1 and A11: y1 in union S by A9, WAYBEL_0:def_16; consider Z being set such that A12: y1 in Z and A13: Z in S by A11, TARSKI:def_4; consider X1 being Subset of F1() such that A14: Z = X1 and A15: P1[X1] by A1, A13; A16: uparrow X1 in { (uparrow X) where X is Subset of F1() : P1[X] } by A15; z in uparrow X1 by A10, A12, A14, WAYBEL_0:def_16; hence z in union { (uparrow X) where X is Subset of F1() : P1[X] } by A16, TARSKI:def_4; ::_thesis: verum end; hence uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] } by A2, XBOOLE_0:def_10; ::_thesis: verum end; scheme :: WAYBEL31:sch 2 DownarrowUnion{ F1() -> RelStr , P1[ set ] } : for S being Subset-Family of F1() st S = { X where X is Subset of F1() : P1[X] } holds downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] } proof let S be Subset-Family of F1(); ::_thesis: ( S = { X where X is Subset of F1() : P1[X] } implies downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] } ) assume A1: S = { X where X is Subset of F1() : P1[X] } ; ::_thesis: downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] } A2: union { (downarrow X) where X is Subset of F1() : P1[X] } c= downarrow (union S) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (downarrow X) where X is Subset of F1() : P1[X] } or z in downarrow (union S) ) assume z in union { (downarrow X) where X is Subset of F1() : P1[X] } ; ::_thesis: z in downarrow (union S) then consider Z being set such that A3: z in Z and A4: Z in { (downarrow X) where X is Subset of F1() : P1[X] } by TARSKI:def_4; consider X1 being Subset of F1() such that A5: Z = downarrow X1 and A6: P1[X1] by A4; reconsider z1 = z as Element of F1() by A3, A5; consider y1 being Element of F1() 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 z in downarrow (union S) by A7, WAYBEL_0:def_15; ::_thesis: verum end; downarrow (union S) c= union { (downarrow X) where X is Subset of F1() : P1[X] } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow (union S) or z in union { (downarrow X) where X is Subset of F1() : P1[X] } ) assume A9: z in downarrow (union S) ; ::_thesis: z in union { (downarrow X) where X is Subset of F1() : P1[X] } then reconsider z1 = z as Element of F1() ; consider y1 being Element of F1() such that A10: y1 >= z1 and A11: y1 in union S by A9, WAYBEL_0:def_15; consider Z being set such that A12: y1 in Z and A13: Z in S by A11, TARSKI:def_4; consider X1 being Subset of F1() such that A14: Z = X1 and A15: P1[X1] by A1, A13; A16: downarrow X1 in { (downarrow X) where X is Subset of F1() : P1[X] } by A15; z in downarrow X1 by A10, A12, A14, WAYBEL_0:def_15; hence z in union { (downarrow X) where X is Subset of F1() : P1[X] } by A16, TARSKI:def_4; ::_thesis: verum end; hence downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] } by A2, XBOOLE_0:def_10; ::_thesis: verum 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 InclPoset (Ids (subrelstr B1)) is algebraic by WAYBEL13:10; end; definition let L1 be continuous sup-Semilattice; func CLweight L1 -> Cardinal equals :: WAYBEL31:def 1 meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; coherence meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal proof set X = { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; defpred S1[ Ordinal] means \$1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; A1: ex A being Ordinal st S1[A] proof take card ([#] L1) ; ::_thesis: S1[ card ([#] L1)] [#] L1 is CLbasis of L1 by YELLOW15:25; hence S1[ card ([#] L1)] ; ::_thesis: verum end; consider A being Ordinal such that A2: S1[A] and A3: for C being Ordinal st S1[C] holds A c= C from ORDINAL1:sch_1(A1); ex B1 being with_bottom CLbasis of L1 st A = card B1 by A2; then reconsider A = A as Cardinal ; A4: now__::_thesis:_for_x_being_set_holds_ (_(_(_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_ x_in_y_)_implies_x_in_A_)_&_(_x_in_A_implies_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_ x_in_y_)_) let x be set ; ::_thesis: ( ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) ) thus ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) implies x in A ) by A2; ::_thesis: ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) assume A5: x in A ; ::_thesis: for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y let y be set ; ::_thesis: ( y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } implies x in y ) assume A6: y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; ::_thesis: x in y then ex B2 being 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; ::_thesis: verum end; [#] L1 is CLbasis of L1 by YELLOW15:25; then card ([#] L1) in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; hence meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal by A4, SETFAM_1:def_1; ::_thesis: verum end; end; :: deftheorem defines CLweight WAYBEL31:def_1_:_ for L1 being continuous sup-Semilattice holds CLweight L1 = meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; theorem Th1: :: WAYBEL31:1 for L1 being continuous sup-Semilattice for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1 proof let L1 be continuous sup-Semilattice; ::_thesis: for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1 let B1 be with_bottom CLbasis of L1; ::_thesis: CLweight L1 c= card B1 card B1 in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; hence CLweight L1 c= card B1 by SETFAM_1:3; ::_thesis: verum end; theorem Th2: :: WAYBEL31:2 for L1 being continuous sup-Semilattice ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 proof let L1 be continuous sup-Semilattice; ::_thesis: ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 defpred S1[ Ordinal] means \$1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; set X = { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; A1: ex A being Ordinal st S1[A] proof take card ([#] L1) ; ::_thesis: S1[ card ([#] L1)] [#] L1 is CLbasis of L1 by YELLOW15:25; hence S1[ card ([#] L1)] ; ::_thesis: verum end; consider A being Ordinal such that A2: S1[A] and A3: for C being Ordinal st S1[C] holds A c= C from ORDINAL1:sch_1(A1); consider B1 being with_bottom CLbasis of L1 such that A4: A = card B1 by A2; A5: now__::_thesis:_for_x_being_set_holds_ (_(_(_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_ x_in_y_)_implies_x_in_A_)_&_(_x_in_A_implies_for_y_being_set_st_y_in__{__(card_B2)_where_B2_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_ x_in_y_)_) let x be set ; ::_thesis: ( ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) ) thus ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) implies x in A ) by A2; ::_thesis: ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y ) assume A6: x in A ; ::_thesis: for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds x in y let y be set ; ::_thesis: ( y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } implies x in y ) assume A7: y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; ::_thesis: x in y then ex B2 being 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; ::_thesis: verum end; take B1 ; ::_thesis: card B1 = CLweight L1 [#] L1 is CLbasis of L1 by YELLOW15:25; then card ([#] L1) in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; hence card B1 = CLweight L1 by A4, A5, SETFAM_1:def_1; ::_thesis: verum end; theorem Th3: :: WAYBEL31:3 for L1 being lower-bounded algebraic LATTICE holds CLweight L1 = card the carrier of (CompactSublatt L1) proof let L1 be lower-bounded algebraic LATTICE; ::_thesis: CLweight L1 = card the carrier of (CompactSublatt L1) set CB = { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; the carrier of (CompactSublatt L1) is with_bottom CLbasis of L1 by WAYBEL23:71; then A1: card the carrier of (CompactSublatt L1) in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; then A2: meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } c= card the carrier of (CompactSublatt L1) by SETFAM_1:3; now__::_thesis:_for_X_being_set_st_X_in__{__(card_B1)_where_B1_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_ card_the_carrier_of_(CompactSublatt_L1)_c=_X let X be set ; ::_thesis: ( X in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } implies card the carrier of (CompactSublatt L1) c= X ) assume X in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; ::_thesis: card the carrier of (CompactSublatt L1) c= X then consider B1 being 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; ::_thesis: verum end; then card the carrier of (CompactSublatt L1) c= meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A1, SETFAM_1:5; hence CLweight L1 = card the carrier of (CompactSublatt L1) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th4: :: WAYBEL31:4 for T being non empty TopSpace for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T proof let T be non empty TopSpace; ::_thesis: for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T let L1 be continuous sup-Semilattice; ::_thesis: ( InclPoset the topology of T = L1 implies for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T ) assume A1: InclPoset the topology of T = L1 ; ::_thesis: for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T let B1 be with_bottom CLbasis of L1; ::_thesis: B1 is Basis of T 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 being Subset of T st A is open holds for p being Point of T st p in A holds ex a being Subset of T st ( a in B2 & p in a & a c= A ) proof let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex a being Subset of T st ( a in B2 & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of T st p in A holds ex a being Subset of T st ( a in B2 & p in a & a c= A ) 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; ::_thesis: ( p in A implies ex a being Subset of T st ( a in B2 & p in a & a c= A ) ) assume A3: p in A ; ::_thesis: ex a being Subset of T st ( a in B2 & p in a & a c= A ) A1 = sup ((waybelow A1) /\ B1) by WAYBEL23:def_7 .= union ((waybelow A1) /\ B1) by A1, YELLOW_1:22 ; then consider a being 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 = a as Subset of T ; take a ; ::_thesis: ( a in B2 & p in a & a c= A ) thus a in B2 by A5, XBOOLE_0:def_4; ::_thesis: ( p in a & a c= A ) thus p in a by A4; ::_thesis: a c= A 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 a c= A by A1, YELLOW_1:3; ::_thesis: verum end; B2 c= the topology of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B2 or x in the topology of T ) assume x in B2 ; ::_thesis: x in the topology of T then reconsider x1 = x as Element of L1 ; x1 in the carrier of L1 ; hence x in the topology of T by A1, YELLOW_1:1; ::_thesis: verum end; hence B1 is Basis of T by A2, YELLOW_9:32; ::_thesis: verum end; theorem Th5: :: WAYBEL31:5 for T being non empty TopSpace for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds for B1 being Basis of T for B2 being Subset of L1 st B1 = B2 holds finsups B2 is with_bottom CLbasis of L1 proof let T be non empty TopSpace; ::_thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds for B1 being Basis of T for B2 being Subset of L1 st B1 = B2 holds finsups B2 is with_bottom CLbasis of L1 let L1 be lower-bounded continuous LATTICE; ::_thesis: ( InclPoset the topology of T = L1 implies for B1 being Basis of T for B2 being Subset of L1 st B1 = B2 holds finsups B2 is with_bottom CLbasis of L1 ) assume A1: InclPoset the topology of T = L1 ; ::_thesis: for B1 being Basis of T for B2 being Subset of L1 st B1 = B2 holds finsups B2 is with_bottom CLbasis of L1 let B1 be Basis of T; ::_thesis: for B2 being Subset of L1 st B1 = B2 holds finsups B2 is with_bottom CLbasis of L1 let B2 be Subset of L1; ::_thesis: ( B1 = B2 implies finsups B2 is with_bottom CLbasis of L1 ) assume A2: B1 = B2 ; ::_thesis: finsups B2 is with_bottom CLbasis of L1 A3: for x, y being Element of L1 st not y <= x holds ex b being Element of L1 st ( b in finsups B2 & not b <= x & b <= y ) proof let x, y be Element of L1; ::_thesis: ( not y <= x implies ex b being Element of L1 st ( b in finsups B2 & not b <= x & b <= y ) ) 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 ; ::_thesis: ex b being Element of L1 st ( b in finsups B2 & not b <= x & b <= y ) then not y c= x by A1, YELLOW_1:3; then consider v being set such that A5: v in y and A6: not v in x by TARSKI:def_3; v in y1 by A5; then reconsider v = v as Point of T ; y1 is open by A4, PRE_TOPC:def_2; then consider b being 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 = b as Element of L1 by A2, A7; for z being set 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 ; ::_thesis: ( b in finsups B2 & not b <= x & b <= y ) ( ex_sup_of {b},L1 & b = "\/" ({b},L1) ) by YELLOW_0:38, YELLOW_0:39; then b in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A10; hence b in finsups B2 by WAYBEL_0:def_27; ::_thesis: ( not b <= x & b <= y ) not b c= x by A6, A8; hence not b <= x by A1, YELLOW_1:3; ::_thesis: b <= y thus b <= y by A1, A9, YELLOW_1:3; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_L1_st_x_in_finsups_B2_&_y_in_finsups_B2_holds_ sup_{x,y}_in_finsups_B2 let x, y be Element of L1; ::_thesis: ( x in finsups B2 & y in finsups B2 implies sup {x,y} in finsups B2 ) assume that A11: x in finsups B2 and A12: y in finsups B2 ; ::_thesis: sup {x,y} in finsups B2 y in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A12, WAYBEL_0:def_27; then consider Y2 being finite Subset of B2 such that A13: y = "\/" (Y2,L1) and A14: ex_sup_of Y2,L1 ; x in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } by A11, WAYBEL_0:def_27; then consider Y1 being 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 is 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; ::_thesis: verum end; then A17: finsups B2 is join-closed by WAYBEL23:18; ( {} c= B2 & ex_sup_of {} ,L1 ) by XBOOLE_1:2, YELLOW_0:42; then "\/" ({},L1) in { ("\/" (Y,L1)) where Y is finite Subset of B2 : ex_sup_of Y,L1 } ; then Bottom L1 in finsups B2 by WAYBEL_0:def_27; hence finsups B2 is with_bottom CLbasis of L1 by A17, A3, WAYBEL23:49, WAYBEL23:def_8; ::_thesis: verum end; theorem Th6: :: WAYBEL31:6 for T being non empty T_0 TopSpace for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds weight T = CLweight L1 proof let T be non empty T_0 TopSpace; ::_thesis: for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds weight T = CLweight L1 let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( InclPoset the topology of T = L1 & T is infinite implies weight T = CLweight L1 ) assume that A1: InclPoset the topology of T = L1 and A2: T is infinite ; ::_thesis: weight T = CLweight L1 A3: { (card B1) where B1 is Basis of T : verum } c= { (card B1) where B1 is with_bottom CLbasis of L1 : verum } proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (card B1) where B1 is Basis of T : verum } or b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ) assume b in { (card B1) where B1 is Basis of T : verum } ; ::_thesis: b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } then consider B2 being 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 b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A4, A5; ::_thesis: verum end; { (card B1) where B1 is with_bottom CLbasis of L1 : verum } c= { (card B1) where B1 is Basis of T : verum } proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } or b in { (card B1) where B1 is Basis of T : verum } ) assume b in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; ::_thesis: b in { (card B1) where B1 is Basis of T : verum } then consider B2 being with_bottom CLbasis of L1 such that A6: b = card B2 ; B2 is Basis of T by A1, Th4; hence b in { (card B1) where B1 is Basis of T : verum } by A6; ::_thesis: verum end; then { (card B1) where B1 is Basis of T : verum } = { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A3, XBOOLE_0:def_10; hence weight T = CLweight L1 by WAYBEL23:def_5; ::_thesis: verum end; theorem Th7: :: WAYBEL31:7 for T being non empty T_0 TopSpace for L1 being 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 non empty T_0 TopSpace; ::_thesis: for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds card the carrier of T c= card the carrier of L1 let L1 be continuous sup-Semilattice; ::_thesis: ( InclPoset the topology of T = L1 implies card the carrier of T c= card the carrier of L1 ) A1: card the carrier of T c= card the topology of T by YELLOW15:28; assume InclPoset the topology of T = L1 ; ::_thesis: card the carrier of T c= card the carrier of L1 hence card the carrier of T c= card the carrier of L1 by A1, YELLOW_1:1; ::_thesis: verum end; theorem Th8: :: WAYBEL31:8 for T being non empty T_0 TopSpace st T is finite holds weight T = card the carrier of T proof let T be non empty T_0 TopSpace; ::_thesis: ( T is finite implies weight T = card the carrier of T ) deffunc H1( set ) -> set = meet { A where A is Element of the topology of T : \$1 in A } ; A1: for x being set st x in the carrier of T holds H1(x) in the carrier of (BoolePoset the carrier of T) proof let x be set ; ::_thesis: ( x in the carrier of T implies H1(x) in the carrier of (BoolePoset the carrier of T) ) assume A2: x in the carrier of T ; ::_thesis: H1(x) in the carrier of (BoolePoset 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 is Element of the topology of T : x in A } by A2; then meet { A where A is Element of the topology of T : x in A } c= the carrier of T by SETFAM_1:3; then meet { A where A is Element of the topology of T : x in A } in bool the carrier of T ; hence H1(x) in the carrier of (BoolePoset the carrier of T) by WAYBEL_7:2; ::_thesis: verum end; consider f being Function of the carrier of T, the carrier of (BoolePoset the carrier of T) such that A3: for x being set st x in the carrier of T holds f . x = H1(x) from FUNCT_2:sch_2(A1); reconsider rf = rng f as Subset-Family of T by WAYBEL_7:2; A4: for A being Subset of T st A is open holds for p being Point of T st p in A holds ex a being Subset of T st ( a in rf & p in a & a c= A ) proof let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds ex a being Subset of T st ( a in rf & p in a & a c= A ) ) assume A is open ; ::_thesis: for p being Point of T st p in A holds ex a being Subset of T st ( a in rf & p in a & a c= A ) then A5: A in the topology of T by PRE_TOPC:def_2; let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st ( a in rf & p in a & a c= A ) ) assume p in A ; ::_thesis: ex a being Subset of T st ( a in rf & p in a & a c= A ) then A6: A in { C where C is Element of the topology of T : p in C } by A5; meet { C where C is Element of the topology of T : p in C } c= the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { C where C is Element of the topology of T : p in C } or z in the carrier of T ) assume z in meet { C where C is Element of the topology of T : p in C } ; ::_thesis: z in the carrier of T then z in A by A6, SETFAM_1:def_1; hence z in the carrier of T ; ::_thesis: verum end; then reconsider a = meet { C where C is Element of the topology of T : p in C } as Subset of T ; take a ; ::_thesis: ( a in rf & p in a & a c= 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; ::_thesis: ( p in a & a c= A ) now__::_thesis:_for_Y_being_set_st_Y_in__{__C_where_C_is_Element_of_the_topology_of_T_:_p_in_C__}__holds_ p_in_Y let Y be set ; ::_thesis: ( Y in { C where C is Element of the topology of T : p in C } implies p in Y ) assume Y in { C where C is Element of the topology of T : p in C } ; ::_thesis: p in Y then ex C being Element of the topology of T st ( Y = C & p in C ) ; hence p in Y ; ::_thesis: verum end; hence p in a by A6, SETFAM_1:def_1; ::_thesis: a c= A thus a c= A ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in a or z in A ) assume z in a ; ::_thesis: z in A hence z in A by A6, SETFAM_1:def_1; ::_thesis: verum end; end; assume A8: T is finite ; ::_thesis: weight T = card the carrier of T rf c= the topology of T proof reconsider tT = the topology of T as non empty finite set by A8; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rf or z in the topology of T ) deffunc H2( set ) -> set = \$1; assume z in rf ; ::_thesis: z in the topology of T then consider y being set such that A9: ( y in dom f & z = f . y ) by FUNCT_1:def_3; { A where A is Element of the topology of T : y in A } c= bool the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { A where A is Element of the topology of T : y in A } or z in bool the carrier of T ) assume z in { A where A is Element of the topology of T : y in A } ; ::_thesis: z in bool the carrier of T then ex A being Element of the topology of T st ( z = A & y in A ) ; hence z in bool the carrier of T ; ::_thesis: verum end; then reconsider sfA = { A where A is Element of the topology of T : y in A } as Subset-Family of T ; defpred S1[ set ] means y in \$1; reconsider sfA = sfA as Subset-Family of T ; now__::_thesis:_for_P_being_Subset_of_T_st_P_in_sfA_holds_ P_is_open let P be Subset of T; ::_thesis: ( P in sfA implies P is open ) assume P in sfA ; ::_thesis: P is open then ex A being Element of the topology of T st ( P = A & y in A ) ; hence P is open by PRE_TOPC:def_2; ::_thesis: verum end; then A10: sfA is open by TOPS_2:def_1; { H2(A) where A is Element of tT : S1[A] } is finite from PRE_CIRC:sch_1(); then A11: meet sfA is open by A10, TOPS_2:20; z = meet { A where A is Element of the topology of T : y in A } by A3, A9; hence z in the topology of T by A11, PRE_TOPC:def_2; ::_thesis: verum end; then rng f is Basis of T by A4, YELLOW_9:32; then A12: card (rng f) in { (card B1) where B1 is Basis of T : verum } ; then A13: meet { (card B1) where B1 is Basis of T : verum } c= card (rng f) by SETFAM_1:3; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ not_x1_<>_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies not x1 <> x2 ) assume that A14: ( x1 in dom f & x2 in dom f ) and A15: f . x1 = f . x2 ; ::_thesis: not x1 <> x2 reconsider x3 = x1, x4 = x2 as Point of T by A14; assume x1 <> x2 ; ::_thesis: contradiction then consider V being 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 is Element of the topology of T : x3 in A } & f . x4 = meet { A where A is Element of the topology of T : x4 in A } ) by A3; now__::_thesis:_contradiction percases ( ( x3 in V & not x4 in V ) or ( x4 in V & not x3 in V ) ) by A17; supposeA19: ( x3 in V & not x4 in V ) ; ::_thesis: contradiction V in the topology of T by A16, PRE_TOPC:def_2; then A20: V in { A where A is Element of the topology of T : x3 in A } by A19; A21: meet { A where A is Element of the topology of T : x3 in A } c= V proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { A where A is Element of the topology of T : x3 in A } or z in V ) assume z in meet { A where A is Element of the topology of T : x3 in A } ; ::_thesis: z in V hence z in V by A20, SETFAM_1:def_1; ::_thesis: verum end; A22: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Element_of_the_topology_of_T_:_x4_in_A__}__holds_ x4_in_Y let Y be set ; ::_thesis: ( Y in { A where A is Element of the topology of T : x4 in A } implies x4 in Y ) assume Y in { A where A is Element of the topology of T : x4 in A } ; ::_thesis: x4 in Y then ex A being Element of the topology of T st ( Y = A & x4 in A ) ; hence x4 in Y ; ::_thesis: verum end; the carrier of T in the topology of T by PRE_TOPC:def_1; then the carrier of T in { A where A is Element of the topology of T : x4 in A } ; then x4 in meet { A where A is Element of the topology of T : x3 in A } by A15, A18, A22, SETFAM_1:def_1; hence contradiction by A19, A21; ::_thesis: verum end; supposeA23: ( x4 in V & not x3 in V ) ; ::_thesis: contradiction V in the topology of T by A16, PRE_TOPC:def_2; then A24: V in { A where A is Element of the topology of T : x4 in A } by A23; A25: meet { A where A is Element of the topology of T : x4 in A } c= V proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet { A where A is Element of the topology of T : x4 in A } or z in V ) assume z in meet { A where A is Element of the topology of T : x4 in A } ; ::_thesis: z in V hence z in V by A24, SETFAM_1:def_1; ::_thesis: verum end; A26: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Element_of_the_topology_of_T_:_x3_in_A__}__holds_ x3_in_Y let Y be set ; ::_thesis: ( Y in { A where A is Element of the topology of T : x3 in A } implies x3 in Y ) assume Y in { A where A is Element of the topology of T : x3 in A } ; ::_thesis: x3 in Y then ex A being Element of the topology of T st ( Y = A & x3 in A ) ; hence x3 in Y ; ::_thesis: verum end; the carrier of T in the topology of T by PRE_TOPC:def_1; then the carrier of T in { A where A is Element of the topology of T : x3 in A } ; then x3 in meet { A where A is Element of the topology of T : x4 in A } by A15, A18, A26, SETFAM_1:def_1; hence contradiction by A23, A25; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; then ( dom f = the carrier of T & f is V13() ) 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 being set st X in { (card B1) where B1 is Basis of T : verum } holds card (rng f) c= X proof let X be set ; ::_thesis: ( X in { (card B1) where B1 is Basis of T : verum } implies card (rng f) c= X ) assume X in { (card B1) where B1 is Basis of T : verum } ; ::_thesis: card (rng f) c= X then consider B2 being Basis of T such that A28: X = card B2 ; rng f c= B2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in B2 ) assume y in rng f ; ::_thesis: y in B2 then consider x being set 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 is Element of the topology of T : x1 in A } by A3, A30; hence y in B2 by A8, YELLOW15:31; ::_thesis: verum end; hence card (rng f) c= X by A28, CARD_1:11; ::_thesis: verum end; then card (rng f) c= meet { (card B1) where B1 is Basis of T : verum } by A12, SETFAM_1:5; then card (rng f) = meet { (card B1) where B1 is Basis of T : verum } by A13, XBOOLE_0:def_10 .= weight T by WAYBEL23:def_5 ; hence weight T = card the carrier of T by A27, CARD_1:5; ::_thesis: verum end; theorem Th9: :: WAYBEL31:9 for T being TopStruct for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds CLweight L1 = card the carrier of L1 proof let T be TopStruct ; ::_thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds CLweight L1 = card the carrier of L1 let L1 be lower-bounded continuous LATTICE; ::_thesis: ( InclPoset the topology of T = L1 & T is finite implies CLweight L1 = card the carrier of L1 ) assume A1: InclPoset the topology of T = L1 ; ::_thesis: ( not T is finite or CLweight L1 = card the carrier of L1 ) [#] L1 is with_bottom CLbasis of L1 by YELLOW15:25; then A2: card the carrier of L1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; A3: CLweight L1 c= card the carrier of L1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in CLweight L1 or z in card the carrier of L1 ) assume z in CLweight L1 ; ::_thesis: z in card the carrier of L1 hence z in card the carrier of L1 by A2, SETFAM_1:def_1; ::_thesis: verum end; assume A4: T is finite ; ::_thesis: CLweight L1 = card the carrier of L1 now__::_thesis:_for_Z_being_set_st_Z_in__{__(card_B1)_where_B1_is_with_bottom_CLbasis_of_L1_:_verum__}__holds_ card_the_carrier_of_L1_c=_Z let Z be set ; ::_thesis: ( Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } implies card the carrier of L1 c= Z ) assume Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; ::_thesis: card the carrier of L1 c= Z then consider B1 being 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; ::_thesis: verum end; then card the carrier of L1 c= meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A2, SETFAM_1:5; hence CLweight L1 = card the carrier of L1 by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th10: :: WAYBEL31:10 for L1 being lower-bounded continuous sup-Semilattice for T1 being Scott TopAugmentation of L1 for T2 being correct Lawson TopAugmentation of L1 for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T1 being Scott TopAugmentation of L1 for T2 being correct Lawson TopAugmentation of L1 for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being correct Lawson TopAugmentation of L1 for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 let T2 be correct Lawson TopAugmentation of L1; ::_thesis: for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 let B2 be Basis of T2; ::_thesis: { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 A1: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) & RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) ) by YELLOW_9:def_4; { (uparrow V) where V is Subset of T2 : V in B2 } c= bool the carrier of T1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow V) where V is Subset of T2 : V in B2 } or z in bool the carrier of T1 ) assume z in { (uparrow V) where V is Subset of T2 : V in B2 } ; ::_thesis: z in bool the carrier of T1 then ex V being Subset of T2 st ( z = uparrow V & V in B2 ) ; hence z in bool the carrier of T1 by A1; ::_thesis: verum end; then reconsider upV = { (uparrow V) where V is Subset of T2 : V in B2 } as Subset-Family of T1 ; reconsider upV = upV as Subset-Family of T1 ; A2: the topology of T1 c= UniCl upV proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the topology of T1 or z in UniCl upV ) assume A3: z in the topology of T1 ; ::_thesis: z in UniCl upV 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 is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the carrier of T1 proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } or v in bool the carrier of T1 ) assume v in { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } ; ::_thesis: v in bool the carrier of T1 then ex G being Subset of T2 st ( v = uparrow G & G in B2 & G c= z1 ) ; hence v in bool the carrier of T1 by A1; ::_thesis: verum end; then reconsider Y = { (uparrow G) where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ; { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } c= bool the carrier of T1 proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } or v in bool the carrier of T1 ) assume v in { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } ; ::_thesis: v in bool the carrier of T1 then ex G being Subset of T2 st ( v = G & G in B2 & G c= z1 ) ; hence v in bool the carrier of T1 by A1; ::_thesis: verum end; then reconsider Y1 = { G where G is Subset of T2 : ( G in B2 & G c= z1 ) } as Subset-Family of T1 ; defpred S1[ set ] means ( \$1 in B2 & \$1 c= z1 ); reconsider Y = Y as Subset-Family of T1 ; reconsider Y1 = Y1 as Subset-Family of T1 ; reconsider Y3 = Y1 as Subset-Family of T2 by A1; A6: Y c= upV proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Y or v in upV ) assume v in Y ; ::_thesis: v in upV then ex G being Subset of T2 st ( v = uparrow G & G in B2 & G c= z1 ) ; hence v in upV ; ::_thesis: verum end; A7: for S being Subset-Family of T2 st S = { X where X is Subset of T2 : S1[X] } holds uparrow (union S) = union { (uparrow X) where X is Subset of T2 : S1[X] } from WAYBEL31:sch_1(); 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 z in UniCl upV by A6, CANTOR_1:def_1; ::_thesis: verum end; upV c= the topology of T1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in upV or z in the topology of T1 ) assume z in upV ; ::_thesis: z in the topology of T1 then consider V being 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 z in the topology of T1 by A8, WAYBEL14:23; ::_thesis: verum end; hence { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1 by A2, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum end; Lm1: for L1 being lower-bounded continuous sup-Semilattice for T1 being Scott TopAugmentation of L1 for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2 proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T1 being Scott TopAugmentation of L1 for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2 let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2 let T2 be correct Lawson TopAugmentation of L1; ::_thesis: weight T1 c= weight T2 consider B1 being Basis of T2 such that A1: card B1 = weight T2 by WAYBEL23:74; defpred S1[ set , set ] means ex y being Subset of T2 st ( y = \$1 & \$2 = uparrow y ); A2: for x being set st x in B1 holds ex z being set st S1[x,z] proof let x be set ; ::_thesis: ( x in B1 implies ex z being set st S1[x,z] ) assume x in B1 ; ::_thesis: ex z being set st S1[x,z] then reconsider y = x as Subset of T2 ; take uparrow y ; ::_thesis: S1[x, uparrow y] take y ; ::_thesis: ( y = x & uparrow y = uparrow y ) thus ( y = x & uparrow y = uparrow y ) ; ::_thesis: verum end; consider f being Function such that A3: dom f = B1 and A4: for x being set st x in B1 holds S1[x,f . x] from CLASSES1:sch_1(A2); { (uparrow V) where V is Subset of T2 : V in B1 } c= rng f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow V) where V is Subset of T2 : V in B1 } or z in rng f ) assume z in { (uparrow V) where V is Subset of T2 : V in B1 } ; ::_thesis: z in rng f then consider V being Subset of T2 such that A5: z = uparrow V and A6: V in B1 ; ex V1 being Subset of T2 st ( V1 = V & f . V = uparrow V1 ) by A4, A6; hence z in rng f by A3, A5, A6, FUNCT_1:def_3; ::_thesis: verum end; then A7: card { (uparrow V) where V is Subset of T2 : V in B1 } c= card B1 by A3, CARD_1:12; { (uparrow V) where V is Subset of T2 : V in B1 } is Basis of T1 by Th10; then card { (uparrow V) where V is Subset of T2 : V in B1 } in { (card B2) where B2 is Basis of T1 : verum } ; then meet { (card B2) where B2 is Basis of T1 : verum } c= card { (uparrow V) where V is Subset of T2 : V in B1 } by SETFAM_1:3; then meet { (card B2) where B2 is Basis of T1 : verum } c= card B1 by A7, XBOOLE_1:1; hence weight T1 c= weight T2 by A1, WAYBEL23:def_5; ::_thesis: verum end; theorem Th11: :: WAYBEL31:11 for L1 being non empty up-complete Poset st L1 is finite holds for x being Element of L1 holds x in compactbelow x proof let L1 be non empty up-complete Poset; ::_thesis: ( L1 is finite implies for x being Element of L1 holds x in compactbelow x ) assume A1: L1 is finite ; ::_thesis: for x being Element of L1 holds x in compactbelow x let x be Element of L1; ::_thesis: x in compactbelow x A2: x <= x ; x is compact by A1, WAYBEL_3:17; hence x in compactbelow x by A2; ::_thesis: verum end; theorem Th12: :: WAYBEL31:12 for L1 being finite LATTICE holds L1 is arithmetic proof let L1 be finite LATTICE; ::_thesis: L1 is arithmetic thus for x being Element of L1 holds ( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def_4,WAYBEL_8:def_5 ::_thesis: ( L1 is up-complete & L1 is satisfying_axiom_K & CompactSublatt L1 is meet-inheriting ) thus L1 is up-complete ; ::_thesis: ( L1 is satisfying_axiom_K & CompactSublatt L1 is meet-inheriting ) thus L1 is satisfying_axiom_K ::_thesis: CompactSublatt L1 is meet-inheriting proof let x be Element of L1; :: according to WAYBEL_8:def_3 ::_thesis: x = "\/" ((compactbelow x),L1) A1: now__::_thesis:_for_y_being_Element_of_L1_st_y_is_>=_than_compactbelow_x_holds_ x_<=_y let y be Element of L1; ::_thesis: ( y is_>=_than compactbelow x implies x <= y ) assume A2: y is_>=_than compactbelow x ; ::_thesis: x <= y x in compactbelow x by Th11; hence x <= y by A2, LATTICE3:def_9; ::_thesis: verum end; for y being 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 x = "\/" ((compactbelow x),L1) by A1, YELLOW_0:30; ::_thesis: verum end; thus CompactSublatt L1 is meet-inheriting ::_thesis: verum proof let x, y be Element of L1; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (CompactSublatt L1) or not y in the carrier of (CompactSublatt L1) or not ex_inf_of {x,y},L1 or "/\" ({x,y},L1) in the carrier of (CompactSublatt 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 ; ::_thesis: "/\" ({x,y},L1) in the carrier of (CompactSublatt L1) x "/\" y is compact by WAYBEL_3:17; then x "/\" y in the carrier of (CompactSublatt L1) by WAYBEL_8:def_1; hence "/\" ({x,y},L1) in the carrier of (CompactSublatt L1) by YELLOW_0:40; ::_thesis: verum end; end; registration cluster finite reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ; coherence for b1 being LATTICE st b1 is finite holds b1 is arithmetic by Th12; end; registration cluster finite 1 -element strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima for RelStr ; existence ex b1 being RelStr st ( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is lower-bounded & b1 is 1 -element & b1 is finite & b1 is strict ) 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 ; ::_thesis: ( T is reflexive & T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict ) thus T is reflexive ::_thesis: ( T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict ) proof let x be Element of T; :: according to YELLOW_0:def_1 ::_thesis: x <= x x = 0 by TARSKI:def_1; then [x,x] in {[0,0]} by TARSKI:def_1; hence x <= x by ORDERS_2:def_5; ::_thesis: verum end; then reconsider T9 = T as 1 -element reflexive RelStr ; reconsider T99 = T9 as LATTICE ; T9 is transitive ; hence T is transitive ; ::_thesis: ( T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict ) T9 is antisymmetric ; hence T is antisymmetric ; ::_thesis: ( T is with_suprema & T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict ) T9 is with_suprema ; hence T is with_suprema ; ::_thesis: ( T is with_infima & T is lower-bounded & T is 1 -element & T is finite & T is strict ) T9 is with_infima ; hence T is with_infima ; ::_thesis: ( T is lower-bounded & T is 1 -element & T is finite & T is strict ) T99 is lower-bounded ; hence T is lower-bounded ; ::_thesis: ( T is 1 -element & T is finite & T is strict ) thus T is 1 -element ; ::_thesis: ( T is finite & T is strict ) thus T is finite ; ::_thesis: T is strict thus T is strict ; ::_thesis: verum end; end; theorem Th13: :: WAYBEL31:13 for L1 being finite LATTICE for B1 being with_bottom CLbasis of L1 holds ( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) ) proof let L1 be finite LATTICE; ::_thesis: for B1 being with_bottom CLbasis of L1 holds ( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) ) let B1 be with_bottom CLbasis of L1; ::_thesis: ( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) ) thus ( card B1 = CLweight L1 implies B1 = the carrier of (CompactSublatt L1) ) ::_thesis: ( B1 = the carrier of (CompactSublatt L1) implies card B1 = CLweight L1 ) proof assume card B1 = CLweight L1 ; ::_thesis: B1 = the carrier of (CompactSublatt L1) then A1: card the carrier of (CompactSublatt L1) = card B1 by Th3; the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:71; hence B1 = the carrier of (CompactSublatt L1) by A1, PRE_POLY:8; ::_thesis: verum end; assume B1 = the carrier of (CompactSublatt L1) ; ::_thesis: card B1 = CLweight L1 hence card B1 = CLweight L1 by Th3; ::_thesis: verum end; definition let L1 be non empty reflexive RelStr ; let A be Subset of L1; let a be Element of L1; func Way_Up (a,A) -> Subset of L1 equals :: WAYBEL31:def 2 (wayabove a) \ (uparrow A); coherence (wayabove a) \ (uparrow A) is Subset of L1 ; end; :: deftheorem defines Way_Up WAYBEL31:def_2_:_ for L1 being non empty reflexive RelStr for A being Subset of L1 for a being Element of L1 holds Way_Up (a,A) = (wayabove a) \ (uparrow A); theorem :: WAYBEL31:14 for L1 being non empty reflexive RelStr for a being Element of L1 holds Way_Up (a,({} L1)) = wayabove a ; theorem :: WAYBEL31:15 for L1 being non empty Poset for A being Subset of L1 for a being Element of L1 st a in uparrow A holds Way_Up (a,A) = {} proof let L1 be non empty Poset; ::_thesis: for A being Subset of L1 for a being Element of L1 st a in uparrow A holds Way_Up (a,A) = {} let A be Subset of L1; ::_thesis: for a being Element of L1 st a in uparrow A holds Way_Up (a,A) = {} let a be Element of L1; ::_thesis: ( a in uparrow A implies Way_Up (a,A) = {} ) assume A1: a in uparrow A ; ::_thesis: Way_Up (a,A) = {} wayabove a c= uparrow A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in wayabove a or z in uparrow A ) assume A2: z in wayabove a ; ::_thesis: z in uparrow A then reconsider z1 = z as Element of L1 ; a << z1 by A2, WAYBEL_3:8; then a <= z1 by WAYBEL_3:1; hence z in uparrow A by A1, WAYBEL_0:def_20; ::_thesis: verum end; hence Way_Up (a,A) = {} by XBOOLE_1:37; ::_thesis: verum end; theorem Th16: :: WAYBEL31:16 for L1 being non empty finite reflexive transitive RelStr holds Ids L1 is finite proof deffunc H1( set ) -> set = \$1; let L1 be non empty finite reflexive transitive RelStr ; ::_thesis: Ids L1 is finite reconsider Y = bool the carrier of L1 as non empty finite set ; A1: { X where X is Ideal of L1 : verum } c= { X where X is Element of Y : X is Ideal of L1 } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { X where X is Ideal of L1 : verum } or z in { X where X is Element of Y : X is Ideal of L1 } ) assume z in { X where X is Ideal of L1 : verum } ; ::_thesis: z in { X where X is Element of Y : X is Ideal of L1 } then ex X1 being Ideal of L1 st z = X1 ; hence z in { X where X is Element of Y : X is Ideal of L1 } ; ::_thesis: verum end; defpred S1[ set ] means \$1 is Ideal of L1; A2: { X where X is Element of Y : X is Ideal of L1 } c= { X where X is Ideal of L1 : verum } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { X where X is Element of Y : X is Ideal of L1 } or z in { X where X is Ideal of L1 : verum } ) assume z in { X where X is Element of Y : X is Ideal of L1 } ; ::_thesis: z in { X where X is Ideal of L1 : verum } then ex X1 being Element of Y st ( z = X1 & X1 is Ideal of L1 ) ; hence z in { X where X is Ideal of L1 : verum } ; ::_thesis: verum end; A3: { H1(X) where X is Element of Y : S1[X] } is finite from PRE_CIRC:sch_1(); Ids L1 = { X where X is Ideal of L1 : verum } by WAYBEL_0:def_23 .= { X where X is Element of Y : X is Ideal of L1 } by A1, A2, XBOOLE_0:def_10 ; hence Ids L1 is finite by A3; ::_thesis: verum end; theorem Th17: :: WAYBEL31:17 for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds for B1 being with_bottom CLbasis of L1 holds B1 is infinite proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( L1 is infinite implies for B1 being with_bottom CLbasis of L1 holds B1 is infinite ) assume A1: L1 is infinite ; ::_thesis: for B1 being with_bottom CLbasis of L1 holds B1 is infinite let B1 be with_bottom CLbasis of L1; ::_thesis: B1 is infinite ( 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 B1 is infinite by YELLOW_0:def_15; ::_thesis: verum end; theorem :: WAYBEL31:18 for L1 being non empty complete Poset for x being Element of L1 st x is compact holds x = inf (wayabove x) proof let L1 be non empty complete Poset; ::_thesis: for x being Element of L1 st x is compact holds x = inf (wayabove x) let x be Element of L1; ::_thesis: ( x is compact implies x = inf (wayabove x) ) assume x is compact ; ::_thesis: x = inf (wayabove x) 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 x = inf (wayabove x) by A1, YELLOW_0:def_3; ::_thesis: verum end; theorem Th19: :: WAYBEL31:19 for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( L1 is infinite implies for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 ) assume A1: L1 is infinite ; ::_thesis: for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 let B1 be with_bottom CLbasis of L1; ::_thesis: card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 consider a1 being set such that A2: a1 in B1 by XBOOLE_0:def_1; reconsider a1 = a1 as Element of L1 by A2; {} L1 c= B1 by XBOOLE_1:2; then Way_Up (a1,({} L1)) in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } by A2; then reconsider WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as non empty set ; defpred S1[ Element of B1 * , set ] means ex y being Element of L1 ex z being Subset of L1 st ( y = \$1 /. 1 & z = rng (Del (\$1,1)) & \$2 = Way_Up (y,z) ); A3: for x being Element of B1 * ex u being Element of WU st S1[x,u] proof let x be Element of B1 * ; ::_thesis: ex u being Element of WU st S1[x,u] 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 is Element of L1, A is 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 ; ::_thesis: S1[x,u] take y ; ::_thesis: ex z being Subset of L1 st ( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) ) take z ; ::_thesis: ( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) ) thus ( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) ) ; ::_thesis: verum end; consider f being Function of (B1 *),WU such that A5: for x being Element of B1 * holds S1[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 set ; :: according to TARSKI:def_3 ::_thesis: ( not z in WU or z in rng f ) assume z in WU ; ::_thesis: z in rng f then consider a being Element of L1, A being 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 being FinSequence such that A11: A = rng p by FINSEQ_1:52; reconsider p = p as FinSequence of B1 by A10, A11, FINSEQ_1:def_4; set q = <*a1*> ^ p; A12: <*a1*> ^ p in B1 * by FINSEQ_1:def_11; then consider y being Element of L1, v being Subset of L1 such that A13: y = (<*a1*> ^ p) /. 1 and A14: v = rng (Del ((<*a1*> ^ p),1)) and A15: f . (<*a1*> ^ p) = Way_Up (y,v) by A5; A16: a = y by A13, FINSEQ_5:15; A = v by A11, A14, WSIERP_1:40; hence z in rng f by A6, A8, A12, A15, A16, FUNCT_1:def_3; ::_thesis: verum end; B1 is infinite by A1, Th17; then card B1 = card (B1 *) by CARD_4:24; hence card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 by A6, A7, CARD_1:12; ::_thesis: verum end; theorem Th20: :: WAYBEL31:20 for T being complete Lawson TopLattice for X being finite Subset of T holds ( (uparrow X) ` is open & (downarrow X) ` is open ) proof let T be complete Lawson TopLattice; ::_thesis: for X being finite Subset of T holds ( (uparrow X) ` is open & (downarrow X) ` is open ) let X be finite Subset of T; ::_thesis: ( (uparrow X) ` is open & (downarrow X) ` is open ) deffunc H1( Element of T) -> Element of K32( the carrier of T) = uparrow \$1; { (uparrow x) where x is Element of T : x in X } c= bool the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow x) where x is Element of T : x in X } or z in bool the carrier of T ) assume z in { (uparrow x) where x is Element of T : x in X } ; ::_thesis: z in bool the carrier of T then ex x being Element of T st ( z = uparrow x & x in X ) ; hence z in bool the carrier of T ; ::_thesis: verum end; then reconsider upx = { (uparrow x) where x is Element of T : x in X } as Subset-Family of T ; { (downarrow x) where x is Element of T : x in X } c= bool the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (downarrow x) where x is Element of T : x in X } or z in bool the carrier of T ) assume z in { (downarrow x) where x is Element of T : x in X } ; ::_thesis: z in bool the carrier of T then ex x being Element of T st ( z = downarrow x & x in X ) ; hence z in bool the carrier of T ; ::_thesis: verum end; then reconsider dox = { (downarrow x) where x is Element of T : x in X } as Subset-Family of T ; reconsider dox = dox as Subset-Family of T ; reconsider upx = upx as Subset-Family of T ; A1: uparrow X = union upx by YELLOW_9:4; now__::_thesis:_for_P_being_Subset_of_T_st_P_in_upx_holds_ P_is_closed let P be Subset of T; ::_thesis: ( P in upx implies P is closed ) assume P in upx ; ::_thesis: P is closed then ex x being Element of T st ( P = uparrow x & x in X ) ; hence P is closed by WAYBEL19:38; ::_thesis: verum end; then A2: upx is closed by TOPS_2:def_2; A3: X is finite ; { H1(x) where x is 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; ::_thesis: (downarrow X) ` is open deffunc H2( Element of T) -> Element of K32( the carrier of T) = downarrow \$1; A4: downarrow X = union dox by YELLOW_9:4; now__::_thesis:_for_P_being_Subset_of_T_st_P_in_dox_holds_ P_is_closed let P be Subset of T; ::_thesis: ( P in dox implies P is closed ) assume P in dox ; ::_thesis: P is closed then ex x being Element of T st ( P = downarrow x & x in X ) ; hence P is closed by WAYBEL19:38; ::_thesis: verum end; then A5: dox is closed by TOPS_2:def_2; { H2(x) where x is 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 (downarrow X) ` is open by TOPS_1:3; ::_thesis: verum end; theorem Th21: :: WAYBEL31:21 for L1 being lower-bounded continuous sup-Semilattice for T being correct Lawson TopAugmentation of L1 for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being correct Lawson TopAugmentation of L1 for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T let T be correct Lawson TopAugmentation of L1; ::_thesis: for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T let B1 be with_bottom CLbasis of L1; ::_thesis: { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= bool the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } or z in bool the carrier of T ) assume z in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } ; ::_thesis: z in bool the carrier of T then ex a being Element of L1 ex A being finite Subset of L1 st ( z = Way_Up (a,A) & a in B1 & A c= B1 ) ; hence z in bool the carrier of T by A1; ::_thesis: verum end; then reconsider WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as Subset-Family of T ; reconsider WU = WU as Subset-Family of T ; A2: now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_ for_pT_being_Point_of_T_st_pT_in_A_holds_ ex_cT_being_Subset_of_T_st_ (_cT_in_WU_&_pT_in_cT_&_cT_c=_A_) reconsider BL = { (W \ (uparrow F)) where W, F is 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; ::_thesis: ( A is open implies for pT being Point of T st pT in A holds ex cT being Subset of T st ( cT in WU & pT in cT & cT c= A ) ) assume A3: A is open ; ::_thesis: for pT being Point of T st pT in A holds ex cT being Subset of T st ( cT in WU & pT in cT & cT c= A ) let pT be Point of T; ::_thesis: ( pT in A implies ex cT being Subset of T st ( cT in WU & pT in cT & cT c= A ) ) assume pT in A ; ::_thesis: ex cT being Subset of T st ( cT in WU & pT in cT & cT c= A ) then consider a being 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 being Subset of T such that A7: a = W \ (uparrow FT) and A8: W in sigma T and A9: FT is finite by A4; A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider pS = pT as Element of the Scott TopAugmentation of T ; reconsider W1 = W as Subset of the Scott TopAugmentation of T by A10; sigma the Scott TopAugmentation of T = sigma T by A10, YELLOW_9:52; then A11: W = union { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 } by A8, WAYBEL14:33; reconsider pL = pS as Element of L1 by A1; defpred S1[ set , set ] means ex b1, y1 being 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 being set such that A13: pT in k and A14: k in { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 } by A11, TARSKI:def_4; consider xS being Element of the Scott TopAugmentation of T 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 being 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 being set st y in FL holds ex b being set st S1[y,b] proof let y be set ; ::_thesis: ( y in FL implies ex b being set st S1[y,b] ) assume A23: y in FL ; ::_thesis: ex b being set st S1[y,b] then reconsider y1 = y as Element of L1 ; not y1 <= pL by A21, A20, A23, WAYBEL_0:def_16; then consider b1 being Element of L1 such that A24: ( b1 in B1 & not b1 <= pL & b1 << y1 ) by WAYBEL23:46; reconsider b = b1 as set ; take b ; ::_thesis: S1[y,b] take b1 ; ::_thesis: ex y1 being Element of L1 st ( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 ) take y1 ; ::_thesis: ( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 ) thus ( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 ) by A24; ::_thesis: verum end; consider f being Function such that A25: dom f = FL and A26: for y being set st y in FL holds S1[y,f . y] from CLASSES1:sch_1(A22); rng f c= the carrier of L1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in the carrier of L1 ) assume z in rng f ; ::_thesis: z in the carrier of L1 then consider v being set such that A27: v in dom f and A28: z = f . v by FUNCT_1:def_3; ex b1, y1 being Element of L1 st ( y1 = v & b1 = f . v & b1 in B1 & not b1 <= pL & b1 << y1 ) by A25, A26, A27; hence z in the carrier of L1 by A28; ::_thesis: verum end; then reconsider FFL = rng f as Subset of L1 ; A29: FFL c= B1 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in FFL or z in B1 ) assume z in FFL ; ::_thesis: z in B1 then consider v being set such that A30: v in dom f and A31: z = f . v by FUNCT_1:def_3; ex b1, y1 being Element of L1 st ( y1 = v & b1 = f . v & b1 in B1 & not b1 <= pL & b1 << y1 ) by A25, A26, A30; hence z in B1 by A31; ::_thesis: verum end; A32: uparrow FL c= uparrow FFL proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow FL or z in uparrow FFL ) assume A33: z in uparrow FL ; ::_thesis: z in uparrow FFL then reconsider z1 = z as Element of L1 ; consider v1 being Element of L1 such that A34: v1 <= z1 and A35: v1 in FL by A33, WAYBEL_0:def_16; consider b1, y1 being 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 z in uparrow FFL by A39, WAYBEL_0:def_16; ::_thesis: verum end; reconsider cT = (wayabove bL) \ (uparrow FFL) as Subset of T by A1; take cT = cT; ::_thesis: ( cT in WU & pT in cT & cT c= A ) ( cT = Way_Up (bL,FFL) & FFL is finite ) by A9, A25, FINSET_1:8; hence cT in WU by A17, A29; ::_thesis: ( pT in cT & cT c= A ) 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 being Element of L1 holds ( not z in FFL or not z <= pL ) proof let z be Element of L1; ::_thesis: ( not z in FFL or not z <= pL ) assume z in FFL ; ::_thesis: not z <= pL then consider v being set such that A41: v in dom f and A42: z = f . v by FUNCT_1:def_3; ex b1, y1 being Element of L1 st ( y1 = v & b1 = f . v & b1 in B1 & not b1 <= pL & b1 << y1 ) by A25, A26, A41; hence not z <= pL by A42; ::_thesis: verum end; then for z being 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; ::_thesis: cT c= A wayabove xL c= W proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in wayabove xL or z in W ) wayabove xL = wayabove xS by A1, A10, YELLOW12:13; then A44: wayabove xL in { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 } by A16; assume z in wayabove xL ; ::_thesis: z in W hence z in W by A11, A44, TARSKI:def_4; ::_thesis: verum end; then (wayabove xL) \ (uparrow FL) c= a by A7, A20, XBOOLE_1:33; then (wayabove bL) \ (uparrow FFL) c= a by A40, XBOOLE_1:1; hence cT c= A by A6, XBOOLE_1:1; ::_thesis: verum end; WU c= the topology of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in WU or z in the topology of T ) assume z in WU ; ::_thesis: z in the topology of T then consider a being Element of L1, A being 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 z in the topology of T by A46, PRE_TOPC:def_2; ::_thesis: verum end; hence { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T by A2, YELLOW_9:32; ::_thesis: verum end; Lm2: for L1 being lower-bounded continuous sup-Semilattice for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1 proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1 let T be correct Lawson TopAugmentation of L1; ::_thesis: weight T c= CLweight L1 consider B1 being with_bottom CLbasis of L1 such that A1: card B1 = CLweight L1 by Th2; A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4; now__::_thesis:_weight_T_c=_CLweight_L1 percases ( L1 is finite or L1 is infinite ) ; supposeA3: L1 is finite ; ::_thesis: weight T c= CLweight L1 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 weight T c= CLweight L1 by A2, A1, A4, Th8; ::_thesis: verum end; supposeA5: L1 is infinite ; ::_thesis: weight T c= CLweight L1 set WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } ; { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T by Th21; then A6: weight T c= card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } by WAYBEL23:73; card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= CLweight L1 by A1, A5, Th19; hence weight T c= CLweight L1 by A6, XBOOLE_1:1; ::_thesis: verum end; end; end; hence weight T c= CLweight L1 ; ::_thesis: verum end; theorem Th22: :: WAYBEL31:22 for L1 being lower-bounded continuous sup-Semilattice for T being Scott TopAugmentation of L1 for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1 for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T let T be Scott TopAugmentation of L1; ::_thesis: for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T let b be Basis of T; ::_thesis: { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T set b2 = { (wayabove (inf u)) where u is Subset of T : u in b } ; { (wayabove (inf u)) where u is Subset of T : u in b } c= bool the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (wayabove (inf u)) where u is Subset of T : u in b } or z in bool the carrier of T ) assume z in { (wayabove (inf u)) where u is Subset of T : u in b } ; ::_thesis: z in bool the carrier of T then ex u being Subset of T st ( z = wayabove (inf u) & u in b ) ; hence z in bool the carrier of T ; ::_thesis: verum end; then reconsider b2 = { (wayabove (inf u)) where u is Subset of T : u in b } as Subset-Family of T ; reconsider b1 = { (wayabove x) where x is Element of T : verum } as Basis of T by WAYBEL11:45; A1: now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_ for_a_being_Point_of_T_st_a_in_A_holds_ ex_u_being_Element_of_K32(_the_carrier_of_T)_st_ (_u_in_b2_&_a_in_u_&_u_c=_A_) let A be Subset of T; ::_thesis: ( A is open implies for a being Point of T st a in A holds ex u being Element of K32( the carrier of T) st ( u in b2 & a in u & u c= A ) ) assume A2: A is open ; ::_thesis: for a being Point of T st a in A holds ex u being Element of K32( the carrier of T) st ( u in b2 & a in u & u c= A ) let a be Point of T; ::_thesis: ( a in A implies ex u being Element of K32( the carrier of T) st ( u in b2 & a in u & u c= A ) ) assume a in A ; ::_thesis: ex u being Element of K32( the carrier of T) st ( u in b2 & a in u & u c= A ) then consider C being 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 being 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 being 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 being Element of T such that A12: E = wayabove z by A9; take u = wayabove (inf D); ::_thesis: ( u in b2 & a in u & u c= A ) thus u in b2 by A6; ::_thesis: ( a in u & u c= A ) reconsider a1 = a as Element of T ; consider x being Element of T such that A13: C = wayabove x by A3; z << a1 by A10, A12, WAYBEL_3:8; then consider y being 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; ::_thesis: u c= A 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, XBOOLE_1:1; ::_thesis: verum end; b2 c= the topology of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in b2 or z in the topology of T ) assume z in b2 ; ::_thesis: z in the topology of T then consider u being Subset of T such that A17: z = wayabove (inf u) and u in b ; wayabove (inf u) is open by WAYBEL11:36; hence z in the topology of T by A17, PRE_TOPC:def_2; ::_thesis: verum end; hence { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T by A1, YELLOW_9:32; ::_thesis: verum end; theorem Th23: :: WAYBEL31:23 for L1 being lower-bounded continuous sup-Semilattice for T being Scott TopAugmentation of L1 for B1 being Basis of T st B1 is infinite holds { (inf u) where u is Subset of T : u in B1 } is infinite proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1 for B1 being Basis of T st B1 is infinite holds { (inf u) where u is Subset of T : u in B1 } is infinite let T be Scott TopAugmentation of L1; ::_thesis: for B1 being Basis of T st B1 is infinite holds { (inf u) where u is Subset of T : u in B1 } is infinite let B1 be Basis of T; ::_thesis: ( B1 is infinite implies { (inf u) where u is Subset of T : u in B1 } is infinite ) reconsider B2 = { (inf u) where u is Subset of T : u in B1 } as set ; defpred S1[ set , set ] means ex y being Element of T st ( \$1 = y & \$2 = wayabove y ); reconsider B3 = { (wayabove (inf u)) where u is Subset of T : u in B1 } as Basis of T by Th22; assume that A1: B1 is infinite and A2: { (inf u) where u is Subset of T : u in B1 } is finite ; ::_thesis: contradiction A3: for x being set st x in B2 holds ex y being set st ( y in B3 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in B2 implies ex y being set st ( y in B3 & S1[x,y] ) ) assume x in B2 ; ::_thesis: ex y being set st ( y in B3 & S1[x,y] ) then A4: ex u1 being Subset of T st ( x = inf u1 & u1 in B1 ) ; then reconsider z = x as Element of T ; take y = wayabove z; ::_thesis: ( y in B3 & S1[x,y] ) thus y in B3 by A4; ::_thesis: S1[x,y] take z ; ::_thesis: ( x = z & y = wayabove z ) thus ( x = z & y = wayabove z ) ; ::_thesis: verum end; consider f being Function such that A5: dom f = B2 and A6: rng f c= B3 and A7: for x being set st x in B2 holds S1[x,f . x] from FUNCT_1:sch_5(A3); B3 c= rng f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B3 or z in rng f ) assume z in B3 ; ::_thesis: z in rng f then consider u1 being 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 being Element of T st ( inf u1 = y & f . (inf u1) = wayabove y ) by A7; inf u1 in B2 by A9; hence z in rng f by A5, A8, A10, FUNCT_1:def_3; ::_thesis: verum 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; ::_thesis: verum end; Lm3: for L1 being lower-bounded continuous sup-Semilattice for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T let T be Scott TopAugmentation of L1; ::_thesis: CLweight L1 c= weight T consider B1 being Basis of T such that A1: card B1 = weight T by WAYBEL23:74; { (inf u) where u is Subset of T : u in B1 } c= the carrier of T proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (inf u) where u is Subset of T : u in B1 } or z in the carrier of T ) assume z in { (inf u) where u is Subset of T : u in B1 } ; ::_thesis: z in the carrier of T then ex u being Subset of T st ( z = inf u & u in B1 ) ; hence z in the carrier of T ; ::_thesis: verum end; then reconsider B0 = { (inf u) where u is Subset of T : u in B1 } as Subset of T ; set B2 = finsups B0; defpred S1[ set , set ] means ex y being Subset of T st ( \$1 = y & \$2 = inf y ); A2: for x being set st x in B1 holds ex y being set st ( y in B0 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in B1 implies ex y being set st ( y in B0 & S1[x,y] ) ) assume A3: x in B1 ; ::_thesis: ex y being set st ( y in B0 & S1[x,y] ) then reconsider z = x as Subset of T ; take y = inf z; ::_thesis: ( y in B0 & S1[x,y] ) thus y in B0 by A3; ::_thesis: S1[x,y] take z ; ::_thesis: ( x = z & y = inf z ) thus ( x = z & y = inf z ) ; ::_thesis: verum end; consider f being Function such that A4: dom f = B1 and rng f c= B0 and A5: for x being set st x in B1 holds S1[x,f . x] from FUNCT_1:sch_5(A2); B0 c= rng f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B0 or z in rng f ) assume z in B0 ; ::_thesis: z in rng f then consider u being Subset of T such that A6: z = inf u and A7: u in B1 ; ex y being Subset of T st ( u = y & f . u = inf y ) by A5, A7; hence z in rng f by A4, A6, A7, FUNCT_1:def_3; ::_thesis: verum end; then A8: card B0 c= card B1 by A4, CARD_1:12; A9: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; A10: now__::_thesis:_card_(finsups_B0)_=_card_B0 percases ( L1 is finite or L1 is infinite ) ; supposeA11: L1 is finite ; ::_thesis: card (finsups B0) = card B0 the carrier of L1 c= B0 proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of L1 or z in B0 ) assume z in the carrier of L1 ; ::_thesis: z in B0 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 being 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 z in B0 by A13; ::_thesis: verum end; then ( B0 c= finsups B0 & finsups B0 c= B0 ) by A9, WAYBEL_0:50, XBOOLE_1:1; hence card (finsups B0) = card B0 by XBOOLE_0:def_10; ::_thesis: verum end; suppose L1 is infinite ; ::_thesis: card (finsups B0) = card B0 then T is infinite by A9; then B0 is infinite by Th23, YELLOW15:30; hence card (finsups B0) = card B0 by YELLOW15:27; ::_thesis: verum end; 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 is finite Subset of B0 : ex_sup_of Y,T } ; then "\/" ({},T) in finsups B0 by WAYBEL_0:def_27; then A17: Bottom L1 in finsups B0 by A9, YELLOW_0:26, YELLOW_0:42; reconsider B2 = finsups B0 as Subset of L1 by A9; now__::_thesis:_for_x,_y_being_Element_of_L1_st_x_in_B2_&_y_in_B2_holds_ sup_{x,y}_in_B2 let x, y be Element of L1; ::_thesis: ( x in B2 & y in B2 implies sup {x,y} in B2 ) assume that A18: x in B2 and A19: y in B2 ; ::_thesis: sup {x,y} in B2 y in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A19, WAYBEL_0:def_27; then consider Y2 being finite Subset of B0 such that A20: y = "\/" (Y2,T) and A21: ex_sup_of Y2,T ; x in { ("\/" (Y,T)) where Y is finite Subset of B0 : ex_sup_of Y,T } by A18, WAYBEL_0:def_27; then consider Y1 being 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 is finite Subset of B0 : ex_sup_of Y,T } by A24; hence sup {x,y} in B2 by WAYBEL_0:def_27; ::_thesis: verum end; then reconsider B2 = B2 as join-closed Subset of L1 by WAYBEL23:18; for x, y being Element of L1 st x << y holds ex b being Element of L1 st ( b in B2 & x <= b & b << y ) proof let x, y be Element of L1; ::_thesis: ( x << y implies ex b being Element of L1 st ( b in B2 & x <= b & b << y ) ) reconsider x1 = x, y1 = y as Element of T by A9; A25: B0 c= B2 by WAYBEL_0:50; assume x << y ; ::_thesis: ex b being Element of L1 st ( b in B2 & x <= b & b << 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 being 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 ; ::_thesis: ( b in B2 & x <= b & b << y ) b in B0 by A27; hence b in B2 by A25; ::_thesis: ( x <= b & b << y ) 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; ::_thesis: b << y u is open by A27, YELLOW_8:10; hence b << y by A9, A28, WAYBEL14:26, WAYBEL_8:8; ::_thesis: verum 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 CLweight L1 c= weight T by A1, A8, XBOOLE_1:1; ::_thesis: verum end; theorem Th24: :: WAYBEL31:24 for L1 being lower-bounded continuous sup-Semilattice for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T let T be Scott TopAugmentation of L1; ::_thesis: CLweight L1 = weight T set T1 = the correct Lawson TopAugmentation of L1; ( weight T c= weight the correct Lawson TopAugmentation of L1 & weight the correct Lawson TopAugmentation of L1 c= CLweight L1 ) by Lm1, Lm2; then A1: weight T c= CLweight L1 by XBOOLE_1:1; CLweight L1 c= weight T by Lm3; hence CLweight L1 = weight T by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: WAYBEL31:25 for L1 being lower-bounded continuous sup-Semilattice for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T let T be correct Lawson TopAugmentation of L1; ::_thesis: CLweight L1 = weight T set T1 = the Scott TopAugmentation of L1; ( CLweight L1 c= weight the Scott TopAugmentation of L1 & weight the Scott TopAugmentation of L1 c= weight T ) by Lm1, Lm3; then A1: CLweight L1 c= weight T by XBOOLE_1:1; weight T c= CLweight L1 by Lm2; hence CLweight L1 = weight T by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th26: :: WAYBEL31:26 for L1, L2 being 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 ; ::_thesis: ( L1,L2 are_isomorphic implies card the carrier of L1 = card the carrier of L2 ) assume L1,L2 are_isomorphic ; ::_thesis: card the carrier of L1 = card the carrier of L2 then consider f being 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 V13() & 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 card the carrier of L1 = card the carrier of L2 by CARD_1:5; ::_thesis: verum end; theorem :: WAYBEL31:27 for L1 being lower-bounded continuous sup-Semilattice for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1))) proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1))) let B1 be with_bottom CLbasis of L1; ::_thesis: ( card B1 = CLweight L1 implies CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1))) ) assume A1: card B1 = CLweight L1 ; ::_thesis: CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1))) 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 ; ::_thesis: verum end; registration let L1 be lower-bounded continuous sup-Semilattice; cluster InclPoset (sigma L1) -> with_suprema continuous ; coherence ( InclPoset (sigma L1) is with_suprema & InclPoset (sigma L1) is continuous ) proof set S = the Scott TopAugmentation of L1; A1: RelStr(# the carrier of the Scott TopAugmentation of L1, the InternalRel of the Scott TopAugmentation of L1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4; InclPoset (sigma the Scott TopAugmentation of L1) is complete ; hence InclPoset (sigma L1) is with_suprema by A1, YELLOW_9:52; ::_thesis: InclPoset (sigma L1) is continuous InclPoset (sigma the Scott TopAugmentation of L1) is continuous by WAYBEL14:36; hence InclPoset (sigma L1) is continuous by A1, YELLOW_9:52; ::_thesis: verum end; end; theorem :: WAYBEL31:28 for L1 being lower-bounded continuous sup-Semilattice holds CLweight L1 c= CLweight (InclPoset (sigma L1)) proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: CLweight L1 c= CLweight (InclPoset (sigma L1)) set S = the Scott TopAugmentation of L1; A1: RelStr(# the carrier of the Scott TopAugmentation of L1, the InternalRel of the Scott TopAugmentation of L1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4; A2: InclPoset the topology of the Scott TopAugmentation of L1 = InclPoset (sigma L1) by YELLOW_9:51; A3: CLweight L1 = weight the Scott TopAugmentation of L1 by Th24; now__::_thesis:_CLweight_L1_c=_CLweight_(InclPoset_(sigma_L1)) percases ( L1 is infinite or L1 is finite ) ; suppose L1 is infinite ; ::_thesis: CLweight L1 c= CLweight (InclPoset (sigma L1)) then the Scott TopAugmentation of L1 is infinite by A1; hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, Th6; ::_thesis: verum end; supposeA4: L1 is finite ; ::_thesis: CLweight L1 c= CLweight (InclPoset (sigma L1)) A5: card the carrier of the Scott TopAugmentation of L1 c= card the carrier of (InclPoset (sigma L1)) by A2, Th7; A6: the Scott TopAugmentation of L1 is finite by A1, A4; then weight the Scott TopAugmentation of L1 = card the carrier of the Scott TopAugmentation of L1 by Th8; hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, A6, A5, Th9; ::_thesis: verum end; end; end; hence CLweight L1 c= CLweight (InclPoset (sigma L1)) ; ::_thesis: verum end; theorem :: WAYBEL31:29 for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds CLweight L1 = CLweight (InclPoset (sigma L1)) proof let L1 be lower-bounded continuous sup-Semilattice; ::_thesis: ( L1 is infinite implies CLweight L1 = CLweight (InclPoset (sigma L1)) ) set S = the Scott TopAugmentation of L1; assume A1: L1 is infinite ; ::_thesis: CLweight L1 = CLweight (InclPoset (sigma L1)) A2: ( CLweight L1 = weight the Scott TopAugmentation of L1 & InclPoset the topology of the Scott TopAugmentation of L1 = InclPoset (sigma L1) ) by Th24, YELLOW_9:51; RelStr(# the carrier of the Scott TopAugmentation of L1, the InternalRel of the Scott TopAugmentation of L1 #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4; then the Scott TopAugmentation of L1 is infinite by A1; hence CLweight L1 = CLweight (InclPoset (sigma L1)) by A2, Th6; ::_thesis: verum end;