:: WAYBEL32 semantic presentation begin definition let T be non empty TopRelStr ; attrT is upper means :Def1: :: WAYBEL32:def 1 { ((downarrow x) `) where x is Element of T : verum } is prebasis of T; end; :: deftheorem Def1 defines upper WAYBEL32:def_1_:_ for T being non empty TopRelStr holds ( T is upper iff { ((downarrow x) `) where x is Element of T : verum } is prebasis of T ); registration cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict Scott for TopRelStr ; existence ex b1 being TopLattice st ( b1 is Scott & b1 is up-complete & b1 is strict ) proof set R = the complete LATTICE; set T = the correct strict Scott TopAugmentation of the complete LATTICE; take the correct strict Scott TopAugmentation of the complete LATTICE ; ::_thesis: ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is up-complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) thus ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is up-complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) ; ::_thesis: verum end; end; definition let T be non empty TopSpace-like reflexive TopRelStr ; attrT is order_consistent means :Def2: :: WAYBEL32:def 2 for x being Element of T holds ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ); end; :: deftheorem Def2 defines order_consistent WAYBEL32:def_2_:_ for T being non empty TopSpace-like reflexive TopRelStr holds ( T is order_consistent iff for x being Element of T holds ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ) ); registration cluster1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive upper for TopRelStr ; coherence for b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 is upper proof let T be 1 -element TopSpace-like reflexive TopRelStr ; ::_thesis: T is upper set BB = { ((downarrow x) `) where x is Element of T : verum } ; { ((downarrow x) `) where x is Element of T : verum } c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in bool the carrier of T ) assume a in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: a in bool the carrier of T then ex x being Element of T st a = (downarrow x) ` ; hence a in bool the carrier of T ; ::_thesis: verum end; then reconsider C = { ((downarrow x) `) where x is Element of T : verum } as Subset-Family of T ; reconsider C = C as Subset-Family of T ; A1: { ((downarrow x) `) where x is Element of T : verum } c= the topology of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in the topology of T ) assume a in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: a in the topology of T then consider x being Element of T such that A2: a = (downarrow x) ` ; a c= {} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in {} ) assume A3: y in a ; ::_thesis: y in {} A4: x <= x ; A5: y = x by A2, A3, STRUCT_0:def_10; x in downarrow x by A4, WAYBEL_0:17; then A6: x in (downarrow x) /\ a by A3, A5, XBOOLE_0:def_4; downarrow x misses a by A2, XBOOLE_1:79; hence y in {} by A6, XBOOLE_0:def_7; ::_thesis: verum end; then a = {} ; hence a in the topology of T by PRE_TOPC:1; ::_thesis: verum end; reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10; { ((downarrow x) `) where x is Element of T : verum } = {{}} proof thus { ((downarrow x) `) where x is Element of T : verum } c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= { ((downarrow x) `) where x is Element of T : verum } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in {{}} ) assume a in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: a in {{}} then consider x being Element of T such that A7: a = (downarrow x) ` ; A8: x <= x ; A9: the carrier of T = {x} by YELLOW_9:9; x in downarrow x by A8, WAYBEL_0:17; then ( a = {} or ( a = the carrier of T & not x in a ) ) by A7, A9, XBOOLE_0:def_5, ZFMISC_1:33; hence a in {{}} by TARSKI:def_1; ::_thesis: verum end; set x = the Element of T; A10: the Element of T <= the Element of T ; A11: the carrier of T = { the Element of T} by YELLOW_9:9; the Element of T in downarrow the Element of T by A10, WAYBEL_0:17; then ( (downarrow the Element of T) ` = {} or ( (downarrow the Element of T) ` = the carrier of T & not the Element of T in (downarrow the Element of T) ` ) ) by A11, XBOOLE_0:def_5, ZFMISC_1:33; then {} in { ((downarrow x) `) where x is Element of T : verum } ; hence {{}} c= { ((downarrow x) `) where x is Element of T : verum } by ZFMISC_1:31; ::_thesis: verum end; then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11; then F c= FinMeetCl C by ZFMISC_1:7; hence { ((downarrow x) `) where x is Element of T : verum } is prebasis of T by A1, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL32:def_1 ::_thesis: verum end; end; registration cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict upper for TopRelStr ; existence ex b1 being TopLattice st ( b1 is upper & b1 is trivial & b1 is up-complete & b1 is strict ) proof set T = the 1 -element up-complete strict TopLattice; take the 1 -element up-complete strict TopLattice ; ::_thesis: ( the 1 -element up-complete strict TopLattice is upper & the 1 -element up-complete strict TopLattice is trivial & the 1 -element up-complete strict TopLattice is up-complete & the 1 -element up-complete strict TopLattice is strict ) thus ( the 1 -element up-complete strict TopLattice is upper & the 1 -element up-complete strict TopLattice is trivial & the 1 -element up-complete strict TopLattice is up-complete & the 1 -element up-complete strict TopLattice is strict ) ; ::_thesis: verum end; end; theorem Th1: :: WAYBEL32:1 for T being non empty up-complete upper TopPoset for A being Subset of T st A is open holds A is upper proof let T be non empty up-complete upper TopPoset; ::_thesis: for A being Subset of T st A is open holds A is upper let A be Subset of T; ::_thesis: ( A is open implies A is upper ) assume A is open ; ::_thesis: A is upper then A1: A in the topology of T by PRE_TOPC:def_2; reconsider BB = { ((downarrow x) `) where x is Element of T : verum } as prebasis of T by Def1; consider F being Basis of T such that A2: F c= FinMeetCl BB by CANTOR_1:def_4; the topology of T c= UniCl F by CANTOR_1:def_2; then consider Y being Subset-Family of T such that A3: Y c= F and A4: A = union Y by A1, CANTOR_1:def_1; let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A ) assume x in A ; ::_thesis: ( not x <= y or y in A ) then consider Z being set such that A5: x in Z and A6: Z in Y by A4, TARSKI:def_4; Z in F by A3, A6; then consider X being Subset-Family of T such that A7: X c= BB and X is finite and A8: Z = Intersect X by A2, CANTOR_1:def_3; assume A9: x <= y ; ::_thesis: y in A now__::_thesis:_for_Q_being_set_st_Q_in_X_holds_ y_in_Q let Q be set ; ::_thesis: ( Q in X implies y in Q ) assume A10: Q in X ; ::_thesis: y in Q then Q in BB by A7; then consider z being Element of T such that A11: Q = (downarrow z) ` ; A12: x in Q by A5, A8, A10, SETFAM_1:43; downarrow z misses Q by A11, XBOOLE_1:79; then not x in downarrow z by A12, XBOOLE_0:3; then not x <= z by WAYBEL_0:17; then not y <= z by A9, ORDERS_2:3; then not y in downarrow z by WAYBEL_0:17; hence y in Q by A11, XBOOLE_0:def_5; ::_thesis: verum end; then y in Z by A8, SETFAM_1:43; hence y in A by A4, A6, TARSKI:def_4; ::_thesis: verum end; theorem :: WAYBEL32:2 for T being non empty up-complete TopPoset st T is upper holds T is order_consistent proof let T be non empty up-complete TopPoset; ::_thesis: ( T is upper implies T is order_consistent ) assume A1: T is upper ; ::_thesis: T is order_consistent then reconsider BB = { ((downarrow x) `) where x is Element of T : verum } as prebasis of T by Def1; for x being Element of T holds ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ) proof let x be Element of T; ::_thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ) A2: downarrow x c= Cl {x} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in Cl {x} ) assume A3: a in downarrow x ; ::_thesis: a in Cl {x} then reconsider a9 = a as Point of T ; for G being Subset of T st G is open & a9 in G holds {x} meets G proof let G be Subset of T; ::_thesis: ( G is open & a9 in G implies {x} meets G ) assume A4: G is open ; ::_thesis: ( not a9 in G or {x} meets G ) assume A5: a9 in G ; ::_thesis: {x} meets G reconsider v = a9 as Element of T ; A6: v <= x by A3, WAYBEL_0:17; G is upper by A1, A4, Th1; then A7: x in G by A5, A6, WAYBEL_0:def_20; x in {x} by TARSKI:def_1; hence {x} meets G by A7, XBOOLE_0:3; ::_thesis: verum end; hence a in Cl {x} by PRE_TOPC:24; ::_thesis: verum end; Cl {x} c= downarrow x proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {x} or a in downarrow x ) assume A8: a in Cl {x} ; ::_thesis: a in downarrow x reconsider BB = BB as Subset-Family of T ; (downarrow x) ` in BB ; then A9: (downarrow x) ` is open by TOPS_2:def_1; (downarrow x) ` = ([#] T) \ (downarrow x) ; then A10: downarrow x is closed by A9, PRE_TOPC:def_3; x <= x ; then x in downarrow x by WAYBEL_0:17; then {x} c= downarrow x by ZFMISC_1:31; hence a in downarrow x by A8, A10, PRE_TOPC:15; ::_thesis: verum end; hence downarrow x = Cl {x} by A2, XBOOLE_0:def_10; ::_thesis: for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V thus for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ::_thesis: verum proof let N be eventually-directed net of T; ::_thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V ) assume x = sup N ; ::_thesis: for V being a_neighborhood of x holds N is_eventually_in V then A11: x = Sup by WAYBEL_2:def_1 .= sup (rng (netmap (N,T))) by YELLOW_2:def_5 ; let V be a_neighborhood of x; ::_thesis: N is_eventually_in V A12: x in Int V by CONNSP_2:def_1; FinMeetCl BB is Basis of T by YELLOW_9:23; then A13: the topology of T = UniCl (FinMeetCl BB) by YELLOW_9:22; Int V in the topology of T by PRE_TOPC:def_2; then consider Y being Subset-Family of T such that A14: Y c= FinMeetCl BB and A15: Int V = union Y by A13, CANTOR_1:def_1; consider Y1 being set such that A16: x in Y1 and A17: Y1 in Y by A12, A15, TARSKI:def_4; consider Z being Subset-Family of T such that A18: Z c= BB and A19: Z is finite and A20: Y1 = Intersect Z by A14, A17, CANTOR_1:def_3; reconsider rngN = rng (netmap (N,T)) as Subset of T ; rngN is directed by WAYBEL_2:18; then ex a being Element of T st ( a is_>=_than rngN & ( for b being Element of T st b is_>=_than rngN holds a <= b ) ) by WAYBEL_0:def_39; then A21: ex_sup_of rngN,T by YELLOW_0:15; defpred S1[ set , set ] means for i, j being Element of N st i = \$2 & j >= i holds N . j in \$1; A22: for Q being set st Q in Z holds ex b being set st ( b in the carrier of N & S1[Q,b] ) proof let Q be set ; ::_thesis: ( Q in Z implies ex b being set st ( b in the carrier of N & S1[Q,b] ) ) assume A23: Q in Z ; ::_thesis: ex b being set st ( b in the carrier of N & S1[Q,b] ) then Q in BB by A18; then consider v1 being Element of T such that A24: Q = (downarrow v1) ` ; x in (downarrow v1) ` by A16, A20, A23, A24, SETFAM_1:43; then not x in downarrow v1 by XBOOLE_0:def_5; then A25: not x <= v1 by WAYBEL_0:17; not rngN c= downarrow v1 proof assume A26: rngN c= downarrow v1 ; ::_thesis: contradiction ex_sup_of downarrow v1,T by WAYBEL_0:34; then sup rngN <= sup (downarrow v1) by A21, A26, YELLOW_0:34; hence contradiction by A11, A25, WAYBEL_0:34; ::_thesis: verum end; then consider w being set such that A27: w in rngN and A28: not w in downarrow v1 by TARSKI:def_3; reconsider w9 = w as Element of T by A27; consider i being set such that A29: i in dom the mapping of N and A30: w9 = the mapping of N . i by A27, FUNCT_1:def_3; reconsider i = i as Element of N by A29; consider b being Element of N such that A31: for l being Element of N st b <= l holds N . i <= N . l by WAYBEL_0:11; take b ; ::_thesis: ( b in the carrier of N & S1[Q,b] ) thus b in the carrier of N ; ::_thesis: S1[Q,b] thus for j, k being Element of N st j = b & k >= j holds N . k in Q ::_thesis: verum proof let j, k be Element of N; ::_thesis: ( j = b & k >= j implies N . k in Q ) assume that A32: j = b and A33: k >= j ; ::_thesis: N . k in Q A34: N . i <= N . k by A31, A32, A33; not N . i <= v1 by A28, A30, WAYBEL_0:17; then not N . k <= v1 by A34, ORDERS_2:3; then not N . k in downarrow v1 by WAYBEL_0:17; hence N . k in Q by A24, XBOOLE_0:def_5; ::_thesis: verum end; end; consider f being Function such that A35: ( dom f = Z & rng f c= the carrier of N ) and A36: for Q being set st Q in Z holds S1[Q,f . Q] from FUNCT_1:sch_5(A22); reconsider rngf = rng f as finite Subset of ([#] N) by A19, A35, FINSET_1:8; [#] N is directed by WAYBEL_0:def_6; then consider k being Element of N such that k in [#] N and A37: k is_>=_than rngf by WAYBEL_0:1; take k ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not k <= b1 or N . b1 in V ) let k1 be Element of N; ::_thesis: ( not k <= k1 or N . k1 in V ) assume A38: k <= k1 ; ::_thesis: N . k1 in V now__::_thesis:_for_Q_being_set_st_Q_in_Z_holds_ N_._k1_in_Q let Q be set ; ::_thesis: ( Q in Z implies N . k1 in Q ) assume A39: Q in Z ; ::_thesis: N . k1 in Q then A40: f . Q in rngf by A35, FUNCT_1:def_3; then reconsider j = f . Q as Element of N ; j <= k by A37, A40, LATTICE3:def_9; hence N . k1 in Q by A36, A38, A39, ORDERS_2:3; ::_thesis: verum end; then A41: N . k1 in Y1 by A20, SETFAM_1:43; Y1 c= union Y by A17, ZFMISC_1:74; then A42: N . k1 in Int V by A15, A41; Int V c= V by TOPS_1:16; hence N . k1 in V by A42; ::_thesis: verum end; end; hence T is order_consistent by Def2; ::_thesis: verum end; theorem Th3: :: WAYBEL32:3 for R being non empty reflexive transitive antisymmetric up-complete RelStr ex T being TopAugmentation of R st T is Scott proof let R be non empty reflexive transitive antisymmetric up-complete RelStr ; ::_thesis: ex T being TopAugmentation of R st T is Scott set T = the Scott TopAugmentation of R; take the Scott TopAugmentation of R ; ::_thesis: the Scott TopAugmentation of R is Scott thus the Scott TopAugmentation of R is Scott ; ::_thesis: verum end; theorem :: WAYBEL32:4 for R being non empty up-complete Poset for T being TopAugmentation of R st T is Scott holds T is correct ; registration let R be non empty reflexive transitive antisymmetric up-complete RelStr ; cluster Scott -> correct for TopAugmentation of R; coherence for b1 being TopAugmentation of R st b1 is Scott holds b1 is correct ; end; registration let R be non empty reflexive transitive antisymmetric up-complete RelStr ; cluster non empty correct reflexive transitive antisymmetric up-complete Scott for TopAugmentation of R; existence ex b1 being TopAugmentation of R st ( b1 is Scott & b1 is correct ) proof consider T being TopAugmentation of R such that A1: T is Scott by Th3; take T ; ::_thesis: ( T is Scott & T is correct ) thus ( T is Scott & T is correct ) by A1; ::_thesis: verum end; end; theorem Th5: :: WAYBEL32:5 for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr for x being Element of T holds Cl {x} = downarrow x proof let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for x being Element of T holds Cl {x} = downarrow x let x be Element of T; ::_thesis: Cl {x} = downarrow x reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44; reconsider dx = downarrow x as Subset of T9 ; reconsider A = {x} as Subset of T9 ; A1: downarrow x is closed by WAYBEL11:11; x <= x ; then x in downarrow x by WAYBEL_0:17; then A2: {x} c= downarrow x by ZFMISC_1:31; now__::_thesis:_for_C_being_Subset_of_T9_st_A_c=_C_&_C_is_closed_holds_ dx_c=_C let C be Subset of T9; ::_thesis: ( A c= C & C is closed implies dx c= C ) assume A3: A c= C ; ::_thesis: ( C is closed implies dx c= C ) reconsider D = C as Subset of T9 ; assume C is closed ; ::_thesis: dx c= C then A4: D is lower by WAYBEL11:7; x in C by A3, ZFMISC_1:31; hence dx c= C by A4, WAYBEL11:6; ::_thesis: verum end; hence Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum end; theorem Th6: :: WAYBEL32:6 for T being non empty up-complete Scott TopPoset holds T is order_consistent proof let T be non empty up-complete Scott TopPoset; ::_thesis: T is order_consistent for x being Element of T holds ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ) proof let x be Element of T; ::_thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ) for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V proof let N be eventually-directed net of T; ::_thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V ) assume x = sup N ; ::_thesis: for V being a_neighborhood of x holds N is_eventually_in V then x = Sup by WAYBEL_2:def_1; then A1: x = sup (rng the mapping of N) by YELLOW_2:def_5; let V be a_neighborhood of x; ::_thesis: N is_eventually_in V A2: x in Int V by CONNSP_2:def_1; reconsider rngN = rng (netmap (N,T)) as Subset of T ; rngN is directed by WAYBEL_2:18; then Int V meets rngN by A1, A2, WAYBEL11:def_1; then consider z being set such that A3: z in Int V and A4: z in rngN by XBOOLE_0:3; reconsider z9 = z as Element of T by A3; consider i being set such that A5: i in dom the mapping of N and A6: z9 = the mapping of N . i by A4, FUNCT_1:def_3; reconsider i = i as Element of N by A5; consider j being Element of N such that A7: for k being Element of N st j <= k holds N . i <= N . k by WAYBEL_0:11; take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not j <= b1 or N . b1 in V ) let l be Element of N; ::_thesis: ( not j <= l or N . l in V ) assume j <= l ; ::_thesis: N . l in V then N . i <= N . l by A7; then A8: N . l in Int V by A3, A6, WAYBEL_0:def_20; Int V c= V by TOPS_1:16; hence N . l in V by A8; ::_thesis: verum end; hence ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds for V being a_neighborhood of x holds N is_eventually_in V ) ) by Th5; ::_thesis: verum end; hence T is order_consistent by Def2; ::_thesis: verum end; theorem Th7: :: WAYBEL32:7 for R being /\-complete Semilattice for Z being net of R for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds ( not D is empty & D is directed ) proof let R be /\-complete Semilattice; ::_thesis: for Z being net of R for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds ( not D is empty & D is directed ) let Z be net of R; ::_thesis: for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds ( not D is empty & D is directed ) let D be Subset of R; ::_thesis: ( D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } implies ( not D is empty & D is directed ) ) assume A1: D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } ; ::_thesis: ( not D is empty & D is directed ) set j = the Element of Z; "/\" ( { (Z . k) where k is Element of Z : k >= the Element of Z } ,R) in D by A1; hence not D is empty ; ::_thesis: D is directed let x, y be Element of R; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D or not y in D or ex b1 being Element of the carrier of R st ( b1 in D & x <= b1 & y <= b1 ) ) assume x in D ; ::_thesis: ( not y in D or ex b1 being Element of the carrier of R st ( b1 in D & x <= b1 & y <= b1 ) ) then consider jx being Element of Z such that A2: x = "/\" ( { (Z . k) where k is Element of Z : k >= jx } ,R) by A1; assume y in D ; ::_thesis: ex b1 being Element of the carrier of R st ( b1 in D & x <= b1 & y <= b1 ) then consider jy being Element of Z such that A3: y = "/\" ( { (Z . k) where k is Element of Z : k >= jy } ,R) by A1; reconsider jx = jx, jy = jy as Element of Z ; consider j being Element of Z such that A4: j >= jx and A5: j >= jy by YELLOW_6:def_3; consider j9 being Element of Z such that A6: j9 >= j and j9 >= j by YELLOW_6:def_3; deffunc H1( Element of Z) -> Element of the carrier of R = Z . \$1; defpred S1[ Element of Z] means \$1 >= jx; defpred S2[ Element of Z] means \$1 >= jy; defpred S3[ Element of Z] means \$1 >= j; set Ex = { H1(k) where k is Element of Z : S1[k] } ; set Ey = { H1(k) where k is Element of Z : S2[k] } ; set E = { H1(k) where k is Element of Z : S3[k] } ; A7: Z . j in { H1(k) where k is Element of Z : S1[k] } by A4; A8: Z . j in { H1(k) where k is Element of Z : S2[k] } by A5; A9: Z . j9 in { H1(k) where k is Element of Z : S3[k] } by A6; A10: { H1(k) where k is Element of Z : S1[k] } is Subset of R from DOMAIN_1:sch_8(); A11: { H1(k) where k is Element of Z : S2[k] } is Subset of R from DOMAIN_1:sch_8(); A12: { H1(k) where k is Element of Z : S3[k] } is Subset of R from DOMAIN_1:sch_8(); take z = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R); ::_thesis: ( z in D & x <= z & y <= z ) reconsider Ex9 = { H1(k) where k is Element of Z : S1[k] } as non empty Subset of R by A7, A10; reconsider Ey9 = { H1(k) where k is Element of Z : S2[k] } as non empty Subset of R by A8, A11; reconsider E9 = { H1(k) where k is Element of Z : S3[k] } as non empty Subset of R by A9, A12; A13: ex_inf_of E9,R by WAYBEL_0:76; A14: ex_inf_of Ex9,R by WAYBEL_0:76; A15: ex_inf_of Ey9,R by WAYBEL_0:76; thus z in D by A1; ::_thesis: ( x <= z & y <= z ) E9 c= Ex9 proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in E9 or e in Ex9 ) assume e in E9 ; ::_thesis: e in Ex9 then consider k being Element of Z such that A16: e = Z . k and A17: k >= j ; reconsider k = k as Element of Z ; k >= jx by A4, A17, YELLOW_0:def_2; hence e in Ex9 by A16; ::_thesis: verum end; hence x <= z by A2, A13, A14, YELLOW_0:35; ::_thesis: y <= z E9 c= Ey9 proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in E9 or e in Ey9 ) assume e in E9 ; ::_thesis: e in Ey9 then consider k being Element of Z such that A18: e = Z . k and A19: k >= j ; reconsider k = k as Element of Z ; k >= jy by A5, A19, YELLOW_0:def_2; hence e in Ey9 by A18; ::_thesis: verum end; hence y <= z by A3, A13, A15, YELLOW_0:35; ::_thesis: verum end; theorem Th8: :: WAYBEL32:8 for R being /\-complete Semilattice for S being Subset of R for a being Element of R st a in S holds "/\" (S,R) <= a proof let R be /\-complete Semilattice; ::_thesis: for S being Subset of R for a being Element of R st a in S holds "/\" (S,R) <= a let S be Subset of R; ::_thesis: for a being Element of R st a in S holds "/\" (S,R) <= a let a be Element of R; ::_thesis: ( a in S implies "/\" (S,R) <= a ) assume A1: a in S ; ::_thesis: "/\" (S,R) <= a then ex_inf_of S,R by WAYBEL_0:76; then S is_>=_than "/\" (S,R) by YELLOW_0:31; hence "/\" (S,R) <= a by A1, LATTICE3:def_8; ::_thesis: verum end; theorem Th9: :: WAYBEL32:9 for R being /\-complete Semilattice for N being reflexive monotone net of R holds lim_inf N = sup N proof let R be /\-complete Semilattice; ::_thesis: for N being reflexive monotone net of R holds lim_inf N = sup N let N be reflexive monotone net of R; ::_thesis: lim_inf N = sup N deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,R); deffunc H2( Element of N) -> Element of the carrier of R = N . \$1; defpred S1[ set ] means verum; set X = { H1(j) where j is Element of N : S1[j] } ; A1: for j being Element of N holds H2(j) = H1(j) proof let j be Element of N; ::_thesis: H2(j) = H1(j) defpred S2[ Element of N] means \$1 >= j; set Y = { H2(i) where i is Element of N : S2[i] } ; j <= j ; then A2: N . j in { H2(i) where i is Element of N : S2[i] } ; { H2(i) where i is Element of N : S2[i] } is Subset of R from DOMAIN_1:sch_8(); then A3: ex_inf_of { H2(i) where i is Element of N : S2[i] } ,R by A2, WAYBEL_0:76; A4: N . j is_<=_than { H2(i) where i is Element of N : S2[i] } proof let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in { H2(i) where i is Element of N : S2[i] } or N . j <= y ) assume y in { H2(i) where i is Element of N : S2[i] } ; ::_thesis: N . j <= y then ex i being Element of N st ( y = N . i & j <= i ) ; hence N . j <= y by WAYBEL11:def_9; ::_thesis: verum end; for b being Element of R st b is_<=_than { H2(i) where i is Element of N : S2[i] } holds N . j >= b proof let b be Element of R; ::_thesis: ( b is_<=_than { H2(i) where i is Element of N : S2[i] } implies N . j >= b ) assume A5: b is_<=_than { H2(i) where i is Element of N : S2[i] } ; ::_thesis: N . j >= b reconsider j9 = j as Element of N ; j9 <= j9 ; then N . j9 in { H2(i) where i is Element of N : S2[i] } ; hence N . j >= b by A5, LATTICE3:def_8; ::_thesis: verum end; hence H2(j) = H1(j) by A3, A4, YELLOW_0:def_10; ::_thesis: verum end; rng the mapping of N = { H2(j) where j is Element of N : S1[j] } by WAYBEL11:19 .= { H1(j) where j is Element of N : S1[j] } from FRAENKEL:sch_5(A1) ; hence lim_inf N = Sup by YELLOW_2:def_5 .= sup N by WAYBEL_2:def_1 ; ::_thesis: verum end; theorem Th10: :: WAYBEL32:10 for R being /\-complete Semilattice for S being Subset of R holds ( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) ) proof let R be /\-complete Semilattice; ::_thesis: for S being Subset of R holds ( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) ) set SC = Scott-Convergence R; set T = ConvergenceSpace (Scott-Convergence R); A1: the topology of (ConvergenceSpace (Scott-Convergence R)) = { V where V is Subset of R : for p being Element of R st p in V holds for N being net of R st [N,p] in Scott-Convergence R holds N is_eventually_in V } by YELLOW_6:def_24; let S be Subset of R; ::_thesis: ( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) ) hereby ::_thesis: ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence R)) ) assume S in the topology of (ConvergenceSpace (Scott-Convergence R)) ; ::_thesis: ( S is inaccessible & S is upper ) then A2: ex V being Subset of R st ( S = V & ( for p being Element of R st p in V holds for N being net of R st [N,p] in Scott-Convergence R holds N is_eventually_in V ) ) by A1; thus S is inaccessible ::_thesis: S is upper proof let D be non empty directed Subset of R; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,R) in S or not D misses S ) assume A3: sup D in S ; ::_thesis: not D misses S A4: dom (id D) = D by RELAT_1:45; A5: rng (id D) = D by RELAT_1:45; then reconsider f = id D as Function of D, the carrier of R by A4, FUNCT_2:def_1, RELSET_1:4; reconsider N = Net-Str (D,f) as reflexive strict monotone net of R by A5, WAYBEL11:20; A6: N in NetUniv R by WAYBEL11:21; lim_inf N = sup N by Th9 .= Sup by WAYBEL_2:def_1 .= "\/" ((rng the mapping of N),R) by YELLOW_2:def_5 .= "\/" ((rng f),R) by WAYBEL11:def_10 .= sup D by RELAT_1:45 ; then sup D is_S-limit_of N by WAYBEL11:def_7; then [N,(sup D)] in Scott-Convergence R by A6, WAYBEL11:def_8; then N is_eventually_in S by A2, A3; then consider i0 being Element of N such that A7: for j being Element of N st i0 <= j holds N . j in S by WAYBEL_0:def_11; consider j0 being Element of N such that A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def_3; A9: N . j0 in S by A7, A8; A10: D = the carrier of N by WAYBEL11:def_10; N . j0 = (id D) . j0 by WAYBEL11:def_10 .= j0 by A10, FUNCT_1:18 ; hence not D misses S by A9, A10, XBOOLE_0:3; ::_thesis: verum end; thus S is upper ::_thesis: verum proof let x, y be Element of R; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in S or not x <= y or y in S ) assume that A11: x in S and A12: x <= y ; ::_thesis: y in S A13: Net-Str y in NetUniv R by WAYBEL11:29; y = lim_inf (Net-Str y) by WAYBEL11:28; then x is_S-limit_of Net-Str y by A12, WAYBEL11:def_7; then [(Net-Str y),x] in Scott-Convergence R by A13, WAYBEL11:def_8; then Net-Str y is_eventually_in S by A2, A11; hence y in S by WAYBEL11:27; ::_thesis: verum end; end; assume that A14: S is inaccessible and A15: S is upper ; ::_thesis: S in the topology of (ConvergenceSpace (Scott-Convergence R)) for p being Element of R st p in S holds for N being net of R st [N,p] in Scott-Convergence R holds N is_eventually_in S proof let p be Element of R; ::_thesis: ( p in S implies for N being net of R st [N,p] in Scott-Convergence R holds N is_eventually_in S ) assume A16: p in S ; ::_thesis: for N being net of R st [N,p] in Scott-Convergence R holds N is_eventually_in S reconsider p9 = p as Element of R ; let N be net of R; ::_thesis: ( [N,p] in Scott-Convergence R implies N is_eventually_in S ) assume A17: [N,p] in Scott-Convergence R ; ::_thesis: N is_eventually_in S Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18; then A18: N in NetUniv R by A17, ZFMISC_1:87; then ex N9 being strict net of R st ( N9 = N & the carrier of N9 in the_universe_of the carrier of R ) by YELLOW_6:def_11; then p is_S-limit_of N by A17, A18, WAYBEL11:def_8; then A19: p9 <= lim_inf N by WAYBEL11:def_7; deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,R); defpred S1[ set ] means verum; set X = { H1(j) where j is Element of N : S1[j] } ; { H1(j) where j is Element of N : S1[j] } is Subset of R from DOMAIN_1:sch_8(); then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of R ; reconsider D = D as non empty directed Subset of R by Th7; sup D in S by A15, A16, A19, WAYBEL_0:def_20; then D meets S by A14, WAYBEL11:def_1; then D /\ S <> {} by XBOOLE_0:def_7; then consider d being Element of R such that A20: d in D /\ S by SUBSET_1:4; reconsider d = d as Element of R ; d in D by A20, XBOOLE_0:def_4; then consider j being Element of N such that A21: d = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ; defpred S2[ Element of N] means \$1 >= j; deffunc H2( Element of N) -> Element of the carrier of R = N . \$1; { H2(i) where i is Element of N : S2[i] } is Subset of R from DOMAIN_1:sch_8(); then reconsider Y = { (N . i) where i is Element of N : i >= j } as Subset of R ; reconsider j = j as Element of N ; take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not j <= b1 or N . b1 in S ) let i0 be Element of N; ::_thesis: ( not j <= i0 or N . i0 in S ) A22: d in S by A20, XBOOLE_0:def_4; assume j <= i0 ; ::_thesis: N . i0 in S then N . i0 in Y ; then d <= N . i0 by A21, Th8; hence N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum end; hence S in the topology of (ConvergenceSpace (Scott-Convergence R)) by A1; ::_thesis: verum end; theorem Th11: :: WAYBEL32:11 for R being up-complete /\-complete Semilattice for T being TopAugmentation of R st the topology of T = sigma R holds T is Scott proof let R be up-complete /\-complete Semilattice; ::_thesis: for T being TopAugmentation of R st the topology of T = sigma R holds T is Scott let T be TopAugmentation of R; ::_thesis: ( the topology of T = sigma R implies T is Scott ) assume A1: the topology of T = sigma R ; ::_thesis: T is Scott A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; T is Scott proof let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( ( not S is open or ( S is inaccessible_by_directed_joins & S is upper ) ) & ( not S is inaccessible_by_directed_joins or not S is upper or S is open ) ) reconsider A = S as Subset of R by A2; thus ( S is open implies ( S is inaccessible & S is upper ) ) ::_thesis: ( not S is inaccessible_by_directed_joins or not S is upper or S is open ) proof assume S is open ; ::_thesis: ( S is inaccessible & S is upper ) then S in the topology of T by PRE_TOPC:def_2; then ( A is inaccessible & A is upper ) by A1, Th10; hence ( S is inaccessible & S is upper ) by A2, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum end; assume A3: ( S is inaccessible & S is upper ) ; ::_thesis: S is open A is inaccessible proof let D be non empty directed Subset of R; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,R) in A or not D misses A ) assume A4: sup D in A ; ::_thesis: not D misses A reconsider E = D as Subset of T by A2; ex a being Element of R st ( a is_>=_than D & ( for b being Element of R st b is_>=_than D holds a <= b ) ) by WAYBEL_0:def_39; then A5: ex_sup_of D,R by YELLOW_0:15; A6: E is directed by A2, WAYBEL_0:3; sup D = sup E by A2, A5, YELLOW_0:26; hence not D misses A by A3, A4, A6, WAYBEL11:def_1; ::_thesis: verum end; then ( A is inaccessible & A is upper ) by A2, A3, WAYBEL_0:25; then A in the topology of T by A1, Th10; hence S is open by PRE_TOPC:def_2; ::_thesis: verum end; hence T is Scott ; ::_thesis: verum end; registration let R be up-complete /\-complete Semilattice; cluster non empty correct reflexive transitive antisymmetric up-complete strict Scott for TopAugmentation of R; existence ex b1 being TopAugmentation of R st ( b1 is strict & b1 is Scott & b1 is correct ) proof set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #); RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopAugmentation of R by YELLOW_9:def_4; take T ; ::_thesis: ( T is strict & T is Scott & T is correct ) thus ( T is strict & T is Scott & T is correct ) by Th11, YELLOW_9:48; ::_thesis: verum end; end; theorem :: WAYBEL32:12 for S being up-complete /\-complete Semilattice for T being Scott TopAugmentation of S holds sigma S = the topology of T proof let S be up-complete /\-complete Semilattice; ::_thesis: for T being Scott TopAugmentation of S holds sigma S = the topology of T let T be Scott TopAugmentation of S; ::_thesis: sigma S = the topology of T thus sigma S c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= sigma S proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in sigma S or e in the topology of T ) assume A1: e in sigma S ; ::_thesis: e in the topology of T then reconsider A = e as Subset of S ; A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider A9 = A as Subset of T ; ( A is inaccessible & A is upper ) by A1, Th10; then ( A9 is inaccessible & A9 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47; hence e in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of T or e in sigma S ) assume A3: e in the topology of T ; ::_thesis: e in sigma S then reconsider A = e as Subset of T ; A4: A is open by A3, PRE_TOPC:def_2; A5: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider A9 = A as Subset of S ; A9 is inaccessible proof let D be non empty directed Subset of S; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,S) in A9 or not D misses A9 ) assume A6: sup D in A9 ; ::_thesis: not D misses A9 reconsider E = D as Subset of T by A5; ex a being Element of S st ( a is_>=_than D & ( for b being Element of S st b is_>=_than D holds a <= b ) ) by WAYBEL_0:def_39; then A7: ex_sup_of D,S by YELLOW_0:15; A8: E is directed by A5, WAYBEL_0:3; sup D = sup E by A5, A7, YELLOW_0:26; hence not D misses A9 by A4, A6, A8, WAYBEL11:def_1; ::_thesis: verum end; then ( A9 is inaccessible & A9 is upper ) by A4, A5, WAYBEL_0:25; hence e in sigma S by Th10; ::_thesis: verum end; theorem :: WAYBEL32:13 for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds T is T_0-TopSpace proof let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: T is T_0-TopSpace reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44; now__::_thesis:_for_x,_y_being_Point_of_T9_st_x_<>_y_holds_ Cl_{x}_<>_Cl_{y} let x, y be Point of T9; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} ) reconsider x9 = x, y9 = y as Element of T9 ; A1: Cl {x9} = downarrow x9 by Th5; A2: Cl {y9} = downarrow y9 by Th5; assume x <> y ; ::_thesis: Cl {x} <> Cl {y} hence Cl {x} <> Cl {y} by A1, A2, WAYBEL_0:19; ::_thesis: verum end; hence T is T_0-TopSpace by TSP_1:def_5; ::_thesis: verum end; registration let R be non empty reflexive transitive antisymmetric up-complete RelStr ; cluster -> up-complete for TopAugmentation of R; coherence for b1 being TopAugmentation of R holds b1 is up-complete ; end; theorem Th14: :: WAYBEL32:14 for R being non empty reflexive transitive antisymmetric up-complete RelStr for T being Scott TopAugmentation of R for x being Element of T for A being upper Subset of T st not x in A holds (downarrow x) ` is a_neighborhood of A proof let R be non empty reflexive transitive antisymmetric up-complete RelStr ; ::_thesis: for T being Scott TopAugmentation of R for x being Element of T for A being upper Subset of T st not x in A holds (downarrow x) ` is a_neighborhood of A let T be Scott TopAugmentation of R; ::_thesis: for x being Element of T for A being upper Subset of T st not x in A holds (downarrow x) ` is a_neighborhood of A let x be Element of T; ::_thesis: for A being upper Subset of T st not x in A holds (downarrow x) ` is a_neighborhood of A let A be upper Subset of T; ::_thesis: ( not x in A implies (downarrow x) ` is a_neighborhood of A ) assume A1: not x in A ; ::_thesis: (downarrow x) ` is a_neighborhood of A downarrow x is closed by WAYBEL11:11; then (downarrow x) ` is open ; then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23; A misses downarrow x by A1, WAYBEL11:5; then A c= (downarrow x) ` by SUBSET_1:23; hence (downarrow x) ` is a_neighborhood of A by A2, CONNSP_2:def_2; ::_thesis: verum end; theorem :: WAYBEL32:15 for R being non empty reflexive transitive antisymmetric up-complete TopRelStr for T being Scott TopAugmentation of R for S being upper Subset of T ex F being Subset-Family of T st ( S = meet F & ( for X being Subset of T st X in F holds X is a_neighborhood of S ) ) proof let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for T being Scott TopAugmentation of R for S being upper Subset of T ex F being Subset-Family of T st ( S = meet F & ( for X being Subset of T st X in F holds X is a_neighborhood of S ) ) let T be Scott TopAugmentation of R; ::_thesis: for S being upper Subset of T ex F being Subset-Family of T st ( S = meet F & ( for X being Subset of T st X in F holds X is a_neighborhood of S ) ) let S be upper Subset of T; ::_thesis: ex F being Subset-Family of T st ( S = meet F & ( for X being Subset of T st X in F holds X is a_neighborhood of S ) ) defpred S1[ set ] means \$1 is a_neighborhood of S; set F = { X where X is Subset of T : S1[X] } ; { X where X is Subset of T : S1[X] } is Subset-Family of T from DOMAIN_1:sch_7(); then reconsider F = { X where X is Subset of T : S1[X] } as Subset-Family of T ; take F ; ::_thesis: ( S = meet F & ( for X being Subset of T st X in F holds X is a_neighborhood of S ) ) thus S = meet F ::_thesis: for X being Subset of T st X in F holds X is a_neighborhood of S proof [#] T is a_neighborhood of S by CONNSP_2:28; then A1: [#] T in F ; now__::_thesis:_for_Z1_being_set_st_Z1_in_F_holds_ S_c=_Z1 let Z1 be set ; ::_thesis: ( Z1 in F implies S c= Z1 ) assume Z1 in F ; ::_thesis: S c= Z1 then ex X being Subset of T st ( Z1 = X & X is a_neighborhood of S ) ; hence S c= Z1 by CONNSP_2:29; ::_thesis: verum end; hence S c= meet F by A1, SETFAM_1:5; :: according to XBOOLE_0:def_10 ::_thesis: meet F c= S let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F or x in S ) assume that A2: x in meet F and A3: not x in S ; ::_thesis: contradiction reconsider p = x as Element of T by A2; (downarrow p) ` is a_neighborhood of S by A3, Th14; then (downarrow p) ` in F ; then A4: meet F c= (downarrow p) ` by SETFAM_1:3; p <= p ; then p in downarrow p by WAYBEL_0:17; hence contradiction by A2, A4, XBOOLE_0:def_5; ::_thesis: verum end; let X be Subset of T; ::_thesis: ( X in F implies X is a_neighborhood of S ) assume X in F ; ::_thesis: X is a_neighborhood of S then ex Y being Subset of T st ( X = Y & Y is a_neighborhood of S ) ; hence X is a_neighborhood of S ; ::_thesis: verum end; theorem :: WAYBEL32:16 for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr for S being Subset of T holds ( S is open iff ( S is upper & S is property(S) ) ) proof let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for S being Subset of T holds ( S is open iff ( S is upper & S is property(S) ) ) let S be Subset of T; ::_thesis: ( S is open iff ( S is upper & S is property(S) ) ) hereby ::_thesis: ( S is upper & S is property(S) implies S is open ) assume A1: S is open ; ::_thesis: ( S is upper & S is property(S) ) hence S is upper ; ::_thesis: S is property(S) thus S is property(S) ::_thesis: verum proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in S or ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in S ) ) ) ) assume sup D in S ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in S ) ) ) then S meets D by A1, WAYBEL11:def_1; then consider y being set such that A2: y in S and A3: y in D by XBOOLE_0:3; reconsider y = y as Element of T by A2; take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in S ) ) ) thus ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in S ) ) ) by A1, A2, A3, WAYBEL_0:def_20; ::_thesis: verum end; end; assume that A4: S is upper and A5: S is property(S) ; ::_thesis: S is open S is inaccessible proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,T) in S or not D misses S ) assume sup D in S ; ::_thesis: not D misses S then consider y being Element of T such that A6: y in D and A7: for x being Element of T st x in D & x >= y holds x in S by A5, WAYBEL11:def_3; y >= y by YELLOW_0:def_1; then y in S by A6, A7; hence not D misses S by A6, XBOOLE_0:3; ::_thesis: verum end; hence S is open by A4; ::_thesis: verum end; theorem Th17: :: WAYBEL32:17 for R being non empty reflexive transitive antisymmetric up-complete TopRelStr for S being non empty directed Subset of R for a being Element of R st a in S holds a <= "\/" (S,R) proof let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for S being non empty directed Subset of R for a being Element of R st a in S holds a <= "\/" (S,R) let S be non empty directed Subset of R; ::_thesis: for a being Element of R st a in S holds a <= "\/" (S,R) let a be Element of R; ::_thesis: ( a in S implies a <= "\/" (S,R) ) assume A1: a in S ; ::_thesis: a <= "\/" (S,R) ex_sup_of S,R by WAYBEL_0:75; then S is_<=_than "\/" (S,R) by YELLOW_0:30; hence a <= "\/" (S,R) by A1, LATTICE3:def_9; ::_thesis: verum end; registration let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ; cluster lower -> property(S) for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is lower holds b1 is property(S) proof let S be Subset of T; ::_thesis: ( S is lower implies S is property(S) ) assume A1: S is lower ; ::_thesis: S is property(S) let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in S or ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in S ) ) ) ) assume A2: sup D in S ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in S ) ) ) consider y being Element of T such that A3: y in D by SUBSET_1:4; take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in S ) ) ) thus y in D by A3; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in S ) let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in S ) assume that A4: x in D and x >= y ; ::_thesis: x in S x <= sup D by A4, Th17; hence x in S by A1, A2, WAYBEL_0:def_19; ::_thesis: verum end; end; theorem :: WAYBEL32:18 for T being non empty finite up-complete Poset for S being Subset of T holds S is inaccessible proof let T be non empty finite up-complete Poset; ::_thesis: for S being Subset of T holds S is inaccessible let S be Subset of T; ::_thesis: S is inaccessible let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,T) in S or not D misses S ) assume A1: sup D in S ; ::_thesis: not D misses S sup D in D proof reconsider D9 = D as finite Subset of T ; D9 c= D9 ; then reconsider E = D9 as finite Subset of D ; consider x being Element of T such that A2: x in D and A3: x is_>=_than E by WAYBEL_0:1; A4: for b being Element of T st D is_<=_than b holds b >= x by A2, LATTICE3:def_9; for c being Element of T st D is_<=_than c & ( for b being Element of T st D is_<=_than b holds b >= c ) holds c = x proof let c be Element of T; ::_thesis: ( D is_<=_than c & ( for b being Element of T st D is_<=_than b holds b >= c ) implies c = x ) assume that A5: D is_<=_than c and A6: for b being Element of T st D is_<=_than b holds b >= c ; ::_thesis: c = x A7: x >= c by A3, A6; c >= x by A2, A5, LATTICE3:def_9; hence c = x by A7, ORDERS_2:2; ::_thesis: verum end; then ex_sup_of D,T by A3, A4, YELLOW_0:def_7; hence sup D in D by A2, A3, A4, YELLOW_0:def_9; ::_thesis: verum end; hence not D misses S by A1, XBOOLE_0:3; ::_thesis: verum end; theorem Th19: :: WAYBEL32:19 for R being complete connected LATTICE for T being Scott TopAugmentation of R for x being Element of T holds (downarrow x) ` is open proof let R be complete connected LATTICE; ::_thesis: for T being Scott TopAugmentation of R for x being Element of T holds (downarrow x) ` is open let T be Scott TopAugmentation of R; ::_thesis: for x being Element of T holds (downarrow x) ` is open let x be Element of T; ::_thesis: (downarrow x) ` is open reconsider S = downarrow x as lower directly_closed Subset of T by WAYBEL11:8; S ` is open ; hence (downarrow x) ` is open ; ::_thesis: verum end; theorem :: WAYBEL32:20 for R being complete connected LATTICE for T being Scott TopAugmentation of R for S being Subset of T holds ( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ) proof let R be complete connected LATTICE; ::_thesis: for T being Scott TopAugmentation of R for S being Subset of T holds ( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ) let T be Scott TopAugmentation of R; ::_thesis: for S being Subset of T holds ( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ) let S be Subset of T; ::_thesis: ( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ) set DD = { ((downarrow x) `) where x is Element of T : verum } ; thus ( not S is open or S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ::_thesis: ( ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) implies S is open ) proof assume A1: S is open ; ::_thesis: ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) assume that A2: S <> the carrier of T and A3: not S in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: contradiction A4: ([#] T) \ S <> {} by A2, PRE_TOPC:4; A5: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then reconsider K = S ` as Subset of R ; reconsider D = K as non empty directed Subset of T by A4, A5, WAYBEL_0:3; A6: D misses S by SUBSET_1:23; reconsider x = sup D as Element of T ; S ` = downarrow x proof thus S ` c= downarrow x :: according to XBOOLE_0:def_10 ::_thesis: downarrow x c= S ` proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S ` or a in downarrow x ) assume A7: a in S ` ; ::_thesis: a in downarrow x then reconsider A = a as Element of T ; x is_>=_than S ` by YELLOW_0:32; then A <= x by A7, LATTICE3:def_9; hence a in downarrow x by WAYBEL_0:17; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in S ` ) assume A8: a in downarrow x ; ::_thesis: a in S ` then reconsider A = a as Element of T ; A9: A <= x by A8, WAYBEL_0:17; not x in S by A1, A6, WAYBEL11:def_1; then not A in S by A1, A9, WAYBEL_0:def_20; hence a in S ` by XBOOLE_0:def_5; ::_thesis: verum end; then (downarrow x) ` = S ; hence contradiction by A3; ::_thesis: verum end; assume A10: ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ; ::_thesis: S is open percases ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) by A10; supposeA11: S = the carrier of T ; ::_thesis: S is open A12: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then S = [#] R by A11; then A13: S is inaccessible by A12, YELLOW_9:47; S is upper proof let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in S or not x <= y or y in S ) assume that x in S and x <= y ; ::_thesis: y in S thus y in S by A11; ::_thesis: verum end; hence S is open by A13; ::_thesis: verum end; suppose S in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: S is open then ex x being Element of T st S = (downarrow x) ` ; hence S is open by Th19; ::_thesis: verum end; end; end; registration let R be non empty up-complete Poset; cluster non empty correct reflexive transitive antisymmetric up-complete order_consistent for TopAugmentation of R; correctness existence ex b1 being correct TopAugmentation of R st b1 is order_consistent ; proof set T = the correct Scott TopAugmentation of R; take the correct Scott TopAugmentation of R ; ::_thesis: the correct Scott TopAugmentation of R is order_consistent thus the correct Scott TopAugmentation of R is order_consistent by Th6; ::_thesis: verum end; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete order_consistent for TopRelStr ; correctness existence ex b1 being TopLattice st ( b1 is order_consistent & b1 is complete ); proof set T = the complete Scott TopLattice; take the complete Scott TopLattice ; ::_thesis: ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete ) thus ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete ) by Th6; ::_thesis: verum end; end; theorem Th21: :: WAYBEL32:21 for R being non empty TopRelStr for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds A is upper proof let R be non empty TopRelStr ; ::_thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds A is upper let A be Subset of R; ::_thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) & A is open implies A is upper ) assume A1: for x being Element of R holds downarrow x = Cl {x} ; ::_thesis: ( not A is open or A is upper ) assume A2: A is open ; ::_thesis: A is upper let x, y be Element of R; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A ) assume that A3: x in A and A4: x <= y ; ::_thesis: y in A x in downarrow y by A4, WAYBEL_0:17; then x in Cl {y} by A1; then A meets {y} by A2, A3, PRE_TOPC:24; then consider z being set such that A5: z in A /\ {y} by XBOOLE_0:4; A6: z in A by A5, XBOOLE_0:def_4; z in {y} by A5, XBOOLE_0:def_4; hence y in A by A6, TARSKI:def_1; ::_thesis: verum end; theorem :: WAYBEL32:22 for R being non empty TopRelStr for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds for A being Subset of R st A is closed holds A is lower proof let R be non empty TopRelStr ; ::_thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds for A being Subset of R st A is closed holds A is lower let A be Subset of R; ::_thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) implies for A being Subset of R st A is closed holds A is lower ) assume A1: for x being Element of R holds downarrow x = Cl {x} ; ::_thesis: for A being Subset of R st A is closed holds A is lower let A be Subset of R; ::_thesis: ( A is closed implies A is lower ) assume A2: A is closed ; ::_thesis: A is lower let x, y be Element of R; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in A or not y <= x or y in A ) assume that A3: x in A and A4: y <= x ; ::_thesis: y in A y in downarrow x by A4, WAYBEL_0:17; then A5: y in Cl {x} by A1; {x} c= A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in A ) assume a in {x} ; ::_thesis: a in A hence a in A by A3, TARSKI:def_1; ::_thesis: verum end; hence y in A by A2, A5, PRE_TOPC:15; ::_thesis: verum end; definition let S be non empty 1-sorted ; let R be non empty RelStr ; let f be Function of the carrier of R, the carrier of S; funcR *' f -> non empty strict NetStr over S means :Def3: :: WAYBEL32:def 3 ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of it = f ); existence ex b1 being non empty strict NetStr over S st ( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f ) proof reconsider M = NetStr(# the carrier of R, the InternalRel of R,f #) as non empty strict NetStr over S ; take M ; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f ) thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f ) ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict NetStr over S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b2 = f holds b1 = b2 ; end; :: deftheorem Def3 defines *' WAYBEL32:def_3_:_ for S being non empty 1-sorted for R being non empty RelStr for f being Function of the carrier of R, the carrier of S for b4 being non empty strict NetStr over S holds ( b4 = R *' f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b4 = f ) ); registration let S be non empty 1-sorted ; let R be non empty transitive RelStr ; let f be Function of the carrier of R, the carrier of S; clusterR *' f -> non empty transitive strict ; coherence R *' f is transitive proof RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3; hence R *' f is transitive by WAYBEL_8:13; ::_thesis: verum end; end; registration let S be non empty 1-sorted ; let R be non empty directed RelStr ; let f be Function of the carrier of R, the carrier of S; clusterR *' f -> non empty strict directed ; coherence R *' f is directed proof A1: RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3; [#] R is directed by WAYBEL_0:def_6; hence [#] (R *' f) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; definition let R be non empty RelStr ; let N be prenet of R; func inf_net N -> strict prenet of R means :Def4: :: WAYBEL32:def 4 ex f being Function of N,R st ( it = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ); existence ex b1 being strict prenet of R ex f being Function of N,R st ( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) proof deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . k) where k is Element of N : k >= \$1 } ,R); consider g being Function of the carrier of N, the carrier of R such that A1: for i being Element of N holds g . i = H1(i) from FUNCT_2:sch_4(); reconsider f = g as Function of N,R ; reconsider M = N *' f as strict prenet of R ; take M ; ::_thesis: ex f being Function of N,R st ( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) thus ex f being Function of N,R st ( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being strict prenet of R st ex f being Function of N,R st ( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st ( b2 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) holds b1 = b2 proof let M, P be strict prenet of R; ::_thesis: ( ex f being Function of N,R st ( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st ( P = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) implies M = P ) assume that A2: ex f being Function of N,R st ( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) and A3: ex f being Function of N,R st ( P = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) ; ::_thesis: M = P consider f1 being Function of N,R such that A4: M = N *' f1 and A5: for i being Element of N holds f1 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A2; consider f2 being Function of N,R such that A6: P = N *' f2 and A7: for i being Element of N holds f2 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A3; for i being set st i in the carrier of N holds f1 . i = f2 . i proof let i be set ; ::_thesis: ( i in the carrier of N implies f1 . i = f2 . i ) assume i in the carrier of N ; ::_thesis: f1 . i = f2 . i then reconsider i = i as Element of N ; f1 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A5 .= f2 . i by A7 ; hence f1 . i = f2 . i ; ::_thesis: verum end; hence M = P by A4, A6, FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def4 defines inf_net WAYBEL32:def_4_:_ for R being non empty RelStr for N being prenet of R for b3 being strict prenet of R holds ( b3 = inf_net N iff ex f being Function of N,R st ( b3 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) ); registration let R be non empty RelStr ; let N be net of R; cluster inf_net N -> transitive strict ; coherence inf_net N is transitive proof ex f being Function of N,R st ( inf_net N = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) by Def4; hence inf_net N is transitive ; ::_thesis: verum end; end; registration let R be non empty RelStr ; let N be net of R; cluster inf_net N -> strict ; coherence inf_net N is directed ; end; registration let R be non empty reflexive antisymmetric /\-complete RelStr ; let N be net of R; cluster inf_net N -> strict monotone ; coherence inf_net N is monotone proof let i, j be Element of (inf_net N); :: according to WAYBEL11:def_9 ::_thesis: ( not i <= j or (inf_net N) . i <= (inf_net N) . j ) assume A1: i <= j ; ::_thesis: (inf_net N) . i <= (inf_net N) . j consider f being Function of N,R such that A2: inf_net N = N *' f and A3: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4; A4: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A2, Def3; then reconsider i9 = i, j9 = j as Element of N ; deffunc H1( Element of N) -> Element of the carrier of R = N . R; defpred S1[ Element of N] means R >= j9; defpred S2[ Element of N] means R >= i9; set J = { H1(k) where k is Element of N : S1[k] } ; set I = { H1(k) where k is Element of N : S2[k] } ; A5: { H1(k) where k is Element of N : S1[k] } is Subset of R from DOMAIN_1:sch_8(); consider j0 being Element of N such that A6: j0 >= j9 and j0 >= j9 by YELLOW_6:def_3; N . j0 in { H1(k) where k is Element of N : S1[k] } by A6; then reconsider J9 = { H1(k) where k is Element of N : S1[k] } as non empty Subset of R by A5; A7: { H1(k) where k is Element of N : S2[k] } is Subset of R from DOMAIN_1:sch_8(); consider j1 being Element of N such that A8: j1 >= i9 and j1 >= i9 by YELLOW_6:def_3; N . j1 in { H1(k) where k is Element of N : S2[k] } by A8; then reconsider I9 = { H1(k) where k is Element of N : S2[k] } as non empty Subset of R by A7; A9: ex_inf_of J9,R by WAYBEL_0:76; A10: ex_inf_of I9,R by WAYBEL_0:76; A11: J9 c= I9 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in J9 or a in I9 ) assume A12: a in J9 ; ::_thesis: a in I9 then reconsider x = a as Element of R ; consider k being Element of N such that A13: x = N . k and A14: k >= j9 by A12; reconsider k9 = k as Element of N ; i9 <= j9 by A1, A4, YELLOW_0:1; then i9 <= k9 by A14, YELLOW_0:def_2; hence a in I9 by A13; ::_thesis: verum end; A15: f . i9 = "/\" ( { H1(k) where k is Element of N : S2[k] } ,R) by A3; A16: f . j9 = "/\" ( { H1(k) where k is Element of N : S1[k] } ,R) by A3; the mapping of (inf_net N) = f by A2, Def3; hence (inf_net N) . i <= (inf_net N) . j by A9, A10, A11, A15, A16, YELLOW_0:35; ::_thesis: verum end; end; registration let R be non empty reflexive antisymmetric /\-complete RelStr ; let N be net of R; cluster inf_net N -> strict eventually-directed ; coherence inf_net N is eventually-directed ; end; theorem Th23: :: WAYBEL32:23 for R being non empty RelStr for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } proof let R be non empty RelStr ; ::_thesis: for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } let N be net of R; ::_thesis: rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } consider f being Function of N,R such that A1: inf_net N = N *' f and A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4; A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3; A4: the mapping of (inf_net N) = f by A1, Def3; then A5: the carrier of (inf_net N) = dom f by FUNCT_2:def_1; thus rng the mapping of (inf_net N) c= { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } :: according to XBOOLE_0:def_10 ::_thesis: { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } c= rng the mapping of (inf_net N) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of (inf_net N) or e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ) assume e in rng the mapping of (inf_net N) ; ::_thesis: e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } then consider u being set such that A6: u in dom f and A7: e = f . u by A4, FUNCT_1:def_3; reconsider u = u as Element of N by A6; f . u = "/\" ( { (N . k) where k is Element of N : k >= u } ,R) by A2; hence e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } by A7; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } or e in rng the mapping of (inf_net N) ) assume e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: e in rng the mapping of (inf_net N) then consider j being Element of N such that A8: e = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ; e = the mapping of (inf_net N) . j by A2, A4, A8; hence e in rng the mapping of (inf_net N) by A3, A4, A5, FUNCT_1:def_3; ::_thesis: verum end; theorem Th24: :: WAYBEL32:24 for R being up-complete /\-complete LATTICE for N being net of R holds sup (inf_net N) = lim_inf N proof let R be up-complete /\-complete LATTICE; ::_thesis: for N being net of R holds sup (inf_net N) = lim_inf N let N be net of R; ::_thesis: sup (inf_net N) = lim_inf N defpred S1[ set ] means verum; deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . l) where l is Element of N : l >= \$1 } ,R); sup (inf_net N) = Sup by WAYBEL_2:def_1 .= sup (rng the mapping of (inf_net N)) by YELLOW_2:def_5 .= lim_inf N by Th23 ; hence sup (inf_net N) = lim_inf N ; ::_thesis: verum end; theorem :: WAYBEL32:25 for R being up-complete /\-complete LATTICE for N being net of R for i being Element of N holds sup (inf_net N) = lim_inf (N | i) proof let R be up-complete /\-complete LATTICE; ::_thesis: for N being net of R for i being Element of N holds sup (inf_net N) = lim_inf (N | i) let N be net of R; ::_thesis: for i being Element of N holds sup (inf_net N) = lim_inf (N | i) let i be Element of N; ::_thesis: sup (inf_net N) = lim_inf (N | i) sup (inf_net N) = lim_inf N by Th24; hence sup (inf_net N) = lim_inf (N | i) by WAYBEL21:41; ::_thesis: verum end; theorem Th26: :: WAYBEL32:26 for R being /\-complete Semilattice for N being net of R for V being upper Subset of R st inf_net N is_eventually_in V holds N is_eventually_in V proof let R be /\-complete Semilattice; ::_thesis: for N being net of R for V being upper Subset of R st inf_net N is_eventually_in V holds N is_eventually_in V let N be net of R; ::_thesis: for V being upper Subset of R st inf_net N is_eventually_in V holds N is_eventually_in V let V be upper Subset of R; ::_thesis: ( inf_net N is_eventually_in V implies N is_eventually_in V ) consider f being Function of N,R such that A1: inf_net N = N *' f and A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4; A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3; assume inf_net N is_eventually_in V ; ::_thesis: N is_eventually_in V then consider i being Element of (inf_net N) such that A4: for j being Element of (inf_net N) st i <= j holds (inf_net N) . j in V by WAYBEL_0:def_11; consider j0 being Element of (inf_net N) such that A5: i <= j0 and i <= j0 by YELLOW_6:def_3; A6: (inf_net N) . j0 in V by A4, A5; reconsider j9 = j0 as Element of N by A3; take j9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not j9 <= b1 or N . b1 in V ) let j be Element of N; ::_thesis: ( not j9 <= j or N . j in V ) assume A7: j9 <= j ; ::_thesis: N . j in V defpred S1[ Element of N] means \$1 >= j9; deffunc H1( Element of N) -> Element of the carrier of R = N . \$1; set E = { H1(k) where k is Element of N : S1[k] } ; { H1(k) where k is Element of N : S1[k] } is Subset of R from DOMAIN_1:sch_8(); then reconsider E = { H1(k) where k is Element of N : S1[k] } as Subset of R ; the mapping of (inf_net N) = f by A1, Def3; then A8: (inf_net N) . j0 = "/\" (E,R) by A2; N . j in E by A7; then "/\" (E,R) <= N . j by Th8; hence N . j in V by A6, A8, WAYBEL_0:def_20; ::_thesis: verum end; theorem :: WAYBEL32:27 for R being /\-complete Semilattice for N being net of R for V being lower Subset of R st N is_eventually_in V holds inf_net N is_eventually_in V proof let R be /\-complete Semilattice; ::_thesis: for N being net of R for V being lower Subset of R st N is_eventually_in V holds inf_net N is_eventually_in V let N be net of R; ::_thesis: for V being lower Subset of R st N is_eventually_in V holds inf_net N is_eventually_in V let V be lower Subset of R; ::_thesis: ( N is_eventually_in V implies inf_net N is_eventually_in V ) consider f being Function of N,R such that A1: inf_net N = N *' f and A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4; A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3; assume N is_eventually_in V ; ::_thesis: inf_net N is_eventually_in V then consider i being Element of N such that A4: for j being Element of N st i <= j holds N . j in V by WAYBEL_0:def_11; reconsider i9 = i as Element of (inf_net N) by A3; take i9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (inf_net N) holds ( not i9 <= b1 or (inf_net N) . b1 in V ) let j be Element of (inf_net N); ::_thesis: ( not i9 <= j or (inf_net N) . j in V ) assume A5: i9 <= j ; ::_thesis: (inf_net N) . j in V reconsider j0 = j as Element of N by A3; defpred S1[ Element of N] means \$1 >= j0; deffunc H1( Element of N) -> Element of the carrier of R = N . \$1; set E = { H1(k) where k is Element of N : S1[k] } ; consider j1 being Element of N such that A6: j1 >= j0 and j1 >= j0 by YELLOW_6:def_3; { H1(k) where k is Element of N : S1[k] } is Subset of R from DOMAIN_1:sch_8(); then reconsider E = { H1(k) where k is Element of N : S1[k] } as Subset of R ; i <= j0 by A3, A5, YELLOW_0:1; then i <= j1 by A6, YELLOW_0:def_2; then A7: N . j1 in V by A4; N . j1 in E by A6; then A8: "/\" (E,R) <= N . j1 by Th8; the mapping of (inf_net N) = f by A1, Def3; then (inf_net N) . j = "/\" (E,R) by A2; hence (inf_net N) . j in V by A7, A8, WAYBEL_0:def_19; ::_thesis: verum end; theorem Th28: :: WAYBEL32:28 for R being non empty up-complete /\-complete order_consistent TopLattice for N being net of R for x being Element of R st x <= lim_inf N holds x is_a_cluster_point_of N proof let R be non empty up-complete /\-complete order_consistent TopLattice; ::_thesis: for N being net of R for x being Element of R st x <= lim_inf N holds x is_a_cluster_point_of N let N be net of R; ::_thesis: for x being Element of R st x <= lim_inf N holds x is_a_cluster_point_of N let x be Element of R; ::_thesis: ( x <= lim_inf N implies x is_a_cluster_point_of N ) assume A1: x <= lim_inf N ; ::_thesis: x is_a_cluster_point_of N defpred S1[ Element of N] means verum; deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,R); set X = { H1(j) where j is Element of N : S1[j] } ; { H1(j) where j is Element of N : S1[j] } is Subset of R from DOMAIN_1:sch_8(); then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of R ; reconsider D = D as non empty directed Subset of R by Th7; sup D = lim_inf N ; then A2: sup D = sup (inf_net N) by Th24; let V be a_neighborhood of x; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in V for a being Element of R holds downarrow a = Cl {a} by Def2; then A3: Int V is upper by Th21; x in Int V by CONNSP_2:def_1; then sup D in Int V by A1, A3, WAYBEL_0:def_20; then reconsider W = Int V as a_neighborhood of sup D by CONNSP_2:3; A4: Int V c= V by TOPS_1:16; inf_net N is_eventually_in W by A2, Def2; then N is_eventually_in W by A3, Th26; then N is_eventually_in V by A4, WAYBEL_0:8; hence N is_often_in V by YELLOW_6:19; ::_thesis: verum end; theorem :: WAYBEL32:29 for R being non empty up-complete /\-complete order_consistent TopLattice for N being eventually-directed net of R for x being Element of R holds ( x <= lim_inf N iff x is_a_cluster_point_of N ) proof let R be non empty up-complete /\-complete order_consistent TopLattice; ::_thesis: for N being eventually-directed net of R for x being Element of R holds ( x <= lim_inf N iff x is_a_cluster_point_of N ) let N be eventually-directed net of R; ::_thesis: for x being Element of R holds ( x <= lim_inf N iff x is_a_cluster_point_of N ) let x be Element of R; ::_thesis: ( x <= lim_inf N iff x is_a_cluster_point_of N ) thus ( x <= lim_inf N implies x is_a_cluster_point_of N ) by Th28; ::_thesis: ( x is_a_cluster_point_of N implies x <= lim_inf N ) thus ( x is_a_cluster_point_of N implies x <= lim_inf N ) ::_thesis: verum proof assume A1: x is_a_cluster_point_of N ; ::_thesis: x <= lim_inf N defpred S1[ Element of N] means verum; deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,R); set X = { H1(j) where j is Element of N : S1[j] } ; { H1(j) where j is Element of N : S1[j] } is Subset of R from DOMAIN_1:sch_8(); then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of R ; reconsider D = D as non empty directed Subset of R by Th7; for G being Subset of R st G is open & x in G holds {(sup D)} meets G proof let G be Subset of R; ::_thesis: ( G is open & x in G implies {(sup D)} meets G ) assume A2: G is open ; ::_thesis: ( not x in G or {(sup D)} meets G ) assume x in G ; ::_thesis: {(sup D)} meets G then reconsider G = G as a_neighborhood of x by A2, CONNSP_2:3; A3: N is_often_in G by A1, WAYBEL_9:def_9; now__::_thesis:_for_i_being_Element_of_N_holds_sup_D_in_G let i be Element of N; ::_thesis: sup D in G consider j1 being Element of N such that i <= j1 and A4: N . j1 in G by A3, WAYBEL_0:def_12; consider j2 being Element of N such that A5: for k being Element of N st j2 <= k holds N . j1 <= N . k by WAYBEL_0:11; defpred S2[ Element of N] means \$1 >= j2; deffunc H2( Element of N) -> Element of the carrier of R = N . \$1; set E = { H2(k) where k is Element of N : S2[k] } ; A6: { H2(k) where k is Element of N : S2[k] } is Subset of R from DOMAIN_1:sch_8(); consider j9 being Element of N such that A7: j9 >= j2 and j9 >= j2 by YELLOW_6:def_3; N . j9 in { H2(k) where k is Element of N : S2[k] } by A7; then reconsider E9 = { H2(k) where k is Element of N : S2[k] } as non empty Subset of R by A6; A8: ex_inf_of E9,R by WAYBEL_0:76; N . j1 is_<=_than E9 proof let b be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not b in E9 or N . j1 <= b ) assume b in E9 ; ::_thesis: N . j1 <= b then ex k being Element of N st ( b = N . k & k >= j2 ) ; hence N . j1 <= b by A5; ::_thesis: verum end; then A9: N . j1 <= "/\" (E9,R) by A8, YELLOW_0:31; for a being Element of R holds downarrow a = Cl {a} by Def2; then A10: G is upper by A2, Th21; then A11: "/\" (E9,R) in G by A4, A9, WAYBEL_0:def_20; "/\" (E9,R) in D ; then "/\" (E9,R) <= sup D by Th17; hence sup D in G by A10, A11, WAYBEL_0:def_20; ::_thesis: verum end; then A12: sup D in G ; sup D in {(sup D)} by TARSKI:def_1; hence {(sup D)} meets G by A12, XBOOLE_0:3; ::_thesis: verum end; then x in Cl {(sup D)} by PRE_TOPC:24; then x in downarrow (sup D) by Def2; hence x <= lim_inf N by WAYBEL_0:17; ::_thesis: verum end; end;