:: WAYBEL33 semantic presentation begin definition let L be non empty Poset; let X be non empty Subset of L; let F be Filter of (BoolePoset X); func lim_inf F -> Element of L equals :: WAYBEL33:def 1 "\/" ( { (inf B) where B is Subset of L : B in F } ,L); correctness coherence "\/" ( { (inf B) where B is Subset of L : B in F } ,L) is Element of L; ; end; :: deftheorem defines lim_inf WAYBEL33:def_1_:_ for L being non empty Poset for X being non empty Subset of L for F being Filter of (BoolePoset X) holds lim_inf F = "\/" ( { (inf B) where B is Subset of L : B in F } ,L); theorem :: WAYBEL33:1 for L1, L2 being complete LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for X1 being non empty Subset of L1 for X2 being non empty Subset of L2 for F1 being Filter of (BoolePoset X1) for F2 being Filter of (BoolePoset X2) st F1 = F2 holds lim_inf F1 = lim_inf F2 proof let L1, L2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being non empty Subset of L1 for X2 being non empty Subset of L2 for F1 being Filter of (BoolePoset X1) for F2 being Filter of (BoolePoset X2) st F1 = F2 holds lim_inf F1 = lim_inf F2 ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being non empty Subset of L1 for X2 being non empty Subset of L2 for F1 being Filter of (BoolePoset X1) for F2 being Filter of (BoolePoset X2) st F1 = F2 holds lim_inf F1 = lim_inf F2 let X1 be non empty Subset of L1; ::_thesis: for X2 being non empty Subset of L2 for F1 being Filter of (BoolePoset X1) for F2 being Filter of (BoolePoset X2) st F1 = F2 holds lim_inf F1 = lim_inf F2 let X2 be non empty Subset of L2; ::_thesis: for F1 being Filter of (BoolePoset X1) for F2 being Filter of (BoolePoset X2) st F1 = F2 holds lim_inf F1 = lim_inf F2 let F1 be Filter of (BoolePoset X1); ::_thesis: for F2 being Filter of (BoolePoset X2) st F1 = F2 holds lim_inf F1 = lim_inf F2 let F2 be Filter of (BoolePoset X2); ::_thesis: ( F1 = F2 implies lim_inf F1 = lim_inf F2 ) assume A2: F1 = F2 ; ::_thesis: lim_inf F1 = lim_inf F2 set Y2 = { (inf B2) where B2 is Subset of L2 : B2 in F2 } ; set Y1 = { (inf B1) where B1 is Subset of L1 : B1 in F1 } ; A3: { (inf B2) where B2 is Subset of L2 : B2 in F2 } c= { (inf B1) where B1 is Subset of L1 : B1 in F1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } or x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } ) assume x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } ; ::_thesis: x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } then consider B2 being Subset of L2 such that A4: x = inf B2 and A5: B2 in F2 ; F1 c= the carrier of (BoolePoset X1) ; then F1 c= bool X1 by WAYBEL_7:2; then reconsider B1 = B2 as Subset of L1 by A2, A5, XBOOLE_1:1; inf B1 = inf B2 by A1, YELLOW_0:17, YELLOW_0:27; hence x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } by A2, A4, A5; ::_thesis: verum end; { (inf B1) where B1 is Subset of L1 : B1 in F1 } c= { (inf B2) where B2 is Subset of L2 : B2 in F2 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } or x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } ) assume x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } ; ::_thesis: x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } then consider B1 being Subset of L1 such that A6: x = inf B1 and A7: B1 in F1 ; F2 c= the carrier of (BoolePoset X2) ; then F2 c= bool X2 by WAYBEL_7:2; then reconsider B2 = B1 as Subset of L2 by A2, A7, XBOOLE_1:1; inf B1 = inf B2 by A1, YELLOW_0:17, YELLOW_0:27; hence x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } by A2, A6, A7; ::_thesis: verum end; then { (inf B1) where B1 is Subset of L1 : B1 in F1 } = { (inf B2) where B2 is Subset of L2 : B2 in F2 } by A3, XBOOLE_0:def_10; hence lim_inf F1 = lim_inf F2 by A1, YELLOW_0:17, YELLOW_0:26; ::_thesis: verum end; definition let L be non empty TopRelStr ; attrL is lim-inf means :Def2: :: WAYBEL33:def 2 the topology of L = xi L; end; :: deftheorem Def2 defines lim-inf WAYBEL33:def_2_:_ for L being non empty TopRelStr holds ( L is lim-inf iff the topology of L = xi L ); registration cluster non empty lim-inf -> non empty TopSpace-like for TopRelStr ; coherence for b1 being non empty TopRelStr st b1 is lim-inf holds b1 is TopSpace-like proof let L be non empty TopRelStr ; ::_thesis: ( L is lim-inf implies L is TopSpace-like ) set T = ConvergenceSpace (lim_inf-Convergence L); assume L is lim-inf ; ::_thesis: L is TopSpace-like then A1: the topology of L = xi L by Def2 .= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def_4 ; A2: for a being Subset-Family of L st a c= the topology of L holds union a in the topology of L proof let a be Subset-Family of L; ::_thesis: ( a c= the topology of L implies union a in the topology of L ) reconsider b = a as Subset-Family of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def_24; assume a c= the topology of L ; ::_thesis: union a in the topology of L then union b in the topology of (ConvergenceSpace (lim_inf-Convergence L)) by A1, PRE_TOPC:def_1; hence union a in the topology of L by A1; ::_thesis: verum end; the carrier of L = the carrier of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def_24; then A3: the carrier of L in the topology of L by A1, PRE_TOPC:def_1; for a, b being Subset of L st a in the topology of L & b in the topology of L holds a /\ b in the topology of L by A1, PRE_TOPC:def_1; hence L is TopSpace-like by A3, A2, PRE_TOPC:def_1; ::_thesis: verum end; end; registration cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima -> lim-inf for TopRelStr ; coherence for b1 being TopLattice st b1 is trivial holds b1 is lim-inf proof let L be TopLattice; ::_thesis: ( L is trivial implies L is lim-inf ) assume L is trivial ; ::_thesis: L is lim-inf then the carrier of L is 1 -element ; then reconsider L9 = L as 1 -element TopLattice by STRUCT_0:def_19; the carrier of (ConvergenceSpace (lim_inf-Convergence L)) = the carrier of L9 by YELLOW_6:def_24; then reconsider S = ConvergenceSpace (lim_inf-Convergence L) as 1 -element TopSpace by STRUCT_0:def_19; set x = the Point of L9; reconsider y = the Point of L9 as Point of S by YELLOW_6:def_24; thus the topology of L = {{},{y}} by YELLOW_9:9 .= the topology of S by YELLOW_9:9 .= xi L by WAYBEL28:def_4 ; :: according to WAYBEL33:def_2 ::_thesis: verum end; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric continuous with_suprema with_infima complete lim-inf for TopRelStr ; existence ex b1 being TopLattice st ( b1 is lim-inf & b1 is continuous & b1 is complete ) proof take the 1 -element TopLattice ; ::_thesis: ( the 1 -element TopLattice is lim-inf & the 1 -element TopLattice is continuous & the 1 -element TopLattice is complete ) thus ( the 1 -element TopLattice is lim-inf & the 1 -element TopLattice is continuous & the 1 -element TopLattice is complete ) ; ::_thesis: verum end; end; theorem Th2: :: WAYBEL33:2 for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) proof let L1, L2 be non empty 1-sorted ; ::_thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ) assume A1: the carrier of L1 = the carrier of L2 ; ::_thesis: for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) let N1 be NetStr over L1; ::_thesis: ex N2 being strict NetStr over L2 st ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) reconsider f = the mapping of N1 as Function of the carrier of N1, the carrier of L2 by A1; take NetStr(# the carrier of N1, the InternalRel of N1,f #) ; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N1, the InternalRel of N1,f #), the InternalRel of NetStr(# the carrier of N1, the InternalRel of N1,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N1, the InternalRel of N1,f #) ) thus ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N1, the InternalRel of N1,f #), the InternalRel of NetStr(# the carrier of N1, the InternalRel of N1,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N1, the InternalRel of N1,f #) ) ; ::_thesis: verum end; theorem Th3: :: WAYBEL33:3 for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds for N1 being NetStr over L1 st N1 in NetUniv L1 holds ex N2 being strict net of L2 st ( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) proof let L1, L2 be non empty 1-sorted ; ::_thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being NetStr over L1 st N1 in NetUniv L1 holds ex N2 being strict net of L2 st ( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ) assume A1: the carrier of L1 = the carrier of L2 ; ::_thesis: for N1 being NetStr over L1 st N1 in NetUniv L1 holds ex N2 being strict net of L2 st ( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) let N1 be NetStr over L1; ::_thesis: ( N1 in NetUniv L1 implies ex N2 being strict net of L2 st ( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ) assume N1 in NetUniv L1 ; ::_thesis: ex N2 being strict net of L2 st ( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) then consider N being strict net of L1 such that A2: ( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by YELLOW_6:def_11; reconsider f = the mapping of N as Function of the carrier of N, the carrier of L2 by A1; take NetStr(# the carrier of N, the InternalRel of N,f #) ; ::_thesis: ( NetStr(# the carrier of N, the InternalRel of N,f #) in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N, the InternalRel of N,f #) ) thus ( NetStr(# the carrier of N, the InternalRel of N,f #) in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N, the InternalRel of N,f #) ) by A1, A2, YELLOW_6:def_11; ::_thesis: verum end; Lm1: now__::_thesis:_for_L1,_L2_being_non_empty_RelStr_ for_N1_being_net_of_L1 for_N2_being_net_of_L2_st_RelStr(#_the_carrier_of_N1,_the_InternalRel_of_N1_#)_=_RelStr(#_the_carrier_of_N2,_the_InternalRel_of_N2_#)_&_the_mapping_of_N1_=_the_mapping_of_N2_holds_ for_j1_being_Element_of_N1 for_j2_being_Element_of_N2_st_j1_=_j2_holds_ H2(j1)_c=_H1(j2) let L1, L2 be non empty RelStr ; ::_thesis: for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for j1 being Element of N1 for j2 being Element of N2 st j1 = j2 holds H2(j1) c= H1(j2) let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for j1 being Element of N1 for j2 being Element of N2 st j1 = j2 holds H2(j1) c= H1(j2) let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for j1 being Element of N1 for j2 being Element of N2 st j1 = j2 holds H2(j1) c= H1(j2) ) assume that A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and A2: the mapping of N1 = the mapping of N2 ; ::_thesis: for j1 being Element of N1 for j2 being Element of N2 st j1 = j2 holds H2(j1) c= H1(j2) let j1 be Element of N1; ::_thesis: for j2 being Element of N2 st j1 = j2 holds H2(j1) c= H1(j2) deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ; deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ; let j2 be Element of N2; ::_thesis: ( j1 = j2 implies H2(j1) c= H1(j2) ) assume A3: j1 = j2 ; ::_thesis: H2(j1) c= H1(j2) thus H2(j1) c= H1(j2) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in H2(j1) or y in H1(j2) ) assume y in H2(j1) ; ::_thesis: y in H1(j2) then consider i1 being Element of N1 such that A4: y = N1 . i1 and A5: i1 >= j1 ; reconsider i1 = i1 as Element of N1 ; reconsider i2 = i1, j2 = j2 as Element of N2 by A1; A6: N1 . i1 = N2 . i2 by A2; i2 >= j2 by A1, A3, A5, YELLOW_0:1; hence y in H1(j2) by A4, A6; ::_thesis: verum end; end; Lm2: now__::_thesis:_for_L1,_L2_being_/\-complete_Semilattice_st_RelStr(#_the_carrier_of_L1,_the_InternalRel_of_L1_#)_=_RelStr(#_the_carrier_of_L2,_the_InternalRel_of_L2_#)_holds_ for_N1_being_net_of_L1 for_N2_being_net_of_L2_st_RelStr(#_the_carrier_of_N1,_the_InternalRel_of_N1_#)_=_RelStr(#_the_carrier_of_N2,_the_InternalRel_of_N2_#)_&_the_mapping_of_N1_=_the_mapping_of_N2_holds_ {__("/\"_(H2(j),L1))_where_j_is_Element_of_N1_:_verum__}__c=__{__("/\"_(H1(j),L2))_where_j_is_Element_of_N2_:_verum__}_ let L1, L2 be /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ) assume that A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and A3: the mapping of N1 = the mapping of N2 ; ::_thesis: { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ; deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ; set U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; set U2 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ; thus { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } or x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ) assume x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; ::_thesis: x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } then consider j1 being Element of N1 such that A4: x = "/\" (H2(j1),L1) ; reconsider j2 = j1 as Element of N2 by A2; ( H2(j1) c= H1(j2) & H1(j2) c= H2(j1) ) by A2, A3, Lm1; then A5: H2(j1) = H1(j2) by XBOOLE_0:def_10; reconsider j1 = j1 as Element of N1 ; A6: H2(j1) c= the carrier of L1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H2(j1) or x in the carrier of L1 ) assume x in H2(j1) ; ::_thesis: x in the carrier of L1 then ex i being Element of N1 st ( x = N1 . i & i >= j1 ) ; hence x in the carrier of L1 ; ::_thesis: verum end; [#] N1 is directed by WAYBEL_0:def_6; then consider j0 being Element of N1 such that j0 in the carrier of N1 and A7: j1 <= j0 and j1 <= j0 by WAYBEL_0:def_1; N1 . j0 in H2(j1) by A7; then reconsider S = H2(j1) as non empty Subset of L1 by A6; ex_inf_of S,L1 by WAYBEL_0:76; then x = "/\" (H1(j2),L2) by A1, A4, A5, YELLOW_0:27; hence x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ; ::_thesis: verum end; end; theorem Th4: :: WAYBEL33:4 for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds lim_inf N1 = lim_inf N2 proof let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds lim_inf N1 = lim_inf N2 ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds lim_inf N1 = lim_inf N2 let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds lim_inf N1 = lim_inf N2 let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies lim_inf N1 = lim_inf N2 ) assume A2: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ; ::_thesis: lim_inf N1 = lim_inf N2 deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ; deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ; set U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; set U2 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ; A3: ( lim_inf N1 = "\/" ( { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ,L1) & lim_inf N2 = "\/" ( { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ,L2) ) by WAYBEL11:def_6; { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= the carrier of L1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } or x in the carrier of L1 ) assume x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; ::_thesis: x in the carrier of L1 then ex j being Element of N1 st x = "/\" (H2(j),L1) ; hence x in the carrier of L1 ; ::_thesis: verum end; then reconsider U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } as Subset of L1 ; ( not U1 is empty & U1 is directed ) by WAYBEL32:7; then A4: ex_sup_of U1,L1 by WAYBEL_0:75; ( U1 c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } & { ("/\" (H1(j),L2)) where j is Element of N2 : verum } c= U1 ) by A1, A2, Lm2; then U1 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } by XBOOLE_0:def_10; hence lim_inf N1 = lim_inf N2 by A1, A3, A4, YELLOW_0:26; ::_thesis: verum end; theorem Th5: :: WAYBEL33:5 for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for S1 being subnet of N1 ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) proof let L1, L2 be non empty 1-sorted ; ::_thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for S1 being subnet of N1 ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) ) assume A1: the carrier of L1 = the carrier of L2 ; ::_thesis: for N1 being net of L1 for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for S1 being subnet of N1 ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for S1 being subnet of N1 ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for S1 being subnet of N1 ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) ) assume that A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and A3: the mapping of N1 = the mapping of N2 ; ::_thesis: for S1 being subnet of N1 ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) let S1 be subnet of N1; ::_thesis: ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) consider S2 being strict NetStr over L2 such that A4: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and A5: the mapping of S1 = the mapping of S2 by A1, Th2; reconsider S2 = S2 as strict net of L2 by A4; consider f being Function of S1,N1 such that A6: the mapping of S1 = the mapping of N1 * f and A7: for B5 being Element of N1 ex B6 being Element of S1 st for B7 being Element of S1 st B6 <= B7 holds B5 <= f . B7 by YELLOW_6:def_9; reconsider g = f as Function of S2,N2 by A2, A4; S2 is subnet of N2 proof take g ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of S2 = the mapping of N2 * g & ( for b1 being Element of the carrier of N2 ex b2 being Element of the carrier of S2 st for b3 being Element of the carrier of S2 holds ( not b2 <= b3 or b1 <= g . b3 ) ) ) thus the mapping of S2 = the mapping of N2 * g by A3, A5, A6; ::_thesis: for b1 being Element of the carrier of N2 ex b2 being Element of the carrier of S2 st for b3 being Element of the carrier of S2 holds ( not b2 <= b3 or b1 <= g . b3 ) let B2 be Element of N2; ::_thesis: ex b1 being Element of the carrier of S2 st for b2 being Element of the carrier of S2 holds ( not b1 <= b2 or B2 <= g . b2 ) reconsider b2 = B2 as Element of N1 by A2; consider b6 being Element of S1 such that A8: for b7 being Element of S1 st b6 <= b7 holds b2 <= f . b7 by A7; reconsider B3 = b6 as Element of S2 by A4; take B3 ; ::_thesis: for b1 being Element of the carrier of S2 holds ( not B3 <= b1 or B2 <= g . b1 ) let B4 be Element of S2; ::_thesis: ( not B3 <= B4 or B2 <= g . B4 ) reconsider b4 = B4 as Element of S1 by A4; assume B3 <= B4 ; ::_thesis: B2 <= g . B4 then b6 <= b4 by A4, YELLOW_0:1; then b2 <= f . b4 by A8; hence B2 <= g . B4 by A2, YELLOW_0:1; ::_thesis: verum end; hence ex S2 being strict subnet of N2 st ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) by A4, A5; ::_thesis: verum end; theorem Th6: :: WAYBEL33:6 for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for N1 being NetStr over L1 for a being set st [N1,a] in lim_inf-Convergence L1 holds ex N2 being strict net of L2 st ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) proof let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being NetStr over L1 for a being set st [N1,a] in lim_inf-Convergence L1 holds ex N2 being strict net of L2 st ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for N1 being NetStr over L1 for a being set st [N1,a] in lim_inf-Convergence L1 holds ex N2 being strict net of L2 st ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) let N1 be NetStr over L1; ::_thesis: for a being set st [N1,a] in lim_inf-Convergence L1 holds ex N2 being strict net of L2 st ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) let a be set ; ::_thesis: ( [N1,a] in lim_inf-Convergence L1 implies ex N2 being strict net of L2 st ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ) assume A2: [N1,a] in lim_inf-Convergence L1 ; ::_thesis: ex N2 being strict net of L2 st ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) lim_inf-Convergence L1 c= [:(NetUniv L1), the carrier of L1:] by YELLOW_6:def_18; then consider N, x being set such that A3: N in NetUniv L1 and A4: x in the carrier of L1 and A5: [N1,a] = [N,x] by A2, ZFMISC_1:def_2; reconsider x = x as Element of L1 by A4; A6: N = N1 by A5, XTUPLE_0:1; then consider N2 being strict net of L2 such that A7: N2 in NetUniv L2 and A8: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) by A1, A3, Th3; ex N being strict net of L1 st ( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by A3, A6, YELLOW_6:def_11; then reconsider N1 = N1 as strict net of L1 ; A9: now__::_thesis:_for_M_being_subnet_of_N2_holds_x_=_lim_inf_M let M be subnet of N2; ::_thesis: x = lim_inf M consider M1 being strict subnet of N1 such that A10: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of M1, the InternalRel of M1 #) & the mapping of M = the mapping of M1 ) by A1, A8, Th5; thus x = lim_inf M1 by A2, A3, A5, A6, WAYBEL28:def_3 .= lim_inf M by A1, A10, Th4 ; ::_thesis: verum end; take N2 ; ::_thesis: ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) x = a by A5, XTUPLE_0:1; hence ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) by A1, A7, A8, A9, WAYBEL28:def_3; ::_thesis: verum end; theorem Th7: :: WAYBEL33:7 for L1, L2 being non empty 1-sorted for N1 being non empty NetStr over L1 for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for X being set st N1 is_eventually_in X holds N2 is_eventually_in X proof let L1, L2 be non empty 1-sorted ; ::_thesis: for N1 being non empty NetStr over L1 for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for X being set st N1 is_eventually_in X holds N2 is_eventually_in X let N1 be non empty NetStr over L1; ::_thesis: for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds for X being set st N1 is_eventually_in X holds N2 is_eventually_in X let N2 be non empty NetStr over L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for X being set st N1 is_eventually_in X holds N2 is_eventually_in X ) assume that A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and A2: the mapping of N1 = the mapping of N2 ; ::_thesis: for X being set st N1 is_eventually_in X holds N2 is_eventually_in X let X be set ; ::_thesis: ( N1 is_eventually_in X implies N2 is_eventually_in X ) given i1 being Element of N1 such that A3: for j being Element of N1 st i1 <= j holds N1 . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: N2 is_eventually_in X reconsider i2 = i1 as Element of N2 by A1; take i2 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds ( not i2 <= b1 or N2 . b1 in X ) let j2 be Element of N2; ::_thesis: ( not i2 <= j2 or N2 . j2 in X ) reconsider j1 = j2 as Element of N1 by A1; assume i2 <= j2 ; ::_thesis: N2 . j2 in X then N1 . j1 in X by A1, A3, YELLOW_0:1; hence N2 . j2 in X by A2; ::_thesis: verum end; Lm3: for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) proof let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (ConvergenceSpace (lim_inf-Convergence L1)) or x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) A2: the topology of (ConvergenceSpace (lim_inf-Convergence L2)) = { V where V is Subset of L2 : for p being Element of L2 st p in V holds for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds N is_eventually_in V } by YELLOW_6:def_24; A3: the topology of (ConvergenceSpace (lim_inf-Convergence L1)) = { V where V is Subset of L1 : for p being Element of L1 st p in V holds for N being net of L1 st [N,p] in lim_inf-Convergence L1 holds N is_eventually_in V } by YELLOW_6:def_24; assume x in the topology of (ConvergenceSpace (lim_inf-Convergence L1)) ; ::_thesis: x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) then consider V being Subset of L1 such that A4: x = V and A5: for p being Element of L1 st p in V holds for N being net of L1 st [N,p] in lim_inf-Convergence L1 holds N is_eventually_in V by A3; reconsider V2 = V as Subset of L2 by A1; now__::_thesis:_for_p_being_Element_of_L2_st_p_in_V2_holds_ for_N_being_net_of_L2_st_[N,p]_in_lim_inf-Convergence_L2_holds_ N_is_eventually_in_V2 let p be Element of L2; ::_thesis: ( p in V2 implies for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds N is_eventually_in V2 ) assume A6: p in V2 ; ::_thesis: for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds N is_eventually_in V2 let N be net of L2; ::_thesis: ( [N,p] in lim_inf-Convergence L2 implies N is_eventually_in V2 ) assume [N,p] in lim_inf-Convergence L2 ; ::_thesis: N is_eventually_in V2 then ex N1 being strict net of L1 st ( [N1,p] in lim_inf-Convergence L1 & RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N1, the InternalRel of N1 #) & the mapping of N = the mapping of N1 ) by A1, Th6; hence N is_eventually_in V2 by A5, A6, Th7; ::_thesis: verum end; hence x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) by A2, A4; ::_thesis: verum end; theorem :: WAYBEL33:8 for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) proof let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) set C2 = lim_inf-Convergence L2; set C1 = lim_inf-Convergence L1; set T1 = ConvergenceSpace (lim_inf-Convergence L1); set T2 = ConvergenceSpace (lim_inf-Convergence L2); ( the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) & the topology of (ConvergenceSpace (lim_inf-Convergence L2)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L1)) ) by A1, Lm3; then ( the carrier of (ConvergenceSpace (lim_inf-Convergence L2)) = the carrier of L2 & the topology of (ConvergenceSpace (lim_inf-Convergence L1)) = the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) by XBOOLE_0:def_10, YELLOW_6:def_24; hence ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) by A1, YELLOW_6:def_24; ::_thesis: verum end; theorem Th9: :: WAYBEL33:9 for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds xi L1 = xi L2 proof let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies xi L1 = xi L2 ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: xi L1 = xi L2 ( xi L1 = the topology of (ConvergenceSpace (lim_inf-Convergence L1)) & xi L2 = the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) by WAYBEL28:def_4; hence ( xi L1 c= xi L2 & xi L2 c= xi L1 ) by A1, Lm3; :: according to XBOOLE_0:def_10 ::_thesis: verum end; registration let R be non empty reflexive /\-complete RelStr ; cluster -> /\-complete for TopAugmentation of R; coherence for b1 being TopAugmentation of R holds b1 is /\-complete proof let T be TopAugmentation of R; ::_thesis: T is /\-complete let X be non empty Subset of T; :: according to WAYBEL_0:def_40 ::_thesis: ex b1 being Element of the carrier of T st ( b1 is_<=_than X & ( for b2 being Element of the carrier of T holds ( not b2 is_<=_than X or b2 <= b1 ) ) ) A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then reconsider Y = X as non empty Subset of R ; consider x being Element of R such that A2: x is_<=_than Y and A3: for y being Element of R st y is_<=_than Y holds x >= y by WAYBEL_0:def_40; reconsider y = x as Element of T by A1; take y ; ::_thesis: ( y is_<=_than X & ( for b1 being Element of the carrier of T holds ( not b1 is_<=_than X or b1 <= y ) ) ) thus y is_<=_than X by A1, A2, YELLOW_0:2; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 is_<=_than X or b1 <= y ) let z be Element of T; ::_thesis: ( not z is_<=_than X or z <= y ) reconsider v = z as Element of R by A1; assume z is_<=_than X ; ::_thesis: z <= y then x >= v by A1, A3, YELLOW_0:2; hence z <= y by A1, YELLOW_0:1; ::_thesis: verum end; end; registration let R be Semilattice; cluster -> with_infima for TopAugmentation of R; coherence for b1 being TopAugmentation of R holds b1 is with_infima proof let T be TopAugmentation of R; ::_thesis: T is with_infima let x, y be Element of T; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of T st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of T holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then reconsider x9 = x, y9 = y as Element of R ; consider z9 being Element of R such that A2: ( z9 <= x9 & z9 <= y9 ) and A3: for v9 being Element of R st v9 <= x9 & v9 <= y9 holds v9 <= z9 by LATTICE3:def_11; reconsider z = z9 as Element of T by A1; take z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of T holds ( not b1 <= x or not b1 <= y or b1 <= z ) ) ) thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:1; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 <= x or not b1 <= y or b1 <= z ) let v be Element of T; ::_thesis: ( not v <= x or not v <= y or v <= z ) reconsider v9 = v as Element of R by A1; assume ( v <= x & v <= y ) ; ::_thesis: v <= z then ( v9 <= x9 & v9 <= y9 ) by A1, YELLOW_0:1; then v9 <= z9 by A3; hence v <= z by A1, YELLOW_0:1; ::_thesis: verum end; end; registration let L be up-complete /\-complete Semilattice; cluster non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict lim-inf for TopAugmentation of L; existence ex b1 being TopAugmentation of L st ( b1 is strict & b1 is lim-inf ) proof set T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #); A1: RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) ; then reconsider T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) as TopAugmentation of L by YELLOW_9:def_4; take T ; ::_thesis: ( T is strict & T is lim-inf ) thus T is strict ; ::_thesis: T is lim-inf thus the topology of T = xi T by A1, Th9; :: according to WAYBEL33:def_2 ::_thesis: verum end; end; theorem Th10: :: WAYBEL33:10 for L being up-complete /\-complete Semilattice for X being lim-inf TopAugmentation of L holds xi L = the topology of X proof let L be up-complete /\-complete Semilattice; ::_thesis: for X being lim-inf TopAugmentation of L holds xi L = the topology of X let X be lim-inf TopAugmentation of L; ::_thesis: xi L = the topology of X ( the topology of X = xi X & RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of L, the InternalRel of L #) ) by Def2, YELLOW_9:def_4; hence xi L = the topology of X by Th9; ::_thesis: verum end; definition let L be up-complete /\-complete Semilattice; func Xi L -> strict TopAugmentation of L means :Def3: :: WAYBEL33:def 3 it is lim-inf ; uniqueness for b1, b2 being strict TopAugmentation of L st b1 is lim-inf & b2 is lim-inf holds b1 = b2 proof let T1, T2 be strict TopAugmentation of L; ::_thesis: ( T1 is lim-inf & T2 is lim-inf implies T1 = T2 ) assume A1: ( the topology of T1 = xi T1 & the topology of T2 = xi T2 ) ; :: according to WAYBEL33:def_2 ::_thesis: T1 = T2 ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4; hence T1 = T2 by A1, Th9; ::_thesis: verum end; existence ex b1 being strict TopAugmentation of L st b1 is lim-inf proof set T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #); A2: RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) ; then reconsider T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) as strict TopAugmentation of L by YELLOW_9:def_4; take T ; ::_thesis: T is lim-inf thus the topology of T = xi T by A2, Th9; :: according to WAYBEL33:def_2 ::_thesis: verum end; end; :: deftheorem Def3 defines Xi WAYBEL33:def_3_:_ for L being up-complete /\-complete Semilattice for b2 being strict TopAugmentation of L holds ( b2 = Xi L iff b2 is lim-inf ); registration let L be up-complete /\-complete Semilattice; cluster Xi L -> strict lim-inf ; coherence Xi L is lim-inf by Def3; end; theorem Th11: :: WAYBEL33:11 for L being complete LATTICE for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) proof let L be complete LATTICE; ::_thesis: for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) let N be net of L; ::_thesis: lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ; set Y = { (inf (N | i)) where i is Element of N : verum } ; for x being set st x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } holds x in { (inf (N | i)) where i is Element of N : verum } proof let x be set ; ::_thesis: ( x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } implies x in { (inf (N | i)) where i is Element of N : verum } ) assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ; ::_thesis: x in { (inf (N | i)) where i is Element of N : verum } then consider j being Element of N such that A1: x = "/\" ( { (N . i) where i is Element of N : i >= j } ,L) ; reconsider x = x as Element of L by A1; set S = { (N . i) where i is Element of N : i >= j } ; reconsider i = j as Element of N ; for b being set st b in rng the mapping of (N | i) holds b in { (N . i) where i is Element of N : i >= j } proof let b be set ; ::_thesis: ( b in rng the mapping of (N | i) implies b in { (N . i) where i is Element of N : i >= j } ) assume b in rng the mapping of (N | i) ; ::_thesis: b in { (N . i) where i is Element of N : i >= j } then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19; then consider k being Element of (N | i) such that A2: b = (N | i) . k ; the carrier of (N | i) c= the carrier of N by WAYBEL_9:13; then reconsider l = k as Element of N by TARSKI:def_3; k in the carrier of (N | i) ; then k in { y where y is Element of N : i <= y } by WAYBEL_9:12; then A3: ex y being Element of N st ( k = y & i <= y ) ; reconsider k = k as Element of (N | i) ; N . l = (N | i) . k by WAYBEL_9:16; hence b in { (N . i) where i is Element of N : i >= j } by A2, A3; ::_thesis: verum end; then A4: rng the mapping of (N | i) c= { (N . i) where i is Element of N : i >= j } by TARSKI:def_3; A5: ex_inf_of { (N . i) where i is Element of N : i >= j } ,L by YELLOW_0:17; then A6: { (N . i) where i is Element of N : i >= j } is_>=_than x by A1, YELLOW_0:def_10; A7: rng the mapping of (N | i) is_>=_than x proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in rng the mapping of (N | i) or x <= b ) thus ( not b in rng the mapping of (N | i) or x <= b ) by A6, A4, LATTICE3:def_8; ::_thesis: verum end; for b being set st b in { (N . i) where i is Element of N : i >= j } holds b in rng the mapping of (N | i) proof let b be set ; ::_thesis: ( b in { (N . i) where i is Element of N : i >= j } implies b in rng the mapping of (N | i) ) assume b in { (N . i) where i is Element of N : i >= j } ; ::_thesis: b in rng the mapping of (N | i) then consider k being Element of N such that A8: b = N . k and A9: k >= j ; reconsider l = k as Element of N ; l in { y where y is Element of N : i <= y } by A9; then reconsider k = k as Element of (N | i) by WAYBEL_9:12; reconsider k = k as Element of (N | i) ; N . l = (N | i) . k by WAYBEL_9:16; then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A8; hence b in rng the mapping of (N | i) by WAYBEL11:19; ::_thesis: verum end; then { (N . i) where i is Element of N : i >= j } c= rng the mapping of (N | i) by TARSKI:def_3; then { (N . i) where i is Element of N : i >= j } = rng the mapping of (N | i) by A4, XBOOLE_0:def_10; then for a being Element of L st rng the mapping of (N | i) is_>=_than a holds a <= x by A1, A5, YELLOW_0:def_10; then consider i being Element of N such that A10: ( ex_inf_of rng the mapping of (N | i),L & rng the mapping of (N | i) is_>=_than x & ( for a being Element of L st rng the mapping of (N | i) is_>=_than a holds a <= x ) ) by A7, YELLOW_0:17; A11: inf (N | i) = Inf by WAYBEL_9:def_2 .= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def_6 ; x = "/\" ((rng the mapping of (N | i)),L) by A10, YELLOW_0:def_10; hence x in { (inf (N | i)) where i is Element of N : verum } by A11; ::_thesis: verum end; then A12: ( lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ,L) & { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } c= { (inf (N | i)) where i is Element of N : verum } ) by TARSKI:def_3, WAYBEL11:def_6; for x being set st x in { (inf (N | i)) where i is Element of N : verum } holds x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } proof let x be set ; ::_thesis: ( x in { (inf (N | i)) where i is Element of N : verum } implies x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ) assume x in { (inf (N | i)) where i is Element of N : verum } ; ::_thesis: x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } then consider i being Element of N such that A13: x = inf (N | i) ; set S = { (N . j) where j is Element of N : j >= i } ; for b being set st b in rng the mapping of (N | i) holds b in { (N . j) where j is Element of N : j >= i } proof let b be set ; ::_thesis: ( b in rng the mapping of (N | i) implies b in { (N . j) where j is Element of N : j >= i } ) assume b in rng the mapping of (N | i) ; ::_thesis: b in { (N . j) where j is Element of N : j >= i } then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19; then consider k being Element of (N | i) such that A14: b = (N | i) . k ; the carrier of (N | i) c= the carrier of N by WAYBEL_9:13; then reconsider l = k as Element of N by TARSKI:def_3; k in the carrier of (N | i) ; then k in { y where y is Element of N : i <= y } by WAYBEL_9:12; then A15: ex y being Element of N st ( k = y & i <= y ) ; reconsider k = k as Element of (N | i) ; N . l = (N | i) . k by WAYBEL_9:16; hence b in { (N . j) where j is Element of N : j >= i } by A14, A15; ::_thesis: verum end; then A16: rng the mapping of (N | i) c= { (N . j) where j is Element of N : j >= i } by TARSKI:def_3; reconsider x = x as Element of L by A13; A17: x = Inf by A13, WAYBEL_9:def_2 .= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def_6 ; for b being set st b in { (N . j) where j is Element of N : j >= i } holds b in rng the mapping of (N | i) proof let b be set ; ::_thesis: ( b in { (N . j) where j is Element of N : j >= i } implies b in rng the mapping of (N | i) ) assume b in { (N . j) where j is Element of N : j >= i } ; ::_thesis: b in rng the mapping of (N | i) then consider k being Element of N such that A18: b = N . k and A19: k >= i ; reconsider l = k as Element of N ; l in { y where y is Element of N : i <= y } by A19; then reconsider k = k as Element of (N | i) by WAYBEL_9:12; reconsider k = k as Element of (N | i) ; N . l = (N | i) . k by WAYBEL_9:16; then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A18; hence b in rng the mapping of (N | i) by WAYBEL11:19; ::_thesis: verum end; then { (N . j) where j is Element of N : j >= i } c= rng the mapping of (N | i) by TARSKI:def_3; then rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i } by A16, XBOOLE_0:def_10; hence x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by A17; ::_thesis: verum end; then { (inf (N | i)) where i is Element of N : verum } c= { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by TARSKI:def_3; hence lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) by A12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th12: :: WAYBEL33:12 for L being complete LATTICE for F being proper Filter of (BoolePoset ([#] L)) for f being Subset of L st f in F holds for i being Element of (a_net F) st i `2 = f holds inf f = inf ((a_net F) | i) proof let L be complete LATTICE; ::_thesis: for F being proper Filter of (BoolePoset ([#] L)) for f being Subset of L st f in F holds for i being Element of (a_net F) st i `2 = f holds inf f = inf ((a_net F) | i) let F be proper Filter of (BoolePoset ([#] L)); ::_thesis: for f being Subset of L st f in F holds for i being Element of (a_net F) st i `2 = f holds inf f = inf ((a_net F) | i) let f be Subset of L; ::_thesis: ( f in F implies for i being Element of (a_net F) st i `2 = f holds inf f = inf ((a_net F) | i) ) assume A1: f in F ; ::_thesis: for i being Element of (a_net F) st i `2 = f holds inf f = inf ((a_net F) | i) let i be Element of (a_net F); ::_thesis: ( i `2 = f implies inf f = inf ((a_net F) | i) ) assume A2: i `2 = f ; ::_thesis: inf f = inf ((a_net F) | i) for b being set st b in f holds b in rng the mapping of ((a_net F) | i) proof let b be set ; ::_thesis: ( b in f implies b in rng the mapping of ((a_net F) | i) ) assume A3: b in f ; ::_thesis: b in rng the mapping of ((a_net F) | i) then reconsider b = b as Element of L ; reconsider f = f as Element of F by A1; [b,f] in { [a,g] where a is Element of L, g is Element of F : a in g } by A3; then reconsider k = [b,f] as Element of (a_net F) by YELLOW19:def_4; reconsider l = k as Element of (a_net F) ; [b,f] `1 = b ; then A4: b = (a_net F) . k by YELLOW19:def_4; [b,f] `2 = f ; then k `2 c= i `2 by A2; then i <= k by YELLOW19:def_4; then l in { y where y is Element of (a_net F) : i <= y } ; then reconsider k = k as Element of ((a_net F) | i) by WAYBEL_9:12; reconsider k = k as Element of ((a_net F) | i) ; (a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16; then b in { (((a_net F) | i) . m) where m is Element of ((a_net F) | i) : verum } by A4; hence b in rng the mapping of ((a_net F) | i) by WAYBEL11:19; ::_thesis: verum end; then A5: f c= rng the mapping of ((a_net F) | i) by TARSKI:def_3; for b being set st b in rng the mapping of ((a_net F) | i) holds b in f proof let b be set ; ::_thesis: ( b in rng the mapping of ((a_net F) | i) implies b in f ) assume b in rng the mapping of ((a_net F) | i) ; ::_thesis: b in f then b in { (((a_net F) | i) . k) where k is Element of ((a_net F) | i) : verum } by WAYBEL11:19; then consider k being Element of ((a_net F) | i) such that A6: b = ((a_net F) | i) . k ; A7: the carrier of ((a_net F) | i) c= the carrier of (a_net F) by WAYBEL_9:13; then reconsider l = k as Element of (a_net F) by TARSKI:def_3; k in the carrier of (a_net F) by A7, TARSKI:def_3; then A8: k in { [c,g] where c is Element of L, g is Element of F : c in g } by YELLOW19:def_4; k in the carrier of ((a_net F) | i) ; then k in { y where y is Element of (a_net F) : i <= y } by WAYBEL_9:12; then ex y being Element of (a_net F) st ( k = y & i <= y ) ; then A9: l `2 c= f by A2, YELLOW19:def_4; consider c being Element of L, g being Element of F such that A10: k = [c,g] and A11: c in g by A8; A12: ( [c,g] `1 = c & [c,g] `2 = g ) ; reconsider k = k as Element of ((a_net F) | i) ; (a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16; then b = l `1 by A6, YELLOW19:def_4; hence b in f by A11, A12, A9, A10; ::_thesis: verum end; then A13: rng the mapping of ((a_net F) | i) c= f by TARSKI:def_3; inf ((a_net F) | i) = Inf by WAYBEL_9:def_2 .= "/\" ((rng the mapping of ((a_net F) | i)),L) by YELLOW_2:def_6 ; hence inf f = inf ((a_net F) | i) by A13, A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th13: :: WAYBEL33:13 for L being complete LATTICE for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F) proof let L be complete LATTICE; ::_thesis: for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F) let F be proper Filter of (BoolePoset ([#] L)); ::_thesis: lim_inf F = lim_inf (a_net F) set X = { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; set Y = { (inf B) where B is Subset of L : B in F } ; for x being set st x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } holds x in { (inf B) where B is Subset of L : B in F } proof let x be set ; ::_thesis: ( x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } implies x in { (inf B) where B is Subset of L : B in F } ) assume x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; ::_thesis: x in { (inf B) where B is Subset of L : B in F } then consider i being Element of (a_net F) such that A1: x = inf ((a_net F) | i) ; reconsider i = i as Element of (a_net F) ; i in the carrier of (a_net F) ; then i in { [b,g] where b is Element of L, g is Element of F : b in g } by YELLOW19:def_4; then consider a being Element of L, f being Element of F such that A2: i = [a,f] and a in f ; reconsider i = i as Element of (a_net F) ; reconsider f = f as Element of (BoolePoset ([#] L)) ; reconsider f = f as Subset of L by WAYBEL_7:2; [a,f] `2 = f ; then inf f = inf ((a_net F) | i) by Th12, A2; hence x in { (inf B) where B is Subset of L : B in F } by A1; ::_thesis: verum end; then A3: { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } c= { (inf B) where B is Subset of L : B in F } by TARSKI:def_3; for x being set st x in { (inf B) where B is Subset of L : B in F } holds x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } proof let x be set ; ::_thesis: ( x in { (inf B) where B is Subset of L : B in F } implies x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ) assume x in { (inf B) where B is Subset of L : B in F } ; ::_thesis: x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } then consider B being Subset of L such that A4: x = inf B and A5: B in F ; not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4; then B <> {} by A5, YELLOW_1:18; then consider a being Element of L such that A6: a in B by SUBSET_1:4; reconsider B = B as Element of F by A5; [a,B] in { [b,f] where b is Element of L, f is Element of F : b in f } by A6; then reconsider i = [a,B] as Element of (a_net F) by YELLOW19:def_4; [a,B] `2 = B ; then x = inf ((a_net F) | i) by A4, Th12; hence x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; ::_thesis: verum end; then A7: { (inf B) where B is Subset of L : B in F } c= { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } by TARSKI:def_3; lim_inf (a_net F) = "\/" ( { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ,L) by Th11; hence lim_inf F = lim_inf (a_net F) by A3, A7, XBOOLE_0:def_10; ::_thesis: verum end; Lm4: for L being LATTICE for F being non empty Subset of (BoolePoset ([#] L)) holds { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):] proof let L be LATTICE; ::_thesis: for F being non empty Subset of (BoolePoset ([#] L)) holds { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):] let F be non empty Subset of (BoolePoset ([#] L)); ::_thesis: { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [a,f] where a is Element of L, f is Element of F : a in f } or x in [: the carrier of L,(bool the carrier of L):] ) assume x in { [a,f] where a is Element of L, f is Element of F : a in f } ; ::_thesis: x in [: the carrier of L,(bool the carrier of L):] then consider a being Element of L, f being Element of F such that A1: x = [a,f] and a in f ; f is Subset of ([#] L) by WAYBEL_7:2; hence x in [: the carrier of L,(bool the carrier of L):] by A1, ZFMISC_1:def_2; ::_thesis: verum end; theorem Th14: :: WAYBEL33:14 for L being complete LATTICE for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L proof let L be complete LATTICE; ::_thesis: for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L let F be proper Filter of (BoolePoset ([#] L)); ::_thesis: a_net F in NetUniv L set S = { [a,f] where a is Element of L, f is Element of F : a in f } ; set UN = the_universe_of the carrier of L; reconsider UN = the_universe_of the carrier of L as universal set ; the_transitive-closure_of the carrier of L in UN by CLASSES1:2; then A1: the carrier of L in UN by CLASSES1:3, CLASSES1:52; then bool the carrier of L in UN by CLASSES2:59; then A2: [: the carrier of L,(bool the carrier of L):] in UN by A1, CLASSES2:61; { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):] by Lm4; then ( { [a,f] where a is Element of L, f is Element of F : a in f } = the carrier of (a_net F) & { [a,f] where a is Element of L, f is Element of F : a in f } in UN ) by A2, CLASSES1:def_1, YELLOW19:def_4; hence a_net F in NetUniv L by YELLOW_6:def_11; ::_thesis: verum end; theorem Th15: :: WAYBEL33:15 for L being complete LATTICE for F being ultra Filter of (BoolePoset ([#] L)) for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p) proof let L be complete LATTICE; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L)) for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p) let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p) let p be greater_or_equal_to_id Function of (a_net F),(a_net F); ::_thesis: lim_inf F >= inf ((a_net F) * p) set M = (a_net F) * p; set rM = rng the mapping of ((a_net F) * p); set C = the Element of F; A1: inf ((a_net F) * p) = Inf by WAYBEL_9:def_2 .= "/\" ((rng the mapping of ((a_net F) * p)),L) by YELLOW_2:def_6 ; F c= the carrier of (BoolePoset ([#] L)) ; then F c= bool ([#] L) by WAYBEL_7:2; then the Element of F in bool ([#] L) by TARSKI:def_3; then A2: the Element of F \ (rng the mapping of ((a_net F) * p)) c= [#] L by XBOOLE_1:1; then reconsider D = the Element of F \ (rng the mapping of ((a_net F) * p)), A = the Element of F /\ (rng the mapping of ((a_net F) * p)) as Element of (BoolePoset ([#] L)) by WAYBEL_7:2; A3: the carrier of ((a_net F) * p) = the carrier of (a_net F) by WAYBEL28:6; then reconsider g = p as Function of ((a_net F) * p),(a_net F) ; A4: now__::_thesis:_not_D_in_F set d = the Element of D; assume A5: D in F ; ::_thesis: contradiction not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4; then A6: D <> {} by A5, YELLOW_1:18; then A7: the Element of D in D ; reconsider D = D as Element of F by A5; reconsider d = the Element of D as Element of L by A2, A7; [d,D] in { [a,f] where a is Element of L, f is Element of F : a in f } by A6; then reconsider dD = [d,D] as Element of (a_net F) by YELLOW19:def_4; reconsider dD9 = dD as Element of ((a_net F) * p) by WAYBEL28:6; A8: dom p = the carrier of (a_net F) by FUNCT_2:52; ex i being Element of ((a_net F) * p) st for j being Element of ((a_net F) * p) st j >= i holds g . j >= dD proof consider i being Element of ((a_net F) * p) such that A9: i = dD9 ; take i ; ::_thesis: for j being Element of ((a_net F) * p) st j >= i holds g . j >= dD for j being Element of ((a_net F) * p) st j >= i holds g . j >= dD proof reconsider i9 = i as Element of (a_net F) by WAYBEL28:6; let j be Element of ((a_net F) * p); ::_thesis: ( j >= i implies g . j >= dD ) reconsider j9 = j as Element of (a_net F) by WAYBEL28:6; A10: j9 <= g . j by WAYBEL28:def_1; reconsider i9 = i9 as Element of (a_net F) ; reconsider j9 = j9 as Element of (a_net F) ; A11: RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def_2; assume j >= i ; ::_thesis: g . j >= dD then i9 <= j9 by A11, YELLOW_0:1; hence g . j >= dD by A9, A10, YELLOW_0:def_2; ::_thesis: verum end; hence for j being Element of ((a_net F) * p) st j >= i holds g . j >= dD ; ::_thesis: verum end; then consider i being Element of ((a_net F) * p) such that A12: for j being Element of ((a_net F) * p) st j >= i holds g . j >= dD ; RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def_2; then (a_net F) * p is reflexive by WAYBEL_8:12; then i >= i by YELLOW_0:def_1; then A13: g . i >= dD by A12; [d,D] `2 = D ; then A14: (p . i) `2 c= D by A13, YELLOW19:def_4; reconsider G = g . i as Element of (a_net F) ; g . i in the carrier of (a_net F) ; then g . i in { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def_4; then consider a being Element of L, f being Element of F such that A15: g . i = [a,f] and A16: a in f ; ( [a,f] `1 = a & [a,f] `2 = f ) ; then A17: (p . i) `1 in (p . i) `2 by A15, A16; ((a_net F) * p) . i = ( the mapping of (a_net F) * p) . i by WAYBEL28:def_2 .= (a_net F) . G by A3, A8, FUNCT_1:13 .= (p . i) `1 by YELLOW19:def_4 ; then not ((a_net F) * p) . i in rng the mapping of ((a_net F) * p) by A14, A17, XBOOLE_0:def_5; hence contradiction by FUNCT_2:4; ::_thesis: verum end; set Y = { (inf B) where B is Subset of L : B in F } ; reconsider A9 = A as Subset of L ; A18: D "\/" A = D \/ A by YELLOW_1:17 .= the Element of F by XBOOLE_1:51 ; F is prime by WAYBEL_7:22; then A in F by A18, A4, WAYBEL_7:def_2; then inf A9 in { (inf B) where B is Subset of L : B in F } ; then A19: inf A9 <= lim_inf F by YELLOW_0:17, YELLOW_4:1; A c= rng the mapping of ((a_net F) * p) by XBOOLE_1:17; then inf ((a_net F) * p) <= inf A9 by A1, WAYBEL_7:1; hence lim_inf F >= inf ((a_net F) * p) by A19, YELLOW_0:def_2; ::_thesis: verum end; theorem Th16: :: WAYBEL33:16 for L being complete LATTICE for F being ultra Filter of (BoolePoset ([#] L)) for M being subnet of a_net F holds lim_inf F = lim_inf M proof let L be complete LATTICE; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L)) for M being subnet of a_net F holds lim_inf F = lim_inf M let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: for M being subnet of a_net F holds lim_inf F = lim_inf M let M be subnet of a_net F; ::_thesis: lim_inf F = lim_inf M ( lim_inf F = lim_inf (a_net F) & ( for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p) ) ) by Th13, Th15; hence lim_inf F = lim_inf M by WAYBEL28:14; ::_thesis: verum end; theorem Th17: :: WAYBEL33:17 for L being non empty 1-sorted for N being net of L for A being set st N is_often_in A holds ex N9 being strict subnet of N st ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) proof let L be non empty 1-sorted ; ::_thesis: for N being net of L for A being set st N is_often_in A holds ex N9 being strict subnet of N st ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) let N be net of L; ::_thesis: for A being set st N is_often_in A holds ex N9 being strict subnet of N st ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) let A be set ; ::_thesis: ( N is_often_in A implies ex N9 being strict subnet of N st ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) ) assume N is_often_in A ; ::_thesis: ex N9 being strict subnet of N st ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) then reconsider N9 = N " A as strict subnet of N by YELLOW_6:22; take N9 ; ::_thesis: ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) rng the mapping of N9 c= A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of N9 or y in A ) assume y in rng the mapping of N9 ; ::_thesis: y in A then consider x being set such that A1: x in dom the mapping of N9 and A2: y = the mapping of N9 . x by FUNCT_1:def_3; A3: x in dom ( the mapping of N | the carrier of N9) by A1, YELLOW_6:def_6; then x in (dom the mapping of N) /\ the carrier of N9 by RELAT_1:61; then x in the carrier of N9 by XBOOLE_0:def_4; then A4: x in the mapping of N " A by YELLOW_6:def_10; y = ( the mapping of N | the carrier of N9) . x by A2, YELLOW_6:def_6; then y = the mapping of N . x by A3, FUNCT_1:47; hence y in A by A4, FUNCT_1:def_7; ::_thesis: verum end; hence ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) ; ::_thesis: verum end; theorem Th18: :: WAYBEL33:18 for L being complete lim-inf TopLattice for A being non empty Subset of L holds ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A ) proof let L be complete lim-inf TopLattice; ::_thesis: for A being non empty Subset of L holds ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A ) let A be non empty Subset of L; ::_thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A ) xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def_4; then A1: xi 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 lim_inf-Convergence L holds N is_eventually_in V } by YELLOW_6:def_24; set V = A ` ; A2: the topology of L = xi L by Def2; hereby ::_thesis: ( ( for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A ) implies A is closed ) assume A is closed ; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A then A ` in xi L by A2, PRE_TOPC:def_2; then A3: ex V being Subset of L st ( V = A ` & ( for p being Element of L st p in V holds for N being net of L st [N,p] in lim_inf-Convergence L holds N is_eventually_in V ) ) by A1; let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: ( A in F implies lim_inf F in A ) assume A4: A in F ; ::_thesis: lim_inf F in A ( ( for M being subnet of a_net F holds lim_inf F = lim_inf M ) & a_net F in NetUniv L ) by Th14, Th16; then A5: [(a_net F),(lim_inf F)] in lim_inf-Convergence L by WAYBEL28:def_3; assume not lim_inf F in A ; ::_thesis: contradiction then lim_inf F in A ` by XBOOLE_0:def_5; then a_net F is_eventually_in A ` by A3, A5; then consider i being Element of (a_net F) such that A6: for j being Element of (a_net F) st i <= j holds (a_net F) . j in A ` by WAYBEL_0:def_11; A7: the carrier of (a_net F) = { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def_4; i in the carrier of (a_net F) ; then consider a being Element of L, f being Element of F such that A8: i = [a,f] and a in f by A7; reconsider A9 = A, f9 = f as Element of (BoolePoset ([#] L)) by A4; consider B being Element of (BoolePoset ([#] L)) such that A9: B in F and A10: A9 >= B and A11: f9 >= B by A4, WAYBEL_0:def_2; set b = the Element of B; not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4; then not B is empty by A9, YELLOW_1:18; then A12: the Element of B in B ; the carrier of (BoolePoset ([#] L)) = bool the carrier of L by WAYBEL_7:2; then [ the Element of B,B] in the carrier of (a_net F) by A7, A9, A12; then reconsider j = [ the Element of B,B] as Element of (a_net F) ; B c= f by A11, YELLOW_1:2; then j `2 c= f by MCART_1:7; then j `2 c= i `2 by A8, MCART_1:7; then j >= i by YELLOW19:def_4; then (a_net F) . j in A ` by A6; then j `1 in A ` by YELLOW19:def_4; then A13: the Element of B in A ` by MCART_1:7; B c= A by A10, YELLOW_1:2; hence contradiction by A12, A13, XBOOLE_0:def_5; ::_thesis: verum end; assume A14: for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds lim_inf F in A ; ::_thesis: A is closed now__::_thesis:_for_p_being_Element_of_L_st_p_in_A_`_holds_ for_N_being_net_of_L_st_[N,p]_in_lim_inf-Convergence_L_holds_ N_is_eventually_in_A_` let p be Element of L; ::_thesis: ( p in A ` implies for N being net of L st [N,p] in lim_inf-Convergence L holds N is_eventually_in A ` ) assume p in A ` ; ::_thesis: for N being net of L st [N,p] in lim_inf-Convergence L holds N is_eventually_in A ` then A15: not p in (A `) ` by XBOOLE_0:def_5; reconsider x = p as Element of L ; let N be net of L; ::_thesis: ( [N,p] in lim_inf-Convergence L implies N is_eventually_in A ` ) assume A16: [N,p] in lim_inf-Convergence L ; ::_thesis: N is_eventually_in A ` assume not N is_eventually_in A ` ; ::_thesis: contradiction then N is_often_in A by WAYBEL_0:10; then consider N9 being strict subnet of N such that A17: rng the mapping of N9 c= A and A18: N9 is SubNetStr of N by Th17; lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18; then A19: N in NetUniv L by A16, ZFMISC_1:87; then A20: ex N1 being strict net of L st ( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def_11; set j0 = the Element of N9; reconsider rj = rng the mapping of (N9 | the Element of N9), a = A as Element of (BoolePoset ([#] L)) by WAYBEL_7:2; set j2 = the Element of N9; set G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ; set g = rng the mapping of (N9 | the Element of N9); A21: rng the mapping of (N9 | the Element of N9) in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ; for g being set st g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } holds g in the carrier of (BoolePoset ([#] L)) proof let g be set ; ::_thesis: ( g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } implies g in the carrier of (BoolePoset ([#] L)) ) assume g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ; ::_thesis: g in the carrier of (BoolePoset ([#] L)) then ex j3 being Element of N9 st g = rng the mapping of (N9 | j3) ; then g in bool ([#] L) ; hence g in the carrier of (BoolePoset ([#] L)) by WAYBEL_7:2; ::_thesis: verum end; then reconsider G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } as non empty Subset of (BoolePoset ([#] L)) by A21, TARSKI:def_3; A22: G c= fininfs G by WAYBEL_0:50; now__::_thesis:_for_p_being_set_st_p_in_rj_holds_ p_in_rng_the_mapping_of_N9 let p be set ; ::_thesis: ( p in rj implies p in rng the mapping of N9 ) assume p in rj ; ::_thesis: p in rng the mapping of N9 then p in rng ( the mapping of N9 | the carrier of (N9 | the Element of N9)) by WAYBEL_9:def_7; then consider q being set such that A23: q in dom ( the mapping of N9 | the carrier of (N9 | the Element of N9)) and A24: p = ( the mapping of N9 | the carrier of (N9 | the Element of N9)) . q by FUNCT_1:def_3; q in (dom the mapping of N9) /\ the carrier of (N9 | the Element of N9) by A23, RELAT_1:61; then A25: q in dom the mapping of N9 by XBOOLE_0:def_4; p = the mapping of N9 . q by A23, A24, FUNCT_1:47; hence p in rng the mapping of N9 by A25, FUNCT_1:3; ::_thesis: verum end; then rj c= rng the mapping of N9 by TARSKI:def_3; then rj c= a by A17, XBOOLE_1:1; then ( rng the mapping of (N9 | the Element of N9) in G & rj <= a ) by YELLOW_1:2; then A26: a in uparrow (fininfs G) by A22, WAYBEL_0:def_16; A27: x = lim_inf N9 by A16, A19, WAYBEL28:def_3; then A28: x = "\/" ( { (inf (N9 | j)) where j is Element of N9 : verum } ,L) by Th11; the carrier of N9 c= the carrier of N by A18, YELLOW_6:10; then the carrier of N9 in the_universe_of the carrier of L by A20, CLASSES1:def_1; then A29: N9 in NetUniv L by YELLOW_6:def_11; A30: not {} in fininfs G proof assume {} in fininfs G ; ::_thesis: contradiction then consider Y being finite Subset of G such that A31: {} = "/\" (Y,(BoolePoset ([#] L))) and ex_inf_of Y, BoolePoset ([#] L) ; defpred S1[ set , set ] means ex j being Element of N9 st ( j = $2 & $1 = rng the mapping of (N9 | j) ); A32: "/\" ({},(BoolePoset ([#] L))) = Top (BoolePoset ([#] L)) by YELLOW_0:def_12 .= [#] L by YELLOW_1:19 ; reconsider Y = Y as finite Subset of (BoolePoset ([#] L)) by XBOOLE_1:1; A33: for x being set st x in Y holds ex y being set st ( y in the carrier of N9 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in Y implies ex y being set st ( y in the carrier of N9 & S1[x,y] ) ) assume x in Y ; ::_thesis: ex y being set st ( y in the carrier of N9 & S1[x,y] ) then x in G ; then A34: ex j being Element of N9 st x = rng the mapping of (N9 | j) ; assume for y being set st y in the carrier of N9 holds not S1[x,y] ; ::_thesis: contradiction hence contradiction by A34; ::_thesis: verum end; consider f being Function such that A35: ( dom f = Y & rng f c= the carrier of N9 ) and A36: for x being set st x in Y holds S1[x,f . x] from FUNCT_1:sch_5(A33); reconsider C = rng f as finite Subset of ([#] N9) by A35, FINSET_1:8; [#] N9 is directed by WAYBEL_0:def_6; then consider j0 being Element of N9 such that j0 in [#] N9 and A37: j0 is_>=_than C by WAYBEL_0:1; for y being set st y in Y holds rng the mapping of (N9 | j0) c= y proof let y be set ; ::_thesis: ( y in Y implies rng the mapping of (N9 | j0) c= y ) assume A38: y in Y ; ::_thesis: rng the mapping of (N9 | j0) c= y consider j1 being Element of N9 such that A39: j1 = f . y and A40: y = rng the mapping of (N9 | j1) by A36, A38; A41: f . y in rng f by A35, A38, FUNCT_1:3; then reconsider f1 = f . y as Element of N9 by A35; A42: f1 <= j0 by A37, A41, LATTICE3:def_9; for p being set st p in rng the mapping of (N9 | j0) holds p in y proof let p be set ; ::_thesis: ( p in rng the mapping of (N9 | j0) implies p in y ) assume p in rng the mapping of (N9 | j0) ; ::_thesis: p in y then p in rng ( the mapping of N9 | the carrier of (N9 | j0)) by WAYBEL_9:def_7; then consider q being set such that A43: q in dom ( the mapping of N9 | the carrier of (N9 | j0)) and A44: p = ( the mapping of N9 | the carrier of (N9 | j0)) . q by FUNCT_1:def_3; A45: q in (dom the mapping of N9) /\ the carrier of (N9 | j0) by A43, RELAT_1:61; then q in the carrier of (N9 | j0) by XBOOLE_0:def_4; then q in { n9 where n9 is Element of N9 : j0 <= n9 } by WAYBEL_9:12; then consider n9 being Element of N9 such that A46: q = n9 and A47: j0 <= n9 ; f1 <= n9 by A42, A47, YELLOW_0:def_2; then q in { m9 where m9 is Element of N9 : j1 <= m9 } by A39, A46; then A48: q in the carrier of (N9 | j1) by WAYBEL_9:12; q in dom the mapping of N9 by A45, XBOOLE_0:def_4; then q in (dom the mapping of N9) /\ the carrier of (N9 | j1) by A48, XBOOLE_0:def_4; then A49: q in dom ( the mapping of N9 | the carrier of (N9 | j1)) by RELAT_1:61; p = the mapping of N9 . q by A43, A44, FUNCT_1:47; then p = ( the mapping of N9 | the carrier of (N9 | j1)) . q by A49, FUNCT_1:47; then p in rng ( the mapping of N9 | the carrier of (N9 | j1)) by A49, FUNCT_1:3; hence p in y by A40, WAYBEL_9:def_7; ::_thesis: verum end; hence rng the mapping of (N9 | j0) c= y by TARSKI:def_3; ::_thesis: verum end; then rng the mapping of (N9 | j0) c= meet Y by A31, A32, SETFAM_1:5; then rng the mapping of (N9 | j0) c= {} by A31, A32, YELLOW_1:20; hence contradiction ; ::_thesis: verum end; for y being Element of (BoolePoset ([#] L)) st Bottom (BoolePoset ([#] L)) >= y holds not y in fininfs G proof let y be Element of (BoolePoset ([#] L)); ::_thesis: ( Bottom (BoolePoset ([#] L)) >= y implies not y in fininfs G ) assume Bottom (BoolePoset ([#] L)) >= y ; ::_thesis: not y in fininfs G then ( {} = Bottom (BoolePoset ([#] L)) & y c= Bottom (BoolePoset ([#] L)) ) by YELLOW_1:2, YELLOW_1:18; hence not y in fininfs G by A30; ::_thesis: verum end; then not Bottom (BoolePoset ([#] L)) in uparrow (fininfs G) by WAYBEL_0:def_16; then uparrow (fininfs G) is proper by WAYBEL_7:4; then consider F being Filter of (BoolePoset ([#] L)) such that A50: uparrow (fininfs G) c= F and A51: F is ultra by WAYBEL_7:26; A52: fininfs G c= uparrow (fininfs G) by WAYBEL_0:16; A53: { (inf (N9 | j)) where j is Element of N9 : verum } c= { (inf f) where f is Subset of L : f in F } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (inf (N9 | j)) where j is Element of N9 : verum } or x in { (inf f) where f is Subset of L : f in F } ) assume x in { (inf (N9 | j)) where j is Element of N9 : verum } ; ::_thesis: x in { (inf f) where f is Subset of L : f in F } then consider j3 being Element of N9 such that A54: x = inf (N9 | j3) ; reconsider f1 = rng the mapping of (N9 | j3) as Subset of L ; fininfs G c= F by A50, A52, XBOOLE_1:1; then A55: ( f1 in G & G c= F ) by A22, XBOOLE_1:1; x = Inf by A54, WAYBEL_9:def_2 .= "/\" ((rng the mapping of (N9 | j3)),L) by YELLOW_2:def_6 ; hence x in { (inf f) where f is Subset of L : f in F } by A55; ::_thesis: verum end; now__::_thesis:_for_M_being_subnet_of_N9_holds_x_=_lim_inf_M let M be subnet of N9; ::_thesis: x = lim_inf M M is subnet of N by YELLOW_6:15; hence x = lim_inf M by A16, A19, WAYBEL28:def_3; ::_thesis: verum end; then A56: for M being subnet of N9 st M in NetUniv L holds x = lim_inf M ; { (inf f) where f is Subset of L : f in F } is_<=_than x proof let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in { (inf f) where f is Subset of L : f in F } or y <= x ) assume y in { (inf f) where f is Subset of L : f in F } ; ::_thesis: y <= x then consider f0 being Subset of L such that A57: y = inf f0 and A58: f0 in F ; defpred S1[ Element of N9, Element of N9] means ( $1 <= $2 & N9 . $2 in f0 ); A59: now__::_thesis:_for_j_being_Element_of_N9_ex_pj_being_Element_of_N9_st_S1[j,pj] let j be Element of N9; ::_thesis: ex pj being Element of N9 st S1[j,pj] not Bottom (BoolePoset ([#] L)) in F by A51, WAYBEL_7:4; then A60: not {} in F by YELLOW_1:18; G c= uparrow (fininfs G) by A22, A52, XBOOLE_1:1; then A61: G c= F by A50, XBOOLE_1:1; rng the mapping of (N9 | j) in G ; then f0 /\ (rng the mapping of (N9 | j)) in F by A58, A61, WAYBEL_7:9; then consider nj being Element of L such that A62: nj in f0 /\ (rng the mapping of (N9 | j)) by A60, SUBSET_1:4; nj in rng the mapping of (N9 | j) by A62, XBOOLE_0:def_4; then consider pj9 being set such that A63: pj9 in dom the mapping of (N9 | j) and A64: nj = the mapping of (N9 | j) . pj9 by FUNCT_1:def_3; pj9 in the carrier of (N9 | j) by A63; then pj9 in { y9 where y9 is Element of N9 : j <= y9 } by WAYBEL_9:12; then consider pj being Element of N9 such that A65: pj = pj9 and A66: j <= pj ; reconsider pj9 = pj9 as Element of (N9 | j) by A63; take pj = pj; ::_thesis: S1[j,pj] N9 . pj = (N9 | j) . pj9 by A65, WAYBEL_9:16 .= the mapping of (N9 | j) . pj9 ; hence S1[j,pj] by A62, A64, A66, XBOOLE_0:def_4; ::_thesis: verum end; consider p being Function of N9,N9 such that A67: for j being Element of N9 holds S1[j,p . j] from FUNCT_2:sch_3(A59); for b being set st b in rng the mapping of (N9 * p) holds b in f0 proof let b be set ; ::_thesis: ( b in rng the mapping of (N9 * p) implies b in f0 ) assume b in rng the mapping of (N9 * p) ; ::_thesis: b in f0 then b in { ((N9 * p) . k) where k is Element of (N9 * p) : verum } by WAYBEL11:19; then consider k being Element of (N9 * p) such that A68: b = (N9 * p) . k ; reconsider l = k as Element of N9 by WAYBEL28:6; the carrier of (N9 * p) = the carrier of N9 by WAYBEL28:6; then k in the carrier of N9 ; then A69: k in dom p by FUNCT_2:52; (N9 * p) . k = ( the mapping of N9 * p) . k by WAYBEL28:def_2 .= N9 . (p . l) by A69, FUNCT_1:13 ; hence b in f0 by A67, A68; ::_thesis: verum end; then rng the mapping of (N9 * p) c= f0 by TARSKI:def_3; then A70: "/\" (f0,L) <= "/\" ((rng the mapping of (N9 * p)),L) by WAYBEL_7:1; A71: for M being subnet of N9 st M in NetUniv L holds x >= inf M by A29, A56, WAYBEL28:3; p is greater_or_equal_to_id by A67, WAYBEL28:def_1; then A72: inf (N9 * p) <= x by A29, A27, A71, WAYBEL28:13; inf (N9 * p) = Inf by WAYBEL_9:def_2 .= "/\" ((rng the mapping of (N9 * p)),L) by YELLOW_2:def_6 ; hence y <= x by A57, A72, A70, YELLOW_0:def_2; ::_thesis: verum end; then A73: lim_inf F <= x by YELLOW_0:32; ( ex_sup_of { (inf f) where f is Subset of L : f in F } ,L & ex_sup_of { (inf (N9 | j)) where j is Element of N9 : verum } ,L ) by YELLOW_0:17; then x <= lim_inf F by A28, A53, YELLOW_0:34; then x = lim_inf F by A73, YELLOW_0:def_3; hence contradiction by A14, A50, A51, A26, A15; ::_thesis: verum end; then A ` in xi L by A1; then A ` is open by A2, PRE_TOPC:def_2; hence A is closed by WAYBEL12:def_1; ::_thesis: verum end; theorem Th19: :: WAYBEL33:19 for L being non empty reflexive RelStr holds sigma L c= xi L proof let L be non empty reflexive RelStr ; ::_thesis: sigma L c= xi L let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sigma L or x in xi L ) assume x in sigma L ; ::_thesis: x in xi L hence x in xi L by WAYBEL28:28; ::_thesis: verum end; theorem Th20: :: WAYBEL33:20 for T1, T2 being non empty TopSpace for B being prebasis of T1 st B c= the topology of T2 & the carrier of T1 in the topology of T2 holds the topology of T1 c= the topology of T2 proof let T1, T2 be non empty TopSpace; ::_thesis: for B being prebasis of T1 st B c= the topology of T2 & the carrier of T1 in the topology of T2 holds the topology of T1 c= the topology of T2 let B be prebasis of T1; ::_thesis: ( B c= the topology of T2 & the carrier of T1 in the topology of T2 implies the topology of T1 c= the topology of T2 ) assume that A1: B c= the topology of T2 and A2: the carrier of T1 in the topology of T2 ; ::_thesis: the topology of T1 c= the topology of T2 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T1 or x in the topology of T2 ) FinMeetCl B is Basis of T1 by YELLOW_9:23; then A3: the topology of T1 = UniCl (FinMeetCl B) by YELLOW_9:22; assume x in the topology of T1 ; ::_thesis: x in the topology of T2 then consider Y being Subset-Family of T1 such that A4: Y c= FinMeetCl B and A5: x = union Y by A3, CANTOR_1:def_1; A6: Y c= the topology of T2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in the topology of T2 ) assume y in Y ; ::_thesis: y in the topology of T2 then consider Z being Subset-Family of T1 such that A7: Z c= B and A8: Z is finite and A9: y = Intersect Z by A4, CANTOR_1:def_3; Z c= the topology of T2 by A1, A7, XBOOLE_1:1; then reconsider Z9 = Z as Subset-Family of T2 by XBOOLE_1:1; ( y = the carrier of T1 or ( Z9 c= the topology of T2 & y = meet Z9 & meet Z9 = Intersect Z9 ) ) by A1, A7, A9, SETFAM_1:def_9, XBOOLE_1:1; then ( y = the carrier of T1 or y in FinMeetCl the topology of T2 ) by A8, CANTOR_1:def_3; hence y in the topology of T2 by A2, CANTOR_1:5; ::_thesis: verum end; then reconsider Y = Y as Subset-Family of T2 by XBOOLE_1:1; union Y in UniCl the topology of T2 by A6, CANTOR_1:def_1; hence x in the topology of T2 by A5, CANTOR_1:6; ::_thesis: verum end; theorem Th21: :: WAYBEL33:21 for L being complete LATTICE holds omega L c= xi L proof let L be complete LATTICE; ::_thesis: omega L c= xi L set S = the correct lower TopAugmentation of L; set X = the lim-inf TopAugmentation of L; reconsider B = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of L : verum } as prebasis of the correct lower TopAugmentation of L by WAYBEL19:def_1; A1: ( RelStr(# the carrier of the correct lower TopAugmentation of L, the InternalRel of the correct lower TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of the lim-inf TopAugmentation of L, the InternalRel of the lim-inf TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4; A2: B c= the topology of the lim-inf TopAugmentation of L proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in B or b in the topology of the lim-inf TopAugmentation of L ) assume b in B ; ::_thesis: b in the topology of the lim-inf TopAugmentation of L then consider x being Element of the correct lower TopAugmentation of L such that A3: b = (uparrow x) ` ; reconsider y = x as Element of the lim-inf TopAugmentation of L by A1; set A = uparrow y; the lim-inf TopAugmentation of L is SubRelStr of the lim-inf TopAugmentation of L by YELLOW_6:6; then the correct lower TopAugmentation of L is SubRelStr of the lim-inf TopAugmentation of L by A1, WAYBEL21:12; then A4: uparrow x c= uparrow y by WAYBEL23:14; A5: inf (uparrow y) = y by WAYBEL_0:39; now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_([#]_the_lim-inf_TopAugmentation_of_L))_st_uparrow_y_in_F_holds_ lim_inf_F_in_uparrow_y let F be ultra Filter of (BoolePoset ([#] the lim-inf TopAugmentation of L)); ::_thesis: ( uparrow y in F implies lim_inf F in uparrow y ) assume uparrow y in F ; ::_thesis: lim_inf F in uparrow y then inf (uparrow y) in { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } ; then inf (uparrow y) <= "\/" ( { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } , the lim-inf TopAugmentation of L) by YELLOW_2:22; hence lim_inf F in uparrow y by A5, WAYBEL_0:18; ::_thesis: verum end; then A6: uparrow y is closed by Th18; the correct lower TopAugmentation of L is SubRelStr of the correct lower TopAugmentation of L by YELLOW_6:6; then the lim-inf TopAugmentation of L is SubRelStr of the correct lower TopAugmentation of L by A1, WAYBEL21:12; then uparrow y c= uparrow x by WAYBEL23:14; then uparrow y = uparrow x by A4, XBOOLE_0:def_10; hence b in the topology of the lim-inf TopAugmentation of L by A1, A3, A6, PRE_TOPC:def_2; ::_thesis: verum end; the carrier of the correct lower TopAugmentation of L in the topology of the lim-inf TopAugmentation of L by A1, PRE_TOPC:def_1; then the topology of the correct lower TopAugmentation of L c= the topology of the lim-inf TopAugmentation of L by A2, Th20; then omega L c= the topology of the lim-inf TopAugmentation of L by WAYBEL19:def_2; hence omega L c= xi L by Th10; ::_thesis: verum end; theorem Th22: :: WAYBEL33:22 for T1, T2 being TopSpace for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds for R being Refinement of T1,T2 holds T is TopExtension of R proof let T1, T2 be TopSpace; ::_thesis: for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds for R being Refinement of T1,T2 holds T is TopExtension of R let T be non empty TopSpace; ::_thesis: ( T is TopExtension of T1 & T is TopExtension of T2 implies for R being Refinement of T1,T2 holds T is TopExtension of R ) assume that A1: the carrier of T1 = the carrier of T and A2: the topology of T1 c= the topology of T and A3: the carrier of T2 = the carrier of T and A4: the topology of T2 c= the topology of T ; :: according to YELLOW_9:def_5 ::_thesis: for R being Refinement of T1,T2 holds T is TopExtension of R let R be Refinement of T1,T2; ::_thesis: T is TopExtension of R A5: the carrier of R = the carrier of T \/ the carrier of T by A1, A3, YELLOW_9:def_6; hence the carrier of R = the carrier of T ; :: according to YELLOW_9:def_5 ::_thesis: the topology of R c= the topology of T reconsider S = the topology of T1 \/ the topology of T2 as prebasis of R by YELLOW_9:def_6; FinMeetCl S is Basis of R by YELLOW_9:23; then A6: UniCl (FinMeetCl S) = the topology of R by YELLOW_9:22; S c= the topology of T by A2, A4, XBOOLE_1:8; then FinMeetCl S c= FinMeetCl the topology of T by A5, CANTOR_1:14; then the topology of R c= UniCl (FinMeetCl the topology of T) by A5, A6, CANTOR_1:9; hence the topology of R c= the topology of T by CANTOR_1:7; ::_thesis: verum end; theorem Th23: :: WAYBEL33:23 for T1 being TopSpace for T2 being TopExtension of T1 for A being Subset of T1 holds ( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) ) proof let T1 be TopSpace; ::_thesis: for T2 being TopExtension of T1 for A being Subset of T1 holds ( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) ) let T2 be TopExtension of T1; ::_thesis: for A being Subset of T1 holds ( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) ) let A be Subset of T1; ::_thesis: ( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) ) A1: the carrier of T1 = the carrier of T2 by YELLOW_9:def_5; reconsider B = A as Subset of T2 by YELLOW_9:def_5; reconsider C = ([#] T2) \ B as Subset of T2 ; A2: the topology of T1 c= the topology of T2 by YELLOW_9:def_5; thus ( A is open implies A is open Subset of T2 ) ::_thesis: ( A is closed implies A is closed Subset of T2 ) proof assume A in the topology of T1 ; :: according to PRE_TOPC:def_2 ::_thesis: A is open Subset of T2 then A in the topology of T2 by A2; hence A is open Subset of T2 by PRE_TOPC:def_2; ::_thesis: verum end; assume ([#] T1) \ A in the topology of T1 ; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: A is closed Subset of T2 then C is open by A2, A1, PRE_TOPC:def_2; hence A is closed Subset of T2 by PRE_TOPC:def_3; ::_thesis: verum end; theorem Th24: :: WAYBEL33:24 for L being complete LATTICE holds lambda L c= xi L proof let L be complete LATTICE; ::_thesis: lambda L c= xi L set T = the correct Lawson TopAugmentation of L; set S = the Scott TopAugmentation of L; set LL = the correct lower TopAugmentation of L; set LI = the lim-inf TopAugmentation of L; A1: RelStr(# the carrier of the lim-inf TopAugmentation of L, the InternalRel of the lim-inf TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; A2: xi L = the topology of the lim-inf TopAugmentation of L by Th10; omega L = the topology of the correct lower TopAugmentation of L by WAYBEL19:def_2; then ( RelStr(# the carrier of the correct lower TopAugmentation of L, the InternalRel of the correct lower TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) & the topology of the correct lower TopAugmentation of L c= xi L ) by Th21, YELLOW_9:def_4; then A3: the lim-inf TopAugmentation of L is TopExtension of the correct lower TopAugmentation of L by A2, A1, YELLOW_9:def_5; sigma L = the topology of the Scott TopAugmentation of L by YELLOW_9:51; then ( RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) & the topology of the Scott TopAugmentation of L c= xi L ) by Th19, YELLOW_9:def_4; then ( the correct Lawson TopAugmentation of L is Refinement of the Scott TopAugmentation of L, the correct lower TopAugmentation of L & the lim-inf TopAugmentation of L is TopExtension of the Scott TopAugmentation of L ) by A2, A1, WAYBEL19:29, YELLOW_9:def_5; then ( lambda L = the topology of the correct Lawson TopAugmentation of L & the lim-inf TopAugmentation of L is TopExtension of the correct Lawson TopAugmentation of L ) by A3, Th22, WAYBEL19:def_4; hence lambda L c= xi L by A2, YELLOW_9:def_5; ::_thesis: verum end; theorem Th25: :: WAYBEL33:25 for L being complete LATTICE for T being lim-inf TopAugmentation of L for S being correct Lawson TopAugmentation of L holds T is TopExtension of S proof let L be complete LATTICE; ::_thesis: for T being lim-inf TopAugmentation of L for S being correct Lawson TopAugmentation of L holds T is TopExtension of S let T be lim-inf TopAugmentation of L; ::_thesis: for S being correct Lawson TopAugmentation of L holds T is TopExtension of S let S be correct Lawson TopAugmentation of L; ::_thesis: T is TopExtension of S ( lambda L = the topology of S & xi L = the topology of T ) by Th10, WAYBEL19:def_4; then A1: the topology of S c= the topology of T by Th24; ( RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4; hence T is TopExtension of S by A1, YELLOW_9:def_5; ::_thesis: verum end; theorem Th26: :: WAYBEL33:26 for L being complete lim-inf TopLattice for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L proof let L be complete lim-inf TopLattice; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: lim_inf F is_a_convergence_point_of F,L set x = lim_inf F; let A be Subset of L; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not lim_inf F in A or A in F ) assume that A1: A is open and A2: lim_inf F in A and A3: not A in F ; ::_thesis: contradiction F is prime by WAYBEL_7:22; then A4: ([#] L) \ A in F by A3, WAYBEL_7:21; then A ` <> {} by YELLOW19:1; then lim_inf F in A ` by A1, A4, Th18; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: WAYBEL33:27 for L being complete lim-inf TopLattice holds ( L is compact & L is T_1 ) proof let L be complete lim-inf TopLattice; ::_thesis: ( L is compact & L is T_1 ) set T = the correct Lawson TopAugmentation of L; now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_([#]_L))_ex_x_being_Point_of_L_st_x_is_a_convergence_point_of_F,L let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: ex x being Point of L st x is_a_convergence_point_of F,L reconsider x = lim_inf F as Point of L ; take x = x; ::_thesis: x is_a_convergence_point_of F,L thus x is_a_convergence_point_of F,L by Th26; ::_thesis: verum end; hence L is compact by YELLOW19:31; ::_thesis: L is T_1 now__::_thesis:_for_x_being_Point_of_L_holds_Cl_{x}_=_{x} let x be Point of L; ::_thesis: Cl {x} = {x} reconsider y = x as Element of L ; RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of the correct Lawson TopAugmentation of L, the InternalRel of the correct Lawson TopAugmentation of L #) by YELLOW_9:def_4; then reconsider z = y as Element of the correct Lawson TopAugmentation of L ; L is TopAugmentation of L by YELLOW_9:44; then A1: L is TopExtension of the correct Lawson TopAugmentation of L by Th25; {z} is closed ; then {y} is closed by A1, Th23; hence Cl {x} = {x} by PRE_TOPC:22; ::_thesis: verum end; hence L is T_1 by FRECHET2:43; ::_thesis: verum end;