:: WAYBEL11 semantic presentation begin Lm1: for R, S being RelStr for p, q being Element of R for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds p9 <= q9 proof let R, S be RelStr ; ::_thesis: for p, q being Element of R for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds p9 <= q9 let p, q be Element of R; ::_thesis: for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds p9 <= q9 let p9, q9 be Element of S; ::_thesis: ( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q implies p9 <= q9 ) assume that A1: p = p9 and A2: q = q9 and A3: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) ; ::_thesis: ( not p <= q or p9 <= q9 ) assume p <= q ; ::_thesis: p9 <= q9 then [p9,q9] in the InternalRel of S by A1, A2, A3, ORDERS_2:def_5; hence p9 <= q9 by ORDERS_2:def_5; ::_thesis: verum end; scheme :: WAYBEL11:sch 1 Irrel{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> set , F4( set , set ) -> set } : { F3(u) where u is Element of F1() : P1[u] } = { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } provided A1: for i being Element of F2() for u being Element of F1() holds F3(u) = F4(i,u) proof set A = { F3(u) where u is Element of F1() : P1[u] } ; set B = { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } ; thus { F3(u) where u is Element of F1() : P1[u] } c= { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } :: according to XBOOLE_0:def_10 ::_thesis: { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } c= { F3(u) where u is Element of F1() : P1[u] } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { F3(u) where u is Element of F1() : P1[u] } or e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } ) set i = the Element of F2(); assume e in { F3(u) where u is Element of F1() : P1[u] } ; ::_thesis: e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } then consider u being Element of F1() such that A2: e = F3(u) and A3: P1[u] ; e = F4( the Element of F2(),u) by A1, A2; hence e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } by A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } or e in { F3(u) where u is Element of F1() : P1[u] } ) assume e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } ; ::_thesis: e in { F3(u) where u is Element of F1() : P1[u] } then consider i being Element of F2(), u being Element of F1() such that A4: e = F4(i,u) and A5: P1[u] ; e = F3(u) by A1, A4; hence e in { F3(u) where u is Element of F1() : P1[u] } by A5; ::_thesis: verum end; theorem Th1: :: WAYBEL11:1 for L being complete LATTICE for X, Y being Subset of L st Y is_coarser_than X holds "/\" (X,L) <= "/\" (Y,L) proof let L be complete LATTICE; ::_thesis: for X, Y being Subset of L st Y is_coarser_than X holds "/\" (X,L) <= "/\" (Y,L) let X, Y be Subset of L; ::_thesis: ( Y is_coarser_than X implies "/\" (X,L) <= "/\" (Y,L) ) assume A1: Y is_coarser_than X ; ::_thesis: "/\" (X,L) <= "/\" (Y,L) "/\" (X,L) is_<=_than Y proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in Y or "/\" (X,L) <= y ) assume y in Y ; ::_thesis: "/\" (X,L) <= y then consider x being Element of L such that A2: x in X and A3: x <= y by A1, YELLOW_4:def_2; "/\" (X,L) <= x by A2, YELLOW_2:22; hence "/\" (X,L) <= y by A3, YELLOW_0:def_2; ::_thesis: verum end; hence "/\" (X,L) <= "/\" (Y,L) by YELLOW_0:33; ::_thesis: verum end; theorem Th2: :: WAYBEL11:2 for L being complete LATTICE for X, Y being Subset of L st X is_finer_than Y holds "\/" (X,L) <= "\/" (Y,L) proof let L be complete LATTICE; ::_thesis: for X, Y being Subset of L st X is_finer_than Y holds "\/" (X,L) <= "\/" (Y,L) let X, Y be Subset of L; ::_thesis: ( X is_finer_than Y implies "\/" (X,L) <= "\/" (Y,L) ) assume A1: X is_finer_than Y ; ::_thesis: "\/" (X,L) <= "\/" (Y,L) "\/" (Y,L) is_>=_than X proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= "\/" (Y,L) ) assume x in X ; ::_thesis: x <= "\/" (Y,L) then consider y being Element of L such that A2: y in Y and A3: x <= y by A1, YELLOW_4:def_1; "\/" (Y,L) >= y by A2, YELLOW_2:22; hence x <= "\/" (Y,L) by A3, YELLOW_0:def_2; ::_thesis: verum end; hence "\/" (X,L) <= "\/" (Y,L) by YELLOW_0:32; ::_thesis: verum end; theorem :: WAYBEL11:3 for T being RelStr for A being upper Subset of T for B being directed Subset of T holds A /\ B is directed proof let T be RelStr ; ::_thesis: for A being upper Subset of T for B being directed Subset of T holds A /\ B is directed let A be upper Subset of T; ::_thesis: for B being directed Subset of T holds A /\ B is directed let B be directed Subset of T; ::_thesis: A /\ B is directed let x, y be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in A /\ B or not y in A /\ B or ex b1 being Element of the carrier of T st ( b1 in A /\ B & x <= b1 & y <= b1 ) ) assume that A1: x in A /\ B and A2: y in A /\ B ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in A /\ B & x <= b1 & y <= b1 ) A3: x in B by A1, XBOOLE_0:def_4; y in B by A2, XBOOLE_0:def_4; then consider z being Element of T such that A4: z in B and A5: x <= z and A6: y <= z by A3, WAYBEL_0:def_1; take z ; ::_thesis: ( z in A /\ B & x <= z & y <= z ) x in A by A1, XBOOLE_0:def_4; then z in A by A5, WAYBEL_0:def_20; hence z in A /\ B by A4, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z ) thus ( x <= z & y <= z ) by A5, A6; ::_thesis: verum end; registration let T be non empty reflexive RelStr ; cluster non empty finite directed for Element of bool the carrier of T; existence ex b1 being Subset of T st ( not b1 is empty & b1 is directed & b1 is finite ) proof set x = the Element of T; take { the Element of T} ; ::_thesis: ( not { the Element of T} is empty & { the Element of T} is directed & { the Element of T} is finite ) thus ( not { the Element of T} is empty & { the Element of T} is directed & { the Element of T} is finite ) by WAYBEL_0:5; ::_thesis: verum end; end; theorem Th4: :: WAYBEL11:4 for T being with_suprema Poset for D being non empty finite directed Subset of T holds sup D in D proof let T be reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for D being non empty finite directed Subset of T holds sup D in D let D be non empty finite directed Subset of T; ::_thesis: sup D in D D c= D ; then reconsider E = D as finite Subset of D ; consider x being Element of T such that A1: x in D and A2: x is_>=_than E by WAYBEL_0:1; A3: for b being Element of T st D is_<=_than b holds b >= x by A1, 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 A4: D is_<=_than c and A5: for b being Element of T st D is_<=_than b holds b >= c ; ::_thesis: c = x A6: x >= c by A2, A5; c >= x by A1, A4, LATTICE3:def_9; hence c = x by A6, ORDERS_2:2; ::_thesis: verum end; then ex_sup_of D,T by A2, A3, YELLOW_0:def_7; hence sup D in D by A1, A2, A3, YELLOW_0:def_9; ::_thesis: verum end; registration cluster finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ; existence ex b1 being RelStr st ( b1 is reflexive & b1 is transitive & b1 is 1 -element & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & 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 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict ) thus T is reflexive ::_thesis: ( T is transitive & T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & 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 ; T9 is transitive ; hence T is transitive ; ::_thesis: ( T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict ) thus T is 1 -element ; ::_thesis: ( T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict ) T9 is antisymmetric ; hence T is antisymmetric ; ::_thesis: ( T is with_suprema & T is with_infima & T is finite & T is strict ) T9 is with_suprema ; hence T is with_suprema ; ::_thesis: ( T is with_infima & T is finite & T is strict ) T9 is with_infima ; hence T is with_infima ; ::_thesis: ( T is finite & T is strict ) thus T is finite ; ::_thesis: T is strict thus T is strict ; ::_thesis: verum end; end; registration let T be finite 1-sorted ; cluster -> finite for Element of bool the carrier of T; coherence for b1 being Subset of T holds b1 is finite ; end; registration let R be RelStr ; cluster empty -> lower upper for Element of bool the carrier of R; coherence for b1 being Subset of R st b1 is empty holds ( b1 is lower & b1 is upper ) proof let S be Subset of R; ::_thesis: ( S is empty implies ( S is lower & S is upper ) ) assume S is empty ; ::_thesis: ( S is lower & S is upper ) then A1: S = {} R ; hence for x, y being Element of R st x in S & y <= x holds y in S ; :: according to WAYBEL_0:def_19 ::_thesis: S is upper thus for x, y being Element of R st x in S & x <= y holds y in S by A1; :: according to WAYBEL_0:def_20 ::_thesis: verum end; end; registration let R be 1 -element RelStr ; cluster -> upper for Element of bool the carrier of R; coherence for b1 being Subset of R holds b1 is upper proof let S be Subset of R; ::_thesis: S is upper ex x being Element of R st the carrier of R = {x} by TEX_1:def_1; then ( S = {} R or S = [#] R ) by ZFMISC_1:33; hence S is upper ; ::_thesis: verum end; end; theorem Th5: :: WAYBEL11:5 for T being non empty RelStr for x being Element of T for A being upper Subset of T st not x in A holds A misses downarrow x proof let T be non empty RelStr ; ::_thesis: for x being Element of T for A being upper Subset of T st not x in A holds A misses downarrow x let x be Element of T; ::_thesis: for A being upper Subset of T st not x in A holds A misses downarrow x let A be upper Subset of T; ::_thesis: ( not x in A implies A misses downarrow x ) assume A1: not x in A ; ::_thesis: A misses downarrow x assume A meets downarrow x ; ::_thesis: contradiction then consider y being set such that A2: y in A and A3: y in downarrow x by XBOOLE_0:3; reconsider y = y as Element of T by A2; y <= x by A3, WAYBEL_0:17; hence contradiction by A1, A2, WAYBEL_0:def_20; ::_thesis: verum end; theorem Th6: :: WAYBEL11:6 for T being non empty RelStr for x being Element of T for A being lower Subset of T st x in A holds downarrow x c= A proof let T be non empty RelStr ; ::_thesis: for x being Element of T for A being lower Subset of T st x in A holds downarrow x c= A let x be Element of T; ::_thesis: for A being lower Subset of T st x in A holds downarrow x c= A let A be lower Subset of T; ::_thesis: ( x in A implies downarrow x c= A ) assume x in A ; ::_thesis: downarrow x c= A then not x in A ` by XBOOLE_0:def_5; then A ` misses downarrow x by Th5; then A ` c= (downarrow x) ` by SUBSET_1:23; hence downarrow x c= A by SUBSET_1:12; ::_thesis: verum end; begin definition let T be non empty reflexive RelStr ; let S be Subset of T; attrS is inaccessible_by_directed_joins means :Def1: :: WAYBEL11:def 1 for D being non empty directed Subset of T st sup D in S holds D meets S; attrS is closed_under_directed_sups means :Def2: :: WAYBEL11:def 2 for D being non empty directed Subset of T st D c= S holds sup D in S; attrS is property(S) means :Def3: :: WAYBEL11:def 3 for D being non empty directed Subset of T st sup D in S holds ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ); end; :: deftheorem Def1 defines inaccessible_by_directed_joins WAYBEL11:def_1_:_ for T being non empty reflexive RelStr for S being Subset of T holds ( S is inaccessible_by_directed_joins iff for D being non empty directed Subset of T st sup D in S holds D meets S ); :: deftheorem Def2 defines closed_under_directed_sups WAYBEL11:def_2_:_ for T being non empty reflexive RelStr for S being Subset of T holds ( S is closed_under_directed_sups iff for D being non empty directed Subset of T st D c= S holds sup D in S ); :: deftheorem Def3 defines property(S) WAYBEL11:def_3_:_ for T being non empty reflexive RelStr for S being Subset of T holds ( S is property(S) iff for D being non empty directed Subset of T st sup D in S holds ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ) ); notation let T be non empty reflexive RelStr ; let S be Subset of T; synonym inaccessible S for inaccessible_by_directed_joins ; synonym directly_closed S for closed_under_directed_sups ; end; registration let T be non empty reflexive RelStr ; cluster empty -> directly_closed property(S) for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is empty holds ( b1 is property(S) & b1 is directly_closed ) proof let S be Subset of T; ::_thesis: ( S is empty implies ( S is property(S) & S is directly_closed ) ) assume S is empty ; ::_thesis: ( S is property(S) & S is directly_closed ) then A1: S = {} T ; for D being non empty directed Subset of T st sup D in {} T holds ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in {} T ) ) ; hence S is property(S) by A1, Def3; ::_thesis: S is directly_closed thus for D being non empty directed Subset of T st D c= S holds sup D in S by A1; :: according to WAYBEL11:def_2 ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; cluster directly_closed property(S) for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is property(S) & b1 is directly_closed ) proof take {} T ; ::_thesis: ( {} T is property(S) & {} T is directly_closed ) thus ( {} T is property(S) & {} T is directly_closed ) ; ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; let S be property(S) Subset of T; clusterS ` -> directly_closed ; coherence S ` is closed_under_directed_sups proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= S ` implies sup D in S ` ) assume A1: D c= S ` ; ::_thesis: sup D in S ` assume not sup D in S ` ; ::_thesis: contradiction then sup D in S by XBOOLE_0:def_5; then consider y being Element of T such that A2: y in D and A3: for x being Element of T st x in D & x >= y holds x in S by Def3; y <= y ; then y in S by A2, A3; then D /\ S <> {} by A2, XBOOLE_0:def_4; then D meets S by XBOOLE_0:def_7; hence contradiction by A1, SUBSET_1:23; ::_thesis: verum end; end; definition let T be non empty reflexive TopRelStr ; attrT is Scott means :Def4: :: WAYBEL11:def 4 for S being Subset of T holds ( S is open iff ( S is inaccessible & S is upper ) ); end; :: deftheorem Def4 defines Scott WAYBEL11:def_4_:_ for T being non empty reflexive TopRelStr holds ( T is Scott iff for S being Subset of T holds ( S is open iff ( S is inaccessible & S is upper ) ) ); registration let T be non empty finite reflexive transitive antisymmetric with_suprema RelStr ; cluster -> inaccessible for Element of bool the carrier of T; coherence for b1 being Subset of T holds b1 is inaccessible proof 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: ( sup D in S implies D meets S ) assume A1: sup D in S ; ::_thesis: D meets S sup D in D by Th4; hence D meets S by A1, XBOOLE_0:3; ::_thesis: verum end; end; definition let T be non empty finite reflexive transitive antisymmetric with_suprema TopRelStr ; redefine attr T is Scott means :: WAYBEL11:def 5 for S being Subset of T holds ( S is open iff S is upper ); compatibility ( T is Scott iff for S being Subset of T holds ( S is open iff S is upper ) ) proof thus ( T is Scott implies for S being Subset of T holds ( S is open iff S is upper ) ) by Def4; ::_thesis: ( ( for S being Subset of T holds ( S is open iff S is upper ) ) implies T is Scott ) assume A1: for S being Subset of T holds ( S is open iff S is upper ) ; ::_thesis: T is Scott let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) ) thus ( S is open iff ( S is inaccessible & S is upper ) ) by A1; ::_thesis: verum end; end; :: deftheorem defines Scott WAYBEL11:def_5_:_ for T being non empty finite reflexive transitive antisymmetric with_suprema TopRelStr holds ( T is Scott iff for S being Subset of T holds ( S is open iff S is upper ) ); registration cluster non empty 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ; existence ex b1 being TopLattice st ( b1 is complete & b1 is strict & b1 is 1 -element & b1 is Scott ) proof set T = the finite 1 -element discrete reflexive strict TopRelStr ; take the finite 1 -element discrete reflexive strict TopRelStr ; ::_thesis: ( the finite 1 -element discrete reflexive strict TopRelStr is complete & the finite 1 -element discrete reflexive strict TopRelStr is strict & the finite 1 -element discrete reflexive strict TopRelStr is 1 -element & the finite 1 -element discrete reflexive strict TopRelStr is Scott ) thus ( the finite 1 -element discrete reflexive strict TopRelStr is complete & the finite 1 -element discrete reflexive strict TopRelStr is strict & the finite 1 -element discrete reflexive strict TopRelStr is 1 -element ) ; ::_thesis: the finite 1 -element discrete reflexive strict TopRelStr is Scott let S be Subset of the finite 1 -element discrete reflexive strict TopRelStr ; :: according to WAYBEL11:def_5 ::_thesis: ( S is open iff S is upper ) thus ( S is open iff S is upper ) by TDLAT_3:15; ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; cluster [#] T -> inaccessible directly_closed ; coherence ( [#] T is closed_under_directed_sups & [#] T is inaccessible_by_directed_joins ) proof thus [#] T is directly_closed ::_thesis: [#] T is inaccessible_by_directed_joins proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= [#] T implies sup D in [#] T ) assume D c= [#] T ; ::_thesis: sup D in [#] T thus sup D in [#] T ; ::_thesis: verum end; let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in [#] T implies D meets [#] T ) assume sup D in [#] T ; ::_thesis: D meets [#] T ex p being Element of T st p in D by SUBSET_1:4; hence D meets [#] T by XBOOLE_0:3; ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; cluster lower upper inaccessible directly_closed for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is directly_closed & b1 is lower & b1 is inaccessible & b1 is upper ) proof take [#] T ; ::_thesis: ( [#] T is directly_closed & [#] T is lower & [#] T is inaccessible & [#] T is upper ) thus ( [#] T is directly_closed & [#] T is lower & [#] T is inaccessible & [#] T is upper ) ; ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; let S be inaccessible Subset of T; clusterS ` -> directly_closed ; coherence S ` is closed_under_directed_sups proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= S ` implies sup D in S ` ) assume D c= S ` ; ::_thesis: sup D in S ` then D misses S by SUBSET_1:23; then not sup D in S by Def1; hence sup D in S ` by XBOOLE_0:def_5; ::_thesis: verum end; end; registration let T be non empty reflexive RelStr ; let S be directly_closed Subset of T; clusterS ` -> inaccessible ; coherence S ` is inaccessible_by_directed_joins proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S ` implies D meets S ` ) assume sup D in S ` ; ::_thesis: D meets S ` then not sup D in S by XBOOLE_0:def_5; then not D c= (S `) ` by Def2; hence D meets S ` by SUBSET_1:23; ::_thesis: verum end; end; theorem Th7: :: WAYBEL11:7 for T being non empty reflexive transitive up-complete Scott TopRelStr for S being Subset of T holds ( S is closed iff ( S is directly_closed & S is lower ) ) proof let T be non empty reflexive transitive up-complete Scott TopRelStr ; ::_thesis: for S being Subset of T holds ( S is closed iff ( S is directly_closed & S is lower ) ) let S be Subset of T; ::_thesis: ( S is closed iff ( S is directly_closed & S is lower ) ) hereby ::_thesis: ( S is directly_closed & S is lower implies S is closed ) assume S is closed ; ::_thesis: ( S is directly_closed & S is lower ) then S ` is open by TOPS_1:3; then reconsider A = S ` as upper inaccessible Subset of T by Def4; ( A ` is directly_closed & A ` is lower ) ; hence ( S is directly_closed & S is lower ) ; ::_thesis: verum end; assume ( S is directly_closed & S is lower ) ; ::_thesis: S is closed then reconsider S = S as lower directly_closed Subset of T ; S ` is open by Def4; hence S is closed by TOPS_1:3; ::_thesis: verum end; theorem Th8: :: WAYBEL11:8 for T being non empty reflexive transitive antisymmetric up-complete TopRelStr for x being Element of T holds downarrow x is directly_closed proof let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for x being Element of T holds downarrow x is directly_closed let x be Element of T; ::_thesis: downarrow x is directly_closed downarrow x is directly_closed proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= downarrow x implies sup D in downarrow x ) assume A1: D c= downarrow x ; ::_thesis: sup D in downarrow x ex a being Element of T st ( a is_>=_than D & ( for b being Element of T st b is_>=_than D holds a <= b ) ) by WAYBEL_0:def_39; then A2: ex_sup_of D,T by YELLOW_0:15; x is_>=_than D proof let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in D or b <= x ) assume b in D ; ::_thesis: b <= x hence b <= x by A1, WAYBEL_0:17; ::_thesis: verum end; then sup D <= x by A2, YELLOW_0:30; hence sup D in downarrow x by WAYBEL_0:17; ::_thesis: verum end; hence downarrow x is directly_closed ; ::_thesis: verum end; theorem Th9: :: WAYBEL11:9 for T being complete Scott TopLattice for x being Element of T holds Cl {x} = downarrow x proof let T be complete Scott TopLattice; ::_thesis: for x being Element of T holds Cl {x} = downarrow x let x be Element of T; ::_thesis: Cl {x} = downarrow x downarrow x is directly_closed by Th8; then A1: downarrow x is closed by Th7; 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_T_st_{x}_c=_C_&_C_is_closed_holds_ downarrow_x_c=_C let C be Subset of T; ::_thesis: ( {x} c= C & C is closed implies downarrow x c= C ) assume A3: {x} c= C ; ::_thesis: ( C is closed implies downarrow x c= C ) reconsider D = C as Subset of T ; assume C is closed ; ::_thesis: downarrow x c= C then A4: D is lower by Th7; x in C by A3, ZFMISC_1:31; hence downarrow x c= C by A4, Th6; ::_thesis: verum end; hence Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum end; theorem :: WAYBEL11:10 for T being complete Scott TopLattice holds T is T_0-TopSpace proof let T be complete Scott TopLattice; ::_thesis: T is T_0-TopSpace now__::_thesis:_for_x,_y_being_Point_of_T_st_x_<>_y_holds_ Cl_{x}_<>_Cl_{y} let x, y be Point of T; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} ) reconsider x9 = x, y9 = y as Element of T ; A1: Cl {x9} = downarrow x9 by Th9; A2: Cl {y9} = downarrow y9 by Th9; 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; theorem Th11: :: WAYBEL11:11 for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr for x being Element of T holds downarrow x is closed proof let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for x being Element of T holds downarrow x is closed let x be Element of T; ::_thesis: downarrow x is closed ( downarrow x is directly_closed & downarrow x is lower ) by Th8; hence downarrow x is closed by Th7; ::_thesis: verum end; theorem Th12: :: WAYBEL11:12 for T being up-complete Scott TopLattice for x being Element of T holds (downarrow x) ` is open proof let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds (downarrow x) ` is open let x be Element of T; ::_thesis: (downarrow x) ` is open downarrow x is closed by Th11; hence (downarrow x) ` is open ; ::_thesis: verum end; theorem Th13: :: WAYBEL11:13 for T being up-complete Scott TopLattice 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 T be up-complete Scott TopLattice; ::_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 open by Th12; then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23; A misses downarrow x by A1, Th5; 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 :: WAYBEL11:14 for T being complete Scott TopLattice 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 T be complete Scott TopLattice; ::_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, Th13; 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 :: WAYBEL11:15 for T being Scott TopLattice for S being Subset of T holds ( S is open iff ( S is upper & S is property(S) ) ) proof let T be Scott TopLattice; ::_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 A2: S is upper by Def4; ::_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: ( sup D in S implies ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ) ) assume A3: sup D in S ; ::_thesis: ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ) S is inaccessible by A1, Def4; then S meets D by A3, Def1; then consider y being set such that A4: y in S and A5: y in D by XBOOLE_0:3; reconsider y = y as Element of T by A4; take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ) thus ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ) by A2, A4, A5, WAYBEL_0:def_20; ::_thesis: verum end; end; assume that A6: S is upper and A7: 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: ( sup D in S implies D meets S ) assume sup D in S ; ::_thesis: D meets S then consider y being Element of T such that A8: y in D and A9: for x being Element of T st x in D & x >= y holds x in S by A7, Def3; y >= y by YELLOW_0:def_1; then y in S by A8, A9; hence D meets S by A8, XBOOLE_0:3; ::_thesis: verum end; hence S is open by A6, Def4; ::_thesis: verum end; registration let T be complete TopLattice; 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: ( sup D in S implies ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in S ) ) ) assume A2: sup D in S ; ::_thesis: ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x 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 x being Element of T st x in D & x >= y holds x in S ) ) thus y in D by A3; ::_thesis: for x being Element of T st x in D & x >= y holds x in S let x be Element of T; ::_thesis: ( x in D & x >= y implies x in S ) assume that A4: x in D and x >= y ; ::_thesis: x in S x <= sup D by A4, YELLOW_2:22; hence x in S by A1, A2, WAYBEL_0:def_19; ::_thesis: verum end; end; Lm2: for T being non empty reflexive TopRelStr holds [#] T is property(S) proof let T be non empty reflexive TopRelStr ; ::_thesis: [#] T is property(S) let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in [#] T implies ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in [#] T ) ) ) assume sup D in [#] T ; ::_thesis: ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in [#] T ) ) consider y being Element of T such that A1: y in D by SUBSET_1:4; take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds x in [#] T ) ) thus y in D by A1; ::_thesis: for x being Element of T st x in D & x >= y holds x in [#] T let x be Element of T; ::_thesis: ( x in D & x >= y implies x in [#] T ) assume that x in D and x >= y ; ::_thesis: x in [#] T thus x in [#] T ; ::_thesis: verum end; theorem :: WAYBEL11:16 for T being non empty reflexive transitive TopRelStr st the topology of T = { S where S is Subset of T : S is property(S) } holds T is TopSpace-like proof let T be non empty reflexive transitive TopRelStr ; ::_thesis: ( the topology of T = { S where S is Subset of T : S is property(S) } implies T is TopSpace-like ) assume A1: the topology of T = { S where S is Subset of T : S is property(S) } ; ::_thesis: T is TopSpace-like [#] T is property(S) by Lm2; hence the carrier of T in the topology of T by A1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds ( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds ( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) ) hereby ::_thesis: for b1, b2 being Element of bool the carrier of T holds ( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) let a be Subset-Family of T; ::_thesis: ( a c= the topology of T implies union a in the topology of T ) assume A2: a c= the topology of T ; ::_thesis: union a in the topology of T union a is property(S) proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in union a implies ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in union a ) ) ) assume sup D in union a ; ::_thesis: ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in union a ) ) then consider x being set such that A3: sup D in x and A4: x in a by TARSKI:def_4; x in the topology of T by A2, A4; then consider X being Subset of T such that A5: x = X and A6: X is property(S) by A1; consider y being Element of T such that A7: y in D and A8: for x being Element of T st x in D & x >= y holds x in X by A3, A5, A6, Def3; take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds x in union a ) ) thus y in D by A7; ::_thesis: for x being Element of T st x in D & x >= y holds x in union a let u be Element of T; ::_thesis: ( u in D & u >= y implies u in union a ) assume that A9: u in D and A10: u >= y ; ::_thesis: u in union a u in X by A8, A9, A10; hence u in union a by A4, A5, TARSKI:def_4; ::_thesis: verum end; hence union a in the topology of T by A1; ::_thesis: verum end; let a, b be Subset of T; ::_thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T ) assume a in the topology of T ; ::_thesis: ( not b in the topology of T or a /\ b in the topology of T ) then consider A being Subset of T such that A11: a = A and A12: A is property(S) by A1; assume b in the topology of T ; ::_thesis: a /\ b in the topology of T then consider B being Subset of T such that A13: b = B and A14: B is property(S) by A1; A /\ B is property(S) proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in A /\ B implies ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in A /\ B ) ) ) assume A15: sup D in A /\ B ; ::_thesis: ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in A /\ B ) ) then sup D in A by XBOOLE_0:def_4; then consider x being Element of T such that A16: x in D and A17: for z being Element of T st z in D & z >= x holds z in A by A12, Def3; sup D in B by A15, XBOOLE_0:def_4; then consider y being Element of T such that A18: y in D and A19: for z being Element of T st z in D & z >= y holds z in B by A14, Def3; consider z being Element of T such that A20: z in D and A21: x <= z and A22: y <= z by A16, A18, WAYBEL_0:def_1; take z ; ::_thesis: ( z in D & ( for x being Element of T st x in D & x >= z holds x in A /\ B ) ) thus z in D by A20; ::_thesis: for x being Element of T st x in D & x >= z holds x in A /\ B let u be Element of T; ::_thesis: ( u in D & u >= z implies u in A /\ B ) assume A23: u in D ; ::_thesis: ( not u >= z or u in A /\ B ) assume A24: u >= z ; ::_thesis: u in A /\ B then u >= x by A21, YELLOW_0:def_2; then A25: u in A by A17, A23; u >= y by A22, A24, YELLOW_0:def_2; then u in B by A19, A23; hence u in A /\ B by A25, XBOOLE_0:def_4; ::_thesis: verum end; hence a /\ b in the topology of T by A1, A11, A13; ::_thesis: verum end; begin definition let R be non empty RelStr ; let N be net of R; func lim_inf N -> Element of R equals :: WAYBEL11:def 6 "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R); correctness coherence "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R) is Element of R; ; end; :: deftheorem defines lim_inf WAYBEL11:def_6_:_ for R being non empty RelStr for N being net of R holds lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R); definition let R be non empty reflexive RelStr ; let N be net of R; let p be Element of R; predp is_S-limit_of N means :Def7: :: WAYBEL11:def 7 p <= lim_inf N; end; :: deftheorem Def7 defines is_S-limit_of WAYBEL11:def_7_:_ for R being non empty reflexive RelStr for N being net of R for p being Element of R holds ( p is_S-limit_of N iff p <= lim_inf N ); definition let R be non empty reflexive RelStr ; func Scott-Convergence R -> Convergence-Class of R means :Def8: :: WAYBEL11:def 8 for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in it iff p is_S-limit_of N ); existence ex b1 being Convergence-Class of R st for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in b1 iff p is_S-limit_of N ) proof defpred S1[ set , Element of R] means ex N being strict net of R st ( N = \$1 & \$2 is_S-limit_of N ); consider C being Relation of (NetUniv R), the carrier of R such that A1: for x being Element of NetUniv R for y being Element of R holds ( [x,y] in C iff S1[x,y] ) from RELSET_1:sch_2(); reconsider C = C as Convergence-Class of R by YELLOW_6:def_18; take C ; ::_thesis: for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in C iff p is_S-limit_of N ) let N be strict net of R; ::_thesis: ( N in NetUniv R implies for p being Element of R holds ( [N,p] in C iff p is_S-limit_of N ) ) assume A2: N in NetUniv R ; ::_thesis: for p being Element of R holds ( [N,p] in C iff p is_S-limit_of N ) let p be Element of R; ::_thesis: ( [N,p] in C iff p is_S-limit_of N ) hereby ::_thesis: ( p is_S-limit_of N implies [N,p] in C ) assume [N,p] in C ; ::_thesis: p is_S-limit_of N then ex M being strict net of R st ( M = N & p is_S-limit_of M ) by A1, A2; hence p is_S-limit_of N ; ::_thesis: verum end; thus ( p is_S-limit_of N implies [N,p] in C ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being Convergence-Class of R st ( for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in b1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in b2 iff p is_S-limit_of N ) ) holds b1 = b2 proof let it1, it2 be Convergence-Class of R; ::_thesis: ( ( for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in it1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in it2 iff p is_S-limit_of N ) ) implies it1 = it2 ) assume that A3: for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in it1 iff p is_S-limit_of N ) and A4: for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in it2 iff p is_S-limit_of N ) ; ::_thesis: it1 = it2 let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) ) A5: it1 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18; A6: it2 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18; hereby ::_thesis: ( not [x,y] in it2 or [x,y] in it1 ) assume A7: [x,y] in it1 ; ::_thesis: [x,y] in it2 then A8: x in NetUniv R by A5, ZFMISC_1:87; then consider N being strict net of R such that A9: N = x and the carrier of N in the_universe_of the carrier of R by YELLOW_6:def_11; reconsider p = y as Element of R by A5, A7, ZFMISC_1:87; p is_S-limit_of N by A3, A7, A8, A9; hence [x,y] in it2 by A4, A8, A9; ::_thesis: verum end; assume A10: [x,y] in it2 ; ::_thesis: [x,y] in it1 then A11: x in NetUniv R by A6, ZFMISC_1:87; then consider N being strict net of R such that A12: N = x and the carrier of N in the_universe_of the carrier of R by YELLOW_6:def_11; reconsider p = y as Element of R by A6, A10, ZFMISC_1:87; p is_S-limit_of N by A4, A10, A11, A12; hence [x,y] in it1 by A3, A11, A12; ::_thesis: verum end; end; :: deftheorem Def8 defines Scott-Convergence WAYBEL11:def_8_:_ for R being non empty reflexive RelStr for b2 being Convergence-Class of R holds ( b2 = Scott-Convergence R iff for N being strict net of R st N in NetUniv R holds for p being Element of R holds ( [N,p] in b2 iff p is_S-limit_of N ) ); theorem :: WAYBEL11:17 for R being complete LATTICE for N being net of R for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds p <= q proof let R be complete LATTICE; ::_thesis: for N being net of R for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds p <= q let N be net of R; ::_thesis: for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds p <= q let p, q be Element of R; ::_thesis: ( p is_S-limit_of N & N is_eventually_in downarrow q implies p <= q ) assume that A1: p <= lim_inf N and A2: N is_eventually_in downarrow q ; :: according to WAYBEL11:def_7 ::_thesis: p <= q consider j0 being Element of N such that A3: for i being Element of N st j0 <= i holds N . i in downarrow q by A2, WAYBEL_0:def_11; set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; reconsider q9 = q as Element of R ; q9 is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } proof let x be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } or x <= q9 ) assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: x <= q9 then consider j1 being Element of N such that A4: x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,R) ; set Y = { (N . i) where i is Element of N : i >= j1 } ; reconsider j1 = j1 as Element of N ; consider j2 being Element of N such that A5: j2 >= j0 and A6: j2 >= j1 by YELLOW_6:def_3; N . j2 in { (N . i) where i is Element of N : i >= j1 } by A6; then A7: x <= N . j2 by A4, YELLOW_2:22; N . j2 in downarrow q by A3, A5; then N . j2 <= q9 by WAYBEL_0:17; hence x <= q9 by A7, YELLOW_0:def_2; ::_thesis: verum end; then lim_inf N <= q9 by YELLOW_0:32; hence p <= q by A1, YELLOW_0:def_2; ::_thesis: verum end; theorem Th18: :: WAYBEL11:18 for R being complete LATTICE for N being net of R for p, q being Element of R st N is_eventually_in uparrow q holds lim_inf N >= q proof let R be complete LATTICE; ::_thesis: for N being net of R for p, q being Element of R st N is_eventually_in uparrow q holds lim_inf N >= q let N be net of R; ::_thesis: for p, q being Element of R st N is_eventually_in uparrow q holds lim_inf N >= q let p, q be Element of R; ::_thesis: ( N is_eventually_in uparrow q implies lim_inf N >= q ) assume N is_eventually_in uparrow q ; ::_thesis: lim_inf N >= q then consider j0 being Element of N such that A1: for i being Element of N st j0 <= i holds N . i in uparrow q by WAYBEL_0:def_11; set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; set Y = { (N . i) where i is Element of N : i >= j0 } ; reconsider q9 = q as Element of R ; "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; then A2: lim_inf N >= "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) by YELLOW_2:22; q9 is_<=_than { (N . i) where i is Element of N : i >= j0 } proof let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in { (N . i) where i is Element of N : i >= j0 } or q9 <= y ) assume y in { (N . i) where i is Element of N : i >= j0 } ; ::_thesis: q9 <= y then consider i1 being Element of N such that A3: y = N . i1 and A4: i1 >= j0 ; reconsider i19 = i1 as Element of N ; N . i19 in uparrow q by A1, A4; hence q9 <= y by A3, WAYBEL_0:18; ::_thesis: verum end; then "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) >= q9 by YELLOW_0:33; hence lim_inf N >= q by A2, YELLOW_0:def_2; ::_thesis: verum end; definition let R be non empty reflexive RelStr ; let N be non empty NetStr over R; redefine attr N is monotone means :Def9: :: WAYBEL11:def 9 for i, j being Element of N st i <= j holds N . i <= N . j; compatibility ( N is monotone iff for i, j being Element of N st i <= j holds N . i <= N . j ) proof hereby ::_thesis: ( ( for i, j being Element of N st i <= j holds N . i <= N . j ) implies N is monotone ) assume N is monotone ; ::_thesis: for i, j being Element of N st i <= j holds N . i <= N . j then A1: netmap (N,R) is monotone by WAYBEL_0:def_9; let i, j be Element of N; ::_thesis: ( i <= j implies N . i <= N . j ) assume i <= j ; ::_thesis: N . i <= N . j hence N . i <= N . j by A1, WAYBEL_1:def_2; ::_thesis: verum end; assume A2: for i, j being Element of N st i <= j holds N . i <= N . j ; ::_thesis: N is monotone netmap (N,R) is monotone proof let x, y be Element of N; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (netmap (N,R)) . x <= (netmap (N,R)) . y ) A3: (netmap (N,R)) . x = N . x ; A4: (netmap (N,R)) . y = N . y ; assume x <= y ; ::_thesis: (netmap (N,R)) . x <= (netmap (N,R)) . y hence (netmap (N,R)) . x <= (netmap (N,R)) . y by A2, A3, A4; ::_thesis: verum end; hence N is monotone by WAYBEL_0:def_9; ::_thesis: verum end; end; :: deftheorem Def9 defines monotone WAYBEL11:def_9_:_ for R being non empty reflexive RelStr for N being non empty NetStr over R holds ( N is monotone iff for i, j being Element of N st i <= j holds N . i <= N . j ); definition let R be non empty RelStr ; let S be non empty set ; let f be Function of S, the carrier of R; func Net-Str (S,f) -> non empty strict NetStr over R means :Def10: :: WAYBEL11:def 10 ( the carrier of it = S & the mapping of it = f & ( for i, j being Element of it holds ( i <= j iff it . i <= it . j ) ) ); existence ex b1 being non empty strict NetStr over R st ( the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds ( i <= j iff b1 . i <= b1 . j ) ) ) proof defpred S1[ Element of S, Element of S] means f . \$1 <= f . \$2; consider R being Relation of S,S such that A1: for x, y being Element of S holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); take N = NetStr(# S,R,f #); ::_thesis: ( the carrier of N = S & the mapping of N = f & ( for i, j being Element of N holds ( i <= j iff N . i <= N . j ) ) ) thus the carrier of N = S ; ::_thesis: ( the mapping of N = f & ( for i, j being Element of N holds ( i <= j iff N . i <= N . j ) ) ) thus the mapping of N = f ; ::_thesis: for i, j being Element of N holds ( i <= j iff N . i <= N . j ) let i, j be Element of N; ::_thesis: ( i <= j iff N . i <= N . j ) reconsider x = i, y = j as Element of S ; ( [x,y] in the InternalRel of N iff f . x <= f . y ) by A1; hence ( i <= j iff N . i <= N . j ) by ORDERS_2:def_5; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict NetStr over R st the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds ( i <= j iff b1 . i <= b1 . j ) ) & the carrier of b2 = S & the mapping of b2 = f & ( for i, j being Element of b2 holds ( i <= j iff b2 . i <= b2 . j ) ) holds b1 = b2 proof let it1, it2 be non empty strict NetStr over R; ::_thesis: ( the carrier of it1 = S & the mapping of it1 = f & ( for i, j being Element of it1 holds ( i <= j iff it1 . i <= it1 . j ) ) & the carrier of it2 = S & the mapping of it2 = f & ( for i, j being Element of it2 holds ( i <= j iff it2 . i <= it2 . j ) ) implies it1 = it2 ) assume that A2: the carrier of it1 = S and A3: the mapping of it1 = f and A4: for i, j being Element of it1 holds ( i <= j iff it1 . i <= it1 . j ) and A5: the carrier of it2 = S and A6: the mapping of it2 = f and A7: for i, j being Element of it2 holds ( i <= j iff it2 . i <= it2 . j ) ; ::_thesis: it1 = it2 the InternalRel of it1 = the InternalRel of it2 proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of it1 or [x,y] in the InternalRel of it2 ) & ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) ) hereby ::_thesis: ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) assume A8: [x,y] in the InternalRel of it1 ; ::_thesis: [x,y] in the InternalRel of it2 then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87; reconsider i9 = x, j9 = y as Element of it2 by A2, A5, A8, ZFMISC_1:87; A9: it1 . i = it2 . i9 by A3, A6; A10: it1 . j = it2 . j9 by A3, A6; i <= j by A8, ORDERS_2:def_5; then it2 . i9 <= it2 . j9 by A4, A9, A10; then i9 <= j9 by A7; hence [x,y] in the InternalRel of it2 by ORDERS_2:def_5; ::_thesis: verum end; assume A11: [x,y] in the InternalRel of it2 ; ::_thesis: [x,y] in the InternalRel of it1 then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87; reconsider i9 = x, j9 = y as Element of it1 by A2, A5, A11, ZFMISC_1:87; A12: it2 . i = it1 . i9 by A3, A6; A13: it2 . j = it1 . j9 by A3, A6; i <= j by A11, ORDERS_2:def_5; then it1 . i9 <= it1 . j9 by A7, A12, A13; then i9 <= j9 by A4; hence [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum end; hence it1 = it2 by A2, A3, A5, A6; ::_thesis: verum end; end; :: deftheorem Def10 defines Net-Str WAYBEL11:def_10_:_ for R being non empty RelStr for S being non empty set for f being Function of S, the carrier of R for b4 being non empty strict NetStr over R holds ( b4 = Net-Str (S,f) iff ( the carrier of b4 = S & the mapping of b4 = f & ( for i, j being Element of b4 holds ( i <= j iff b4 . i <= b4 . j ) ) ) ); theorem Th19: :: WAYBEL11:19 for L being non empty 1-sorted for N being non empty NetStr over L holds rng the mapping of N = { (N . i) where i is Element of N : verum } proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L holds rng the mapping of N = { (N . i) where i is Element of N : verum } let N be non empty NetStr over L; ::_thesis: rng the mapping of N = { (N . i) where i is Element of N : verum } set X = { (N . i) where i is Element of N : verum } ; A1: the carrier of N = dom the mapping of N by FUNCT_2:def_1; thus rng the mapping of N c= { (N . i) where i is Element of N : verum } :: according to XBOOLE_0:def_10 ::_thesis: { (N . i) where i is Element of N : verum } c= rng the mapping of N proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of N or e in { (N . i) where i is Element of N : verum } ) assume e in rng the mapping of N ; ::_thesis: e in { (N . i) where i is Element of N : verum } then consider u being set such that A2: u in dom the mapping of N and A3: e = the mapping of N . u by FUNCT_1:def_3; reconsider u = u as Element of N by A2; e = N . u by A3; hence e in { (N . i) where i is Element of N : verum } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (N . i) where i is Element of N : verum } or e in rng the mapping of N ) assume e in { (N . i) where i is Element of N : verum } ; ::_thesis: e in rng the mapping of N then ex i being Element of N st e = N . i ; hence e in rng the mapping of N by A1, FUNCT_1:def_3; ::_thesis: verum end; theorem Th20: :: WAYBEL11:20 for R being non empty RelStr for S being non empty set for f being Function of S, the carrier of R st rng f is directed holds Net-Str (S,f) is directed proof let R be non empty RelStr ; ::_thesis: for S being non empty set for f being Function of S, the carrier of R st rng f is directed holds Net-Str (S,f) is directed let S be non empty set ; ::_thesis: for f being Function of S, the carrier of R st rng f is directed holds Net-Str (S,f) is directed let f be Function of S, the carrier of R; ::_thesis: ( rng f is directed implies Net-Str (S,f) is directed ) assume A1: rng f is directed ; ::_thesis: Net-Str (S,f) is directed set N = Net-Str (S,f); let x, y be Element of (Net-Str (S,f)); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of (Net-Str (S,f)) st ( x <= b1 & y <= b1 ) f = the mapping of (Net-Str (S,f)) by Def10; then A2: rng f = { ((Net-Str (S,f)) . i) where i is Element of (Net-Str (S,f)) : verum } by Th19; then A3: (Net-Str (S,f)) . x in rng f ; (Net-Str (S,f)) . y in rng f by A2; then consider p being Element of R such that A4: p in rng f and A5: (Net-Str (S,f)) . x <= p and A6: (Net-Str (S,f)) . y <= p by A1, A3, WAYBEL_0:def_1; consider z being set such that A7: z in dom f and A8: p = f . z by A4, FUNCT_1:def_3; reconsider z = z as Element of (Net-Str (S,f)) by A7, Def10; take z ; ::_thesis: ( x <= z & y <= z ) p = (Net-Str (S,f)) . z by A8, Def10; hence ( x <= z & y <= z ) by A5, A6, Def10; ::_thesis: verum end; registration let R be non empty RelStr ; let S be non empty set ; let f be Function of S, the carrier of R; cluster Net-Str (S,f) -> non empty strict monotone ; coherence Net-Str (S,f) is monotone proof set N = Net-Str (S,f); netmap ((Net-Str (S,f)),R) is monotone proof let x, y be Element of (Net-Str (S,f)); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y ) A1: (netmap ((Net-Str (S,f)),R)) . x = (Net-Str (S,f)) . x ; A2: (netmap ((Net-Str (S,f)),R)) . y = (Net-Str (S,f)) . y ; assume x <= y ; ::_thesis: (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y hence (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y by A1, A2, Def10; ::_thesis: verum end; hence Net-Str (S,f) is monotone by WAYBEL_0:def_9; ::_thesis: verum end; end; registration let R be non empty transitive RelStr ; let S be non empty set ; let f be Function of S, the carrier of R; cluster Net-Str (S,f) -> non empty transitive strict ; coherence Net-Str (S,f) is transitive proof set N = Net-Str (S,f); let x, y, z be Element of (Net-Str (S,f)); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that A1: x <= y and A2: y <= z ; ::_thesis: x <= z A3: (Net-Str (S,f)) . x <= (Net-Str (S,f)) . y by A1, Def10; (Net-Str (S,f)) . y <= (Net-Str (S,f)) . z by A2, Def10; then (Net-Str (S,f)) . x <= (Net-Str (S,f)) . z by A3, YELLOW_0:def_2; hence x <= z by Def10; ::_thesis: verum end; end; registration let R be non empty reflexive RelStr ; let S be non empty set ; let f be Function of S, the carrier of R; cluster Net-Str (S,f) -> non empty reflexive strict ; coherence Net-Str (S,f) is reflexive proof let x be Element of (Net-Str (S,f)); :: according to YELLOW_0:def_1 ::_thesis: x <= x (Net-Str (S,f)) . x <= (Net-Str (S,f)) . x ; hence x <= x by Def10; ::_thesis: verum end; end; theorem Th21: :: WAYBEL11:21 for R being non empty transitive RelStr for S being non empty set for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds Net-Str (S,f) in NetUniv R proof let R be non empty transitive RelStr ; ::_thesis: for S being non empty set for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds Net-Str (S,f) in NetUniv R let S be non empty set ; ::_thesis: for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds Net-Str (S,f) in NetUniv R let f be Function of S, the carrier of R; ::_thesis: ( S c= the carrier of R & Net-Str (S,f) is directed implies Net-Str (S,f) in NetUniv R ) assume that A1: S c= the carrier of R and A2: Net-Str (S,f) is directed ; ::_thesis: Net-Str (S,f) in NetUniv R reconsider N = Net-Str (S,f) as strict net of R by A2; set UN = the_universe_of the carrier of R; reconsider UN = the_universe_of the carrier of R as universal set ; the_transitive-closure_of the carrier of R in UN by CLASSES1:2; then the carrier of R in UN by CLASSES1:3, CLASSES1:52; then A3: S in UN by A1, CLASSES1:def_1; the carrier of N = S by Def10; hence Net-Str (S,f) in NetUniv R by A3, YELLOW_6:def_11; ::_thesis: verum end; registration let R be LATTICE; cluster non empty reflexive transitive strict directed monotone for NetStr over R; existence ex b1 being net of R st ( b1 is monotone & b1 is reflexive & b1 is strict ) proof reconsider f = id the carrier of R as Function of the carrier of R, the carrier of R ; rng f = [#] R by RELAT_1:45; then reconsider N = Net-Str ( the carrier of R,f) as reflexive strict net of R by Th20; take N ; ::_thesis: ( N is monotone & N is reflexive & N is strict ) thus ( N is monotone & N is reflexive & N is strict ) ; ::_thesis: verum end; end; theorem Th22: :: WAYBEL11:22 for R being complete LATTICE for N being reflexive monotone net of R holds lim_inf N = sup N proof let R be complete LATTICE; ::_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 defpred S1[ set ] 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] } ; deffunc H2( Element of N) -> Element of the carrier of R = N . \$1; A1: for j being Element of N holds H2(j) = H1(j) proof let j be Element of N; ::_thesis: H2(j) = H1(j) set Y = { (N . i) where i is Element of N : i >= j } ; A2: N . j is_<=_than { (N . i) where i is Element of N : i >= j } proof let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in { (N . i) where i is Element of N : i >= j } or N . j <= y ) assume y in { (N . i) where i is Element of N : i >= j } ; ::_thesis: N . j <= y then ex i being Element of N st ( y = N . i & j <= i ) ; hence N . j <= y by Def9; ::_thesis: verum end; for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= j } holds N . j >= b proof let b be Element of R; ::_thesis: ( b is_<=_than { (N . i) where i is Element of N : i >= j } implies N . j >= b ) assume A3: b is_<=_than { (N . i) where i is Element of N : i >= j } ; ::_thesis: N . j >= b reconsider j9 = j as Element of N ; j9 <= j9 ; then N . j9 in { (N . i) where i is Element of N : i >= j } ; hence N . j >= b by A3, LATTICE3:def_8; ::_thesis: verum end; hence H2(j) = H1(j) by A2, YELLOW_0:33; ::_thesis: verum end; rng the mapping of N = { H2(j) where j is Element of N : S1[j] } by Th19 .= { 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 Th23: :: WAYBEL11:23 for R being complete LATTICE for N being constant net of R holds the_value_of N = lim_inf N proof let R be complete LATTICE; ::_thesis: for N being constant net of R holds the_value_of N = lim_inf N let N be constant net of R; ::_thesis: the_value_of N = lim_inf N set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; set j = the Element of N; A1: N . the Element of N is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } proof let b be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } or b <= N . the Element of N ) assume b in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: b <= N . the Element of N then consider j0 being Element of N such that A2: b = "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) ; reconsider j0 = j0 as Element of N ; consider i0 being Element of N such that A3: i0 >= j0 and i0 >= j0 by YELLOW_6:def_3; A4: N . i0 in { (N . i) where i is Element of N : i >= j0 } by A3; N . i0 = the_value_of N by YELLOW_6:16 .= N . the Element of N by YELLOW_6:16 ; hence b <= N . the Element of N by A2, A4, YELLOW_2:22; ::_thesis: verum end; A5: for b being Element of R st b is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } holds N . the Element of N <= b proof let b be Element of R; ::_thesis: ( b is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } implies N . the Element of N <= b ) set Y = { (N . i) where i is Element of N : i >= the Element of N } ; A6: "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,R) in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; assume b is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: N . the Element of N <= b then A7: b >= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,R) by A6, LATTICE3:def_9; A8: N . the Element of N is_<=_than { (N . i) where i is Element of N : i >= the Element of N } proof let c be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not c in { (N . i) where i is Element of N : i >= the Element of N } or N . the Element of N <= c ) assume c in { (N . i) where i is Element of N : i >= the Element of N } ; ::_thesis: N . the Element of N <= c then consider i0 being Element of N such that A9: c = N . i0 and i0 >= the Element of N ; N . the Element of N = the_value_of N by YELLOW_6:16 .= N . i0 by YELLOW_6:16 ; hence N . the Element of N <= c by A9; ::_thesis: verum end; for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= the Element of N } holds N . the Element of N >= b proof let c be Element of R; ::_thesis: ( c is_<=_than { (N . i) where i is Element of N : i >= the Element of N } implies N . the Element of N >= c ) consider i0 being Element of N such that A10: i0 >= the Element of N and i0 >= the Element of N by YELLOW_6:def_3; A11: N . i0 in { (N . i) where i is Element of N : i >= the Element of N } by A10; assume A12: c is_<=_than { (N . i) where i is Element of N : i >= the Element of N } ; ::_thesis: N . the Element of N >= c N . the Element of N = the_value_of N by YELLOW_6:16 .= N . i0 by YELLOW_6:16 ; hence N . the Element of N >= c by A11, A12, LATTICE3:def_8; ::_thesis: verum end; hence N . the Element of N <= b by A7, A8, YELLOW_0:33; ::_thesis: verum end; thus the_value_of N = N . the Element of N by YELLOW_6:16 .= lim_inf N by A1, A5, YELLOW_0:32 ; ::_thesis: verum end; theorem Th24: :: WAYBEL11:24 for R being complete LATTICE for N being constant net of R holds the_value_of N is_S-limit_of N proof let R be complete LATTICE; ::_thesis: for N being constant net of R holds the_value_of N is_S-limit_of N let N be constant net of R; ::_thesis: the_value_of N is_S-limit_of N the_value_of N <= lim_inf N by Th23; hence the_value_of N is_S-limit_of N by Def7; ::_thesis: verum end; definition let S be non empty 1-sorted ; let e be Element of S; func Net-Str e -> strict NetStr over S means :Def11: :: WAYBEL11:def 11 ( the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e} ); existence ex b1 being strict NetStr over S st ( the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} ) proof e in {e} by TARSKI:def_1; then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3; A1: dom (id {e}) = {e} by RELAT_1:45; rng (id {e}) = {e} by RELAT_1:45; then reconsider f = id {e} as Function of {e}, the carrier of S by A1, RELSET_1:4; take NetStr(# {e},r,f #) ; ::_thesis: ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} ) thus ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict NetStr over S st the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} & the carrier of b2 = {e} & the InternalRel of b2 = {[e,e]} & the mapping of b2 = id {e} holds b1 = b2 ; end; :: deftheorem Def11 defines Net-Str WAYBEL11:def_11_:_ for S being non empty 1-sorted for e being Element of S for b3 being strict NetStr over S holds ( b3 = Net-Str e iff ( the carrier of b3 = {e} & the InternalRel of b3 = {[e,e]} & the mapping of b3 = id {e} ) ); registration let S be non empty 1-sorted ; let e be Element of S; cluster Net-Str e -> non empty strict ; coherence not Net-Str e is empty proof set N = Net-Str e; the carrier of (Net-Str e) = {e} by Def11; hence not the carrier of (Net-Str e) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem Th25: :: WAYBEL11:25 for S being non empty 1-sorted for e being Element of S for x being Element of (Net-Str e) holds x = e proof let S be non empty 1-sorted ; ::_thesis: for e being Element of S for x being Element of (Net-Str e) holds x = e let e be Element of S; ::_thesis: for x being Element of (Net-Str e) holds x = e let x be Element of (Net-Str e); ::_thesis: x = e the carrier of (Net-Str e) = {e} by Def11; hence x = e by TARSKI:def_1; ::_thesis: verum end; theorem Th26: :: WAYBEL11:26 for S being non empty 1-sorted for e being Element of S for x being Element of (Net-Str e) holds (Net-Str e) . x = e proof let S be non empty 1-sorted ; ::_thesis: for e being Element of S for x being Element of (Net-Str e) holds (Net-Str e) . x = e let e be Element of S; ::_thesis: for x being Element of (Net-Str e) holds (Net-Str e) . x = e let x be Element of (Net-Str e); ::_thesis: (Net-Str e) . x = e set N = Net-Str e; A1: the carrier of (Net-Str e) = {e} by Def11; then A2: x = e by TARSKI:def_1; thus (Net-Str e) . x = (id {e}) . x by Def11 .= e by A1, A2, FUNCT_1:18 ; ::_thesis: verum end; registration let S be non empty 1-sorted ; let e be Element of S; cluster Net-Str e -> reflexive transitive antisymmetric strict directed ; coherence ( Net-Str e is reflexive & Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric ) proof set N = Net-Str e; the carrier of (Net-Str e) = {e} by Def11; then reconsider e = e as Element of (Net-Str e) by TARSKI:def_1; the InternalRel of (Net-Str e) = {[e,e]} by Def11; then A1: [e,e] in the InternalRel of (Net-Str e) by TARSKI:def_1; thus Net-Str e is reflexive ::_thesis: ( Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric ) proof let x be Element of (Net-Str e); :: according to YELLOW_0:def_1 ::_thesis: x <= x x = e by Th25; hence x <= x by A1, ORDERS_2:def_5; ::_thesis: verum end; thus Net-Str e is transitive ::_thesis: ( Net-Str e is directed & Net-Str e is antisymmetric ) proof let x, y, z be Element of (Net-Str e); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that x <= y and y <= z ; ::_thesis: x <= z A2: x = e by Th25; z = e by Th25; hence x <= z by A1, A2, ORDERS_2:def_5; ::_thesis: verum end; thus Net-Str e is directed ::_thesis: Net-Str e is antisymmetric proof let x, y be Element of (Net-Str e); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of (Net-Str e) st ( x <= b1 & y <= b1 ) take e ; ::_thesis: ( x <= e & y <= e ) A3: x = e by Th25; y = e by Th25; hence ( x <= e & y <= e ) by A1, A3, ORDERS_2:def_5; ::_thesis: verum end; let x, y be Element of (Net-Str e); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) assume that x <= y and y <= x ; ::_thesis: x = y x = e by Th25; hence x = y by Th25; ::_thesis: verum end; end; theorem Th27: :: WAYBEL11:27 for S being non empty 1-sorted for e being Element of S for X being set holds ( Net-Str e is_eventually_in X iff e in X ) proof let S be non empty 1-sorted ; ::_thesis: for e being Element of S for X being set holds ( Net-Str e is_eventually_in X iff e in X ) let e be Element of S; ::_thesis: for X being set holds ( Net-Str e is_eventually_in X iff e in X ) let X be set ; ::_thesis: ( Net-Str e is_eventually_in X iff e in X ) set N = Net-Str e; the carrier of (Net-Str e) = {e} by Def11; then reconsider d = e as Element of (Net-Str e) by TARSKI:def_1; hereby ::_thesis: ( e in X implies Net-Str e is_eventually_in X ) assume Net-Str e is_eventually_in X ; ::_thesis: e in X then consider x being Element of (Net-Str e) such that A1: for y being Element of (Net-Str e) st x <= y holds (Net-Str e) . y in X by WAYBEL_0:def_11; (Net-Str e) . x in X by A1; hence e in X by Th26; ::_thesis: verum end; assume A2: e in X ; ::_thesis: Net-Str e is_eventually_in X take d ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (Net-Str e) holds ( not d <= b1 or (Net-Str e) . b1 in X ) let j be Element of (Net-Str e); ::_thesis: ( not d <= j or (Net-Str e) . j in X ) assume d <= j ; ::_thesis: (Net-Str e) . j in X thus (Net-Str e) . j in X by A2, Th26; ::_thesis: verum end; theorem Th28: :: WAYBEL11:28 for S being non empty reflexive antisymmetric RelStr for e being Element of S holds e = lim_inf (Net-Str e) proof let S be non empty reflexive antisymmetric RelStr ; ::_thesis: for e being Element of S holds e = lim_inf (Net-Str e) let e be Element of S; ::_thesis: e = lim_inf (Net-Str e) set N = Net-Str e; set X = { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ; reconsider e9 = e as Element of S ; A1: { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } c= {e9} proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } or u in {e9} ) assume u in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ; ::_thesis: u in {e9} then consider j being Element of (Net-Str e) such that A2: u = "/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S) ; set Y = { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ; A3: { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } c= {e9} proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } or v in {e9} ) assume v in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ; ::_thesis: v in {e9} then consider i being Element of (Net-Str e) such that A4: v = (Net-Str e) . i and i >= j ; reconsider i9 = i as Element of (Net-Str e) ; (Net-Str e) . i9 = e by Th26; hence v in {e9} by A4, TARSKI:def_1; ::_thesis: verum end; reconsider j9 = j as Element of (Net-Str e) ; j9 <= j9 ; then (Net-Str e) . j in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ; then { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } = {e9} by A3, ZFMISC_1:33; then u = e9 by A2, YELLOW_0:39; hence u in {e9} by TARSKI:def_1; ::_thesis: verum end; set j = the Element of (Net-Str e); "/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= the Element of (Net-Str e) } ,S) in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ; then { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } = {e9} by A1, ZFMISC_1:33; hence e = lim_inf (Net-Str e) by YELLOW_0:39; ::_thesis: verum end; theorem Th29: :: WAYBEL11:29 for S being non empty reflexive RelStr for e being Element of S holds Net-Str e in NetUniv S proof let S be non empty reflexive RelStr ; ::_thesis: for e being Element of S holds Net-Str e in NetUniv S let e be Element of S; ::_thesis: Net-Str e in NetUniv S set N = Net-Str e; set UN = the_universe_of the carrier of S; A1: the carrier of (Net-Str e) = {e} by Def11; reconsider UN = the_universe_of the carrier of S as universal set ; the_transitive-closure_of the carrier of S in UN by CLASSES1:2; then the carrier of S in UN by CLASSES1:3, CLASSES1:52; then the carrier of (Net-Str e) in the_universe_of the carrier of S by A1, CLASSES1:def_1; hence Net-Str e in NetUniv S by YELLOW_6:def_11; ::_thesis: verum end; theorem Th30: :: WAYBEL11:30 for R being complete LATTICE 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 LATTICE; ::_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; set E1 = { (Z . k) where k is Element of Z : k >= jx } ; set Ey = { (Z . k) where k is Element of Z : k >= jy } ; set E = { (Z . k) where k is Element of Z : k >= j } ; take z = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R); ::_thesis: ( z in D & x <= z & y <= z ) thus z in D by A1; ::_thesis: ( x <= z & y <= z ) { (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jx } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (Z . k) where k is Element of Z : k >= j } or e in { (Z . k) where k is Element of Z : k >= jx } ) assume e in { (Z . k) where k is Element of Z : k >= j } ; ::_thesis: e in { (Z . k) where k is Element of Z : k >= jx } then consider k being Element of Z such that A6: e = Z . k and A7: k >= j ; reconsider k = k as Element of Z ; k >= jx by A4, A7, YELLOW_0:def_2; hence e in { (Z . k) where k is Element of Z : k >= jx } by A6; ::_thesis: verum end; hence x <= z by A2, WAYBEL_7:1; ::_thesis: y <= z { (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jy } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (Z . k) where k is Element of Z : k >= j } or e in { (Z . k) where k is Element of Z : k >= jy } ) assume e in { (Z . k) where k is Element of Z : k >= j } ; ::_thesis: e in { (Z . k) where k is Element of Z : k >= jy } then consider k being Element of Z such that A8: e = Z . k and A9: k >= j ; reconsider k = k as Element of Z ; k >= jy by A5, A9, YELLOW_0:def_2; hence e in { (Z . k) where k is Element of Z : k >= jy } by A8; ::_thesis: verum end; hence y <= z by A3, WAYBEL_7:1; ::_thesis: verum end; theorem Th31: :: WAYBEL11:31 for L being complete LATTICE for S being Subset of L holds ( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) ) proof let L be complete LATTICE; ::_thesis: for S being Subset of L holds ( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) ) set SC = Scott-Convergence L; set T = ConvergenceSpace (Scott-Convergence L); A1: the topology of (ConvergenceSpace (Scott-Convergence L)) = { V where V is Subset of L : for p being Element of L st p in V holds for N being net of L st [N,p] in Scott-Convergence L holds N is_eventually_in V } by YELLOW_6:def_24; let S be Subset of L; ::_thesis: ( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) ) hereby ::_thesis: ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence L)) ) assume S in the topology of (ConvergenceSpace (Scott-Convergence L)) ; ::_thesis: ( S is inaccessible & S is upper ) then A2: ex V being Subset of L st ( S = V & ( for p being Element of L st p in V holds for N being net of L st [N,p] in Scott-Convergence L 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 L; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S ) assume A3: sup D in S ; ::_thesis: D meets 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 L by A4, RELSET_1:4; reconsider N = Net-Str (D,f) as reflexive strict monotone net of L by A5, Th20; A6: N in NetUniv L by Th21; lim_inf N = sup N by Th22 .= Sup by WAYBEL_2:def_1 .= "\/" ((rng the mapping of N),L) by YELLOW_2:def_5 .= "\/" ((rng f),L) by Def10 .= sup D by RELAT_1:45 ; then sup D is_S-limit_of N by Def7; then [N,(sup D)] in Scott-Convergence L by A6, Def8; 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 Def10; N . j0 = (id D) . j0 by Def10 .= j0 by A10, FUNCT_1:18 ; hence D meets S by A9, A10, XBOOLE_0:3; ::_thesis: verum end; thus S is upper ::_thesis: verum proof let x, y be Element of L; :: 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 L by Th29; y = lim_inf (Net-Str y) by Th28; then x is_S-limit_of Net-Str y by A12, Def7; then [(Net-Str y),x] in Scott-Convergence L by A13, Def8; then Net-Str y is_eventually_in S by A2, A11; hence y in S by Th27; ::_thesis: verum end; end; assume that A14: S is inaccessible and A15: S is upper ; ::_thesis: S in the topology of (ConvergenceSpace (Scott-Convergence L)) for p being Element of L st p in S holds for N being net of L st [N,p] in Scott-Convergence L holds N is_eventually_in S proof let p be Element of L; ::_thesis: ( p in S implies for N being net of L st [N,p] in Scott-Convergence L holds N is_eventually_in S ) assume A16: p in S ; ::_thesis: for N being net of L st [N,p] in Scott-Convergence L holds N is_eventually_in S reconsider p9 = p as Element of L ; let N be net of L; ::_thesis: ( [N,p] in Scott-Convergence L implies N is_eventually_in S ) assume A17: [N,p] in Scott-Convergence L ; ::_thesis: N is_eventually_in S Scott-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; then A18: N in NetUniv L by A17, ZFMISC_1:87; then ex N9 being strict net of L st ( N9 = N & the carrier of N9 in the_universe_of the carrier of L ) by YELLOW_6:def_11; then p is_S-limit_of N by A17, A18, Def8; then A19: p9 <= lim_inf N by Def7; defpred S1[ set ] means verum; deffunc H1( Element of N) -> Element of the carrier of L = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,L); 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 L from DOMAIN_1:sch_8(); then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of L ; reconsider D = D as non empty directed Subset of L by Th30; sup D in S by A15, A16, A19, WAYBEL_0:def_20; then D meets S by A14, Def1; then D /\ S <> {} by XBOOLE_0:def_7; then consider d being Element of L such that A20: d in D /\ S by SUBSET_1:4; reconsider d = d as Element of L ; 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 } ,L) ; 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 { (N . i) where i is Element of N : i >= j } ; then d <= N . i0 by A21, YELLOW_2:22; hence N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum end; hence S in the topology of (ConvergenceSpace (Scott-Convergence L)) by A1; ::_thesis: verum end; theorem Th32: :: WAYBEL11:32 for T being complete Scott TopLattice holds TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) proof let T be complete Scott TopLattice; ::_thesis: TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) set CSC = ConvergenceSpace (Scott-Convergence T); the topology of T = the topology of (ConvergenceSpace (Scott-Convergence T)) proof thus the topology of T c= the topology of (ConvergenceSpace (Scott-Convergence T)) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (ConvergenceSpace (Scott-Convergence T)) c= the topology of T proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of T or e in the topology of (ConvergenceSpace (Scott-Convergence T)) ) assume A1: e in the topology of T ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence T)) then reconsider A = e as Subset of T ; A is open by A1, PRE_TOPC:def_2; then ( A is inaccessible & A is upper ) by Def4; hence e in the topology of (ConvergenceSpace (Scott-Convergence T)) by Th31; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence T)) or e in the topology of T ) assume A2: e in the topology of (ConvergenceSpace (Scott-Convergence T)) ; ::_thesis: e in the topology of T then reconsider A = e as Subset of T by YELLOW_6:def_24; ( A is inaccessible & A is upper ) by A2, Th31; then A is open by Def4; hence e in the topology of T by PRE_TOPC:def_2; ::_thesis: verum end; hence TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by YELLOW_6:def_24; ::_thesis: verum end; theorem Th33: :: WAYBEL11:33 for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds for S being Subset of T holds ( S is open iff ( S is inaccessible & S is upper ) ) proof let T be complete TopLattice; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies for S being Subset of T holds ( S is open iff ( S is inaccessible & S is upper ) ) ) set SC = Scott-Convergence T; assume TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; ::_thesis: for S being Subset of T holds ( S is open iff ( S is inaccessible & S is upper ) ) then A1: the topology of T = { V where V is Subset of T : for p being Element of T st p in V holds for N being net of T st [N,p] in Scott-Convergence T holds N is_eventually_in V } by YELLOW_6:def_24; let S be Subset of T; ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) ) hereby ::_thesis: ( S is inaccessible & S is upper implies S is open ) assume S is open ; ::_thesis: ( S is inaccessible & S is upper ) then S in the topology of T by PRE_TOPC:def_2; then A2: ex V being Subset of T st ( S = V & ( for p being Element of T st p in V holds for N being net of T st [N,p] in Scott-Convergence T 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 T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S ) assume A3: sup D in S ; ::_thesis: D meets 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 T by A4, RELSET_1:4; reconsider N = Net-Str (D,f) as reflexive strict monotone net of T by A5, Th20; A6: N in NetUniv T by Th21; lim_inf N = sup N by Th22 .= Sup by WAYBEL_2:def_1 .= "\/" ((rng the mapping of N),T) by YELLOW_2:def_5 .= "\/" ((rng f),T) by Def10 .= sup D by RELAT_1:45 ; then sup D is_S-limit_of N by Def7; then [N,(sup D)] in Scott-Convergence T by A6, Def8; 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 Def10; N . j0 = (id D) . j0 by Def10 .= j0 by A10, FUNCT_1:18 ; hence D meets S by A9, A10, XBOOLE_0:3; ::_thesis: verum end; thus S is upper ::_thesis: verum 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 A11: x in S and A12: x <= y ; ::_thesis: y in S A13: Net-Str y in NetUniv T by Th29; y = lim_inf (Net-Str y) by Th28; then x is_S-limit_of Net-Str y by A12, Def7; then [(Net-Str y),x] in Scott-Convergence T by A13, Def8; then Net-Str y is_eventually_in S by A2, A11; hence y in S by Th27; ::_thesis: verum end; end; assume that A14: S is inaccessible and A15: S is upper ; ::_thesis: S is open for p being Element of T st p in S holds for N being net of T st [N,p] in Scott-Convergence T holds N is_eventually_in S proof let p be Element of T; ::_thesis: ( p in S implies for N being net of T st [N,p] in Scott-Convergence T holds N is_eventually_in S ) assume A16: p in S ; ::_thesis: for N being net of T st [N,p] in Scott-Convergence T holds N is_eventually_in S reconsider p9 = p as Element of T ; let N be net of T; ::_thesis: ( [N,p] in Scott-Convergence T implies N is_eventually_in S ) assume A17: [N,p] in Scott-Convergence T ; ::_thesis: N is_eventually_in S Scott-Convergence T c= [:(NetUniv T), the carrier of T:] by YELLOW_6:def_18; then A18: N in NetUniv T by A17, ZFMISC_1:87; then ex N9 being strict net of T st ( N9 = N & the carrier of N9 in the_universe_of the carrier of T ) by YELLOW_6:def_11; then p is_S-limit_of N by A17, A18, Def8; then A19: p9 <= lim_inf N by Def7; defpred S1[ set ] means verum; deffunc H1( Element of N) -> Element of the carrier of T = "/\" ( { (N . i) where i is Element of N : i >= \$1 } ,T); 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 T from DOMAIN_1:sch_8(); then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of T ; reconsider D = D as non empty directed Subset of T by Th30; sup D in S by A15, A16, A19, WAYBEL_0:def_20; then D meets S by A14, Def1; then D /\ S <> {} by XBOOLE_0:def_7; then consider d being Element of T such that A20: d in D /\ S by SUBSET_1:4; reconsider d = d as Element of T ; 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 } ,T) ; 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 { (N . i) where i is Element of N : i >= j } ; then d <= N . i0 by A21, YELLOW_2:22; hence N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum end; then S in the topology of T by A1; hence S is open by PRE_TOPC:def_2; ::_thesis: verum end; theorem Th34: :: WAYBEL11:34 for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds T is Scott proof let T be complete TopLattice; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies T is Scott ) assume TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; ::_thesis: T is Scott hence for S being Subset of T holds ( S is open iff ( S is inaccessible & S is upper ) ) by Th33; :: according to WAYBEL11:def_4 ::_thesis: verum end; registration let R be complete LATTICE; cluster Scott-Convergence R -> (CONSTANTS) ; coherence Scott-Convergence R is (CONSTANTS) proof let N be constant net of R; :: according to YELLOW_6:def_20 ::_thesis: ( not N in NetUniv R or [N,(the_value_of N)] in Scott-Convergence R ) assume A1: N in NetUniv R ; ::_thesis: [N,(the_value_of N)] in Scott-Convergence R then consider M being strict net of R such that A2: M = N and the carrier of M in the_universe_of the carrier of R by YELLOW_6:def_11; the_value_of M is_S-limit_of M by A2, Th24; hence [N,(the_value_of N)] in Scott-Convergence R by A1, A2, Def8; ::_thesis: verum end; end; registration let R be complete LATTICE; cluster Scott-Convergence R -> (SUBNETS) ; coherence Scott-Convergence R is (SUBNETS) proof set S = Scott-Convergence R; let N be net of R; :: according to YELLOW_6:def_21 ::_thesis: for b1 being subnet of N holds ( not b1 in NetUniv R or for b2 being Element of the carrier of R holds ( not [N,b2] in Scott-Convergence R or [b1,b2] in Scott-Convergence R ) ) let Y be subnet of N; ::_thesis: ( not Y in NetUniv R or for b1 being Element of the carrier of R holds ( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R ) ) A1: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18; assume A2: Y in NetUniv R ; ::_thesis: for b1 being Element of the carrier of R holds ( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R ) then consider Y9 being strict net of R such that A3: Y9 = Y and the carrier of Y9 in the_universe_of the carrier of R by YELLOW_6:def_11; let p be Element of R; ::_thesis: ( not [N,p] in Scott-Convergence R or [Y,p] in Scott-Convergence R ) assume A4: [N,p] in Scott-Convergence R ; ::_thesis: [Y,p] in Scott-Convergence R then A5: N in NetUniv R by A1, ZFMISC_1:87; then consider N9 being strict net of R such that A6: N9 = N and the carrier of N9 in the_universe_of the carrier of R by YELLOW_6:def_11; deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= R } ,R); defpred S1[ set ] means verum; reconsider X1 = { H1(j) where j is Element of N : S1[j] } as Subset of R from DOMAIN_1:sch_8(); deffunc H2( Element of Y) -> Element of the carrier of R = "/\" ( { (Y . i) where i is Element of Y : i >= R } ,R); reconsider X2 = { H2(j) where j is Element of Y : S1[j] } as Subset of R from DOMAIN_1:sch_8(); p is_S-limit_of N9 by A4, A5, A6, Def8; then A7: p <= lim_inf N by A6, Def7; consider f being Function of Y,N such that A8: the mapping of Y = the mapping of N * f and A9: for m being Element of N ex n being Element of Y st for p being Element of Y st n <= p holds m <= f . p by YELLOW_6:def_9; X1 is_finer_than X2 proof let a be Element of R; :: according to YELLOW_4:def_1 ::_thesis: ( not a in X1 or ex b1 being Element of the carrier of R st ( b1 in X2 & a <= b1 ) ) assume a in X1 ; ::_thesis: ex b1 being Element of the carrier of R st ( b1 in X2 & a <= b1 ) then consider j being Element of N such that A10: a = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ; reconsider j = j as Element of N ; consider n being Element of Y such that A11: for p being Element of Y st n <= p holds j <= f . p by A9; set X3 = { (Y . i) where i is Element of Y : i >= n } ; set X4 = { (N . i) where i is Element of N : i >= j } ; take b = "/\" ( { (Y . i) where i is Element of Y : i >= n } ,R); ::_thesis: ( b in X2 & a <= b ) thus b in X2 ; ::_thesis: a <= b { (Y . i) where i is Element of Y : i >= n } c= { (N . i) where i is Element of N : i >= j } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (Y . i) where i is Element of Y : i >= n } or u in { (N . i) where i is Element of N : i >= j } ) assume u in { (Y . i) where i is Element of Y : i >= n } ; ::_thesis: u in { (N . i) where i is Element of N : i >= j } then consider m being Element of Y such that A12: u = Y . m and A13: m >= n ; reconsider m = m as Element of Y ; A14: f . m >= j by A11, A13; u = N . (f . m) by A8, A12, FUNCT_2:15; hence u in { (N . i) where i is Element of N : i >= j } by A14; ::_thesis: verum end; hence a <= b by A10, WAYBEL_7:1; ::_thesis: verum end; then "\/" (X1,R) <= "\/" (X2,R) by Th2; then p <= lim_inf Y by A7, YELLOW_0:def_2; then p is_S-limit_of Y9 by A3, Def7; hence [Y,p] in Scott-Convergence R by A2, A3, Def8; ::_thesis: verum end; end; theorem Th35: :: WAYBEL11:35 for S being non empty 1-sorted for N being net of S for X being set for M being subnet of N st M = N " X holds for i being Element of M holds M . i in X proof let S be non empty 1-sorted ; ::_thesis: for N being net of S for X being set for M being subnet of N st M = N " X holds for i being Element of M holds M . i in X let N be net of S; ::_thesis: for X being set for M being subnet of N st M = N " X holds for i being Element of M holds M . i in X let X be set ; ::_thesis: for M being subnet of N st M = N " X holds for i being Element of M holds M . i in X let M be subnet of N; ::_thesis: ( M = N " X implies for i being Element of M holds M . i in X ) assume A1: M = N " X ; ::_thesis: for i being Element of M holds M . i in X let j be Element of M; ::_thesis: M . j in X j in the carrier of M ; then j in the mapping of N " X by A1, YELLOW_6:def_10; then A2: the mapping of N . j in X by FUNCT_1:def_7; the mapping of M = the mapping of N | the carrier of M by A1, YELLOW_6:def_6; hence M . j in X by A2, FUNCT_1:49; ::_thesis: verum end; definition let L be non empty reflexive RelStr ; func sigma L -> Subset-Family of L equals :: WAYBEL11:def 12 the topology of (ConvergenceSpace (Scott-Convergence L)); coherence the topology of (ConvergenceSpace (Scott-Convergence L)) is Subset-Family of L by YELLOW_6:def_24; end; :: deftheorem defines sigma WAYBEL11:def_12_:_ for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)); theorem Th36: :: WAYBEL11:36 for L being complete continuous Scott TopLattice for x being Element of L holds wayabove x is open proof let L be complete continuous Scott TopLattice; ::_thesis: for x being Element of L holds wayabove x is open let x be Element of L; ::_thesis: wayabove x is open set W = wayabove x; wayabove x is inaccessible proof let D be non empty directed Subset of L; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in wayabove x implies D meets wayabove x ) assume sup D in wayabove x ; ::_thesis: D meets wayabove x then x << sup D by WAYBEL_3:8; then consider d being Element of L such that A1: d in D and A2: x << d by WAYBEL_4:53; d in wayabove x by A2; hence D meets wayabove x by A1, XBOOLE_0:3; ::_thesis: verum end; hence wayabove x is open by Def4; ::_thesis: verum end; theorem Th37: :: WAYBEL11:37 for T being complete TopLattice st the topology of T = sigma T holds T is Scott proof let T be complete TopLattice; ::_thesis: ( the topology of T = sigma T implies T is Scott ) set CSC = ConvergenceSpace (Scott-Convergence T); assume the topology of T = sigma T ; ::_thesis: T is Scott then TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (ConvergenceSpace (Scott-Convergence T)), the topology of (ConvergenceSpace (Scott-Convergence T)) #) by YELLOW_6:def_24; hence T is Scott by Th34; ::_thesis: verum end; Lm3: for T1, T2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like holds T2 is TopSpace-like proof let T1, T2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like implies T2 is TopSpace-like ) assume that A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) and A2: T1 is TopSpace-like ; ::_thesis: T2 is TopSpace-like thus the carrier of T2 in the topology of T2 by A1, A2, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T2) holds ( not b1 c= the topology of T2 or union b1 in the topology of T2 ) ) & ( for b1, b2 being Element of bool the carrier of T2 holds ( not b1 in the topology of T2 or not b2 in the topology of T2 or b1 /\ b2 in the topology of T2 ) ) ) thus ( ( for b1 being Element of bool (bool the carrier of T2) holds ( not b1 c= the topology of T2 or union b1 in the topology of T2 ) ) & ( for b1, b2 being Element of bool the carrier of T2 holds ( not b1 in the topology of T2 or not b2 in the topology of T2 or b1 /\ b2 in the topology of T2 ) ) ) by A1, A2, PRE_TOPC:def_1; ::_thesis: verum end; Lm4: for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds for N being strict net of S1 holds N is strict net of S2 ; Lm5: for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds NetUniv S1 = NetUniv S2 proof let S1, S2 be non empty 1-sorted ; ::_thesis: ( the carrier of S1 = the carrier of S2 implies NetUniv S1 = NetUniv S2 ) assume A1: the carrier of S1 = the carrier of S2 ; ::_thesis: NetUniv S1 = NetUniv S2 defpred S1[ set ] means ex N being strict net of S2 st ( N = \$1 & the carrier of N in the_universe_of the carrier of S2 ); A2: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_NetUniv_S1_implies_S1[x]_)_&_(_S1[x]_implies_x_in_NetUniv_S1_)_) let x be set ; ::_thesis: ( ( x in NetUniv S1 implies S1[x] ) & ( S1[x] implies x in NetUniv S1 ) ) hereby ::_thesis: ( S1[x] implies x in NetUniv S1 ) assume x in NetUniv S1 ; ::_thesis: S1[x] then consider N being strict net of S1 such that A3: N = x and A4: the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def_11; reconsider N = N as strict net of S2 by A1; thus S1[x] ::_thesis: verum proof take N ; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S2 ) thus ( N = x & the carrier of N in the_universe_of the carrier of S2 ) by A1, A3, A4; ::_thesis: verum end; end; assume S1[x] ; ::_thesis: x in NetUniv S1 then consider N being strict net of S2 such that A5: N = x and A6: the carrier of N in the_universe_of the carrier of S2 ; reconsider N = N as strict net of S1 by A1; now__::_thesis:_ex_N_being_strict_net_of_S1_st_ (_N_=_x_&_the_carrier_of_N_in_the_universe_of_the_carrier_of_S1_) take N = N; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S1 ) thus ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by A1, A5, A6; ::_thesis: verum end; hence x in NetUniv S1 by YELLOW_6:def_11; ::_thesis: verum end; A7: for x being set holds ( x in NetUniv S2 iff S1[x] ) by YELLOW_6:def_11; thus NetUniv S1 = NetUniv S2 from XBOOLE_0:sch_2(A2, A7); ::_thesis: verum end; Lm6: for T1, T2 being non empty 1-sorted for X being set for N1 being net of T1 for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds N2 is_eventually_in X proof let T1, T2 be non empty 1-sorted ; ::_thesis: for X being set for N1 being net of T1 for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds N2 is_eventually_in X let X be set ; ::_thesis: for N1 being net of T1 for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds N2 is_eventually_in X let N1 be net of T1; ::_thesis: for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds N2 is_eventually_in X let N2 be net of T2; ::_thesis: ( N1 = N2 & N1 is_eventually_in X implies N2 is_eventually_in X ) assume A1: N1 = N2 ; ::_thesis: ( not N1 is_eventually_in X or N2 is_eventually_in X ) assume N1 is_eventually_in X ; ::_thesis: N2 is_eventually_in X then consider i being Element of N1 such that A2: for j being Element of N1 st i <= j holds N1 . j in X by WAYBEL_0:def_11; reconsider ii = i as Element of N2 by A1; take ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds ( not ii <= b1 or N2 . b1 in X ) let jj be Element of N2; ::_thesis: ( not ii <= jj or N2 . jj in X ) reconsider j = jj as Element of N1 by A1; assume A3: ii <= jj ; ::_thesis: N2 . jj in X N2 . jj = N1 . j by A1; hence N2 . jj in X by A1, A2, A3; ::_thesis: verum end; Lm7: for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds for N1 being net of T1 for N2 being net of T2 st N1 = N2 holds for p1 being Point of T1 for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 proof let T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies for N1 being net of T1 for N2 being net of T2 st N1 = N2 holds for p1 being Point of T1 for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 ) assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: for N1 being net of T1 for N2 being net of T2 st N1 = N2 holds for p1 being Point of T1 for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 let N1 be net of T1; ::_thesis: for N2 being net of T2 st N1 = N2 holds for p1 being Point of T1 for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 let N2 be net of T2; ::_thesis: ( N1 = N2 implies for p1 being Point of T1 for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 ) assume A2: N1 = N2 ; ::_thesis: for p1 being Point of T1 for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 let p1 be Point of T1; ::_thesis: for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds p2 in Lim N2 let p2 be Point of T2; ::_thesis: ( p1 = p2 & p1 in Lim N1 implies p2 in Lim N2 ) assume that A3: p1 = p2 and A4: p1 in Lim N1 ; ::_thesis: p2 in Lim N2 for V being a_neighborhood of p2 holds N2 is_eventually_in V proof let V be a_neighborhood of p2; ::_thesis: N2 is_eventually_in V reconsider W = V as Subset of T1 by A1; p2 in Int V by CONNSP_2:def_1; then consider G being Subset of T2 such that A5: G is open and A6: G c= V and A7: p2 in G by TOPS_1:22; reconsider H = G as Subset of T1 by A1; G in the topology of T2 by A5, PRE_TOPC:def_2; then H is open by A1, PRE_TOPC:def_2; then p1 in Int W by A3, A6, A7, TOPS_1:22; then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def_1; thus N2 is_eventually_in V ::_thesis: verum proof N1 is_eventually_in W by A4, YELLOW_6:def_15; then consider i being Element of N1 such that A8: for j being Element of N1 st i <= j holds N1 . j in W by WAYBEL_0:def_11; reconsider ii = i as Element of N2 by A2; take ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds ( not ii <= b1 or N2 . b1 in V ) let jj be Element of N2; ::_thesis: ( not ii <= jj or N2 . jj in V ) reconsider j = jj as Element of N1 by A2; assume A9: ii <= jj ; ::_thesis: N2 . jj in V N2 . jj = N1 . j by A2; hence N2 . jj in V by A2, A8, A9; ::_thesis: verum end; end; hence p2 in Lim N2 by YELLOW_6:def_15; ::_thesis: verum end; Lm8: for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds Convergence T1 = Convergence T2 proof let T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies Convergence T1 = Convergence T2 ) assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: Convergence T1 = Convergence T2 A2: Convergence T1 c= [:(NetUniv T1), the carrier of T1:] by YELLOW_6:def_18; A3: Convergence T2 c= [:(NetUniv T2), the carrier of T2:] by YELLOW_6:def_18; let u1, u2 be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [u1,u2] in Convergence T1 or [u1,u2] in Convergence T2 ) & ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 ) ) hereby ::_thesis: ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 ) assume A4: [u1,u2] in Convergence T1 ; ::_thesis: [u1,u2] in Convergence T2 then consider N1 being Element of NetUniv T1, p1 being Point of T1 such that A5: [u1,u2] = [N1,p1] by A2, DOMAIN_1:1; A6: N1 in NetUniv T1 ; ex N being strict net of T1 st ( N = N1 & the carrier of N in the_universe_of the carrier of T1 ) by YELLOW_6:def_11; then reconsider N1 = N1 as net of T1 ; A7: p1 in Lim N1 by A4, A5, YELLOW_6:def_19; reconsider N2 = N1 as net of T2 by A1; reconsider p2 = p1 as Point of T2 by A1; A8: N2 in NetUniv T2 by A1, A6, Lm5; p2 in Lim N2 by A1, A7, Lm7; hence [u1,u2] in Convergence T2 by A5, A8, YELLOW_6:def_19; ::_thesis: verum end; assume A9: [u1,u2] in Convergence T2 ; ::_thesis: [u1,u2] in Convergence T1 then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that A10: [u1,u2] = [N1,p1] by A3, DOMAIN_1:1; A11: N1 in NetUniv T2 ; ex N being strict net of T2 st ( N = N1 & the carrier of N in the_universe_of the carrier of T2 ) by YELLOW_6:def_11; then reconsider N1 = N1 as net of T2 ; A12: p1 in Lim N1 by A9, A10, YELLOW_6:def_19; reconsider N2 = N1 as net of T1 by A1; reconsider p2 = p1 as Point of T1 by A1; A13: N2 in NetUniv T1 by A1, A11, Lm5; p2 in Lim N2 by A1, A12, Lm7; hence [u1,u2] in Convergence T1 by A10, A13, YELLOW_6:def_19; ::_thesis: verum end; Lm9: for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE holds R2 is LATTICE proof let R1, R2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE implies R2 is LATTICE ) assume that A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and A2: R1 is LATTICE ; ::_thesis: R2 is LATTICE A3: R2 is with_infima proof let x, y be Element of R2; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of R2 st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of R2 holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) reconsider x9 = x, y9 = y as Element of R1 by A1; consider z9 being Element of R1 such that A4: z9 <= x9 and A5: z9 <= y9 and A6: for w9 being Element of R1 st w9 <= x9 & w9 <= y9 holds w9 <= z9 by A2, LATTICE3:def_11; reconsider z = z9 as Element of R2 by A1; take z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of R2 holds ( not b1 <= x or not b1 <= y or b1 <= z ) ) ) thus ( z <= x & z <= y ) by A1, A4, A5, Lm1; ::_thesis: for b1 being Element of the carrier of R2 holds ( not b1 <= x or not b1 <= y or b1 <= z ) let w be Element of R2; ::_thesis: ( not w <= x or not w <= y or w <= z ) reconsider w9 = w as Element of R1 by A1; assume that A7: w <= x and A8: w <= y ; ::_thesis: w <= z A9: w9 <= x9 by A1, A7, Lm1; w9 <= y9 by A1, A8, Lm1; then w9 <= z9 by A6, A9; hence w <= z by A1, Lm1; ::_thesis: verum end; A10: R2 is with_suprema proof let x, y be Element of R2; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of R2 st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of R2 holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) reconsider x9 = x, y9 = y as Element of R1 by A1; consider z9 being Element of R1 such that A11: z9 >= x9 and A12: z9 >= y9 and A13: for w9 being Element of R1 st w9 >= x9 & w9 >= y9 holds w9 >= z9 by A2, LATTICE3:def_10; reconsider z = z9 as Element of R2 by A1; take z ; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of R2 holds ( not x <= b1 or not y <= b1 or z <= b1 ) ) ) thus ( z >= x & z >= y ) by A1, A11, A12, Lm1; ::_thesis: for b1 being Element of the carrier of R2 holds ( not x <= b1 or not y <= b1 or z <= b1 ) let w be Element of R2; ::_thesis: ( not x <= w or not y <= w or z <= w ) reconsider w9 = w as Element of R1 by A1; assume that A14: w >= x and A15: w >= y ; ::_thesis: z <= w A16: w9 >= x9 by A1, A14, Lm1; w9 >= y9 by A1, A15, Lm1; then w9 >= z9 by A13, A16; hence z <= w by A1, Lm1; ::_thesis: verum end; A17: R2 is reflexive proof let x be Element of R2; :: according to YELLOW_0:def_1 ::_thesis: x <= x reconsider x9 = x as Element of R1 by A1; x9 <= x9 by A2, YELLOW_0:def_1; hence x <= x by A1, Lm1; ::_thesis: verum end; A18: R2 is transitive proof let x, y, z be Element of R2; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1; assume that A19: x <= y and A20: y <= z ; ::_thesis: x <= z A21: x9 <= y9 by A1, A19, Lm1; y9 <= z9 by A1, A20, Lm1; then x9 <= z9 by A2, A21, YELLOW_0:def_2; hence x <= z by A1, Lm1; ::_thesis: verum end; R2 is antisymmetric proof let x, y be Element of R2; :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y ) reconsider x9 = x, y9 = y as Element of R1 by A1; assume that A22: x <= y and A23: y <= x ; ::_thesis: x = y A24: x9 <= y9 by A1, A22, Lm1; y9 <= x9 by A1, A23, Lm1; hence x = y by A2, A24, YELLOW_0:def_3; ::_thesis: verum end; hence R2 is LATTICE by A3, A10, A17, A18; ::_thesis: verum end; Lm10: for R1, R2 being LATTICE for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 proof let R1, R2 be LATTICE; ::_thesis: for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 let X be set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 let p1 be Element of R1; ::_thesis: for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 let p2 be Element of R2; ::_thesis: ( p1 = p2 & X is_<=_than p1 implies X is_<=_than p2 ) assume that A2: p1 = p2 and A3: X is_<=_than p1 ; ::_thesis: X is_<=_than p2 let b2 be Element of R2; :: according to LATTICE3:def_9 ::_thesis: ( not b2 in X or b2 <= p2 ) reconsider b1 = b2 as Element of R1 by A1; assume b2 in X ; ::_thesis: b2 <= p2 then p1 >= b1 by A3, LATTICE3:def_9; hence b2 <= p2 by A1, A2, Lm1; ::_thesis: verum end; Lm11: for R1, R2 being LATTICE for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 proof let R1, R2 be LATTICE; ::_thesis: for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 let X be set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p1 being Element of R1 for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 let p1 be Element of R1; ::_thesis: for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 let p2 be Element of R2; ::_thesis: ( p1 = p2 & X is_>=_than p1 implies X is_>=_than p2 ) assume that A2: p1 = p2 and A3: X is_>=_than p1 ; ::_thesis: X is_>=_than p2 let b2 be Element of R2; :: according to LATTICE3:def_8 ::_thesis: ( not b2 in X or p2 <= b2 ) reconsider b1 = b2 as Element of R1 by A1; assume b2 in X ; ::_thesis: p2 <= b2 then p1 <= b1 by A3, LATTICE3:def_8; hence p2 <= b2 by A1, A2, Lm1; ::_thesis: verum end; Lm12: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for D being set holds "\/" (D,R1) = "\/" (D,R2) proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "\/" (D,R1) = "\/" (D,R2) ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being set holds "\/" (D,R1) = "\/" (D,R2) let D be set ; ::_thesis: "\/" (D,R1) = "\/" (D,R2) reconsider b = "\/" (D,R1) as Element of R2 by A1; A2: ex_sup_of D,R2 by YELLOW_0:17; A3: ex_sup_of D,R1 by YELLOW_0:17; then D is_<=_than "\/" (D,R1) by YELLOW_0:def_9; then A4: D is_<=_than b by A1, Lm10; for a being Element of R2 st D is_<=_than a holds a >= b proof let a be Element of R2; ::_thesis: ( D is_<=_than a implies a >= b ) reconsider a9 = a as Element of R1 by A1; assume D is_<=_than a ; ::_thesis: a >= b then D is_<=_than a9 by A1, Lm10; then a9 >= "\/" (D,R1) by A3, YELLOW_0:def_9; hence a >= b by A1, Lm1; ::_thesis: verum end; hence "\/" (D,R1) = "\/" (D,R2) by A2, A4, YELLOW_0:def_9; ::_thesis: verum end; Lm13: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for D being set holds "/\" (D,R1) = "/\" (D,R2) proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "/\" (D,R1) = "/\" (D,R2) ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being set holds "/\" (D,R1) = "/\" (D,R2) let D be set ; ::_thesis: "/\" (D,R1) = "/\" (D,R2) reconsider b = "/\" (D,R1) as Element of R2 by A1; A2: ex_inf_of D,R2 by YELLOW_0:17; A3: ex_inf_of D,R1 by YELLOW_0:17; then D is_>=_than "/\" (D,R1) by YELLOW_0:def_10; then A4: D is_>=_than b by A1, Lm11; for a being Element of R2 st D is_>=_than a holds a <= b proof let a be Element of R2; ::_thesis: ( D is_>=_than a implies a <= b ) reconsider a9 = a as Element of R1 by A1; assume D is_>=_than a ; ::_thesis: a <= b then D is_>=_than a9 by A1, Lm11; then a9 <= "/\" (D,R1) by A3, YELLOW_0:def_10; hence a <= b by A1, Lm1; ::_thesis: verum end; hence "/\" (D,R1) = "/\" (D,R2) by A2, A4, YELLOW_0:def_10; ::_thesis: verum end; Lm14: for R1, R2 being non empty reflexive RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for D being Subset of R1 for D9 being Subset of R2 st D = D9 & D is directed holds D9 is directed proof let R1, R2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being Subset of R1 for D9 being Subset of R2 st D = D9 & D is directed holds D9 is directed ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being Subset of R1 for D9 being Subset of R2 st D = D9 & D is directed holds D9 is directed let D be Subset of R1; ::_thesis: for D9 being Subset of R2 st D = D9 & D is directed holds D9 is directed let D9 be Subset of R2; ::_thesis: ( D = D9 & D is directed implies D9 is directed ) assume that A2: D = D9 and A3: D is directed ; ::_thesis: D9 is directed let x2, y2 be Element of R2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x2 in D9 or not y2 in D9 or ex b1 being Element of the carrier of R2 st ( b1 in D9 & x2 <= b1 & y2 <= b1 ) ) assume that A4: x2 in D9 and A5: y2 in D9 ; ::_thesis: ex b1 being Element of the carrier of R2 st ( b1 in D9 & x2 <= b1 & y2 <= b1 ) reconsider x1 = x2, y1 = y2 as Element of R1 by A1; consider z1 being Element of R1 such that A6: z1 in D and A7: x1 <= z1 and A8: y1 <= z1 by A2, A3, A4, A5, WAYBEL_0:def_1; reconsider z2 = z1 as Element of R2 by A1; take z2 ; ::_thesis: ( z2 in D9 & x2 <= z2 & y2 <= z2 ) thus z2 in D9 by A2, A6; ::_thesis: ( x2 <= z2 & y2 <= z2 ) thus ( x2 <= z2 & y2 <= z2 ) by A1, A7, A8, Lm1; ::_thesis: verum end; Lm15: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for p, q being Element of R1 st p << q holds for p9, q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9 proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p, q being Element of R1 st p << q holds for p9, q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p, q being Element of R1 st p << q holds for p9, q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9 let p, q be Element of R1; ::_thesis: ( p << q implies for p9, q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9 ) assume A2: p << q ; ::_thesis: for p9, q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9 let p9, q9 be Element of R2; ::_thesis: ( p = p9 & q = q9 implies p9 << q9 ) assume that A3: p = p9 and A4: q = q9 ; ::_thesis: p9 << q9 let D9 be non empty directed Subset of R2; :: according to WAYBEL_3:def_1 ::_thesis: ( not q9 <= "\/" (D9,R2) or ex b1 being Element of the carrier of R2 st ( b1 in D9 & p9 <= b1 ) ) assume A5: q9 <= sup D9 ; ::_thesis: ex b1 being Element of the carrier of R2 st ( b1 in D9 & p9 <= b1 ) reconsider D = D9 as non empty Subset of R1 by A1; reconsider D = D as non empty directed Subset of R1 by A1, Lm14; sup D = sup D9 by A1, Lm12; then q <= sup D by A1, A4, A5, Lm1; then consider d being Element of R1 such that A6: d in D and A7: p <= d by A2, WAYBEL_3:def_1; reconsider d9 = d as Element of R2 by A1; take d9 ; ::_thesis: ( d9 in D9 & p9 <= d9 ) thus d9 in D9 by A6; ::_thesis: p9 <= d9 thus p9 <= d9 by A1, A3, A7, Lm1; ::_thesis: verum end; Lm16: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds lim_inf N1 = lim_inf N2 proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds lim_inf N1 = lim_inf N2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds lim_inf N1 = lim_inf N2 let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds lim_inf N1 = lim_inf N2 let N2 be net of R2; ::_thesis: ( N1 = N2 implies lim_inf N1 = lim_inf N2 ) assume A2: N1 = N2 ; ::_thesis: lim_inf N1 = lim_inf N2 set X1 = { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; set X2 = { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } = { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } proof thus { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } c= { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } :: according to XBOOLE_0:def_10 ::_thesis: { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } c= { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } or e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ) assume e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; ::_thesis: e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } then consider j1 being Element of N1 such that A3: e = "/\" ( { (N1 . i) where i is Element of N1 : i >= j1 } ,R1) ; reconsider j2 = j1 as Element of N2 by A2; set Y1 = { (N1 . i) where i is Element of N1 : i >= j1 } ; set Y2 = { (N2 . i) where i is Element of N2 : i >= j2 } ; { (N1 . i) where i is Element of N1 : i >= j1 } = { (N2 . i) where i is Element of N2 : i >= j2 } proof thus { (N1 . i) where i is Element of N1 : i >= j1 } c= { (N2 . i) where i is Element of N2 : i >= j2 } :: according to XBOOLE_0:def_10 ::_thesis: { (N2 . i) where i is Element of N2 : i >= j2 } c= { (N1 . i) where i is Element of N1 : i >= j1 } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N1 . i) where i is Element of N1 : i >= j1 } or u in { (N2 . i) where i is Element of N2 : i >= j2 } ) assume u in { (N1 . i) where i is Element of N1 : i >= j1 } ; ::_thesis: u in { (N2 . i) where i is Element of N2 : i >= j2 } then consider i1 being Element of N1 such that A4: u = N1 . i1 and A5: j1 <= i1 ; reconsider i2 = i1 as Element of N2 by A2; N2 . i2 = u by A2, A4; hence u in { (N2 . i) where i is Element of N2 : i >= j2 } by A2, A5; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N2 . i) where i is Element of N2 : i >= j2 } or u in { (N1 . i) where i is Element of N1 : i >= j1 } ) assume u in { (N2 . i) where i is Element of N2 : i >= j2 } ; ::_thesis: u in { (N1 . i) where i is Element of N1 : i >= j1 } then consider i2 being Element of N2 such that A6: u = N2 . i2 and A7: j2 <= i2 ; reconsider i1 = i2 as Element of N1 by A2; N1 . i1 = u by A2, A6; hence u in { (N1 . i) where i is Element of N1 : i >= j1 } by A2, A7; ::_thesis: verum end; then e = "/\" ( { (N2 . i) where i is Element of N2 : i >= j2 } ,R2) by A1, A3, Lm13; hence e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } or e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ) assume e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; ::_thesis: e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } then consider j1 being Element of N2 such that A8: e = "/\" ( { (N2 . i) where i is Element of N2 : i >= j1 } ,R2) ; reconsider j2 = j1 as Element of N1 by A2; set Y1 = { (N2 . i) where i is Element of N2 : i >= j1 } ; set Y2 = { (N1 . i) where i is Element of N1 : i >= j2 } ; { (N2 . i) where i is Element of N2 : i >= j1 } = { (N1 . i) where i is Element of N1 : i >= j2 } proof thus { (N2 . i) where i is Element of N2 : i >= j1 } c= { (N1 . i) where i is Element of N1 : i >= j2 } :: according to XBOOLE_0:def_10 ::_thesis: { (N1 . i) where i is Element of N1 : i >= j2 } c= { (N2 . i) where i is Element of N2 : i >= j1 } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N2 . i) where i is Element of N2 : i >= j1 } or u in { (N1 . i) where i is Element of N1 : i >= j2 } ) assume u in { (N2 . i) where i is Element of N2 : i >= j1 } ; ::_thesis: u in { (N1 . i) where i is Element of N1 : i >= j2 } then consider i1 being Element of N2 such that A9: u = N2 . i1 and A10: j1 <= i1 ; reconsider i2 = i1 as Element of N1 by A2; N1 . i2 = u by A2, A9; hence u in { (N1 . i) where i is Element of N1 : i >= j2 } by A2, A10; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N1 . i) where i is Element of N1 : i >= j2 } or u in { (N2 . i) where i is Element of N2 : i >= j1 } ) assume u in { (N1 . i) where i is Element of N1 : i >= j2 } ; ::_thesis: u in { (N2 . i) where i is Element of N2 : i >= j1 } then consider i2 being Element of N1 such that A11: u = N1 . i2 and A12: j2 <= i2 ; reconsider i1 = i2 as Element of N2 by A2; N2 . i1 = u by A2, A11; hence u in { (N2 . i) where i is Element of N2 : i >= j1 } by A2, A12; ::_thesis: verum end; then e = "/\" ( { (N1 . i) where i is Element of N1 : i >= j2 } ,R1) by A1, A8, Lm13; hence e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; ::_thesis: verum end; hence lim_inf N1 = lim_inf N2 by A1, Lm12; ::_thesis: verum end; Lm17: for R1, R2 being non empty reflexive RelStr for X being non empty set for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 proof let R1, R2 be non empty reflexive RelStr ; ::_thesis: for X being non empty set for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 let X be non empty set ; ::_thesis: for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 let N2 be net of R2; ::_thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1 for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 ) assume A1: N1 = N2 ; ::_thesis: for J1 being net_set of the carrier of N1,R1 for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 let J1 be net_set of the carrier of N1,R1; ::_thesis: for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds Iterated J1 = Iterated J2 let J2 be net_set of the carrier of N2,R2; ::_thesis: ( J1 = J2 implies Iterated J1 = Iterated J2 ) assume A2: J1 = J2 ; ::_thesis: Iterated J1 = Iterated J2 A3: RelStr(# the carrier of (Iterated J1), the InternalRel of (Iterated J1) #) = [:N1,(product J1):] by YELLOW_6:def_13; A4: RelStr(# the carrier of (Iterated J2), the InternalRel of (Iterated J2) #) = [:N2,(product J2):] by YELLOW_6:def_13; set f = the mapping of (Iterated J1); set g = the mapping of (Iterated J2); A5: dom the mapping of (Iterated J1) = the carrier of (Iterated J2) by A1, A2, A3, A4, FUNCT_2:def_1 .= dom the mapping of (Iterated J2) by FUNCT_2:def_1 ; for x being set st x in dom the mapping of (Iterated J1) holds the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x proof let x be set ; ::_thesis: ( x in dom the mapping of (Iterated J1) implies the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x ) assume x in dom the mapping of (Iterated J1) ; ::_thesis: the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x then x in the carrier of (Iterated J1) ; then x in [: the carrier of N1, the carrier of (product J1):] by A3, YELLOW_3:def_2; then consider x1 being Element of N1, x2 being Element of (product J1) such that A6: x = [x1,x2] by DOMAIN_1:1; reconsider y1 = x1 as Element of N2 by A1; reconsider y2 = x2 as Element of (product J2) by A1, A2; thus the mapping of (Iterated J1) . x = the mapping of (Iterated J1) . (x1,x2) by A6 .= the mapping of (J1 . x1) . (x2 . x1) by YELLOW_6:def_13 .= the mapping of (J2 . y1) . (y2 . y1) by A2 .= the mapping of (Iterated J2) . (y1,y2) by YELLOW_6:def_13 .= the mapping of (Iterated J2) . x by A6 ; ::_thesis: verum end; then the mapping of (Iterated J1) = the mapping of (Iterated J2) by A5, FUNCT_1:2; hence Iterated J1 = Iterated J2 by A1, A2, A3, A4; ::_thesis: verum end; Lm18: for R1, R2 being non empty reflexive RelStr for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 proof let R1, R2 be non empty reflexive RelStr ; ::_thesis: for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 let X be non empty set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for N1 being net of R1 for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 let N2 be net of R2; ::_thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 ) assume A2: N1 = N2 ; ::_thesis: for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 let J1 be net_set of the carrier of N1,R1; ::_thesis: J1 is net_set of the carrier of N2,R2 reconsider J2 = J1 as ManySortedSet of the carrier of N2 by A2; for i being set st i in rng J2 holds i is net of R2 proof let i be set ; ::_thesis: ( i in rng J2 implies i is net of R2 ) assume i in rng J2 ; ::_thesis: i is net of R2 then reconsider N = i as net of R1 by YELLOW_6:def_12; N is NetStr over R2 by A1; hence i is net of R2 ; ::_thesis: verum end; hence J1 is net_set of the carrier of N2,R2 by YELLOW_6:def_12; ::_thesis: verum end; Lm19: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds Scott-Convergence R1 c= Scott-Convergence R2 proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 c= Scott-Convergence R2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: Scott-Convergence R1 c= Scott-Convergence R2 A2: Scott-Convergence R1 c= [:(NetUniv R1), the carrier of R1:] by YELLOW_6:def_18; for e being set st e in Scott-Convergence R1 holds e in Scott-Convergence R2 proof let e be set ; ::_thesis: ( e in Scott-Convergence R1 implies e in Scott-Convergence R2 ) assume A3: e in Scott-Convergence R1 ; ::_thesis: e in Scott-Convergence R2 then consider N1 being Element of NetUniv R1, p1 being Element of R1 such that A4: e = [N1,p1] by A2, DOMAIN_1:1; A5: N1 in NetUniv R1 ; A6: ex N being strict net of R1 st ( N1 = N & the carrier of N in the_universe_of the carrier of R1 ) by YELLOW_6:def_11; then reconsider N2 = N1 as strict net of R2 by A1, Lm4; reconsider N1 = N1 as strict net of R1 by A6; reconsider p2 = p1 as Element of R2 by A1; A7: N2 in NetUniv R2 by A1, A5, Lm5; A8: lim_inf N1 = lim_inf N2 by A1, Lm16; p1 is_S-limit_of N1 by A3, A4, Def8; then p1 <= lim_inf N1 by Def7; then p2 <= lim_inf N2 by A1, A8, Lm1; then p2 is_S-limit_of N2 by Def7; hence e in Scott-Convergence R2 by A4, A7, Def8; ::_thesis: verum end; hence Scott-Convergence R1 c= Scott-Convergence R2 by TARSKI:def_3; ::_thesis: verum end; Lm20: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds Scott-Convergence R1 = Scott-Convergence R2 proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 = Scott-Convergence R2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: Scott-Convergence R1 = Scott-Convergence R2 then A2: Scott-Convergence R1 c= Scott-Convergence R2 by Lm19; Scott-Convergence R2 c= Scott-Convergence R1 by A1, Lm19; hence Scott-Convergence R1 = Scott-Convergence R2 by A2, XBOOLE_0:def_10; ::_thesis: verum end; Lm21: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds sigma R1 = sigma R2 proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies sigma R1 = sigma R2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: sigma R1 = sigma R2 set T1 = ConvergenceSpace (Scott-Convergence R1); set T2 = ConvergenceSpace (Scott-Convergence R2); A2: the topology of (ConvergenceSpace (Scott-Convergence R1)) = { V where V is Subset of R1 : for p being Element of R1 st p in V holds for N being net of R1 st [N,p] in Scott-Convergence R1 holds N is_eventually_in V } by YELLOW_6:def_24; A3: the topology of (ConvergenceSpace (Scott-Convergence R2)) = { V where V is Subset of R2 : for p being Element of R2 st p in V holds for N being net of R2 st [N,p] in Scott-Convergence R2 holds N is_eventually_in V } by YELLOW_6:def_24; the topology of (ConvergenceSpace (Scott-Convergence R1)) = the topology of (ConvergenceSpace (Scott-Convergence R2)) proof thus the topology of (ConvergenceSpace (Scott-Convergence R1)) c= the topology of (ConvergenceSpace (Scott-Convergence R2)) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (ConvergenceSpace (Scott-Convergence R2)) c= the topology of (ConvergenceSpace (Scott-Convergence R1)) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R1)) or e in the topology of (ConvergenceSpace (Scott-Convergence R2)) ) assume e in the topology of (ConvergenceSpace (Scott-Convergence R1)) ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R2)) then consider V1 being Subset of R1 such that A4: e = V1 and A5: for p being Element of R1 st p in V1 holds for N being net of R1 st [N,p] in Scott-Convergence R1 holds N is_eventually_in V1 by A2; reconsider V2 = V1 as Subset of R2 by A1; for p being Element of R2 st p in V2 holds for N being net of R2 st [N,p] in Scott-Convergence R2 holds N is_eventually_in V2 proof let p2 be Element of R2; ::_thesis: ( p2 in V2 implies for N being net of R2 st [N,p2] in Scott-Convergence R2 holds N is_eventually_in V2 ) assume A6: p2 in V2 ; ::_thesis: for N being net of R2 st [N,p2] in Scott-Convergence R2 holds N is_eventually_in V2 reconsider p1 = p2 as Element of R1 by A1; let N2 be net of R2; ::_thesis: ( [N2,p2] in Scott-Convergence R2 implies N2 is_eventually_in V2 ) reconsider N1 = N2 as net of R1 by A1; assume [N2,p2] in Scott-Convergence R2 ; ::_thesis: N2 is_eventually_in V2 then [N1,p1] in Scott-Convergence R1 by A1, Lm20; hence N2 is_eventually_in V2 by A5, A6, Lm6; ::_thesis: verum end; hence e in the topology of (ConvergenceSpace (Scott-Convergence R2)) by A3, A4; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R2)) or e in the topology of (ConvergenceSpace (Scott-Convergence R1)) ) assume e in the topology of (ConvergenceSpace (Scott-Convergence R2)) ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R1)) then consider V1 being Subset of R2 such that A7: e = V1 and A8: for p being Element of R2 st p in V1 holds for N being net of R2 st [N,p] in Scott-Convergence R2 holds N is_eventually_in V1 by A3; reconsider V2 = V1 as Subset of R1 by A1; for p being Element of R1 st p in V2 holds for N being net of R1 st [N,p] in Scott-Convergence R1 holds N is_eventually_in V2 proof let p2 be Element of R1; ::_thesis: ( p2 in V2 implies for N being net of R1 st [N,p2] in Scott-Convergence R1 holds N is_eventually_in V2 ) assume A9: p2 in V2 ; ::_thesis: for N being net of R1 st [N,p2] in Scott-Convergence R1 holds N is_eventually_in V2 reconsider p1 = p2 as Element of R2 by A1; let N2 be net of R1; ::_thesis: ( [N2,p2] in Scott-Convergence R1 implies N2 is_eventually_in V2 ) reconsider N1 = N2 as net of R2 by A1; assume [N2,p2] in Scott-Convergence R1 ; ::_thesis: N2 is_eventually_in V2 then [N1,p1] in Scott-Convergence R2 by A1, Lm20; hence N2 is_eventually_in V2 by A8, A9, Lm6; ::_thesis: verum end; hence e in the topology of (ConvergenceSpace (Scott-Convergence R1)) by A2, A7; ::_thesis: verum end; hence sigma R1 = sigma R2 ; ::_thesis: verum end; Lm22: for R1, R2 being LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete holds R2 is complete proof let R1, R2 be LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete implies R2 is complete ) assume that A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and A2: R1 is complete ; ::_thesis: R2 is complete let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of R2 st ( X is_<=_than b1 & ( for b2 being Element of the carrier of R2 holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) consider a1 being Element of R1 such that A3: X is_<=_than a1 and A4: for b being Element of R1 st X is_<=_than b holds a1 <= b by A2, LATTICE3:def_12; reconsider a2 = a1 as Element of R2 by A1; take a2 ; ::_thesis: ( X is_<=_than a2 & ( for b1 being Element of the carrier of R2 holds ( not X is_<=_than b1 or a2 <= b1 ) ) ) thus X is_<=_than a2 by A1, A3, Lm10; ::_thesis: for b1 being Element of the carrier of R2 holds ( not X is_<=_than b1 or a2 <= b1 ) let b2 be Element of R2; ::_thesis: ( not X is_<=_than b2 or a2 <= b2 ) reconsider b1 = b2 as Element of R1 by A1; assume X is_<=_than b2 ; ::_thesis: a2 <= b2 then X is_<=_than b1 by A1, Lm10; hence a2 <= b2 by A1, A4, Lm1; ::_thesis: verum end; Lm23: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous holds R2 is continuous proof let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous implies R2 is continuous ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: ( not R1 is continuous or R2 is continuous ) assume A2: R1 is continuous ; ::_thesis: R2 is continuous thus A3: for x being Element of R2 holds ( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( R2 is up-complete & R2 is satisfying_axiom_of_approximation ) thus R2 is up-complete ; ::_thesis: R2 is satisfying_axiom_of_approximation A4: for x being Element of R1 holds ( not waybelow x is empty & waybelow x is directed ) ; for x, y being Element of R2 st not x <= y holds ex u being Element of R2 st ( u << x & not u <= y ) proof let x2, y2 be Element of R2; ::_thesis: ( not x2 <= y2 implies ex u being Element of R2 st ( u << x2 & not u <= y2 ) ) reconsider x1 = x2, y1 = y2 as Element of R1 by A1; assume not x2 <= y2 ; ::_thesis: ex u being Element of R2 st ( u << x2 & not u <= y2 ) then not x1 <= y1 by A1, Lm1; then consider u1 being Element of R1 such that A5: u1 << x1 and A6: not u1 <= y1 by A2, A4, WAYBEL_3:24; reconsider u2 = u1 as Element of R2 by A1; take u2 ; ::_thesis: ( u2 << x2 & not u2 <= y2 ) thus u2 << x2 by A1, A5, Lm15; ::_thesis: not u2 <= y2 thus not u2 <= y2 by A1, A6, Lm1; ::_thesis: verum end; hence R2 is satisfying_axiom_of_approximation by A3, WAYBEL_3:24; ::_thesis: verum end; registration let R be complete continuous LATTICE; cluster Scott-Convergence R -> topological ; coherence Scott-Convergence R is topological proof set C = Scott-Convergence R; thus ( Scott-Convergence R is (CONSTANTS) & Scott-Convergence R is (SUBNETS) ) ; :: according to YELLOW_6:def_25 ::_thesis: ( Scott-Convergence R is (DIVERGENCE) & Scott-Convergence R is (ITERATED_LIMITS) ) thus Scott-Convergence R is (DIVERGENCE) ::_thesis: Scott-Convergence R is (ITERATED_LIMITS) proof let X be net of R; :: according to YELLOW_6:def_22 ::_thesis: for b1 being Element of the carrier of R holds ( not X in NetUniv R or [X,b1] in Scott-Convergence R or ex b2 being subnet of X st ( b2 in NetUniv R & ( for b3 being subnet of b2 holds not [b3,b1] in Scott-Convergence R ) ) ) let p be Element of R; ::_thesis: ( not X in NetUniv R or [X,p] in Scott-Convergence R or ex b1 being subnet of X st ( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) ) ) assume that A1: X in NetUniv R and A2: not [X,p] in Scott-Convergence R ; ::_thesis: ex b1 being subnet of X st ( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) ) A3: for x being Element of R holds ( not waybelow x is empty & waybelow x is directed ) ; reconsider p9 = p as Element of R ; consider N being strict net of R such that A4: N = X and the carrier of N in the_universe_of the carrier of R by A1, YELLOW_6:def_11; not p is_S-limit_of N by A1, A2, A4, Def8; then not p <= lim_inf X by A4, Def7; then consider u being Element of R such that A5: u << p9 and A6: not u <= lim_inf X by A3, WAYBEL_3:24; set A = { a where a is Element of R : not a >= u } ; X is_often_in { a where a is Element of R : not a >= u } proof let i be Element of X; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of X st ( i <= b1 & X . b1 in { a where a is Element of R : not a >= u } ) set B = { (X . j) where j is Element of X : j >= i } ; set C = { ("/\" ( { (X . k) where k is Element of X : k >= j } ,R)) where j is Element of X : verum } ; "/\" ( { (X . j) where j is Element of X : j >= i } ,R) in { ("/\" ( { (X . k) where k is Element of X : k >= j } ,R)) where j is Element of X : verum } ; then "/\" ( { (X . j) where j is Element of X : j >= i } ,R) <= lim_inf X by YELLOW_2:22; then not u <= "/\" ( { (X . j) where j is Element of X : j >= i } ,R) by A6, YELLOW_0:def_2; then not u is_<=_than { (X . j) where j is Element of X : j >= i } by YELLOW_0:33; then consider b being Element of R such that A7: b in { (X . j) where j is Element of X : j >= i } and A8: not u <= b by LATTICE3:def_8; consider j being Element of X such that A9: b = X . j and A10: j >= i by A7; take j ; ::_thesis: ( i <= j & X . j in { a where a is Element of R : not a >= u } ) thus i <= j by A10; ::_thesis: X . j in { a where a is Element of R : not a >= u } thus X . j in { a where a is Element of R : not a >= u } by A8, A9; ::_thesis: verum end; then reconsider Y = X " { a where a is Element of R : not a >= u } as subnet of X by YELLOW_6:22; take Y ; ::_thesis: ( Y in NetUniv R & ( for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R ) ) reconsider UN = the_universe_of the carrier of R as universal set ; A11: ex N being strict net of R st ( X = N & the carrier of N in UN ) by A1, YELLOW_6:def_11; X " { a where a is Element of R : not a >= u } is SubRelStr of X by YELLOW_6:def_6; then the carrier of (X " { a where a is Element of R : not a >= u } ) c= the carrier of X by YELLOW_0:def_13; then the carrier of Y in UN by A11, CLASSES1:def_1; hence Y in NetUniv R by YELLOW_6:def_11; ::_thesis: for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R let Z be subnet of Y; ::_thesis: not [Z,p] in Scott-Convergence R assume A12: [Z,p] in Scott-Convergence R ; ::_thesis: contradiction Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18; then A13: Z in NetUniv R by A12, ZFMISC_1:87; then consider ZZ being strict net of R such that A14: ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def_11; deffunc H1( Element of Z) -> Element of the carrier of R = "/\" ( { (Z . i) where i is Element of Z : i >= R } ,R); defpred S1[ set ] means verum; set D = { H1(j) where j is Element of Z : S1[j] } ; { H1(j) where j is Element of Z : S1[j] } is Subset of R from DOMAIN_1:sch_8(); then reconsider D = { H1(j) where j is Element of Z : S1[j] } as Subset of R ; reconsider D = D as non empty directed Subset of R by Th30; p is_S-limit_of ZZ by A12, A13, A14, Def8; then p <= lim_inf Z by A14, Def7; then consider d being Element of R such that A15: d in D and A16: u <= d by A5, WAYBEL_3:def_1; consider j being Element of Z such that A17: d = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R) by A15; reconsider j9 = j as Element of Z ; consider i being Element of Z such that A18: i >= j9 and i >= j9 by YELLOW_6:def_3; consider f being Function of Z,Y such that A19: the mapping of Z = the mapping of Y * f and for m being Element of Y ex n being Element of Z st for p being Element of Z st n <= p holds m <= f . p by YELLOW_6:def_9; Z . i in { (Z . k) where k is Element of Z : k >= j } by A18; then A20: d <= Z . i by A17, YELLOW_2:22; Y . (f . i) = Z . i by A19, FUNCT_2:15; then Z . i in { a where a is Element of R : not a >= u } by Th35; then ex a being Element of R st ( a = Z . i & not a >= u ) ; hence contradiction by A16, A20, YELLOW_0:def_2; ::_thesis: verum end; thus Scott-Convergence R is (ITERATED_LIMITS) ::_thesis: verum proof let X be net of R; :: according to YELLOW_6:def_23 ::_thesis: for b1 being Element of the carrier of R holds ( not [X,b1] in Scott-Convergence R or for b2 being net_set of the carrier of X,R holds ( ex b3 being Element of the carrier of X st not [(b2 . b3),(X . b3)] in Scott-Convergence R or [(Iterated b2),b1] in Scott-Convergence R ) ) let p be Element of R; ::_thesis: ( not [X,p] in Scott-Convergence R or for b1 being net_set of the carrier of X,R holds ( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R ) ) assume A21: [X,p] in Scott-Convergence R ; ::_thesis: for b1 being net_set of the carrier of X,R holds ( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R ) let J be net_set of the carrier of X,R; ::_thesis: ( ex b1 being Element of the carrier of X st not [(J . b1),(X . b1)] in Scott-Convergence R or [(Iterated J),p] in Scott-Convergence R ) assume A22: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence R ; ::_thesis: [(Iterated J),p] in Scott-Convergence R A23: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18; then A24: X in NetUniv R by A21, ZFMISC_1:87; for i being Element of X holds J . i in NetUniv R proof let i be Element of X; ::_thesis: J . i in NetUniv R [(J . i),(X . i)] in Scott-Convergence R by A22; hence J . i in NetUniv R by A23, ZFMISC_1:87; ::_thesis: verum end; then A25: Iterated J in NetUniv R by A24, YELLOW_6:25; reconsider p9 = p as Element of R ; set q = lim_inf (Iterated J); lim_inf (Iterated J) is_>=_than waybelow p9 proof let u be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not u in waybelow p9 or u <= lim_inf (Iterated J) ) assume u in waybelow p9 ; ::_thesis: u <= lim_inf (Iterated J) then A26: u << p9 by WAYBEL_3:7; set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #); A27: 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 #) ; A28: the carrier of R = the carrier of (ConvergenceSpace (Scott-Convergence R)) by YELLOW_6:def_24; then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopLattice by A27, Lm3, Lm9; reconsider T = T as complete TopLattice by A27, Lm22; reconsider T = T as complete continuous TopLattice by A27, Lm23; the topology of T = sigma T by A27, Lm21; then reconsider T = T as complete continuous Scott TopLattice by Th37; reconsider XX = X as net of T ; reconsider JJ = J as net_set of the carrier of XX,T by A27, Lm18; reconsider uu = u, qq = lim_inf (Iterated J), pp = p9 as Element of T ; set N = Iterated JJ; set CC = Convergence T; Convergence T = Convergence (ConvergenceSpace (Scott-Convergence R)) by A28, Lm8; then A29: Scott-Convergence R c= Convergence T by YELLOW_6:40; A30: uu << pp by A26, A27, Lm15; A31: qq = lim_inf (Iterated JJ) by A27, Lm16, Lm17; for i being Element of XX holds [(JJ . i),(XX . i)] in Convergence T proof let i be Element of XX; ::_thesis: [(JJ . i),(XX . i)] in Convergence T reconsider ii = i as Element of X ; [(J . ii),(X . ii)] in Scott-Convergence R by A22; hence [(JJ . i),(XX . i)] in Convergence T by A29; ::_thesis: verum end; then [(Iterated JJ),pp] in Convergence T by A21, A29, YELLOW_6:def_23; then A32: pp in Lim (Iterated JJ) by YELLOW_6:def_19; pp in wayabove uu by A30; then wayabove uu is a_neighborhood of pp by Th36, CONNSP_2:3; then A33: Iterated JJ is_eventually_in wayabove uu by A32, YELLOW_6:def_15; wayabove uu c= uparrow uu by WAYBEL_3:11; then Iterated JJ is_eventually_in uparrow uu by A33, WAYBEL_0:8; hence u <= lim_inf (Iterated J) by A27, A31, Lm1, Th18; ::_thesis: verum end; then sup (waybelow p9) <= lim_inf (Iterated J) by YELLOW_0:32; then p <= lim_inf (Iterated J) by WAYBEL_3:def_5; then p is_S-limit_of Iterated J by Def7; hence [(Iterated J),p] in Scott-Convergence R by A25, Def8; ::_thesis: verum end; end; end; theorem :: WAYBEL11:38 for T being complete continuous Scott TopLattice for x being Element of T for N being net of T st N in NetUniv T holds ( x is_S-limit_of N iff x in Lim N ) proof let T be complete continuous Scott TopLattice; ::_thesis: for x being Element of T for N being net of T st N in NetUniv T holds ( x is_S-limit_of N iff x in Lim N ) let x be Element of T; ::_thesis: for N being net of T st N in NetUniv T holds ( x is_S-limit_of N iff x in Lim N ) let N be net of T; ::_thesis: ( N in NetUniv T implies ( x is_S-limit_of N iff x in Lim N ) ) assume A1: N in NetUniv T ; ::_thesis: ( x is_S-limit_of N iff x in Lim N ) A2: Convergence (ConvergenceSpace (Scott-Convergence T)) = Scott-Convergence T by YELLOW_6:44; consider M being strict net of T such that A3: M = N and the carrier of M in the_universe_of the carrier of T by A1, YELLOW_6:def_11; TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32; then A4: Convergence T = Convergence (ConvergenceSpace (Scott-Convergence T)) by Lm8; thus ( x is_S-limit_of N implies x in Lim N ) ::_thesis: ( x in Lim N implies x is_S-limit_of N ) proof assume x is_S-limit_of N ; ::_thesis: x in Lim N then [N,x] in Convergence T by A1, A2, A3, A4, Def8; hence x in Lim N by YELLOW_6:def_19; ::_thesis: verum end; assume x in Lim N ; ::_thesis: x is_S-limit_of N then [M,x] in Scott-Convergence T by A1, A2, A3, A4, YELLOW_6:def_19; hence x is_S-limit_of N by A1, A3, Def8; ::_thesis: verum end; theorem Th39: :: WAYBEL11:39 for L being non empty complete Poset st Scott-Convergence L is (ITERATED_LIMITS) holds L is continuous proof let L be non empty complete Poset; ::_thesis: ( Scott-Convergence L is (ITERATED_LIMITS) implies L is continuous ) assume A1: Scott-Convergence L is (ITERATED_LIMITS) ; ::_thesis: L is continuous set C = Scott-Convergence L; now__::_thesis:_for_I_being_non_empty_set_st_I_in_the_universe_of_the_carrier_of_L_holds_ for_K_being_V8()_ManySortedSet_of_I_st_(_for_j_being_Element_of_I_holds_K_._j_in_the_universe_of_the_carrier_of_L_)_holds_ for_F_being_DoubleIndexedSet_of_K,L_st_(_for_j_being_Element_of_I_holds_rng_(F_._j)_is_directed_)_holds_ Inf_=_Sup let I be non empty set ; ::_thesis: ( I in the_universe_of the carrier of L implies for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds Inf = Sup ) assume A2: I in the_universe_of the carrier of L ; ::_thesis: for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds Inf = Sup let K be V8() ManySortedSet of I; ::_thesis: ( ( for j being Element of I holds K . j in the_universe_of the carrier of L ) implies for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds Inf = Sup ) assume A3: for j being Element of I holds K . j in the_universe_of the carrier of L ; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds Inf = Sup let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of I holds rng (F . j) is directed ) implies Inf = Sup ) assume A4: for j being Element of I holds rng (F . j) is directed ; ::_thesis: Inf = Sup set x = Inf ; A5: Inf >= Sup by WAYBEL_5:16; [:I,I:] c= [:I,I:] ; then reconsider r = [:I,I:] as Relation of I ; dom F = I by PARTFUN1:def_2; then reconsider f = Sups as Function of I, the carrier of L ; set X = NetStr(# I,r,f #); A6: for i, j being Element of NetStr(# I,r,f #) holds i <= j proof let i, j be Element of NetStr(# I,r,f #); ::_thesis: i <= j [i,j] in the InternalRel of NetStr(# I,r,f #) by ZFMISC_1:87; hence i <= j by ORDERS_2:def_5; ::_thesis: verum end; A7: NetStr(# I,r,f #) is transitive proof let x, y, z be Element of NetStr(# I,r,f #); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume that x <= y and y <= z ; ::_thesis: x <= z thus x <= z by A6; ::_thesis: verum end; NetStr(# I,r,f #) is directed proof let x, y be Element of NetStr(# I,r,f #); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of NetStr(# I,r,f #) st ( x <= b1 & y <= b1 ) take x ; ::_thesis: ( x <= x & y <= x ) thus ( x <= x & y <= x ) by A6; ::_thesis: verum end; then reconsider X = NetStr(# I,r,f #) as strict net of L by A7; deffunc H1( Element of I) -> non empty strict NetStr over L = Net-Str ((K . \$1),(F . \$1)); consider J being ManySortedSet of I such that A8: for i being Element of I holds J . i = H1(i) from PBOOLE:sch_5(); for i being set st i in the carrier of X holds J . i is net of L proof let i be set ; ::_thesis: ( i in the carrier of X implies J . i is net of L ) assume i in the carrier of X ; ::_thesis: J . i is net of L then reconsider i9 = i as Element of I ; reconsider rFi = rng (F . i9) as Subset of L ; A9: rFi is directed by A4; J . i9 = Net-Str ((K . i9),(F . i9)) by A8; hence J . i is net of L by A9, Th20; ::_thesis: verum end; then reconsider J = J as net_set of the carrier of X,L by YELLOW_6:24; A10: for j being set st j in I holds ex R being 1-sorted st ( R = J . j & K . j = the carrier of R ) proof let i be set ; ::_thesis: ( i in I implies ex R being 1-sorted st ( R = J . i & K . i = the carrier of R ) ) assume i in I ; ::_thesis: ex R being 1-sorted st ( R = J . i & K . i = the carrier of R ) then reconsider i9 = i as Element of I ; take R = Net-Str ((K . i9),(F . i9)); ::_thesis: ( R = J . i & K . i = the carrier of R ) thus R = J . i by A8; ::_thesis: K . i = the carrier of R thus K . i = the carrier of R by Def10; ::_thesis: verum end; A11: doms F = K by YELLOW_7:45 .= Carrier J by A10, PRALG_1:def_13 ; A12: dom (Frege F) = product (doms F) by PARTFUN1:def_2; then A13: dom (Infs ) = product (doms F) by FUNCT_2:def_1; A14: for i being Element of X holds J . i in NetUniv L proof let i be Element of X; ::_thesis: J . i in NetUniv L reconsider i9 = i as Element of I ; A15: J . i = Net-Str ((K . i9),(F . i9)) by A8; then reconsider Ji = J . i as strict net of L ; K . i9 in the_universe_of the carrier of L by A3; then the carrier of Ji in the_universe_of the carrier of L by A15, Def10; hence J . i in NetUniv L by YELLOW_6:def_11; ::_thesis: verum end; A16: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence L proof let i be Element of X; ::_thesis: [(J . i),(X . i)] in Scott-Convergence L reconsider i9 = i as Element of I ; A17: J . i = Net-Str ((K . i9),(F . i9)) by A8; then reconsider Ji = J . i as reflexive monotone net of L ; A18: J . i in NetUniv L by A14; i in I ; then i9 in dom F by PARTFUN1:def_2; then X . i = Sup by WAYBEL_5:def_1 .= Sup by A17, Def10 .= sup Ji by WAYBEL_2:def_1 .= lim_inf Ji by Th22 ; then X . i is_S-limit_of J . i by Def7; hence [(J . i),(X . i)] in Scott-Convergence L by A17, A18, Def8; ::_thesis: verum end; A19: X in NetUniv L by A2, YELLOW_6:def_11; then A20: Iterated J in NetUniv L by A14, YELLOW_6:25; deffunc H2( Element of (Iterated J)) -> set = { ((Iterated J) . p) where p is Element of (Iterated J) : p >= \$1 } ; the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by YELLOW_6:26; then reconsider G = the mapping of (Iterated J) as Function of [: the carrier of X,(product (doms F)):], the carrier of L by A11; deffunc H3( Element of X, Element of product (doms F)) -> set = { (G . (i,\$2)) where i is Element of X : i >= \$1 } ; defpred S1[ set ] means verum; deffunc H4( Element of product (doms F)) -> Element of the carrier of L = "/\" ((rng ((Frege F) . \$1)),L); deffunc H5( Element of X, Element of product (doms F)) -> Element of the carrier of L = "/\" (H3(\$1,\$2),L); set D = { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ; set D9 = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ; set E9 = { H4(g) where g is Element of product (doms F) : S1[g] } ; A21: for i being Element of X for g being Element of product (doms F) holds H4(g) = H5(i,g) proof let j be Element of X; ::_thesis: for g being Element of product (doms F) holds H4(g) = H5(j,g) let g be Element of product (doms F); ::_thesis: H4(g) = H5(j,g) for y being set holds ( y in H3(j,g) iff ex x being set st ( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) ) proof let y be set ; ::_thesis: ( y in H3(j,g) iff ex x being set st ( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) ) g in product (Carrier J) by A11; then A22: g in the carrier of (product J) by YELLOW_1:def_4; hereby ::_thesis: ( ex x being set st ( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) implies y in H3(j,g) ) assume y in H3(j,g) ; ::_thesis: ex x being set st ( x in dom ((Frege F) . g) & ((Frege F) . g) . x = y ) then consider i being Element of X such that A23: y = G . (i,g) and i >= j ; reconsider x = i as set ; take x = x; ::_thesis: ( x in dom ((Frege F) . g) & ((Frege F) . g) . x = y ) reconsider i9 = i as Element of I ; A24: i in I ; then A25: i9 in dom F by PARTFUN1:def_2; thus x in dom ((Frege F) . g) by A24, PARTFUN1:def_2; ::_thesis: ((Frege F) . g) . x = y thus ((Frege F) . g) . x = (F . i9) . (g . i) by A12, A25, WAYBEL_5:9 .= the mapping of (Net-Str ((K . i9),(F . i9))) . (g . i) by Def10 .= the mapping of (J . i) . (g . i) by A8 .= y by A22, A23, YELLOW_6:def_13 ; ::_thesis: verum end; given x being set such that A26: x in dom ((Frege F) . g) and A27: y = ((Frege F) . g) . x ; ::_thesis: y in H3(j,g) A28: x in dom F by A12, A26, WAYBEL_5:8; reconsider i9 = x as Element of I by A26; reconsider i = i9 as Element of X ; A29: i >= j by A6; y = (F . x) . (g . x) by A12, A27, A28, WAYBEL_5:9 .= the mapping of (Net-Str ((K . i9),(F . i9))) . (g . i) by Def10 .= the mapping of (J . i) . (g . i) by A8 .= G . (i,g) by A22, YELLOW_6:def_13 ; hence y in H3(j,g) by A29; ::_thesis: verum end; hence H4(g) = H5(j,g) by FUNCT_1:def_3; ::_thesis: verum end; A30: { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } proof A31: the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by YELLOW_6:26; A32: for p being Element of (Iterated J) for i being Element of X for g being Element of product (doms F) st p = [i,g] holds "/\" (H2(p),L) = "/\" (H3(i,g),L) proof let p be Element of (Iterated J); ::_thesis: for i being Element of X for g being Element of product (doms F) st p = [i,g] holds "/\" (H2(p),L) = "/\" (H3(i,g),L) let i be Element of X; ::_thesis: for g being Element of product (doms F) st p = [i,g] holds "/\" (H2(p),L) = "/\" (H3(i,g),L) let g be Element of product (doms F); ::_thesis: ( p = [i,g] implies "/\" (H2(p),L) = "/\" (H3(i,g),L) ) assume A33: p = [i,g] ; ::_thesis: "/\" (H2(p),L) = "/\" (H3(i,g),L) A34: RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = RelStr(# the carrier of [:X,(product J):], the InternalRel of [:X,(product J):] #) by YELLOW_6:def_13; reconsider g9 = g as Element of (product J) by A11, YELLOW_1:def_4; g9 in the carrier of (product J) ; then A35: g9 in product (Carrier J) by YELLOW_1:def_4; reconsider i9 = i as Element of X ; for i being set st i in the carrier of X holds ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) proof let i be set ; ::_thesis: ( i in the carrier of X implies ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) ) assume i in the carrier of X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st ( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) then reconsider ii = i as Element of X ; reconsider i9 = ii as Element of I ; A36: J . i = Net-Str ((K . i9),(F . i9)) by A8; set R = Net-Str ((K . i9),(F . i9)); g9 . ii in the carrier of (Net-Str ((K . i9),(F . i9))) by A36; then reconsider x = g9 . i as Element of (Net-Str ((K . i9),(F . i9))) ; take Net-Str ((K . i9),(F . i9)) ; ::_thesis: ex xi, yi being Element of (Net-Str ((K . i9),(F . i9))) st ( Net-Str ((K . i9),(F . i9)) = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) take x ; ::_thesis: ex yi being Element of (Net-Str ((K . i9),(F . i9))) st ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & yi = g9 . i & x <= yi ) take x ; ::_thesis: ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x ) x <= x ; hence ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x ) by A8; ::_thesis: verum end; then A37: g9 <= g9 by A35, YELLOW_1:def_4; H3(i,g) c= H2(p) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in H3(i,g) or u in H2(p) ) assume u in H3(i,g) ; ::_thesis: u in H2(p) then consider j being Element of X such that A38: u = the mapping of (Iterated J) . (j,g) and A39: j >= i ; reconsider j9 = j as Element of X ; reconsider q = [j,g] as Element of (Iterated J) by A11, YELLOW_6:26; [j9,g9] >= [i9,g9] by A37, A39, YELLOW_3:11; then A40: q >= p by A33, A34, Lm1; u = (Iterated J) . q by A38; hence u in H2(p) by A40; ::_thesis: verum end; then A41: "/\" (H2(p),L) <= "/\" (H3(i,g),L) by WAYBEL_7:1; defpred S2[ Element of X] means \$1 >= i; deffunc H6( Element of X) -> Element of the carrier of L = G . (\$1,g); { H6(k) where k is Element of X : S2[k] } is Subset of L from DOMAIN_1:sch_8(); then reconsider A = H3(i,g) as Subset of L ; defpred S3[ Element of (Iterated J)] means \$1 >= p; deffunc H7( Element of (Iterated J)) -> Element of the carrier of L = (Iterated J) . \$1; { H7(z) where z is Element of (Iterated J) : S3[z] } is Subset of L from DOMAIN_1:sch_8(); then reconsider B = H2(p) as Subset of L ; B is_coarser_than A proof let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not b in B or ex b1 being Element of the carrier of L st ( b1 in A & b1 <= b ) ) assume b in B ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in A & b1 <= b ) then consider q being Element of (Iterated J) such that A42: b = (Iterated J) . q and A43: p <= q ; consider k being Element of X, f being Element of product (Carrier J) such that A44: q = [k,f] by A31, DOMAIN_1:1; reconsider k9 = k as Element of X ; set a = the mapping of (Iterated J) . (k,g); the mapping of (Iterated J) . (k,g) = G . (k,g) ; then reconsider a = the mapping of (Iterated J) . (k,g) as Element of L ; take a ; ::_thesis: ( a in A & a <= b ) reconsider f9 = f as Element of (product J) by YELLOW_1:def_4; A45: [k9,f9] >= [i9,g9] by A33, A34, A43, A44, Lm1; then i <= k by YELLOW_3:11; hence a in A ; ::_thesis: a <= b reconsider k9 = k as Element of I ; set N = Net-Str ((K . k9),(F . k9)); A46: J . k = Net-Str ((K . k9),(F . k9)) by A8; reconsider g9k = g9 . k, f9k = f9 . k as Element of (Net-Str ((K . k9),(F . k9))) by A8; A47: b = (Net-Str ((K . k9),(F . k9))) . f9k by A42, A44, A46, YELLOW_6:27; reconsider kg = [k,g] as Element of (Iterated J) by A11, YELLOW_6:26; A48: a = (Iterated J) . kg .= (Net-Str ((K . k9),(F . k9))) . g9k by A46, YELLOW_6:27 ; g9 <= f9 by A45, YELLOW_3:11; then g9 . k <= f9 . k by WAYBEL_3:28; hence a <= b by A46, A47, A48, Def10; ::_thesis: verum end; then "/\" (H3(i,g),L) <= "/\" (H2(p),L) by Th1; hence "/\" (H2(p),L) = "/\" (H3(i,g),L) by A41, YELLOW_0:def_3; ::_thesis: verum end; thus { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } c= { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } :: according to XBOOLE_0:def_10 ::_thesis: { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } c= { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } or e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ) assume e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ; ::_thesis: e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } then consider p being Element of (Iterated J) such that A49: e = "/\" (H2(p),L) ; consider j being Element of X, g being Element of product (doms F) such that A50: p = [j,g] by A11, A31, DOMAIN_1:1; e = "/\" (H3(j,g),L) by A32, A49, A50; hence e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } or e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ) assume e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ; ::_thesis: e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } then consider i being Element of X, g being Element of product (doms F) such that A51: e = "/\" (H3(i,g),L) ; reconsider j = [i,g] as Element of (Iterated J) by A11, YELLOW_6:26; e = "/\" (H2(j),L) by A32, A51; hence e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ; ::_thesis: verum end; A52: { H4(g) where g is Element of product (doms F) : S1[g] } = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } from WAYBEL11:sch_1(A21); for y being set holds ( y in { H4(g) where g is Element of product (doms F) : S1[g] } iff ex x being set st ( x in dom (Infs ) & y = (Infs ) . x ) ) proof let y be set ; ::_thesis: ( y in { H4(g) where g is Element of product (doms F) : S1[g] } iff ex x being set st ( x in dom (Infs ) & y = (Infs ) . x ) ) thus ( y in { H4(g) where g is Element of product (doms F) : S1[g] } implies ex x being set st ( x in dom (Infs ) & y = (Infs ) . x ) ) ::_thesis: ( ex x being set st ( x in dom (Infs ) & y = (Infs ) . x ) implies y in { H4(g) where g is Element of product (doms F) : S1[g] } ) proof assume y in { H4(g) where g is Element of product (doms F) : S1[g] } ; ::_thesis: ex x being set st ( x in dom (Infs ) & y = (Infs ) . x ) then consider g being Element of product (doms F) such that A53: y = "/\" ((rng ((Frege F) . g)),L) ; take g ; ::_thesis: ( g in dom (Infs ) & y = (Infs ) . g ) thus A54: g in dom (Infs ) by A13; ::_thesis: y = (Infs ) . g thus y = //\ (((Frege F) . g),L) by A53, YELLOW_2:def_6 .= (Infs ) . g by A54, WAYBEL_5:def_2 ; ::_thesis: verum end; given x being set such that A55: x in dom (Infs ) and A56: y = (Infs ) . x ; ::_thesis: y in { H4(g) where g is Element of product (doms F) : S1[g] } reconsider x = x as Element of product (doms F) by A55, PARTFUN1:def_2; y = //\ (((Frege F) . x),L) by A55, A56, WAYBEL_5:def_2 .= "/\" ((rng ((Frege F) . x)),L) by YELLOW_2:def_6 ; hence y in { H4(g) where g is Element of product (doms F) : S1[g] } ; ::_thesis: verum end; then rng (Infs ) = { H4(g) where g is Element of product (doms F) : S1[g] } by FUNCT_1:def_3; then A57: Sup = lim_inf (Iterated J) by A30, A52, YELLOW_2:def_5; reconsider x9 = Inf as Element of L ; set X1 = { (Inf ) where j9 is Element of X : verum } ; set X2 = { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ; A58: { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } = { (Inf ) where j9 is Element of X : verum } proof A59: for j being Element of X holds Inf = "/\" ( { (X . i) where i is Element of X : i >= j } ,L) proof let j be Element of X; ::_thesis: Inf = "/\" ( { (X . i) where i is Element of X : i >= j } ,L) set X3 = { (X . i) where i is Element of X : i >= j } ; for e being set holds ( e in { (X . i) where i is Element of X : i >= j } iff ex u being set st ( u in dom (Sups ) & e = (Sups ) . u ) ) proof let e be set ; ::_thesis: ( e in { (X . i) where i is Element of X : i >= j } iff ex u being set st ( u in dom (Sups ) & e = (Sups ) . u ) ) hereby ::_thesis: ( ex u being set st ( u in dom (Sups ) & e = (Sups ) . u ) implies e in { (X . i) where i is Element of X : i >= j } ) assume e in { (X . i) where i is Element of X : i >= j } ; ::_thesis: ex u being set st ( u in dom (Sups ) & e = (Sups ) . u ) then consider i being Element of X such that A60: e = X . i and i >= j ; reconsider u = i as set ; take u = u; ::_thesis: ( u in dom (Sups ) & e = (Sups ) . u ) u in I ; hence u in dom (Sups ) by FUNCT_2:def_1; ::_thesis: e = (Sups ) . u thus e = (Sups ) . u by A60; ::_thesis: verum end; given u being set such that A61: u in dom (Sups ) and A62: e = (Sups ) . u ; ::_thesis: e in { (X . i) where i is Element of X : i >= j } reconsider i = u as Element of X by A61, FUNCT_2:def_1; A63: i >= j by A6; e = X . i by A62; hence e in { (X . i) where i is Element of X : i >= j } by A63; ::_thesis: verum end; then rng (Sups ) = { (X . i) where i is Element of X : i >= j } by FUNCT_1:def_3; hence Inf = "/\" ( { (X . i) where i is Element of X : i >= j } ,L) by YELLOW_2:def_6; ::_thesis: verum end; thus { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } c= { (Inf ) where j9 is Element of X : verum } :: according to XBOOLE_0:def_10 ::_thesis: { (Inf ) where j9 is Element of X : verum } c= { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } or u in { (Inf ) where j9 is Element of X : verum } ) assume u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ; ::_thesis: u in { (Inf ) where j9 is Element of X : verum } then ex j being Element of X st u = "/\" ( { (X . i) where i is Element of X : i >= j } ,L) ; then u = Inf by A59; hence u in { (Inf ) where j9 is Element of X : verum } ; ::_thesis: verum end; let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (Inf ) where j9 is Element of X : verum } or u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ) set j = the Element of X; assume u in { (Inf ) where j9 is Element of X : verum } ; ::_thesis: u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } then ex j being Element of X st u = Inf ; then u = "/\" ( { (X . i) where i is Element of X : i >= the Element of X } ,L) by A59; hence u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ; ::_thesis: verum end; now__::_thesis:_for_u_being_set_holds_ (_u_in__{__(Inf_)_where_j9_is_Element_of_X_:_verum__}__iff_u_in_{(Inf_)}_) let u be set ; ::_thesis: ( u in { (Inf ) where j9 is Element of X : verum } iff u in {(Inf )} ) ( u in { (Inf ) where j9 is Element of X : verum } iff ex j9 being Element of X st u = Inf ) ; then ( u in { (Inf ) where j9 is Element of X : verum } iff u = Inf ) ; hence ( u in { (Inf ) where j9 is Element of X : verum } iff u in {(Inf )} ) by TARSKI:def_1; ::_thesis: verum end; then "\/" ( { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ,L) = sup {x9} by A58, TARSKI:1 .= Inf by YELLOW_0:39 ; then Inf <= lim_inf X ; then Inf is_S-limit_of X by Def7; then [X,(Inf )] in Scott-Convergence L by A19, Def8; then [(Iterated J),(Inf )] in Scott-Convergence L by A1, A16, YELLOW_6:def_23; then Inf is_S-limit_of Iterated J by A20, Def8; then Inf <= Sup by A57, Def7; hence Inf = Sup by A5, ORDERS_2:2; ::_thesis: verum end; hence L is continuous by WAYBEL_5:18; ::_thesis: verum end; theorem :: WAYBEL11:40 for T being complete Scott TopLattice holds ( T is continuous iff Convergence T = Scott-Convergence T ) proof let T be complete Scott TopLattice; ::_thesis: ( T is continuous iff Convergence T = Scott-Convergence T ) hereby ::_thesis: ( Convergence T = Scott-Convergence T implies T is continuous ) assume T is continuous ; ::_thesis: Convergence T = Scott-Convergence T then reconsider L = T as complete continuous Scott TopLattice ; TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32; hence Convergence T = Convergence (ConvergenceSpace (Scott-Convergence L)) by Lm8 .= Scott-Convergence T by YELLOW_6:44 ; ::_thesis: verum end; thus ( Convergence T = Scott-Convergence T implies T is continuous ) by Th39; ::_thesis: verum end; theorem Th41: :: WAYBEL11:41 for T being complete Scott TopLattice for S being upper Subset of T st S is Open holds S is open proof let T be complete Scott TopLattice; ::_thesis: for S being upper Subset of T st S is Open holds S is open let S be upper Subset of T; ::_thesis: ( S is Open implies S is open ) assume A1: for x being Element of T st x in S holds ex y being Element of T st ( y in S & y << x ) ; :: according to WAYBEL_6:def_1 ::_thesis: S is open S is inaccessible proof let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S ) assume sup D in S ; ::_thesis: D meets S then consider y being Element of T such that A2: y in S and A3: y << sup D by A1; consider d being Element of T such that A4: d in D and A5: y <= d by A3, WAYBEL_3:def_1; d in S by A2, A5, WAYBEL_0:def_20; hence D meets S by A4, XBOOLE_0:3; ::_thesis: verum end; hence S is open by Def4; ::_thesis: verum end; theorem Th42: :: WAYBEL11:42 for L being non empty RelStr for S being upper Subset of L for x being Element of L st x in S holds uparrow x c= S proof let L be non empty RelStr ; ::_thesis: for S being upper Subset of L for x being Element of L st x in S holds uparrow x c= S let S be upper Subset of L; ::_thesis: for x being Element of L st x in S holds uparrow x c= S let x be Element of L; ::_thesis: ( x in S implies uparrow x c= S ) assume A1: x in S ; ::_thesis: uparrow x c= S let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in uparrow x or e in S ) assume A2: e in uparrow x ; ::_thesis: e in S then reconsider y = e as Element of L ; x <= y by A2, WAYBEL_0:18; hence e in S by A1, WAYBEL_0:def_20; ::_thesis: verum end; theorem Th43: :: WAYBEL11:43 for L being complete continuous Scott TopLattice for p being Element of L for S being Subset of L st S is open & p in S holds ex q being Element of L st ( q << p & q in S ) proof let L be complete continuous Scott TopLattice; ::_thesis: for p being Element of L for S being Subset of L st S is open & p in S holds ex q being Element of L st ( q << p & q in S ) let p be Element of L; ::_thesis: for S being Subset of L st S is open & p in S holds ex q being Element of L st ( q << p & q in S ) let S be Subset of L; ::_thesis: ( S is open & p in S implies ex q being Element of L st ( q << p & q in S ) ) assume that A1: S is open and A2: p in S ; ::_thesis: ex q being Element of L st ( q << p & q in S ) A3: S is inaccessible by A1, Def4; sup (waybelow p) = p by WAYBEL_3:def_5; then waybelow p meets S by A2, A3, Def1; then (waybelow p) /\ S <> {} by XBOOLE_0:def_7; then consider u being Element of L such that A4: u in (waybelow p) /\ S by SUBSET_1:4; reconsider u = u as Element of L ; take u ; ::_thesis: ( u << p & u in S ) u in waybelow p by A4, XBOOLE_0:def_4; hence u << p by WAYBEL_3:7; ::_thesis: u in S thus u in S by A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th44: :: WAYBEL11:44 for L being complete continuous Scott TopLattice for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of proof let L be complete continuous Scott TopLattice; ::_thesis: for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of let p be Element of L; ::_thesis: { (wayabove q) where q is Element of L : q << p } is Basis of set X = { (wayabove q) where q is Element of L : q << p } ; { (wayabove q) where q is Element of L : q << p } c= bool the carrier of L proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove q) where q is Element of L : q << p } or e in bool the carrier of L ) assume e in { (wayabove q) where q is Element of L : q << p } ; ::_thesis: e in bool the carrier of L then ex q being Element of L st ( e = wayabove q & q << p ) ; hence e in bool the carrier of L ; ::_thesis: verum end; then reconsider X = { (wayabove q) where q is Element of L : q << p } as Subset-Family of L ; X is Basis of proof A1: X is open proof let e be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not e in X or e is open ) assume e in X ; ::_thesis: e is open then consider q being Element of L such that A2: e = wayabove q and q << p ; wayabove q is open by Th36; hence e is open by A2; ::_thesis: verum end; X is p -quasi_basis proof for Y being set st Y in X holds p in Y proof let e be set ; ::_thesis: ( e in X implies p in e ) assume e in X ; ::_thesis: p in e then ex q being Element of L st ( e = wayabove q & q << p ) ; hence p in e ; ::_thesis: verum end; hence p in Intersect X by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds ( not b1 is open or not p in b1 or ex b2 being Element of bool the carrier of L st ( b2 in X & b2 c= b1 ) ) let S be Subset of L; ::_thesis: ( not S is open or not p in S or ex b1 being Element of bool the carrier of L st ( b1 in X & b1 c= S ) ) assume that A3: S is open and A4: p in S ; ::_thesis: ex b1 being Element of bool the carrier of L st ( b1 in X & b1 c= S ) consider u being Element of L such that A5: u << p and A6: u in S by A3, A4, Th43; take V = wayabove u; ::_thesis: ( V in X & V c= S ) thus V in X by A5; ::_thesis: V c= S A7: S is upper by A3, Def4; A8: wayabove u c= uparrow u by WAYBEL_3:11; uparrow u c= S by A6, A7, Th42; hence V c= S by A8, XBOOLE_1:1; ::_thesis: verum end; hence X is Basis of by A1; ::_thesis: verum end; hence { (wayabove q) where q is Element of L : q << p } is Basis of ; ::_thesis: verum end; theorem Th45: :: WAYBEL11:45 for T being complete continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T proof let T be complete continuous Scott TopLattice; ::_thesis: { (wayabove x) where x is Element of T : verum } is Basis of T set B = { (wayabove x) where x is Element of T : verum } ; A1: { (wayabove x) where x is Element of T : verum } c= the topology of T proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove x) where x is Element of T : verum } or e in the topology of T ) assume e in { (wayabove x) where x is Element of T : verum } ; ::_thesis: e in the topology of T then consider x being Element of T such that A2: e = wayabove x ; wayabove x is open by Th36; hence e in the topology of T by A2, PRE_TOPC:def_2; ::_thesis: verum end; then reconsider P = { (wayabove x) where x is Element of T : verum } as Subset-Family of T by XBOOLE_1:1; for x being Point of T ex B being Basis of st B c= P proof let x be Point of T; ::_thesis: ex B being Basis of st B c= P reconsider p = x as Element of T ; reconsider A = { (wayabove q) where q is Element of T : q << p } as Basis of by Th44; take A ; ::_thesis: A c= P let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in A or u in P ) assume u in A ; ::_thesis: u in P then ex q being Element of T st ( u = wayabove q & q << p ) ; hence u in P ; ::_thesis: verum end; hence { (wayabove x) where x is Element of T : verum } is Basis of T by A1, YELLOW_8:14; ::_thesis: verum end; theorem :: WAYBEL11:46 for T being complete continuous Scott TopLattice for S being upper Subset of T holds ( S is open iff S is Open ) proof let T be complete continuous Scott TopLattice; ::_thesis: for S being upper Subset of T holds ( S is open iff S is Open ) let S be upper Subset of T; ::_thesis: ( S is open iff S is Open ) thus ( S is open implies S is Open ) ::_thesis: ( S is Open implies S is open ) proof assume A1: S is open ; ::_thesis: S is Open let x be Element of T; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in S or ex b1 being Element of the carrier of T st ( b1 in S & b1 is_way_below x ) ) assume x in S ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in S & b1 is_way_below x ) then ex y being Element of T st ( y << x & y in S ) by A1, Th43; hence ex b1 being Element of the carrier of T st ( b1 in S & b1 is_way_below x ) ; ::_thesis: verum end; thus ( S is Open implies S is open ) by Th41; ::_thesis: verum end; theorem :: WAYBEL11:47 for T being complete continuous Scott TopLattice for p being Element of T holds Int (uparrow p) = wayabove p proof let T be complete continuous Scott TopLattice; ::_thesis: for p being Element of T holds Int (uparrow p) = wayabove p let p be Element of T; ::_thesis: Int (uparrow p) = wayabove p thus Int (uparrow p) c= wayabove p :: according to XBOOLE_0:def_10 ::_thesis: wayabove p c= Int (uparrow p) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Int (uparrow p) or y in wayabove p ) assume A1: y in Int (uparrow p) ; ::_thesis: y in wayabove p then reconsider q = y as Element of T ; reconsider S = Int (uparrow p) as Subset of T ; consider u being Element of T such that A2: u << q and A3: u in S by A1, Th43; S c= uparrow p by TOPS_1:16; then p <= u by A3, WAYBEL_0:18; then p << q by A2, WAYBEL_3:2; hence y in wayabove p ; ::_thesis: verum end; wayabove p c= uparrow p by WAYBEL_3:11; hence wayabove p c= Int (uparrow p) by Th36, TOPS_1:24; ::_thesis: verum end; theorem :: WAYBEL11:48 for T being complete continuous Scott TopLattice for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } proof let T be complete continuous Scott TopLattice; ::_thesis: for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } let S be Subset of T; ::_thesis: Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } set B = { (wayabove x) where x is Element of T : verum } ; set I = { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; set P = { (wayabove x) where x is Element of T : wayabove x c= S } ; A1: { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } = { (wayabove x) where x is Element of T : wayabove x c= S } proof thus { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } c= { (wayabove x) where x is Element of T : wayabove x c= S } :: according to XBOOLE_0:def_10 ::_thesis: { (wayabove x) where x is Element of T : wayabove x c= S } c= { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } or e in { (wayabove x) where x is Element of T : wayabove x c= S } ) assume e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; ::_thesis: e in { (wayabove x) where x is Element of T : wayabove x c= S } then consider G being Subset of T such that A2: e = G and A3: G in { (wayabove x) where x is Element of T : verum } and A4: G c= S ; ex x being Element of T st G = wayabove x by A3; hence e in { (wayabove x) where x is Element of T : wayabove x c= S } by A2, A4; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove x) where x is Element of T : wayabove x c= S } or e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ) assume e in { (wayabove x) where x is Element of T : wayabove x c= S } ; ::_thesis: e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } then consider x being Element of T such that A5: e = wayabove x and A6: wayabove x c= S ; wayabove x in { (wayabove x) where x is Element of T : verum } ; hence e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } by A5, A6; ::_thesis: verum end; { (wayabove x) where x is Element of T : verum } is Basis of T by Th45; hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; ::_thesis: verum end;