:: WAYBEL19 semantic presentation begin definition let T be non empty TopRelStr ; attrT is lower means :Def1: :: WAYBEL19:def 1 { ((uparrow x) `) where x is Element of T : verum } is prebasis of T; end; :: deftheorem Def1 defines lower WAYBEL19:def_1_:_ for T being non empty TopRelStr holds ( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T ); Lm1: now__::_thesis:_for_LL,_T_being_non_empty_RelStr_st_RelStr(#_the_carrier_of_LL,_the_InternalRel_of_LL_#)_=_RelStr(#_the_carrier_of_T,_the_InternalRel_of_T_#)_holds_ {__((uparrow_x)_`)_where_x_is_Element_of_LL_:_verum__}__=__{__((uparrow_x)_`)_where_x_is_Element_of_T_:_verum__}_ let LL, T be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) implies { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } ) assume A1: RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } set BB = { ((uparrow x) `) where x is Element of T : verum } ; set A = { ((uparrow x) `) where x is Element of LL : verum } ; thus { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } ::_thesis: verum proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { ((uparrow x) `) where x is Element of T : verum } c= { ((uparrow x) `) where x is Element of LL : verum } let a be set ; ::_thesis: ( a in { ((uparrow x) `) where x is Element of LL : verum } implies a in { ((uparrow x) `) where x is Element of T : verum } ) assume a in { ((uparrow x) `) where x is Element of LL : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of T : verum } then consider x being Element of LL such that A2: a = (uparrow x) ` ; reconsider y = x as Element of T by A1; a = (uparrow y) ` by A1, A2, WAYBEL_0:13; hence a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in { ((uparrow x) `) where x is Element of LL : verum } ) assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of LL : verum } then consider x being Element of T such that A3: a = (uparrow x) ` ; reconsider y = x as Element of LL by A1; a = (uparrow y) ` by A1, A3, WAYBEL_0:13; hence a in { ((uparrow x) `) where x is Element of LL : verum } ; ::_thesis: verum end; end; registration cluster1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive lower for TopRelStr ; coherence for b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 is lower proof let T be 1 -element TopSpace-like reflexive TopRelStr ; ::_thesis: T is lower set BB = { ((uparrow x) `) where x is Element of T : verum } ; reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10; { ((uparrow x) `) where x is Element of T : verum } c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in bool the carrier of T ) assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in bool the carrier of T then ex x being Element of T st a = (uparrow x) ` ; hence a in bool the carrier of T ; ::_thesis: verum end; then reconsider C = { ((uparrow x) `) where x is Element of T : verum } as Subset-Family of T ; reconsider C = C as Subset-Family of T ; { ((uparrow x) `) where x is Element of T : verum } = {{}} proof set x = the Element of T; thus { ((uparrow x) `) where x is Element of T : verum } c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= { ((uparrow x) `) where x is Element of T : verum } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in {{}} ) assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in {{}} then consider x being Element of T such that A1: a = (uparrow x) ` ; x <= x ; then A2: x in uparrow x by WAYBEL_0:18; the carrier of T = {x} by YELLOW_9:9; then ( a = {} or ( a = the carrier of T & not x in a ) ) by A2, A1, XBOOLE_0:def_5, ZFMISC_1:33; hence a in {{}} by TARSKI:def_1; ::_thesis: verum end; the Element of T <= the Element of T ; then A3: the Element of T in uparrow the Element of T by WAYBEL_0:18; the carrier of T = { the Element of T} by YELLOW_9:9; then ( (uparrow the Element of T) ` = {} or ( (uparrow the Element of T) ` = the carrier of T & not the Element of T in (uparrow the Element of T) ` ) ) by A3, XBOOLE_0:def_5, ZFMISC_1:33; then {} in { ((uparrow x) `) where x is Element of T : verum } ; hence {{}} c= { ((uparrow x) `) where x is Element of T : verum } by ZFMISC_1:31; ::_thesis: verum end; then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11; then A4: F c= FinMeetCl C by ZFMISC_1:7; { ((uparrow x) `) where x is Element of T : verum } c= the topology of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in the topology of T ) assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in the topology of T then consider x being Element of T such that A5: a = (uparrow x) ` ; a c= {} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in {} ) x <= x ; then A6: x in uparrow x by WAYBEL_0:18; A7: uparrow x misses a by A5, XBOOLE_1:79; assume A8: y in a ; ::_thesis: y in {} then y = x by A5, STRUCT_0:def_10; then x in (uparrow x) /\ a by A6, A8, XBOOLE_0:def_4; hence y in {} by A7, XBOOLE_0:def_7; ::_thesis: verum end; then a = {} ; hence a in the topology of T by PRE_TOPC:1; ::_thesis: verum end; hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A4, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL19:def_1 ::_thesis: verum end; end; registration cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict non void lower for TopRelStr ; existence ex b1 being TopLattice st ( b1 is lower & b1 is trivial & b1 is complete & b1 is strict ) proof set T = the 1 -element complete strict TopLattice; take the 1 -element complete strict TopLattice ; ::_thesis: ( the 1 -element complete strict TopLattice is lower & the 1 -element complete strict TopLattice is trivial & the 1 -element complete strict TopLattice is complete & the 1 -element complete strict TopLattice is strict ) thus ( the 1 -element complete strict TopLattice is lower & the 1 -element complete strict TopLattice is trivial & the 1 -element complete strict TopLattice is complete & the 1 -element complete strict TopLattice is strict ) ; ::_thesis: verum end; end; theorem Th1: :: WAYBEL19:1 for LL being non empty RelStr ex T being correct strict TopAugmentation of LL st T is lower proof let LL be non empty RelStr ; ::_thesis: ex T being correct strict TopAugmentation of LL st T is lower set A = { ((uparrow x) `) where x is Element of LL : verum } ; { ((uparrow x) `) where x is Element of LL : verum } c= bool the carrier of LL proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of LL : verum } or a in bool the carrier of LL ) assume a in { ((uparrow x) `) where x is Element of LL : verum } ; ::_thesis: a in bool the carrier of LL then ex x being Element of LL st a = (uparrow x) ` ; hence a in bool the carrier of LL ; ::_thesis: verum end; then reconsider A = { ((uparrow x) `) where x is Element of LL : verum } as Subset-Family of LL ; set T = TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); reconsider S = TopStruct(# the carrier of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace by CANTOR_1:15; A1: TopStruct(# the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #), the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) #) = S ; TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) is TopSpace-like proof thus the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) by A1, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #)) holds ( not b1 c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) holds ( not b1 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) ) ) hereby ::_thesis: for b1, b2 being Element of bool the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) holds ( not b1 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) let a be Subset-Family of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); ::_thesis: ( a c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) reconsider b = a as Subset-Family of S ; assume a c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) then union b in the topology of S by PRE_TOPC:def_1; hence union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum end; let a, b be Subset of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); ::_thesis: ( not a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) assume that A2: a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) and A3: b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) a /\ b in the topology of S by A2, A3, PRE_TOPC:def_1; hence a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum end; then reconsider T = TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace-like strict TopRelStr ; take T ; ::_thesis: ( T is correct strict TopAugmentation of LL & T is lower ) set BB = { ((uparrow x) `) where x is Element of T : verum } ; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of LL, the InternalRel of LL #) ; hence T is correct strict TopAugmentation of LL by YELLOW_9:def_4; ::_thesis: T is lower A4: A is prebasis of S by CANTOR_1:18; then consider F being Basis of S such that A5: F c= FinMeetCl A by CANTOR_1:def_4; A6: the topology of T c= UniCl F by CANTOR_1:def_2; F c= the topology of T by TOPS_2:64; then A7: F is Basis of T by A6, CANTOR_1:def_2, TOPS_2:64; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of LL, the InternalRel of LL #) ; then A8: A = { ((uparrow x) `) where x is Element of T : verum } by Lm1; A c= the topology of S by A4, TOPS_2:64; hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A7, A5, A8, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL19:def_1 ::_thesis: verum end; registration let R be non empty RelStr ; cluster non empty correct strict lower for TopAugmentation of R; existence ex b1 being correct strict TopAugmentation of R st b1 is lower by Th1; end; theorem Th2: :: WAYBEL19:2 for L1, L2 being non empty TopSpace-like lower TopRelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds the topology of L1 = the topology of L2 proof let L1, L2 be non empty TopSpace-like lower TopRelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies the topology of L1 = the topology of 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 L1 = the topology of L2 set B2 = { ((uparrow x) `) where x is Element of L2 : verum } ; set B1 = { ((uparrow x) `) where x is Element of L1 : verum } ; A2: { ((uparrow x) `) where x is Element of L1 : verum } is prebasis of L1 by Def1; A3: { ((uparrow x) `) where x is Element of L2 : verum } is prebasis of L2 by Def1; { ((uparrow x) `) where x is Element of L1 : verum } = { ((uparrow x) `) where x is Element of L2 : verum } by A1, Lm1; hence the topology of L1 = the topology of L2 by A1, A2, A3, YELLOW_9:26; ::_thesis: verum end; definition let R be non empty RelStr ; func omega R -> Subset-Family of R means :Def2: :: WAYBEL19:def 2 for T being correct lower TopAugmentation of R holds it = the topology of T; uniqueness for b1, b2 being Subset-Family of R st ( for T being correct lower TopAugmentation of R holds b1 = the topology of T ) & ( for T being correct lower TopAugmentation of R holds b2 = the topology of T ) holds b1 = b2 proof set T = the correct lower TopAugmentation of R; let X1, X2 be Subset-Family of R; ::_thesis: ( ( for T being correct lower TopAugmentation of R holds X1 = the topology of T ) & ( for T being correct lower TopAugmentation of R holds X2 = the topology of T ) implies X1 = X2 ) assume for T being correct lower TopAugmentation of R holds X1 = the topology of T ; ::_thesis: ( ex T being correct lower TopAugmentation of R st not X2 = the topology of T or X1 = X2 ) then X1 = the topology of the correct lower TopAugmentation of R ; hence ( ex T being correct lower TopAugmentation of R st not X2 = the topology of T or X1 = X2 ) ; ::_thesis: verum end; existence ex b1 being Subset-Family of R st for T being correct lower TopAugmentation of R holds b1 = the topology of T proof set S = the correct lower TopAugmentation of R; A1: RelStr(# the carrier of the correct lower TopAugmentation of R, the InternalRel of the correct lower TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then reconsider X = the topology of the correct lower TopAugmentation of R as Subset-Family of R ; take X ; ::_thesis: for T being correct lower TopAugmentation of R holds X = the topology of T let T be correct lower TopAugmentation of R; ::_thesis: X = the topology of T RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; hence X = the topology of T by A1, Th2; ::_thesis: verum end; end; :: deftheorem Def2 defines omega WAYBEL19:def_2_:_ for R being non empty RelStr for b2 being Subset-Family of R holds ( b2 = omega R iff for T being correct lower TopAugmentation of R holds b2 = the topology of T ); theorem Th3: :: WAYBEL19:3 for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds omega R1 = omega R2 proof let R1, R2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies omega R1 = omega R2 ) assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: omega R1 = omega R2 set S = the correct lower TopAugmentation of R1; RelStr(# the carrier of the correct lower TopAugmentation of R1, the InternalRel of the correct lower TopAugmentation of R1 #) = RelStr(# the carrier of R1, the InternalRel of R1 #) by YELLOW_9:def_4; then A2: the correct lower TopAugmentation of R1 is TopAugmentation of R2 by A1, YELLOW_9:def_4; omega R1 = the topology of the correct lower TopAugmentation of R1 by Def2; hence omega R1 = omega R2 by A2, Def2; ::_thesis: verum end; theorem Th4: :: WAYBEL19:4 for T being non empty lower TopRelStr for x being Point of T holds ( (uparrow x) ` is open & uparrow x is closed ) proof let T be non empty lower TopRelStr ; ::_thesis: for x being Point of T holds ( (uparrow x) ` is open & uparrow x is closed ) set BB = { ((uparrow x) `) where x is Element of T : verum } ; let x be Point of T; ::_thesis: ( (uparrow x) ` is open & uparrow x is closed ) reconsider a = x as Element of T ; { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by Def1; then A1: { ((uparrow x) `) where x is Element of T : verum } c= the topology of T by TOPS_2:64; A2: (uparrow a) ` in { ((uparrow x) `) where x is Element of T : verum } ; hence (uparrow x) ` in the topology of T by A1; :: according to PRE_TOPC:def_2 ::_thesis: uparrow x is closed thus ([#] T) \ (uparrow x) in the topology of T by A2, A1; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum end; theorem Th5: :: WAYBEL19:5 for T being non empty transitive lower TopRelStr for A being Subset of T st A is open holds A is lower proof let T be non empty transitive lower TopRelStr ; ::_thesis: for A being Subset of T st A is open holds A is lower reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1; let A be Subset of T; ::_thesis: ( A is open implies A is lower ) assume A1: A in the topology of T ; :: according to PRE_TOPC:def_2 ::_thesis: A is lower let x, y be Element of T; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in A or not y <= x or y in A ) consider F being Basis of T such that A2: F c= FinMeetCl BB by CANTOR_1:def_4; the topology of T c= UniCl F by CANTOR_1:def_2; then consider Y being Subset-Family of T such that A3: Y c= F and A4: A = union Y by A1, CANTOR_1:def_1; assume x in A ; ::_thesis: ( not y <= x or y in A ) then consider Z being set such that A5: x in Z and A6: Z in Y by A4, TARSKI:def_4; Z in F by A3, A6; then consider X being Subset-Family of T such that A7: X c= BB and X is finite and A8: Z = Intersect X by A2, CANTOR_1:def_3; assume A9: x >= y ; ::_thesis: y in A now__::_thesis:_for_Q_being_set_st_Q_in_X_holds_ y_in_Q let Q be set ; ::_thesis: ( Q in X implies y in Q ) assume A10: Q in X ; ::_thesis: y in Q then Q in BB by A7; then consider z being Element of T such that A11: Q = (uparrow z) ` ; uparrow z misses Q by A11, XBOOLE_1:79; then A12: (uparrow z) /\ Q = {} T by XBOOLE_0:def_7; x in Q by A5, A8, A10, SETFAM_1:43; then not x in uparrow z by A12, XBOOLE_0:def_4; then not x >= z by WAYBEL_0:18; then not y >= z by A9, ORDERS_2:3; then not y in uparrow z by WAYBEL_0:18; hence y in Q by A11, XBOOLE_0:def_5; ::_thesis: verum end; then y in Z by A8, SETFAM_1:43; hence y in A by A4, A6, TARSKI:def_4; ::_thesis: verum end; theorem Th6: :: WAYBEL19:6 for T being non empty transitive lower TopRelStr for A being Subset of T st A is closed holds A is upper proof let T be non empty transitive lower TopRelStr ; ::_thesis: for A being Subset of T st A is closed holds A is upper let A be Subset of T; ::_thesis: ( A is closed implies A is upper ) assume ([#] T) \ A in the topology of T ; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: A is upper then A ` is open by PRE_TOPC:def_2; then A1: A ` is lower by Th5; let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A ) assume that A2: x in A and A3: x <= y and A4: not y in A ; ::_thesis: contradiction A5: y in A ` by A4, XBOOLE_0:def_5; not x in A ` by A2, XBOOLE_0:def_5; hence contradiction by A5, A1, A3, WAYBEL_0:def_19; ::_thesis: verum end; theorem Th7: :: WAYBEL19:7 for T being non empty TopSpace-like TopRelStr holds ( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T ) proof let T be non empty TopSpace-like TopRelStr ; ::_thesis: ( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T ) set BB = { ((uparrow x) `) where x is Element of T : verum } ; { ((uparrow x) `) where x is Element of T : verum } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((uparrow x) `) where x is Element of T : verum } or x in bool the carrier of T ) assume x in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: x in bool the carrier of T then ex y being Element of T st x = (uparrow y) ` ; hence x in bool the carrier of T ; ::_thesis: verum end; then reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as Subset-Family of T ; reconsider T9 = T as non empty RelStr ; set A = { ((uparrow F) `) where F is Subset of T : F is finite } ; reconsider BB = BB as Subset-Family of T ; A1: { ((uparrow F) `) where F is Subset of T : F is finite } = FinMeetCl BB proof deffunc H1( Element of T9) -> Element of bool the carrier of T9 = uparrow \$1; defpred S1[ set , set ] means ex x being Element of T st ( x = \$2 & \$1 = (uparrow x) ` ); hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: FinMeetCl BB c= { ((uparrow F) `) where F is Subset of T : F is finite } deffunc H2( Element of T9) -> Element of bool the carrier of T9 = uparrow \$1; let a be set ; ::_thesis: ( a in { ((uparrow F) `) where F is Subset of T : F is finite } implies a in FinMeetCl BB ) assume a in { ((uparrow F) `) where F is Subset of T : F is finite } ; ::_thesis: a in FinMeetCl BB then consider F being Subset of T such that A2: a = (uparrow F) ` and A3: F is finite ; set Y = { (uparrow x) where x is Element of T : x in F } ; { (uparrow x) where x is Element of T : x in F } c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (uparrow x) where x is Element of T : x in F } or a in bool the carrier of T ) assume a in { (uparrow x) where x is Element of T : x in F } ; ::_thesis: a in bool the carrier of T then ex x being Element of T st ( a = uparrow x & x in F ) ; hence a in bool the carrier of T ; ::_thesis: verum end; then reconsider Y = { (uparrow x) where x is Element of T : x in F } as Subset-Family of T ; reconsider Y = Y as Subset-Family of T ; uparrow F = union Y by YELLOW_9:4; then A4: a = Intersect (COMPLEMENT Y) by A2, YELLOW_8:6; reconsider Y9 = Y as Subset-Family of T9 ; A5: Y9 = { H2(x) where x is Element of T9 : x in F } ; A6: COMPLEMENT Y9 = { (H2(x) `) where x is Element of T9 : x in F } from YELLOW_9:sch_2(A5); A7: COMPLEMENT Y c= BB proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in COMPLEMENT Y or b in BB ) assume b in COMPLEMENT Y ; ::_thesis: b in BB then ex x being Element of T st ( b = (uparrow x) ` & x in F ) by A6; hence b in BB ; ::_thesis: verum end; deffunc H3( Element of T) -> Element of bool the carrier of T = (uparrow \$1) ` ; { H3(x) where x is Element of T : x in F } is finite from FRAENKEL:sch_21(A3); hence a in FinMeetCl BB by A7, A6, A4, CANTOR_1:def_3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in FinMeetCl BB or a in { ((uparrow F) `) where F is Subset of T : F is finite } ) assume a in FinMeetCl BB ; ::_thesis: a in { ((uparrow F) `) where F is Subset of T : F is finite } then consider Y being Subset-Family of T such that A8: Y c= BB and A9: Y is finite and A10: a = Intersect Y by CANTOR_1:def_3; A11: now__::_thesis:_for_y_being_set_st_y_in_Y_holds_ ex_b_being_set_st_ (_b_in_the_carrier_of_T_&_S1[y,b]_) let y be set ; ::_thesis: ( y in Y implies ex b being set st ( b in the carrier of T & S1[y,b] ) ) assume y in Y ; ::_thesis: ex b being set st ( b in the carrier of T & S1[y,b] ) then y in BB by A8; then ex x being Element of T st y = (uparrow x) ` ; hence ex b being set st ( b in the carrier of T & S1[y,b] ) ; ::_thesis: verum end; consider f being Function such that A12: ( dom f = Y & rng f c= the carrier of T ) and A13: for y being set st y in Y holds S1[y,f . y] from FUNCT_1:sch_5(A11); reconsider F = rng f as Subset of T by A12; A14: F is finite by A9, A12, FINSET_1:8; set X = { (uparrow x) where x is Element of T : x in F } ; { (uparrow x) where x is Element of T : x in F } c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (uparrow x) where x is Element of T : x in F } or a in bool the carrier of T ) assume a in { (uparrow x) where x is Element of T : x in F } ; ::_thesis: a in bool the carrier of T then ex x being Element of T st ( a = uparrow x & x in F ) ; hence a in bool the carrier of T ; ::_thesis: verum end; then reconsider X = { (uparrow x) where x is Element of T : x in F } as Subset-Family of T ; reconsider X = X as Subset-Family of T ; reconsider X9 = X as Subset-Family of T9 ; A15: X9 = { H1(x) where x is Element of T9 : x in F } ; A16: COMPLEMENT X9 = { (H1(x) `) where x is Element of T9 : x in F } from YELLOW_9:sch_2(A15); A17: COMPLEMENT X = Y proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Y c= COMPLEMENT X let a be set ; ::_thesis: ( a in COMPLEMENT X implies a in Y ) assume a in COMPLEMENT X ; ::_thesis: a in Y then consider x being Element of T9 such that A18: a = (uparrow x) ` and A19: x in F by A16; consider y being set such that A20: y in Y and A21: x = f . y by A12, A19, FUNCT_1:def_3; ex z being Element of T st ( z = f . y & y = (uparrow z) ` ) by A13, A20; hence a in Y by A18, A20, A21; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in COMPLEMENT X ) assume A22: a in Y ; ::_thesis: a in COMPLEMENT X then consider z being Element of T such that A23: z = f . a and A24: a = (uparrow z) ` by A13; z in F by A12, A22, A23, FUNCT_1:def_3; hence a in COMPLEMENT X by A16, A24; ::_thesis: verum end; uparrow F = union X by YELLOW_9:4; then a = (uparrow F) ` by A10, A17, YELLOW_8:6; hence a in { ((uparrow F) `) where F is Subset of T : F is finite } by A14; ::_thesis: verum end; ( T is lower iff BB is prebasis of T ) by Def1; hence ( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T ) by A1, YELLOW_9:23; ::_thesis: verum end; theorem Th8: :: WAYBEL19:8 for S, T being complete lower TopLattice for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds f is continuous proof let S, T be non empty complete lower TopLattice; ::_thesis: for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds f is continuous reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1; let f be Function of S,T; ::_thesis: ( ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous ) assume A1: for X being non empty Subset of S holds f preserves_inf_of X ; ::_thesis: f is continuous now__::_thesis:_for_A_being_Subset_of_T_st_A_in_BB_holds_ f_"_(A_`)_is_closed let A be Subset of T; ::_thesis: ( A in BB implies f " (b1 `) is closed ) A2: ex_inf_of f " (A `),S by YELLOW_0:17; A3: ex_inf_of A ` ,T by YELLOW_0:17; A4: ex_inf_of f .: (f " (A `)),T by YELLOW_0:17; assume A in BB ; ::_thesis: f " (b1 `) is closed then consider x being Element of T such that A5: A = (uparrow x) ` ; set s = inf (f " (uparrow x)); percases ( f " (A `) = {} S or f " (A `) <> {} ) ; suppose f " (A `) = {} S ; ::_thesis: f " (b1 `) is closed hence f " (A `) is closed ; ::_thesis: verum end; suppose f " (A `) <> {} ; ::_thesis: f " (b1 `) is closed then f preserves_inf_of f " (A `) by A1; then A6: f . (inf (f " (uparrow x))) = inf (f .: (f " (A `))) by A5, A2, WAYBEL_0:def_30; inf (A `) = x by A5, WAYBEL_0:39; then A7: x <= f . (inf (f " (uparrow x))) by A6, A3, A4, FUNCT_1:75, YELLOW_0:35; f " (A `) = uparrow (inf (f " (uparrow x))) proof thus f " (A `) c= uparrow (inf (f " (uparrow x))) :: according to XBOOLE_0:def_10 ::_thesis: uparrow (inf (f " (uparrow x))) c= f " (A `) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f " (A `) or a in uparrow (inf (f " (uparrow x))) ) assume A8: a in f " (A `) ; ::_thesis: a in uparrow (inf (f " (uparrow x))) then reconsider a = a as Element of S ; inf (f " (uparrow x)) <= a by A5, A8, YELLOW_2:22; hence a in uparrow (inf (f " (uparrow x))) by WAYBEL_0:18; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in uparrow (inf (f " (uparrow x))) or a in f " (A `) ) assume A9: a in uparrow (inf (f " (uparrow x))) ; ::_thesis: a in f " (A `) then reconsider a = a as Element of S ; f preserves_inf_of {(inf (f " (uparrow x))),a} by A1; then A10: f . ((inf (f " (uparrow x))) "/\" a) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by YELLOW_3:8; inf (f " (uparrow x)) <= a by A9, WAYBEL_0:18; then f . (inf (f " (uparrow x))) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by A10, YELLOW_5:10; then f . (inf (f " (uparrow x))) <= f . a by YELLOW_0:23; then x <= f . a by A7, ORDERS_2:3; then f . a in uparrow x by WAYBEL_0:18; hence a in f " (A `) by A5, FUNCT_2:38; ::_thesis: verum end; hence f " (A `) is closed by Th4; ::_thesis: verum end; end; end; hence f is continuous by YELLOW_9:35; ::_thesis: verum end; theorem Th9: :: WAYBEL19:9 for S, T being complete lower TopLattice for f being Function of S,T st f is infs-preserving holds f is continuous proof let S, T be non empty complete lower TopLattice; ::_thesis: for f being Function of S,T st f is infs-preserving holds f is continuous let f be Function of S,T; ::_thesis: ( f is infs-preserving implies f is continuous ) assume f is infs-preserving ; ::_thesis: f is continuous then for X being non empty Subset of S holds f preserves_inf_of X by WAYBEL_0:def_32; hence f is continuous by Th8; ::_thesis: verum end; theorem Th10: :: WAYBEL19:10 for T being complete lower TopLattice for BB being prebasis of T for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds F meets A ) holds inf F in Cl F proof let T be complete lower TopLattice; ::_thesis: for BB being prebasis of T for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds F meets A ) holds inf F in Cl F let BB be prebasis of T; ::_thesis: for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds F meets A ) holds inf F in Cl F let F be non empty filtered Subset of T; ::_thesis: ( ( for A being Subset of T st A in BB & inf F in A holds F meets A ) implies inf F in Cl F ) assume A1: for A being Subset of T st A in BB & inf F in A holds F meets A ; ::_thesis: inf F in Cl F set N = F opp+id ; set x = inf F; A2: for A being Subset of T st A in BB & inf F in A holds F opp+id is_eventually_in A proof let A be Subset of T; ::_thesis: ( A in BB & inf F in A implies F opp+id is_eventually_in A ) assume that A3: A in BB and A4: inf F in A ; ::_thesis: F opp+id is_eventually_in A A is open by A3, TOPS_2:def_1; then A5: A is lower by Th5; F meets A by A3, A4, A1; then consider i being set such that A6: i in F and A7: i in A by XBOOLE_0:3; reconsider i = i as Element of (F opp+id) by A6, YELLOW_9:7; take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds ( not i <= b1 or (F opp+id) . b1 in A ) let j be Element of (F opp+id); ::_thesis: ( not i <= j or (F opp+id) . j in A ) A8: F opp+id is full SubRelStr of T opp by YELLOW_9:7; then reconsider a = i, b = j as Element of (T opp) by YELLOW_0:58; assume i <= j ; ::_thesis: (F opp+id) . j in A then a <= b by A8, YELLOW_0:59; then A9: ~ b <= ~ a by YELLOW_7:1; (F opp+id) . j = j by YELLOW_9:7; hence (F opp+id) . j in A by A9, A7, A5, WAYBEL_0:def_19; ::_thesis: verum end; A10: the carrier of (F opp+id) = F by YELLOW_9:7; rng (netmap ((F opp+id),T)) c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (netmap ((F opp+id),T)) or x in F ) assume x in rng (netmap ((F opp+id),T)) ; ::_thesis: x in F then consider a being set such that A11: a in dom (netmap ((F opp+id),T)) and A12: x = (netmap ((F opp+id),T)) . a by FUNCT_1:def_3; reconsider a = a as Element of (F opp+id) by A11; x = (F opp+id) . a by A12 .= a by YELLOW_9:7 ; hence x in F by A10; ::_thesis: verum end; hence inf F in Cl F by A2, YELLOW_9:39; ::_thesis: verum end; theorem Th11: :: WAYBEL19:11 for S, T being complete lower TopLattice for f being Function of S,T st f is continuous holds f is filtered-infs-preserving proof let S, T be complete lower TopLattice; ::_thesis: for f being Function of S,T st f is continuous holds f is filtered-infs-preserving reconsider BB = { ((uparrow x) `) where x is Element of S : verum } as prebasis of S by Def1; let f be Function of S,T; ::_thesis: ( f is continuous implies f is filtered-infs-preserving ) assume A1: f is continuous ; ::_thesis: f is filtered-infs-preserving let F be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( F is empty or not F is filtered or f preserves_inf_of F ) assume that A2: ( not F is empty & F is filtered ) and ex_inf_of F,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: F,T & "/\" ((f .: F),T) = K76( the carrier of S, the carrier of T,f,("/\" (F,S))) ) for A being Subset of S st A in BB & inf F in A holds F meets A proof let A be Subset of S; ::_thesis: ( A in BB & inf F in A implies F meets A ) assume A in BB ; ::_thesis: ( not inf F in A or F meets A ) then consider x being Element of S such that A3: A = (uparrow x) ` ; assume inf F in A ; ::_thesis: F meets A then not inf F >= x by A3, YELLOW_9:1; then not F is_>=_than x by YELLOW_0:33; then consider y being Element of S such that A4: y in F and A5: not y >= x by LATTICE3:def_8; y in A by A3, A5, YELLOW_9:1; hence F meets A by A4, XBOOLE_0:3; ::_thesis: verum end; then A6: inf F in Cl F by A2, Th10; A7: f is monotone proof let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or K76( the carrier of S, the carrier of T,f,x) <= K76( the carrier of S, the carrier of T,f,y) ) assume A8: x <= y ; ::_thesis: K76( the carrier of S, the carrier of T,f,x) <= K76( the carrier of S, the carrier of T,f,y) f . x <= f . x ; then f . x in uparrow (f . x) by WAYBEL_0:18; then A9: x in f " (uparrow (f . x)) by FUNCT_2:38; uparrow (f . x) is closed by Th4; then f " (uparrow (f . x)) is closed by A1, PRE_TOPC:def_6; then f " (uparrow (f . x)) is upper by Th6; then y in f " (uparrow (f . x)) by A9, A8, WAYBEL_0:def_20; then f . y in uparrow (f . x) by FUNCT_2:38; hence K76( the carrier of S, the carrier of T,f,x) <= K76( the carrier of S, the carrier of T,f,y) by WAYBEL_0:18; ::_thesis: verum end; f . (inf F) is_<=_than f .: F proof let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: F or f . (inf F) <= x ) assume x in f .: F ; ::_thesis: f . (inf F) <= x then consider a being set such that A10: a in the carrier of S and A11: a in F and A12: x = f . a by FUNCT_2:64; reconsider a = a as Element of S by A10; inf F is_<=_than F by YELLOW_0:33; then inf F <= a by A11, LATTICE3:def_8; hence f . (inf F) <= x by A7, A12, WAYBEL_1:def_2; ::_thesis: verum end; then A13: f . (inf F) <= inf (f .: F) by YELLOW_0:33; thus ex_inf_of f .: F,T by YELLOW_0:17; ::_thesis: "/\" ((f .: F),T) = K76( the carrier of S, the carrier of T,f,("/\" (F,S))) F c= f " (uparrow (inf (f .: F))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in f " (uparrow (inf (f .: F))) ) assume A14: x in F ; ::_thesis: x in f " (uparrow (inf (f .: F))) then reconsider s = x as Element of S ; f . s in f .: F by A14, FUNCT_2:35; then inf (f .: F) <= f . s by YELLOW_2:22; then f . s in uparrow (inf (f .: F)) by WAYBEL_0:18; hence x in f " (uparrow (inf (f .: F))) by FUNCT_2:38; ::_thesis: verum end; then A15: Cl F c= Cl (f " (uparrow (inf (f .: F)))) by PRE_TOPC:19; uparrow (inf (f .: F)) is closed by Th4; then f " (uparrow (inf (f .: F))) is closed by A1, PRE_TOPC:def_6; then Cl F c= f " (uparrow (inf (f .: F))) by A15, PRE_TOPC:22; then f . (inf F) in uparrow (inf (f .: F)) by A6, FUNCT_2:38; then f . (inf F) >= inf (f .: F) by WAYBEL_0:18; hence inf (f .: F) = f . (inf F) by A13, ORDERS_2:2; ::_thesis: verum end; theorem :: WAYBEL19:12 for S, T being complete lower TopLattice for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds f is infs-preserving proof let S, T be complete lower TopLattice; ::_thesis: for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds f is infs-preserving let f be Function of S,T; ::_thesis: ( f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) implies f is infs-preserving ) assume f is continuous ; ::_thesis: ( ex X being finite Subset of S st not f preserves_inf_of X or f is infs-preserving ) then f is filtered-infs-preserving by Th11; then for F being non empty filtered Subset of S holds f preserves_inf_of F by WAYBEL_0:def_36; hence ( ex X being finite Subset of S st not f preserves_inf_of X or f is infs-preserving ) by WAYBEL_0:71; ::_thesis: verum end; theorem :: WAYBEL19:13 for T being non empty TopSpace-like reflexive transitive lower TopRelStr for x being Point of T holds Cl {x} = uparrow x proof let T be non empty TopSpace-like reflexive transitive lower TopRelStr ; ::_thesis: for x being Point of T holds Cl {x} = uparrow x let x be Point of T; ::_thesis: Cl {x} = uparrow x reconsider y = x as Element of T ; y <= y ; then x in uparrow x by WAYBEL_0:18; then {x} c= uparrow x by ZFMISC_1:31; hence Cl {x} c= uparrow x by Th4, TOPS_1:5; :: according to XBOOLE_0:def_10 ::_thesis: uparrow x c= Cl {x} Cl {x} is upper by Th6; then A1: uparrow (Cl {x}) c= Cl {x} by WAYBEL_0:24; uparrow {x} c= uparrow (Cl {x}) by PRE_TOPC:18, YELLOW_3:7; hence uparrow x c= Cl {x} by A1, XBOOLE_1:1; ::_thesis: verum end; definition mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr ; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric lower -> non empty T_0 for TopRelStr ; coherence for b1 being non empty TopPoset st b1 is lower holds b1 is T_0 proof let T be non empty TopPoset; ::_thesis: ( T is lower implies T is T_0 ) assume A1: T is lower ; ::_thesis: T is T_0 now__::_thesis:_(_not_T_is_empty_implies_for_x,_y_being_Point_of_T_holds_ (_not_x_<>_y_or_ex_V_being_Subset_of_T_st_ (_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_V_being_Subset_of_T_st_ (_V_is_open_&_not_x_in_V_&_y_in_V_)_)_) assume not T is empty ; ::_thesis: for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( b5 is open & V in b5 & not b4 in b5 ) or ex V being Subset of T st ( b5 is open & not V in b5 & b4 in b5 ) ) let x, y be Point of T; ::_thesis: ( not x <> y or ex V being Subset of T st ( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st ( b3 is open & not V in b3 & b2 in b3 ) ) assume A2: x <> y ; ::_thesis: ( ex V being Subset of T st ( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st ( b3 is open & not V in b3 & b2 in b3 ) ) reconsider a = x, b = y as Element of T ; set Vy = (uparrow a) ` ; set Vx = (uparrow b) ` ; a <= a ; then A3: not x in (uparrow a) ` by YELLOW_9:1; b <= b ; then A4: not y in (uparrow b) ` by YELLOW_9:1; A5: (uparrow b) ` is open by A1, Th4; A6: (uparrow a) ` is open by A1, Th4; percases ( not b <= a or not a <= b ) by A2, YELLOW_0:def_3; suppose not b <= a ; ::_thesis: ( ex V being Subset of T st ( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st ( b3 is open & not V in b3 & b2 in b3 ) ) then a in (uparrow b) ` by YELLOW_9:1; hence ( ex V being Subset of T st ( V is open & x in V & not y in V ) or ex V being Subset of T st ( V is open & not x in V & y in V ) ) by A5, A4; ::_thesis: verum end; suppose not a <= b ; ::_thesis: ( ex V being Subset of T st ( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st ( b3 is open & not V in b3 & b2 in b3 ) ) then b in (uparrow a) ` by YELLOW_9:1; hence ( ex V being Subset of T st ( V is open & x in V & not y in V ) or ex V being Subset of T st ( V is open & not x in V & y in V ) ) by A6, A3; ::_thesis: verum end; end; end; hence T is T_0 by TSP_1:def_3; ::_thesis: verum end; end; registration let R be non empty lower-bounded RelStr ; cluster -> lower-bounded for TopAugmentation of R; coherence for b1 being TopAugmentation of R holds b1 is lower-bounded proof let T be TopAugmentation of R; ::_thesis: T is lower-bounded RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; hence T is lower-bounded by YELLOW_0:13; ::_thesis: verum end; end; theorem Th14: :: WAYBEL19:14 for S, T being non empty RelStr for s being Element of S for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] proof let S, T be non empty RelStr ; ::_thesis: for s being Element of S for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] let s be Element of S; ::_thesis: for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] let t be Element of T; ::_thesis: (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] thus (uparrow [s,t]) ` = [: the carrier of S, the carrier of T:] \ (uparrow [s,t]) by YELLOW_3:def_2 .= [: the carrier of S, the carrier of T:] \ [:(uparrow s),(uparrow t):] by YELLOW10:40 .= [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] by ZFMISC_1:103 ; ::_thesis: verum end; theorem Th15: :: WAYBEL19:15 for S, T being non empty lower-bounded Poset for S9 being correct lower TopAugmentation of S for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:] proof let S, T be non empty lower-bounded Poset; ::_thesis: for S9 being correct lower TopAugmentation of S for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:] set ST = the correct lower TopAugmentation of [:S,T:]; reconsider BX = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of [:S,T:] : verum } as prebasis of the correct lower TopAugmentation of [:S,T:] by Def1; let S9 be correct lower TopAugmentation of S; ::_thesis: for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:] reconsider BS = { ((uparrow x) `) where x is Element of S9 : verum } as prebasis of S9 by Def1; let T9 be correct lower TopAugmentation of T; ::_thesis: omega [:S,T:] = the topology of [:S9,T9:] set SxT = [:S9,T9:]; set B2 = { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ; A1: RelStr(# the carrier of T9, the InternalRel of T9 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; reconsider BT = { ((uparrow x) `) where x is Element of T9 : verum } as prebasis of T9 by Def1; A2: RelStr(# the carrier of S9, the InternalRel of S9 #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then A3: the carrier of [:S9,T9:] = [: the carrier of S, the carrier of T:] by A1, BORSUK_1:def_2; A4: RelStr(# the carrier of the correct lower TopAugmentation of [:S,T:], the InternalRel of the correct lower TopAugmentation of [:S,T:] #) = [:S,T:] by YELLOW_9:def_4; then A5: the carrier of the correct lower TopAugmentation of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2; A6: BX c= the topology of [:S9,T9:] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in BX or z in the topology of [:S9,T9:] ) A7: [#] T9 is open ; assume z in BX ; ::_thesis: z in the topology of [:S9,T9:] then consider x being Element of the correct lower TopAugmentation of [:S,T:] such that A8: z = (uparrow x) ` ; consider s, t being set such that A9: s in the carrier of S and A10: t in the carrier of T and A11: x = [s,t] by A5, ZFMISC_1:def_2; reconsider t = t as Element of T by A10; reconsider s = s as Element of S by A9; uparrow x = uparrow [s,t] by A4, A11, WAYBEL_0:13; then A12: z = [:((uparrow s) `),([#] T):] \/ [:([#] S),((uparrow t) `):] by A4, A8, Th14; reconsider s9 = s as Element of S9 by A2; reconsider t9 = t as Element of T9 by A1; (uparrow t9) ` in BT ; then A13: (uparrow t9) ` is open by TOPS_2:def_1; reconsider A1 = [:((uparrow s) `),([#] T):], A2 = [:([#] S),((uparrow t) `):] as Subset of [:S9,T9:] by A3, YELLOW_3:def_2; A14: [#] S9 is open ; (uparrow s9) ` in BS ; then A15: (uparrow s9) ` is open by TOPS_2:def_1; uparrow t = uparrow t9 by A1, WAYBEL_0:13; then A16: A2 is open by A13, A14, A2, A1, BORSUK_1:6; uparrow s = uparrow s9 by A2, WAYBEL_0:13; then A1 is open by A15, A7, A2, A1, BORSUK_1:6; then A1 \/ A2 is open by A16; hence z in the topology of [:S9,T9:] by A12, PRE_TOPC:def_2; ::_thesis: verum end; set B1 = { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } ; reconsider BB = { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } \/ { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } as prebasis of [:S9,T9:] by YELLOW_9:41; A17: UniCl the topology of [:S9,T9:] = the topology of [:S9,T9:] by CANTOR_1:6; BB c= BX proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in BB or z in BX ) assume A18: z in BB ; ::_thesis: z in BX percases ( z in { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } or z in { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ) by A18, XBOOLE_0:def_3; suppose z in { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } ; ::_thesis: z in BX then consider b being Subset of T9 such that A19: z = [: the carrier of S9,b:] and A20: b in BT ; consider t9 being Element of T9 such that A21: b = (uparrow t9) ` by A20; reconsider t = t9 as Element of T by A1; reconsider x = [(Bottom S),t] as Element of the correct lower TopAugmentation of [:S,T:] by A4; A22: uparrow x = uparrow [(Bottom S),t] by A4, WAYBEL_0:13; uparrow (Bottom S) = the carrier of S by WAYBEL14:10; then A23: (uparrow (Bottom S)) ` = {} by XBOOLE_1:37; uparrow t = uparrow t9 by A1, WAYBEL_0:13; then (uparrow [(Bottom S),t]) ` = [:{}, the carrier of T:] \/ [: the carrier of S,b:] by A23, A1, A21, Th14 .= {} \/ [: the carrier of S,b:] by ZFMISC_1:90 .= z by A2, A19 ; hence z in BX by A4, A22; ::_thesis: verum end; suppose z in { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ; ::_thesis: z in BX then consider a being Subset of S9 such that A24: z = [:a, the carrier of T9:] and A25: a in BS ; consider s9 being Element of S9 such that A26: a = (uparrow s9) ` by A25; reconsider s = s9 as Element of S by A2; reconsider x = [s,(Bottom T)] as Element of the correct lower TopAugmentation of [:S,T:] by A4; A27: uparrow x = uparrow [s,(Bottom T)] by A4, WAYBEL_0:13; uparrow (Bottom T) = the carrier of T by WAYBEL14:10; then A28: (uparrow (Bottom T)) ` = {} by XBOOLE_1:37; uparrow s = uparrow s9 by A2, WAYBEL_0:13; then (uparrow [s,(Bottom T)]) ` = [:a, the carrier of T:] \/ [: the carrier of S,{}:] by A28, A2, A26, Th14 .= [:a, the carrier of T:] \/ {} by ZFMISC_1:90 .= z by A1, A24 ; hence z in BX by A4, A27; ::_thesis: verum end; end; end; then FinMeetCl BB c= FinMeetCl BX by A5, A3, CANTOR_1:14; then A29: UniCl (FinMeetCl BB) c= UniCl (FinMeetCl BX) by A5, A3, CANTOR_1:9; FinMeetCl BB is Basis of [:S9,T9:] by YELLOW_9:23; then A30: the topology of [:S9,T9:] = UniCl (FinMeetCl BB) by YELLOW_9:22; FinMeetCl BX is Basis of the correct lower TopAugmentation of [:S,T:] by YELLOW_9:23; then A31: the topology of the correct lower TopAugmentation of [:S,T:] = UniCl (FinMeetCl BX) by YELLOW_9:22; FinMeetCl the topology of [:S9,T9:] = the topology of [:S9,T9:] by CANTOR_1:5; then FinMeetCl BX c= the topology of [:S9,T9:] by A6, A5, A3, CANTOR_1:14; then UniCl (FinMeetCl BX) c= the topology of [:S9,T9:] by A5, A3, A17, CANTOR_1:9; then the topology of the correct lower TopAugmentation of [:S,T:] = the topology of [:S9,T9:] by A31, A30, A29, XBOOLE_0:def_10; hence omega [:S,T:] = the topology of [:S9,T9:] by Def2; ::_thesis: verum end; theorem :: WAYBEL19:16 for S, T being non empty lower-bounded lower TopPoset holds omega [:S,T:] = the topology of [:S,T:] proof let S, T be non empty lower-bounded lower TopPoset; ::_thesis: omega [:S,T:] = the topology of [:S,T:] A1: T is TopAugmentation of T by YELLOW_9:44; S is TopAugmentation of S by YELLOW_9:44; hence omega [:S,T:] = the topology of [:S,T:] by A1, Th15; ::_thesis: verum end; theorem :: WAYBEL19:17 for T, T2 being complete lower TopLattice st T2 is TopAugmentation of [:T,T:] holds for f being Function of T2,T st f = inf_op T holds f is continuous proof let T, T2 be complete lower TopLattice; ::_thesis: ( T2 is TopAugmentation of [:T,T:] implies for f being Function of T2,T st f = inf_op T holds f is continuous ) assume A1: RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of [:T,T:], the InternalRel of [:T,T:] #) ; :: according to YELLOW_9:def_4 ::_thesis: for f being Function of T2,T st f = inf_op T holds f is continuous let f be Function of T2,T; ::_thesis: ( f = inf_op T implies f is continuous ) assume A2: f = inf_op T ; ::_thesis: f is continuous f is infs-preserving proof let X be Subset of T2; :: according to WAYBEL_0:def_32 ::_thesis: f preserves_inf_of X reconsider Y = X as Subset of [:T,T:] by A1; assume A3: ex_inf_of X,T2 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = K76( the carrier of T2, the carrier of T,f,("/\" (X,T2))) ) thus ex_inf_of f .: X,T by YELLOW_0:17; ::_thesis: "/\" ((f .: X),T) = K76( the carrier of T2, the carrier of T,f,("/\" (X,T2))) A4: inf_op T preserves_inf_of Y by WAYBEL_0:def_32; ex_inf_of Y,[:T,T:] by A3, A1, YELLOW_0:14; hence inf (f .: X) = (inf_op T) . (inf Y) by A2, A4, WAYBEL_0:def_30 .= f . (inf X) by A1, A2, A3, YELLOW_0:27 ; ::_thesis: verum end; hence f is continuous by Th9; ::_thesis: verum end; begin scheme :: WAYBEL19:sch 1 TopInd{ F1() -> TopLattice, P1[ set ] } : for A being Subset of F1() st A is open holds P1[A] provided A1: ex K being prebasis of F1() st for A being Subset of F1() st A in K holds P1[A] and A2: for F being Subset-Family of F1() st ( for A being Subset of F1() st A in F holds P1[A] ) holds P1[ union F] and A3: for A1, A2 being Subset of F1() st P1[A1] & P1[A2] holds P1[A1 /\ A2] and A4: P1[ [#] F1()] proof consider K being prebasis of F1() such that A5: for A being Subset of F1() st A in K holds P1[A] by A1; let A be Subset of F1(); ::_thesis: ( A is open implies P1[A] ) assume A6: A in the topology of F1() ; :: according to PRE_TOPC:def_2 ::_thesis: P1[A] FinMeetCl K is Basis of F1() by YELLOW_9:23; then UniCl (FinMeetCl K) = the topology of F1() by YELLOW_9:22; then consider X being Subset-Family of F1() such that A7: X c= FinMeetCl K and A8: A = union X by A6, CANTOR_1:def_1; reconsider X = X as Subset-Family of F1() ; now__::_thesis:_for_A_being_Subset_of_F1()_st_A_in_X_holds_ P1[A] defpred S1[ set ] means for a being Subset-Family of F1() st a = \$1 holds P1[ Intersect a]; let A be Subset of F1(); ::_thesis: ( A in X implies P1[A] ) assume A in X ; ::_thesis: P1[A] then consider Y being Subset-Family of F1() such that A9: Y c= K and A10: Y is finite and A11: A = Intersect Y by A7, CANTOR_1:def_3; A12: for x, Z being set st x in Y & Z c= Y & S1[Z] holds S1[Z \/ {x}] proof let x, Z be set ; ::_thesis: ( x in Y & Z c= Y & S1[Z] implies S1[Z \/ {x}] ) assume that A13: x in Y and A14: Z c= Y and A15: S1[Z] ; ::_thesis: S1[Z \/ {x}] reconsider xx = {x}, Z9 = Z as Subset-Family of F1() by A13, A14, XBOOLE_1:1, ZFMISC_1:31; reconsider xx = xx, Z9 = Z9 as Subset-Family of F1() ; reconsider xx = xx, Z9 = Z9 as Subset-Family of F1() ; reconsider Ax = x, Ay = Intersect Z9 as Subset of F1() by A13; A16: P1[Ay] by A15; let a be Subset-Family of F1(); ::_thesis: ( a = Z \/ {x} implies P1[ Intersect a] ) assume A17: a = Z \/ {x} ; ::_thesis: P1[ Intersect a] Intersect xx = Ax by MSSUBFAM:9; then A18: Intersect a = Ax /\ Ay by A17, MSSUBFAM:8; P1[Ax] by A5, A9, A13; hence P1[ Intersect a] by A18, A3, A16; ::_thesis: verum end; A19: S1[ {} ] by A4, SETFAM_1:def_9; S1[Y] from FINSET_1:sch_2(A10, A19, A12); hence P1[A] by A11; ::_thesis: verum end; hence P1[A] by A2, A8; ::_thesis: verum end; theorem :: WAYBEL19:18 for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & ( for x being Element of L1 holds ( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation holds L2 is satisfying_axiom_of_approximation proof let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & ( for x being Element of L1 holds ( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation implies L2 is satisfying_axiom_of_approximation ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: for x being Element of L1 holds ( waybelow x is directed & not waybelow x is empty ) and A3: for x being Element of L1 holds x = sup (waybelow x) ; :: according to WAYBEL_3:def_5 ::_thesis: L2 is satisfying_axiom_of_approximation let x be Element of L2; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),L2) reconsider y = x as Element of L1 by A1; A4: y = sup (waybelow y) by A3; ( waybelow y is directed & not waybelow y is empty ) by A2; then A5: ex_sup_of waybelow y,L1 by WAYBEL_0:75; waybelow y = waybelow x by A1, YELLOW12:13; hence x = "\/" ((waybelow x),L2) by A4, A5, A1, YELLOW_0:26; ::_thesis: verum end; registration let T be non empty continuous Poset; cluster -> continuous for TopAugmentation of T; coherence for b1 being TopAugmentation of T holds b1 is continuous proof let S be TopAugmentation of T; ::_thesis: S is continuous RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; hence S is continuous by YELLOW12:15; ::_thesis: verum end; end; theorem Th19: :: WAYBEL19:19 for T, S being TopSpace for R being Refinement of T,S for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds W is open proof let T, S be TopSpace; ::_thesis: for R being Refinement of T,S for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds W is open let R be Refinement of T,S; ::_thesis: for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds W is open let W be Subset of R; ::_thesis: ( ( W in the topology of T or W in the topology of S ) implies W is open ) the topology of T \/ the topology of S is prebasis of R by YELLOW_9:def_6; then A1: the topology of T \/ the topology of S c= the topology of R by TOPS_2:64; assume ( W in the topology of T or W in the topology of S ) ; ::_thesis: W is open then W in the topology of T \/ the topology of S by XBOOLE_0:def_3; hence W in the topology of R by A1; :: according to PRE_TOPC:def_2 ::_thesis: verum end; theorem Th20: :: WAYBEL19:20 for T, S being TopSpace for R being Refinement of T,S for V being Subset of T for W being Subset of R st W = V & V is open holds W is open proof let T, S be TopSpace; ::_thesis: for R being Refinement of T,S for V being Subset of T for W being Subset of R st W = V & V is open holds W is open let R be Refinement of T,S; ::_thesis: for V being Subset of T for W being Subset of R st W = V & V is open holds W is open let V be Subset of T; ::_thesis: for W being Subset of R st W = V & V is open holds W is open let W be Subset of R; ::_thesis: ( W = V & V is open implies W is open ) assume A1: W = V ; ::_thesis: ( not V is open or W is open ) assume V in the topology of T ; :: according to PRE_TOPC:def_2 ::_thesis: W is open hence W is open by A1, Th19; ::_thesis: verum end; theorem Th21: :: WAYBEL19:21 for T, S being TopSpace st the carrier of T = the carrier of S holds for R being Refinement of T,S for V being Subset of T for W being Subset of R st W = V & V is closed holds W is closed proof let T, S be TopSpace; ::_thesis: ( the carrier of T = the carrier of S implies for R being Refinement of T,S for V being Subset of T for W being Subset of R st W = V & V is closed holds W is closed ) assume A1: the carrier of T = the carrier of S ; ::_thesis: for R being Refinement of T,S for V being Subset of T for W being Subset of R st W = V & V is closed holds W is closed let R be Refinement of T,S; ::_thesis: for V being Subset of T for W being Subset of R st W = V & V is closed holds W is closed let V be Subset of T; ::_thesis: for W being Subset of R st W = V & V is closed holds W is closed let W be Subset of R; ::_thesis: ( W = V & V is closed implies W is closed ) assume A2: W = V ; ::_thesis: ( not V is closed or W is closed ) assume V is closed ; ::_thesis: W is closed then A3: V ` is open ; the carrier of R = the carrier of T \/ the carrier of S by YELLOW_9:def_6 .= the carrier of T by A1 ; then W ` in the topology of T by A3, A2, PRE_TOPC:def_2; then W ` is open by Th19; hence W is closed by TOPS_1:3; ::_thesis: verum end; theorem Th22: :: WAYBEL19:22 for T being non empty TopSpace for K, O being set st K c= O & O c= the topology of T holds ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) ) proof let T be non empty TopSpace; ::_thesis: for K, O being set st K c= O & O c= the topology of T holds ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) ) let K, O be set ; ::_thesis: ( K c= O & O c= the topology of T implies ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) ) ) assume that A1: K c= O and A2: O c= the topology of T ; ::_thesis: ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) ) K c= the topology of T by A1, A2, XBOOLE_1:1; then reconsider K9 = K, O9 = O as Subset-Family of T by A2, XBOOLE_1:1; reconsider K9 = K9, O9 = O9 as Subset-Family of T ; reconsider K9 = K9, O9 = O9 as Subset-Family of T ; A3: UniCl K9 c= UniCl O9 by A1, CANTOR_1:9; A4: UniCl the topology of T = the topology of T by CANTOR_1:6; then A5: UniCl O9 c= the topology of T by A2, CANTOR_1:9; hereby ::_thesis: ( K is prebasis of T implies O is prebasis of T ) assume K is Basis of T ; ::_thesis: O is Basis of T then UniCl K9 = the topology of T by YELLOW_9:22; then UniCl O9 = the topology of T by A5, A3, XBOOLE_0:def_10; hence O is Basis of T by YELLOW_9:22; ::_thesis: verum end; FinMeetCl the topology of T = the topology of T by CANTOR_1:5; then FinMeetCl O9 c= the topology of T by A2, CANTOR_1:14; then A6: UniCl (FinMeetCl O9) c= the topology of T by A4, CANTOR_1:9; assume K is prebasis of T ; ::_thesis: O is prebasis of T then FinMeetCl K9 is Basis of T by YELLOW_9:23; then A7: UniCl (FinMeetCl K9) = the topology of T by YELLOW_9:22; FinMeetCl K9 c= FinMeetCl O9 by A1, CANTOR_1:14; then UniCl (FinMeetCl K9) c= UniCl (FinMeetCl O9) by CANTOR_1:9; then UniCl (FinMeetCl O9) = the topology of T by A7, A6, XBOOLE_0:def_10; then FinMeetCl O9 is Basis of T by YELLOW_9:22; hence O is prebasis of T by YELLOW_9:23; ::_thesis: verum end; theorem Th23: :: WAYBEL19:23 for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds for T being Refinement of T1,T2 for B1 being prebasis of T1 for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T proof let T1, T2 be non empty TopSpace; ::_thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2 for B1 being prebasis of T1 for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T ) assume A1: the carrier of T1 = the carrier of T2 ; ::_thesis: for T being Refinement of T1,T2 for B1 being prebasis of T1 for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T let T be Refinement of T1,T2; ::_thesis: for B1 being prebasis of T1 for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T let B1 be prebasis of T1; ::_thesis: for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T let B2 be prebasis of T2; ::_thesis: B1 \/ B2 is prebasis of T the carrier of T = the carrier of T1 \/ the carrier of T2 by YELLOW_9:def_6 .= the carrier of T1 by A1 ; then { the carrier of T1, the carrier of T2} = { the carrier of T} by A1, ENUMSET1:29; then reconsider K = (B1 \/ B2) \/ { the carrier of T} as prebasis of T by YELLOW_9:58; B1 \/ B2 c= K by XBOOLE_1:7; then reconsider K9 = B1 \/ B2 as Subset-Family of T by XBOOLE_1:1; K c= FinMeetCl K9 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in K or a in FinMeetCl K9 ) assume a in K ; ::_thesis: a in FinMeetCl K9 then ( ( a in K9 & K9 c= FinMeetCl K9 ) or ( a in { the carrier of T} & the carrier of T in FinMeetCl K9 ) ) by CANTOR_1:4, CANTOR_1:8, XBOOLE_0:def_3; hence a in FinMeetCl K9 by TARSKI:def_1; ::_thesis: verum end; then FinMeetCl K c= FinMeetCl (FinMeetCl K9) by CANTOR_1:14; then A2: FinMeetCl K c= FinMeetCl K9 by CANTOR_1:11; FinMeetCl K9 c= FinMeetCl K by CANTOR_1:14, XBOOLE_1:7; then FinMeetCl K9 = FinMeetCl K by A2, XBOOLE_0:def_10; then FinMeetCl K9 is Basis of T by YELLOW_9:23; hence B1 \/ B2 is prebasis of T by YELLOW_9:23; ::_thesis: verum end; theorem :: WAYBEL19:24 for T1, S1, T2, S2 being non empty TopSpace for R1 being Refinement of T1,S1 for R2 being Refinement of T2,S2 for f being Function of T1,T2 for g being Function of S1,S2 for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds h is continuous proof let T1, S1, T2, S2 be non empty TopSpace; ::_thesis: for R1 being Refinement of T1,S1 for R2 being Refinement of T2,S2 for f being Function of T1,T2 for g being Function of S1,S2 for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds h is continuous let R1 be Refinement of T1,S1; ::_thesis: for R2 being Refinement of T2,S2 for f being Function of T1,T2 for g being Function of S1,S2 for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds h is continuous let R2 be Refinement of T2,S2; ::_thesis: for f being Function of T1,T2 for g being Function of S1,S2 for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds h is continuous let f be Function of T1,T2; ::_thesis: for g being Function of S1,S2 for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds h is continuous let g be Function of S1,S2; ::_thesis: for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds h is continuous let h be Function of R1,R2; ::_thesis: ( h = f & h = g & f is continuous & g is continuous implies h is continuous ) assume that A1: h = f and A2: h = g ; ::_thesis: ( not f is continuous or not g is continuous or h is continuous ) A3: [#] S2 <> {} ; reconsider K = the topology of T2 \/ the topology of S2 as prebasis of R2 by YELLOW_9:def_6; A4: [#] T2 <> {} ; assume A5: f is continuous ; ::_thesis: ( not g is continuous or h is continuous ) assume A6: g is continuous ; ::_thesis: h is continuous now__::_thesis:_for_A_being_Subset_of_R2_st_A_in_K_holds_ h_"_A_is_open let A be Subset of R2; ::_thesis: ( A in K implies h " b1 is open ) assume A7: A in K ; ::_thesis: h " b1 is open percases ( A in the topology of T2 or A in the topology of S2 ) by A7, XBOOLE_0:def_3; supposeA8: A in the topology of T2 ; ::_thesis: h " b1 is open then reconsider A1 = A as Subset of T2 ; A1 is open by A8, PRE_TOPC:def_2; then f " A1 is open by A4, A5, TOPS_2:43; hence h " A is open by A1, Th20; ::_thesis: verum end; supposeA9: A in the topology of S2 ; ::_thesis: h " b1 is open then reconsider A1 = A as Subset of S2 ; A1 is open by A9, PRE_TOPC:def_2; then A10: g " A1 is open by A3, A6, TOPS_2:43; R1 is Refinement of S1,T1 by YELLOW_9:55; hence h " A is open by A10, A2, Th20; ::_thesis: verum end; end; end; hence h is continuous by YELLOW_9:36; ::_thesis: verum end; theorem Th25: :: WAYBEL19:25 for T being non empty TopSpace for K being prebasis of T for N being net of T for p being Point of T st ( for A being Subset of T st p in A & A in K holds N is_eventually_in A ) holds p in Lim N proof let T be non empty TopSpace; ::_thesis: for K being prebasis of T for N being net of T for p being Point of T st ( for A being Subset of T st p in A & A in K holds N is_eventually_in A ) holds p in Lim N let K be prebasis of T; ::_thesis: for N being net of T for p being Point of T st ( for A being Subset of T st p in A & A in K holds N is_eventually_in A ) holds p in Lim N let N be net of T; ::_thesis: for p being Point of T st ( for A being Subset of T st p in A & A in K holds N is_eventually_in A ) holds p in Lim N let x be Point of T; ::_thesis: ( ( for A being Subset of T st x in A & A in K holds N is_eventually_in A ) implies x in Lim N ) assume A1: for A being Subset of T st x in A & A in K holds N is_eventually_in A ; ::_thesis: x in Lim N now__::_thesis:_for_A_being_a_neighborhood_of_x_holds_N_is_eventually_in_A defpred S1[ set , set ] means for i, j being Element of N st i = \$2 & j >= i holds N . j in \$1; let A be a_neighborhood of x; ::_thesis: N is_eventually_in A A2: Int A in the topology of T by PRE_TOPC:def_2; FinMeetCl K is Basis of T by YELLOW_9:23; then the topology of T = UniCl (FinMeetCl K) by YELLOW_9:22; then consider Y being Subset-Family of T such that A3: Y c= FinMeetCl K and A4: Int A = union Y by A2, CANTOR_1:def_1; x in Int A by CONNSP_2:def_1; then consider y being set such that A5: x in y and A6: y in Y by A4, TARSKI:def_4; consider Z being Subset-Family of T such that A7: Z c= K and A8: Z is finite and A9: y = Intersect Z by A3, A6, CANTOR_1:def_3; A10: for a being set st a in Z holds ex b being set st ( b in the carrier of N & S1[a,b] ) proof let a be set ; ::_thesis: ( a in Z implies ex b being set st ( b in the carrier of N & S1[a,b] ) ) assume A11: a in Z ; ::_thesis: ex b being set st ( b in the carrier of N & S1[a,b] ) then reconsider a = a as Subset of T ; x in a by A5, A9, A11, SETFAM_1:43; then N is_eventually_in a by A1, A7, A11; then consider i being Element of N such that A12: for j being Element of N st j >= i holds N . j in a by WAYBEL_0:def_11; take i ; ::_thesis: ( i in the carrier of N & S1[a,i] ) thus ( i in the carrier of N & S1[a,i] ) by A12; ::_thesis: verum end; consider f being Function such that A13: ( dom f = Z & rng f c= the carrier of N ) and A14: for a being set st a in Z holds S1[a,f . a] from FUNCT_1:sch_5(A10); reconsider z = rng f as finite Subset of ([#] N) by A8, A13, FINSET_1:8; [#] N is directed by WAYBEL_0:def_6; then consider k being Element of N such that k in [#] N and A15: k is_>=_than z by WAYBEL_0:1; thus N is_eventually_in A ::_thesis: verum proof take k ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not k <= b1 or N . b1 in A ) let i be Element of N; ::_thesis: ( not k <= i or N . i in A ) A16: Int A c= A by TOPS_1:16; assume A17: i >= k ; ::_thesis: N . i in A now__::_thesis:_for_a_being_set_st_a_in_Z_holds_ N_._i_in_a let a be set ; ::_thesis: ( a in Z implies N . i in a ) assume A18: a in Z ; ::_thesis: N . i in a then A19: f . a in z by A13, FUNCT_1:def_3; then reconsider j = f . a as Element of N ; j <= k by A15, A19, LATTICE3:def_9; hence N . i in a by A14, A17, A18, ORDERS_2:3; ::_thesis: verum end; then A20: N . i in y by A9, SETFAM_1:43; y c= union Y by A6, ZFMISC_1:74; then N . i in Int A by A20, A4; hence N . i in A by A16; ::_thesis: verum end; end; hence x in Lim N by YELLOW_6:def_15; ::_thesis: verum end; theorem Th26: :: WAYBEL19:26 for T being non empty TopSpace for N being net of T for S being Subset of T st N is_eventually_in S holds Lim N c= Cl S proof let T be non empty TopSpace; ::_thesis: for N being net of T for S being Subset of T st N is_eventually_in S holds Lim N c= Cl S let N be net of T; ::_thesis: for S being Subset of T st N is_eventually_in S holds Lim N c= Cl S let S be Subset of T; ::_thesis: ( N is_eventually_in S implies Lim N c= Cl S ) given i being Element of N such that A1: for j being Element of N st j >= i holds N . j in S ; :: according to WAYBEL_0:def_11 ::_thesis: Lim N c= Cl S let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim N or x in Cl S ) assume A2: x in Lim N ; ::_thesis: x in Cl S then reconsider x = x as Element of T ; now__::_thesis:_for_G_being_a_neighborhood_of_x_holds_G_meets_S let G be a_neighborhood of x; ::_thesis: G meets S N is_eventually_in G by A2, YELLOW_6:def_15; then consider k being Element of N such that A3: for j being Element of N st j >= k holds N . j in G by WAYBEL_0:def_11; [#] N is directed by WAYBEL_0:def_6; then consider j being Element of N such that j in [#] N and A4: j >= i and A5: j >= k by WAYBEL_0:def_1; A6: N . j in G by A3, A5; N . j in S by A1, A4; hence G meets S by A6, XBOOLE_0:3; ::_thesis: verum end; hence x in Cl S by CONNSP_2:27; ::_thesis: verum end; theorem Th27: :: WAYBEL19:27 for R being non empty RelStr for X being non empty Subset of R holds ( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X ) proof let R be non empty RelStr ; ::_thesis: for X being non empty Subset of R holds ( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X ) let X be non empty Subset of R; ::_thesis: ( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X ) A1: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ the_mapping_of_(X_+id)_._x_=_x let x be set ; ::_thesis: ( x in X implies the mapping of (X +id) . x = x ) assume x in X ; ::_thesis: the mapping of (X +id) . x = x then reconsider i = x as Element of (X +id) by YELLOW_9:6; thus the mapping of (X +id) . x = (X +id) . i .= x by YELLOW_9:6 ; ::_thesis: verum end; the carrier of (X +id) = X by YELLOW_9:6; then dom the mapping of (X +id) = X by FUNCT_2:def_1; hence the mapping of (X +id) = id X by A1, FUNCT_1:17; ::_thesis: the mapping of (X opp+id) = id X A2: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ the_mapping_of_(X_opp+id)_._x_=_x let x be set ; ::_thesis: ( x in X implies the mapping of (X opp+id) . x = x ) assume x in X ; ::_thesis: the mapping of (X opp+id) . x = x then reconsider i = x as Element of (X opp+id) by YELLOW_9:7; thus the mapping of (X opp+id) . x = (X opp+id) . i .= x by YELLOW_9:7 ; ::_thesis: verum end; the carrier of (X opp+id) = X by YELLOW_9:7; then dom the mapping of (X opp+id) = X by FUNCT_2:def_1; hence the mapping of (X opp+id) = id X by A2, FUNCT_1:17; ::_thesis: verum end; theorem Th28: :: WAYBEL19:28 for R being non empty reflexive antisymmetric RelStr for x being Element of R holds (uparrow x) /\ (downarrow x) = {x} proof let R be non empty reflexive antisymmetric RelStr ; ::_thesis: for x being Element of R holds (uparrow x) /\ (downarrow x) = {x} let x be Element of R; ::_thesis: (uparrow x) /\ (downarrow x) = {x} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {x} c= (uparrow x) /\ (downarrow x) let a be set ; ::_thesis: ( a in (uparrow x) /\ (downarrow x) implies a in {x} ) assume A1: a in (uparrow x) /\ (downarrow x) ; ::_thesis: a in {x} then reconsider y = a as Element of R ; y in downarrow x by A1, XBOOLE_0:def_4; then A2: y <= x by WAYBEL_0:17; y in uparrow x by A1, XBOOLE_0:def_4; then x <= y by WAYBEL_0:18; then x = a by A2, ORDERS_2:2; hence a in {x} by TARSKI:def_1; ::_thesis: verum end; A3: x <= x ; then A4: x in downarrow x by WAYBEL_0:17; x in uparrow x by A3, WAYBEL_0:18; then x in (uparrow x) /\ (downarrow x) by A4, XBOOLE_0:def_4; hence {x} c= (uparrow x) /\ (downarrow x) by ZFMISC_1:31; ::_thesis: verum end; begin definition let T be non empty reflexive TopRelStr ; attrT is Lawson means :Def3: :: WAYBEL19:def 3 (omega T) \/ (sigma T) is prebasis of T; end; :: deftheorem Def3 defines Lawson WAYBEL19:def_3_:_ for T being non empty reflexive TopRelStr holds ( T is Lawson iff (omega T) \/ (sigma T) is prebasis of T ); theorem Th29: :: WAYBEL19:29 for R being complete LATTICE for LL being correct lower TopAugmentation of R for S being Scott TopAugmentation of R for T being correct TopAugmentation of R holds ( T is Lawson iff T is Refinement of S,LL ) proof let R be complete LATTICE; ::_thesis: for LL being correct lower TopAugmentation of R for S being Scott TopAugmentation of R for T being correct TopAugmentation of R holds ( T is Lawson iff T is Refinement of S,LL ) let LL be correct lower TopAugmentation of R; ::_thesis: for S being Scott TopAugmentation of R for T being correct TopAugmentation of R holds ( T is Lawson iff T is Refinement of S,LL ) let S be Scott TopAugmentation of R; ::_thesis: for T being correct TopAugmentation of R holds ( T is Lawson iff T is Refinement of S,LL ) let T be correct TopAugmentation of R; ::_thesis: ( T is Lawson iff T is Refinement of S,LL ) A1: the topology of S = sigma R by YELLOW_9:51; A2: the carrier of R \/ the carrier of R = the carrier of R ; A3: the topology of LL = omega R by Def2; A4: RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; A5: ( (omega T) \/ (sigma T) is prebasis of T iff T is Lawson ) by Def3; A6: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; A7: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then A8: sigma T = sigma R by YELLOW_9:52; omega T = omega R by A7, Th3; hence ( T is Lawson iff T is Refinement of S,LL ) by A8, A3, A1, A5, A2, A4, A6, A7, YELLOW_9:def_6; ::_thesis: verum end; registration let R be complete LATTICE; cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete strict non void Lawson for TopAugmentation of R; existence ex b1 being TopAugmentation of R st ( b1 is Lawson & b1 is strict & b1 is correct ) proof set S = the correct Scott TopAugmentation of R; set T = the correct lower TopAugmentation of R; A1: RelStr(# the carrier of the correct Scott TopAugmentation of R, the InternalRel of the correct Scott TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; set RR = the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R; A2: the carrier of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R = the carrier of the correct Scott TopAugmentation of R \/ the carrier of the correct lower TopAugmentation of R by YELLOW_9:def_6; A3: RelStr(# the carrier of the correct lower TopAugmentation of R, the InternalRel of the correct lower TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then reconsider O = the topology of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R as Subset-Family of R by A2, A1; set LL = TopRelStr(# the carrier of R, the InternalRel of R,O #); RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,O #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,O #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; then reconsider LL = TopRelStr(# the carrier of R, the InternalRel of R,O #) as TopAugmentation of R by YELLOW_9:def_4; TopStruct(# the carrier of LL, the topology of LL #) = TopStruct(# the carrier of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R, the topology of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R #) by A3, A1, A2; then A4: LL is correct by TEX_2:7; reconsider A = the topology of the correct Scott TopAugmentation of R \/ the topology of the correct lower TopAugmentation of R as prebasis of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by YELLOW_9:def_6; reconsider A9 = A as Subset-Family of LL by A3, A1, A2; take LL ; ::_thesis: ( LL is Lawson & LL is strict & LL is correct ) FinMeetCl A is Basis of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by YELLOW_9:23; then UniCl (FinMeetCl A) = O by YELLOW_9:22; then FinMeetCl A9 is Basis of LL by A3, A1, A2, A4, YELLOW_9:22; then the topology of the correct Scott TopAugmentation of R \/ the topology of the correct lower TopAugmentation of R is prebasis of LL by A4, YELLOW_9:23; then LL is Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by A3, A1, A2, A4, YELLOW_9:def_6; hence ( LL is Lawson & LL is strict & LL is correct ) by Th29; ::_thesis: verum end; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott non void for TopRelStr ; existence ex b1 being TopLattice st ( b1 is Scott & b1 is complete & b1 is strict ) proof set R = the complete LATTICE; set T = the correct strict Scott TopAugmentation of the complete LATTICE; take the correct strict Scott TopAugmentation of the complete LATTICE ; ::_thesis: ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) thus ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) ; ::_thesis: verum end; cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() continuous up-complete /\-complete strict non void Lawson for TopRelStr ; existence ex b1 being complete strict TopLattice st ( b1 is Lawson & b1 is continuous ) proof set R = the complete continuous LATTICE; set T = the correct strict Lawson TopAugmentation of the complete continuous LATTICE; take the correct strict Lawson TopAugmentation of the complete continuous LATTICE ; ::_thesis: ( the correct strict Lawson TopAugmentation of the complete continuous LATTICE is Lawson & the correct strict Lawson TopAugmentation of the complete continuous LATTICE is continuous ) thus ( the correct strict Lawson TopAugmentation of the complete continuous LATTICE is Lawson & the correct strict Lawson TopAugmentation of the complete continuous LATTICE is continuous ) ; ::_thesis: verum end; end; theorem Th30: :: WAYBEL19:30 for T being complete Lawson TopLattice holds (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T proof let T be complete Lawson TopLattice; ::_thesis: (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T set R = the correct lower TopAugmentation of T; set S = the Scott TopAugmentation of T; A1: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; T is TopAugmentation of T by YELLOW_9:44; then A2: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29; set K = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ; set O = { ((uparrow x) `) where x is Element of T : verum } ; the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51; then sigma T is Basis of the Scott TopAugmentation of T by CANTOR_1:2; then A3: sigma T is prebasis of the Scott TopAugmentation of T by YELLOW_9:27; A4: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; { ((uparrow x) `) where x is Element of T : verum } = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } c= { ((uparrow x) `) where x is Element of T : verum } let a be set ; ::_thesis: ( a in { ((uparrow x) `) where x is Element of T : verum } implies a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ) assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } then consider x being Element of T such that A5: a = (uparrow x) ` ; reconsider y = x as Element of the correct lower TopAugmentation of T by A4; uparrow x = uparrow y by A4, WAYBEL_0:13; hence a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } by A4, A5; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } or a in { ((uparrow x) `) where x is Element of T : verum } ) assume a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of T : verum } then consider x being Element of the correct lower TopAugmentation of T such that A6: a = (uparrow x) ` ; reconsider y = x as Element of T by A4; uparrow x = uparrow y by A4, WAYBEL_0:13; hence a in { ((uparrow x) `) where x is Element of T : verum } by A4, A6; ::_thesis: verum end; then reconsider O = { ((uparrow x) `) where x is Element of T : verum } as prebasis of the correct lower TopAugmentation of T by Def1; O = O ; hence (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A3, A2, A1, A4, Th23; ::_thesis: verum end; theorem :: WAYBEL19:31 for T being complete Lawson TopLattice holds (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T proof let T be complete Lawson TopLattice; ::_thesis: (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T set R = the correct lower TopAugmentation of T; reconsider K = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } as prebasis of the correct lower TopAugmentation of T by Def1; set O = { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } ; { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } c= bool the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } or a in bool the carrier of T ) assume a in { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } ; ::_thesis: a in bool the carrier of T then ex W being Subset of T ex x being Element of T st ( a = W \ (uparrow x) & W in sigma T ) ; hence a in bool the carrier of T ; ::_thesis: verum end; then reconsider O = { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } as Subset-Family of T ; reconsider O = O as Subset-Family of T ; set S = the Scott TopAugmentation of T; A1: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; (sigma T) \/ (omega T) is prebasis of T by Def3; then A2: (sigma T) \/ (omega T) c= the topology of T by TOPS_2:64; omega T c= (sigma T) \/ (omega T) by XBOOLE_1:7; then A3: omega T c= the topology of T by A2, XBOOLE_1:1; sigma T c= (sigma T) \/ (omega T) by XBOOLE_1:7; then A4: sigma T c= the topology of T by A2, XBOOLE_1:1; A5: omega T = the topology of the correct lower TopAugmentation of T by Def2; O c= the topology of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in O or a in the topology of T ) assume a in O ; ::_thesis: a in the topology of T then consider W being Subset of T, x being Element of T such that A6: a = W \ (uparrow x) and A7: W in sigma T ; A8: a = W /\ ((uparrow x) `) by A6, SUBSET_1:13; reconsider y = x as Element of the correct lower TopAugmentation of T by A1; uparrow x = uparrow y by A1, WAYBEL_0:13; then A9: (uparrow x) ` in K by A1; K c= omega T by A5, TOPS_2:64; then (uparrow x) ` in omega T by A9; hence a in the topology of T by A4, A3, A7, A8, PRE_TOPC:def_1; ::_thesis: verum end; then A10: (sigma T) \/ O c= the topology of T by A4, XBOOLE_1:8; A11: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; A12: sigma T = the topology of the Scott TopAugmentation of T by YELLOW_9:51; then sigma T is Basis of the Scott TopAugmentation of T by CANTOR_1:2; then A13: sigma T is prebasis of the Scott TopAugmentation of T by YELLOW_9:27; A14: the carrier of the Scott TopAugmentation of T in sigma T by A12, PRE_TOPC:def_1; K c= O proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in K or a in O ) assume a in K ; ::_thesis: a in O then consider x being Element of the correct lower TopAugmentation of T such that A15: a = (uparrow x) ` ; reconsider y = x as Element of T by A1; a = ([#] T) \ (uparrow y) by A1, A15, WAYBEL_0:13; hence a in O by A11, A14; ::_thesis: verum end; then A16: (sigma T) \/ K c= (sigma T) \/ O by XBOOLE_1:9; T is TopAugmentation of T by YELLOW_9:44; then T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29; hence (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T by A13, A1, A11, Th23, A16, A10, Th22; ::_thesis: verum end; theorem :: WAYBEL19:32 for T being complete Lawson TopLattice holds { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T proof let T be complete Lawson TopLattice; ::_thesis: { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T set R = the correct lower TopAugmentation of T; reconsider B2 = { ((uparrow F) `) where F is Subset of the correct lower TopAugmentation of T : F is finite } as Basis of the correct lower TopAugmentation of T by Th7; set Z = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ; set S = the Scott TopAugmentation of T; A1: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51; then reconsider B1 = sigma T as Basis of the Scott TopAugmentation of T by CANTOR_1:2; A2: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; B1 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } proof set F9 = {} the correct lower TopAugmentation of T; reconsider G = {} the correct lower TopAugmentation of T as Subset of T by A2; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B1 or x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ) assume A3: x in B1 ; ::_thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } then reconsider x9 = x as Subset of T ; uparrow G = uparrow ({} the correct lower TopAugmentation of T) ; then x9 \ (uparrow G) = x9 ; hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A3; ::_thesis: verum end; then A4: B1 \/ { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by XBOOLE_1:12; A5: INTERSECTION (B1,B2) = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } c= INTERSECTION (B1,B2) let x be set ; ::_thesis: ( x in INTERSECTION (B1,B2) implies x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ) assume x in INTERSECTION (B1,B2) ; ::_thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } then consider y, z being set such that A6: y in B1 and A7: z in B2 and A8: x = y /\ z by SETFAM_1:def_5; reconsider y = y as Subset of T by A6; A9: ([#] T) /\ y = y by XBOOLE_1:28; consider F being Subset of the correct lower TopAugmentation of T such that A10: z = (uparrow F) ` and A11: F is finite by A7; reconsider G = F as Subset of T by A2; z = (uparrow G) ` by A2, A10, WAYBEL_0:13; then x = y \ (uparrow G) by A9, A8, XBOOLE_1:49; hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A6, A11; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } or x in INTERSECTION (B1,B2) ) assume x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ; ::_thesis: x in INTERSECTION (B1,B2) then consider W, F being Subset of T such that A12: x = W \ (uparrow F) and A13: W in sigma T and A14: F is finite ; W /\ ([#] T) = W by XBOOLE_1:28; then A15: x = W /\ (([#] T) \ (uparrow F)) by A12, XBOOLE_1:49; reconsider G = F as Subset of the correct lower TopAugmentation of T by A2; A16: (uparrow G) ` in B2 by A14; (uparrow F) ` = (uparrow G) ` by A2, WAYBEL_0:13; hence x in INTERSECTION (B1,B2) by A16, A13, A15, SETFAM_1:def_5; ::_thesis: verum end; A17: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; B2 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B2 or x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ) assume x in B2 ; ::_thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } then consider F being Subset of the correct lower TopAugmentation of T such that A18: x = (uparrow F) ` and A19: F is finite ; A20: the carrier of the Scott TopAugmentation of T in B1 by A1, PRE_TOPC:def_1; reconsider G = F as Subset of T by A2; uparrow F = uparrow G by A2, WAYBEL_0:13; hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A17, A20, A2, A18, A19; ::_thesis: verum end; then A21: B2 \/ { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by XBOOLE_1:12; T is TopAugmentation of T by YELLOW_9:44; then T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29; then (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T by YELLOW_9:59; hence { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T by A4, A5, A21, XBOOLE_1:4; ::_thesis: verum end; definition let T be complete LATTICE; func lambda T -> Subset-Family of T means :Def4: :: WAYBEL19:def 4 for S being correct Lawson TopAugmentation of T holds it = the topology of S; uniqueness for b1, b2 being Subset-Family of T st ( for S being correct Lawson TopAugmentation of T holds b1 = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds b2 = the topology of S ) holds b1 = b2 proof set S = the correct Lawson TopAugmentation of T; let L1, L2 be Subset-Family of T; ::_thesis: ( ( for S being correct Lawson TopAugmentation of T holds L1 = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds L2 = the topology of S ) implies L1 = L2 ) assume for S being correct Lawson TopAugmentation of T holds L1 = the topology of S ; ::_thesis: ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 ) then L1 = the topology of the correct Lawson TopAugmentation of T ; hence ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 ) ; ::_thesis: verum end; existence ex b1 being Subset-Family of T st for S being correct Lawson TopAugmentation of T holds b1 = the topology of S proof set S = the correct Lawson TopAugmentation of T; A1: RelStr(# the carrier of the correct Lawson TopAugmentation of T, the InternalRel of the correct Lawson TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider t = the topology of the correct Lawson TopAugmentation of T as Subset-Family of T ; take t ; ::_thesis: for S being correct Lawson TopAugmentation of T holds t = the topology of S let S9 be correct Lawson TopAugmentation of T; ::_thesis: t = the topology of S9 A2: RelStr(# the carrier of S9, the InternalRel of S9 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then A3: sigma S9 = sigma the correct Lawson TopAugmentation of T by A1, YELLOW_9:52; (omega S9) \/ (sigma S9) is prebasis of S9 by Def3; then A4: FinMeetCl ((omega S9) \/ (sigma S9)) is Basis of S9 by YELLOW_9:23; A5: omega S9 = omega the correct Lawson TopAugmentation of T by A2, A1, Th3; (omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T) is prebasis of the correct Lawson TopAugmentation of T by Def3; then FinMeetCl ((omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T)) is Basis of the correct Lawson TopAugmentation of T by YELLOW_9:23; hence t = UniCl (FinMeetCl ((omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T))) by YELLOW_9:22 .= the topology of S9 by A1, A2, A5, A3, A4, YELLOW_9:22 ; ::_thesis: verum end; end; :: deftheorem Def4 defines lambda WAYBEL19:def_4_:_ for T being complete LATTICE for b2 being Subset-Family of T holds ( b2 = lambda T iff for S being correct Lawson TopAugmentation of T holds b2 = the topology of S ); theorem Th33: :: WAYBEL19:33 for R being complete LATTICE holds lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) proof let R be complete LATTICE; ::_thesis: lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) set S = the correct Lawson TopAugmentation of R; A1: RelStr(# the carrier of the correct Lawson TopAugmentation of R, the InternalRel of the correct Lawson TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then A2: sigma R = sigma the correct Lawson TopAugmentation of R by YELLOW_9:52; (omega the correct Lawson TopAugmentation of R) \/ (sigma the correct Lawson TopAugmentation of R) is prebasis of the correct Lawson TopAugmentation of R by Def3; then FinMeetCl ((omega the correct Lawson TopAugmentation of R) \/ (sigma the correct Lawson TopAugmentation of R)) is Basis of the correct Lawson TopAugmentation of R by YELLOW_9:23; then A3: the topology of the correct Lawson TopAugmentation of R = UniCl (FinMeetCl ((omega the correct Lawson TopAugmentation of R) \/ (sigma the correct Lawson TopAugmentation of R))) by YELLOW_9:22; omega R = omega the correct Lawson TopAugmentation of R by A1, Th3; hence lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) by A3, A1, A2, Def4; ::_thesis: verum end; theorem :: WAYBEL19:34 for R being complete LATTICE for T being correct lower TopAugmentation of R for S being correct Scott TopAugmentation of R for M being Refinement of S,T holds lambda R = the topology of M proof let R be complete LATTICE; ::_thesis: for T being correct lower TopAugmentation of R for S being correct Scott TopAugmentation of R for M being Refinement of S,T holds lambda R = the topology of M let T be correct lower TopAugmentation of R; ::_thesis: for S being correct Scott TopAugmentation of R for M being Refinement of S,T holds lambda R = the topology of M let S be correct Scott TopAugmentation of R; ::_thesis: for M being Refinement of S,T holds lambda R = the topology of M let M be Refinement of S,T; ::_thesis: lambda R = the topology of M A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; A2: the carrier of R \/ the carrier of R = the carrier of R ; RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; then A3: the carrier of M = the carrier of R by A2, A1, YELLOW_9:def_6; A4: sigma R = the topology of S by YELLOW_9:51; omega R = the topology of T by Def2; then (sigma R) \/ (omega R) is prebasis of M by A4, YELLOW_9:def_6; then A5: FinMeetCl ((sigma R) \/ (omega R)) is Basis of M by A3, YELLOW_9:23; thus lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) by Th33 .= the topology of M by A3, A5, YELLOW_9:22 ; ::_thesis: verum end; Lm2: for T being LATTICE for F being Subset-Family of T st ( for A being Subset of T st A in F holds A is property(S) ) holds union F is property(S) proof let T be LATTICE; ::_thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds A is property(S) ) holds union F is property(S) let F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T st A in F holds A is property(S) ) implies union F is property(S) ) assume A1: for A being Subset of T st A in F holds A is property(S) ; ::_thesis: union F is property(S) let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in union F or ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in union F ) ) ) ) assume sup D in union F ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in union F ) ) ) then consider A being set such that A2: sup D in A and A3: A in F by TARSKI:def_4; reconsider A = A as Subset of T by A3; A is property(S) by A1, A3; then consider y being Element of T such that A4: y in D and A5: for x being Element of T st x in D & x >= y holds x in A by A2, WAYBEL11:def_3; take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in union F ) ) ) thus y in D by A4; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in union F ) let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in union F ) assume that A6: x in D and A7: x >= y ; ::_thesis: x in union F x in A by A6, A7, A5; hence x in union F by A3, TARSKI:def_4; ::_thesis: verum end; Lm3: for T being LATTICE for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds A1 /\ A2 is property(S) proof let T be LATTICE; ::_thesis: for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds A1 /\ A2 is property(S) let A1, A2 be Subset of T; ::_thesis: ( A1 is property(S) & A2 is property(S) implies A1 /\ A2 is property(S) ) assume that A1: for D being non empty directed Subset of T st sup D in A1 holds ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in A1 ) ) and A2: for D being non empty directed Subset of T st sup D in A2 holds ex y being Element of T st ( y in D & ( for x being Element of T st x in D & x >= y holds x in A2 ) ) ; :: according to WAYBEL11:def_3 ::_thesis: A1 /\ A2 is property(S) let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in A1 /\ A2 or ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in A1 /\ A2 ) ) ) ) assume A3: sup D in A1 /\ A2 ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in A1 /\ A2 ) ) ) then sup D in A1 by XBOOLE_0:def_4; then consider y1 being Element of T such that A4: y1 in D and A5: for x being Element of T st x in D & x >= y1 holds x in A1 by A1; sup D in A2 by A3, XBOOLE_0:def_4; then consider y2 being Element of T such that A6: y2 in D and A7: for x being Element of T st x in D & x >= y2 holds x in A2 by A2; consider y being Element of T such that A8: y in D and A9: y1 <= y and A10: y2 <= y by A4, A6, WAYBEL_0:def_1; take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in A1 /\ A2 ) ) ) thus y in D by A8; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in A1 /\ A2 ) let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in A1 /\ A2 ) assume that A11: x in D and A12: x >= y ; ::_thesis: x in A1 /\ A2 A13: x in A2 by A12, A10, A7, A11, ORDERS_2:3; x in A1 by A12, A9, A5, A11, ORDERS_2:3; hence x in A1 /\ A2 by A13, XBOOLE_0:def_4; ::_thesis: verum end; Lm4: for T being LATTICE holds [#] T is property(S) proof let T be LATTICE; ::_thesis: [#] T is property(S) let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in [#] T or ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in [#] T ) ) ) ) assume sup D in [#] T ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in [#] T ) ) ) set y = the Element of D; reconsider y = the Element of D as Element of T ; take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in [#] T ) ) ) thus ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in [#] T ) ) ) ; ::_thesis: verum end; theorem Th35: :: WAYBEL19:35 for T being up-complete lower TopLattice for A being Subset of T st A is open holds A is property(S) proof let T be up-complete lower TopLattice; ::_thesis: for A being Subset of T st A is open holds A is property(S) defpred S1[ Subset of T] means \$1 is property(S) ; A1: ex K being prebasis of T st for A being Subset of T st A in K holds S1[A] proof reconsider K = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1; take K ; ::_thesis: for A being Subset of T st A in K holds S1[A] let A be Subset of T; ::_thesis: ( A in K implies S1[A] ) assume A in K ; ::_thesis: S1[A] then consider x being Element of T such that A2: A = (uparrow x) ` ; let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in A or ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in A ) ) ) ) assume A3: sup D in A ; ::_thesis: ex b1 being Element of the carrier of T st ( b1 in D & ( for b2 being Element of the carrier of T holds ( not b2 in D or not b1 <= b2 or b2 in A ) ) ) set y = the Element of D; reconsider y = the Element of D as Element of T ; take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in A ) ) ) thus y in D ; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 in D or not y <= b1 or b1 in A ) let z be Element of T; ::_thesis: ( not z in D or not y <= z or z in A ) assume that A4: z in D and z >= y and A5: not z in A ; ::_thesis: contradiction A6: z >= x by A5, A2, YELLOW_9:1; not x <= sup D by A3, A2, YELLOW_9:1; then A7: not z <= sup D by A6, ORDERS_2:3; A8: ex_sup_of D,T by WAYBEL_0:75; A9: ex_sup_of {z},T by YELLOW_0:38; {z} c= D by A4, ZFMISC_1:31; then sup {z} <= sup D by A8, A9, YELLOW_0:34; hence contradiction by A7, YELLOW_0:39; ::_thesis: verum end; A10: for A1, A2 being Subset of T st S1[A1] & S1[A2] holds S1[A1 /\ A2] by Lm3; A11: S1[ [#] T] by Lm4; A12: for F being Subset-Family of T st ( for A being Subset of T st A in F holds S1[A] ) holds S1[ union F] by Lm2; thus for A being Subset of T st A is open holds S1[A] from WAYBEL19:sch_1(A1, A12, A10, A11); ::_thesis: verum end; theorem Th36: :: WAYBEL19:36 for T being complete Lawson TopLattice for A being Subset of T st A is open holds A is property(S) proof let T be complete Lawson TopLattice; ::_thesis: for A being Subset of T st A is open holds A is property(S) defpred S1[ Subset of T] means \$1 is property(S) ; set S = the Scott TopAugmentation of T; set R = the correct lower TopAugmentation of T; A1: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; A3: ex K being prebasis of T st for A being Subset of T st A in K holds S1[A] proof reconsider K = (sigma T) \/ (omega T) as prebasis of T by Def3; take K ; ::_thesis: for A being Subset of T st A in K holds S1[A] let A be Subset of T; ::_thesis: ( A in K implies S1[A] ) reconsider AS = A as Subset of the Scott TopAugmentation of T by A2; reconsider AR = A as Subset of the correct lower TopAugmentation of T by A1; assume A in K ; ::_thesis: S1[A] then ( ( A in sigma T & sigma T = the topology of the Scott TopAugmentation of T ) or ( A in omega T & omega T = the topology of the correct lower TopAugmentation of T ) ) by Def2, XBOOLE_0:def_3, YELLOW_9:51; then ( AS is open or AR is open ) by PRE_TOPC:def_2; then ( AS is property(S) or AR is property(S) ) by Th35, WAYBEL11:15; hence S1[A] by A2, A1, YELLOW12:19; ::_thesis: verum end; A4: S1[ [#] T] ; A5: for A1, A2 being Subset of T st S1[A1] & S1[A2] holds S1[A1 /\ A2] by Lm3; A6: for F being Subset-Family of T st ( for A being Subset of T st A in F holds S1[A] ) holds S1[ union F] by Lm2; thus for A being Subset of T st A is open holds S1[A] from WAYBEL19:sch_1(A3, A6, A5, A4); ::_thesis: verum end; theorem Th37: :: WAYBEL19:37 for S being complete Scott TopLattice for T being correct Lawson TopAugmentation of S for A being Subset of S st A is open holds for C being Subset of T st C = A holds C is open proof let S be complete Scott TopLattice; ::_thesis: for T being correct Lawson TopAugmentation of S for A being Subset of S st A is open holds for C being Subset of T st C = A holds C is open let T be correct Lawson TopAugmentation of S; ::_thesis: for A being Subset of S st A is open holds for C being Subset of T st C = A holds C is open let A be Subset of S; ::_thesis: ( A is open implies for C being Subset of T st C = A holds C is open ) assume A1: A in the topology of S ; :: according to PRE_TOPC:def_2 ::_thesis: for C being Subset of T st C = A holds C is open let C be Subset of T; ::_thesis: ( C = A implies C is open ) assume A2: C = A ; ::_thesis: C is open (sigma T) \/ (omega T) is prebasis of T by Def3; then A3: (sigma T) \/ (omega T) c= the topology of T by TOPS_2:64; RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then S is Scott TopAugmentation of T by YELLOW_9:def_4; then A in sigma T by A1, YELLOW_9:51; then C in (sigma T) \/ (omega T) by A2, XBOOLE_0:def_3; hence C in the topology of T by A3; :: according to PRE_TOPC:def_2 ::_thesis: verum end; theorem Th38: :: WAYBEL19:38 for T being complete Lawson TopLattice for x being Element of T holds ( uparrow x is closed & downarrow x is closed & {x} is closed ) proof let T be complete Lawson TopLattice; ::_thesis: for x being Element of T holds ( uparrow x is closed & downarrow x is closed & {x} is closed ) set S = the Scott TopAugmentation of T; set R = the correct lower TopAugmentation of T; let x be Element of T; ::_thesis: ( uparrow x is closed & downarrow x is closed & {x} is closed ) A1: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider y = x as Element of the Scott TopAugmentation of T ; A2: downarrow y is closed by WAYBEL11:11; T is TopAugmentation of T by YELLOW_9:44; then A3: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29; A4: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider z = x as Element of the correct lower TopAugmentation of T ; A5: uparrow z = uparrow x by A4, WAYBEL_0:13; downarrow y = downarrow x by A1, WAYBEL_0:13; hence ( uparrow x is closed & downarrow x is closed ) by A2, A5, Th4, A1, A4, A3, Th21; ::_thesis: {x} is closed then (uparrow x) /\ (downarrow x) is closed ; hence {x} is closed by Th28; ::_thesis: verum end; theorem Th39: :: WAYBEL19:39 for T being complete Lawson TopLattice for x being Element of T holds ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) proof let T be complete Lawson TopLattice; ::_thesis: for x being Element of T holds ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) let x be Element of T; ::_thesis: ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) A1: downarrow x is closed by Th38; A2: {x} is closed by Th38; uparrow x is closed by Th38; hence ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) by A1, A2; ::_thesis: verum end; theorem Th40: :: WAYBEL19:40 for T being complete continuous Lawson TopLattice for x being Element of T holds ( wayabove x is open & (wayabove x) ` is closed ) proof let T be complete continuous Lawson TopLattice; ::_thesis: for x being Element of T holds ( wayabove x is open & (wayabove x) ` is closed ) let x be Element of T; ::_thesis: ( wayabove x is open & (wayabove x) ` is closed ) set S = the Scott TopAugmentation of T; A1: T is TopAugmentation of the Scott TopAugmentation of T by YELLOW_9:45; A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider v = x as Element of the Scott TopAugmentation of T ; wayabove v is open by WAYBEL11:36; hence wayabove x is open by A2, A1, Th37, YELLOW12:13; ::_thesis: (wayabove x) ` is closed hence (wayabove x) ` is closed ; ::_thesis: verum end; theorem :: WAYBEL19:41 for S being complete Scott TopLattice for T being correct Lawson TopAugmentation of S for A being upper Subset of T st A is open holds for C being Subset of S st C = A holds C is open proof let S be complete Scott TopLattice; ::_thesis: for T being correct Lawson TopAugmentation of S for A being upper Subset of T st A is open holds for C being Subset of S st C = A holds C is open let T be correct Lawson TopAugmentation of S; ::_thesis: for A being upper Subset of T st A is open holds for C being Subset of S st C = A holds C is open let A be upper Subset of T; ::_thesis: ( A is open implies for C being Subset of S st C = A holds C is open ) assume A1: A is open ; ::_thesis: for C being Subset of S st C = A holds C is open let C be Subset of S; ::_thesis: ( C = A implies C is open ) A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; assume C = A ; ::_thesis: C is open then ( C is upper & C is property(S) ) by A1, Th36, A2, WAYBEL_0:25, YELLOW12:19; hence C is open by WAYBEL11:15; ::_thesis: verum end; theorem :: WAYBEL19:42 for T being complete Lawson TopLattice for A being lower Subset of T holds ( A is closed iff A is closed_under_directed_sups ) proof let T be complete Lawson TopLattice; ::_thesis: for A being lower Subset of T holds ( A is closed iff A is closed_under_directed_sups ) let A be lower Subset of T; ::_thesis: ( A is closed iff A is closed_under_directed_sups ) set S = the Scott TopAugmentation of T; hereby ::_thesis: ( A is closed_under_directed_sups implies A is closed ) assume A is closed ; ::_thesis: A is directly_closed then A ` is open ; then reconsider mA = A ` as property(S) Subset of T by Th36; mA ` = A ; hence A is directly_closed ; ::_thesis: verum end; assume A is directly_closed ; ::_thesis: A is closed then reconsider dA = A as lower directly_closed Subset of T ; A1: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; then reconsider mA = dA ` as Subset of the Scott TopAugmentation of T ; ( mA is upper & mA is inaccessible ) by A1, WAYBEL_0:25, YELLOW_9:47; then A2: mA is open by WAYBEL11:def_4; T is TopAugmentation of the Scott TopAugmentation of T by A1, YELLOW_9:def_4; then dA ` is open by A2, Th37; hence A is closed by TOPS_1:3; ::_thesis: verum end; theorem :: WAYBEL19:43 for T being complete Lawson TopLattice for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)} proof let T be complete Lawson TopLattice; ::_thesis: for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)} reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Th30; set S = the Scott TopAugmentation of T; let F be non empty filtered Subset of T; ::_thesis: Lim (F opp+id) = {(inf F)} set N = F opp+id ; A1: the carrier of (F opp+id) = F by YELLOW_9:7; A2: F opp+id is full SubRelStr of T opp by YELLOW_9:7; thus Lim (F opp+id) c= {(inf F)} :: according to XBOOLE_0:def_10 ::_thesis: {(inf F)} c= Lim (F opp+id) proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Lim (F opp+id) or p in {(inf F)} ) assume A3: p in Lim (F opp+id) ; ::_thesis: p in {(inf F)} then reconsider p = p as Element of T ; the mapping of (F opp+id) = id F by Th27; then rng the mapping of (F opp+id) = F by RELAT_1:45; then A4: p in Cl F by A3, WAYBEL_9:24; p is_<=_than F proof let u be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not u in F or p <= u ) assume A5: u in F ; ::_thesis: p <= u A6: F opp+id is_eventually_in downarrow u proof reconsider i = u as Element of (F opp+id) by A5, YELLOW_9:7; take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds ( not i <= b1 or (F opp+id) . b1 in downarrow u ) let j be Element of (F opp+id); ::_thesis: ( not i <= j or (F opp+id) . j in downarrow u ) j in F by A1; then reconsider z = j as Element of T ; assume j >= i ; ::_thesis: (F opp+id) . j in downarrow u then z ~ >= u ~ by A2, YELLOW_0:59; then z <= u by LATTICE3:9; then z in downarrow u by WAYBEL_0:17; hence (F opp+id) . j in downarrow u by YELLOW_9:7; ::_thesis: verum end; downarrow u is closed by Th38; then Cl (downarrow u) = downarrow u by PRE_TOPC:22; then Lim (F opp+id) c= downarrow u by A6, Th26; hence p <= u by A3, WAYBEL_0:17; ::_thesis: verum end; then A7: p <= inf F by YELLOW_0:33; inf F is_<=_than F by YELLOW_0:33; then A8: F c= uparrow (inf F) by YELLOW_2:2; uparrow (inf F) is closed by Th38; then Cl (uparrow (inf F)) = uparrow (inf F) by PRE_TOPC:22; then Cl F c= uparrow (inf F) by A8, PRE_TOPC:19; then p >= inf F by A4, WAYBEL_0:18; then p = inf F by A7, ORDERS_2:2; hence p in {(inf F)} by TARSKI:def_1; ::_thesis: verum end; A9: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51; A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; now__::_thesis:_for_A_being_Subset_of_T_st_inf_F_in_A_&_A_in_K_holds_ F_opp+id_is_eventually_in_A let A be Subset of T; ::_thesis: ( inf F in A & A in K implies F opp+id is_eventually_in b1 ) assume that A11: inf F in A and A12: A in K ; ::_thesis: F opp+id is_eventually_in b1 percases ( A in sigma T or A in { ((uparrow x) `) where x is Element of T : verum } ) by A12, XBOOLE_0:def_3; supposeA13: A in sigma T ; ::_thesis: F opp+id is_eventually_in b1 then reconsider a = A as Subset of the Scott TopAugmentation of T by A9; set i = the Element of (F opp+id); a is open by A9, A13, PRE_TOPC:def_2; then a is upper by WAYBEL11:def_4; then A14: A is upper by A10, WAYBEL_0:25; thus F opp+id is_eventually_in A ::_thesis: verum proof take the Element of (F opp+id) ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds ( not the Element of (F opp+id) <= b1 or (F opp+id) . b1 in A ) let j be Element of (F opp+id); ::_thesis: ( not the Element of (F opp+id) <= j or (F opp+id) . j in A ) j in F by A1; then reconsider z = j as Element of T ; z >= inf F by A1, YELLOW_2:22; then z in A by A11, A14, WAYBEL_0:def_20; hence ( not the Element of (F opp+id) <= j or (F opp+id) . j in A ) by YELLOW_9:7; ::_thesis: verum end; end; suppose A in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: F opp+id is_eventually_in b1 then consider x being Element of T such that A15: A = (uparrow x) ` ; not inf F >= x by A11, A15, YELLOW_9:1; then not F is_>=_than x by YELLOW_0:33; then consider y being Element of T such that A16: y in F and A17: not y >= x by LATTICE3:def_8; thus F opp+id is_eventually_in A ::_thesis: verum proof reconsider i = y as Element of (F opp+id) by A16, YELLOW_9:7; take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds ( not i <= b1 or (F opp+id) . b1 in A ) let j be Element of (F opp+id); ::_thesis: ( not i <= j or (F opp+id) . j in A ) j in F by A1; then reconsider z = j as Element of T ; assume j >= i ; ::_thesis: (F opp+id) . j in A then z ~ >= y ~ by A2, YELLOW_0:59; then z <= y by LATTICE3:9; then not z >= x by A17, ORDERS_2:3; then z in A by A15, YELLOW_9:1; hence (F opp+id) . j in A by YELLOW_9:7; ::_thesis: verum end; end; end; end; then inf F in Lim (F opp+id) by Th25; hence {(inf F)} c= Lim (F opp+id) by ZFMISC_1:31; ::_thesis: verum end; registration cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson -> T_1 complete compact for TopRelStr ; coherence for b1 being complete TopLattice st b1 is Lawson holds ( b1 is T_1 & b1 is compact ) proof let T be complete TopLattice; ::_thesis: ( T is Lawson implies ( T is T_1 & T is compact ) ) assume A1: T is Lawson ; ::_thesis: ( T is T_1 & T is compact ) for x being Point of T holds {x} is closed by A1, Th38; hence T is T_1 by URYSOHN1:19; ::_thesis: T is compact set O1 = sigma T; set O2 = { ((uparrow x) `) where x is Element of T : verum } ; reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by A1, Th30; set S = the Scott TopAugmentation of T; the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1; then reconsider X = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:def_1; A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; for F being Subset of K st X c= union F holds ex G being finite Subset of F st X c= union G proof deffunc H1( Element of T) -> Element of bool the carrier of T = (uparrow c1) ` ; let F be Subset of K; ::_thesis: ( X c= union F implies ex G being finite Subset of F st X c= union G ) set I2 = { x where x is Element of T : (uparrow x) ` in F } ; set x = "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T); A3: { x where x is Element of T : (uparrow x) ` in F } c= the carrier of T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x where x is Element of T : (uparrow x) ` in F } or a in the carrier of T ) assume a in { x where x is Element of T : (uparrow x) ` in F } ; ::_thesis: a in the carrier of T then ex x being Element of T st ( a = x & (uparrow x) ` in F ) ; hence a in the carrier of T ; ::_thesis: verum end; reconsider z = "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) as Element of the Scott TopAugmentation of T by A2; assume A4: X c= union F ; ::_thesis: ex G being finite Subset of F st X c= union G "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) in X ; then consider Y being set such that A5: "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) in Y and A6: Y in F by A4, TARSKI:def_4; Y in K by A6; then reconsider I2 = { x where x is Element of T : (uparrow x) ` in F } , Y = Y as Subset of T by A3; reconsider Z = Y, J2 = I2 as Subset of the Scott TopAugmentation of T by A2; now__::_thesis:_Y_in_sigma_T assume not Y in sigma T ; ::_thesis: contradiction then Y in { ((uparrow x) `) where x is Element of T : verum } by A6, XBOOLE_0:def_3; then consider y being Element of T such that A7: Y = (uparrow y) ` ; y in I2 by A6, A7; then y <= "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) by YELLOW_2:22; hence contradiction by A5, A7, YELLOW_9:1; ::_thesis: verum end; then Z in the topology of the Scott TopAugmentation of T by YELLOW_9:51; then A8: Z is open by PRE_TOPC:def_2; then A9: Z is upper by WAYBEL11:15; A10: z = sup J2 by A2, YELLOW_0:17, YELLOW_0:26 .= sup (finsups J2) by WAYBEL_0:55 ; Z is property(S) by A8, WAYBEL11:15; then consider y being Element of the Scott TopAugmentation of T such that A11: y in finsups J2 and A12: for x being Element of the Scott TopAugmentation of T st x in finsups J2 & x >= y holds x in Z by A10, A5, WAYBEL11:def_3; consider a being finite Subset of J2 such that A13: y = "\/" (a, the Scott TopAugmentation of T) and ex_sup_of a, the Scott TopAugmentation of T by A11; set AA = { ((uparrow c) `) where c is Element of T : c in a } ; set G = {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } ; A14: {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } c= F proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } or i in F ) assume that A15: i in {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } and A16: not i in F ; ::_thesis: contradiction ( i in {Y} or i in { ((uparrow c) `) where c is Element of T : c in a } ) by A15, XBOOLE_0:def_3; then consider c being Element of T such that A17: i = (uparrow c) ` and A18: c in a by A6, A16, TARSKI:def_1; c in J2 by A18; then ex c9 being Element of T st ( c = c9 & (uparrow c9) ` in F ) ; hence contradiction by A16, A17; ::_thesis: verum end; A19: a is finite ; { H1(c) where c is Element of T : c in a } is finite from FRAENKEL:sch_21(A19); then reconsider G = {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } as finite Subset of F by A14; take G ; ::_thesis: X c= union G let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in X or u in union G ) assume that A20: u in X and A21: not u in union G ; ::_thesis: contradiction reconsider u = u as Element of the Scott TopAugmentation of T by A20, A2; A22: union G = (union {Y}) \/ (union { ((uparrow c) `) where c is Element of T : c in a } ) by ZFMISC_1:78 .= Y \/ (union { ((uparrow c) `) where c is Element of T : c in a } ) by ZFMISC_1:25 ; then A23: not u in Y by A21, XBOOLE_0:def_3; A24: not u in union { ((uparrow c) `) where c is Element of T : c in a } by A22, A21, XBOOLE_0:def_3; A25: ( y <= y & u is_>=_than a ) proof thus y <= y ; ::_thesis: u is_>=_than a let v be Element of the Scott TopAugmentation of T; :: according to LATTICE3:def_9 ::_thesis: ( not v in a or v <= u ) assume A26: v in a ; ::_thesis: v <= u then v in J2 ; then consider c being Element of T such that A27: v = c and (uparrow c) ` in F ; (uparrow c) ` in { ((uparrow c) `) where c is Element of T : c in a } by A26, A27; then A28: not u in (uparrow c) ` by A24, TARSKI:def_4; (uparrow c) ` = (uparrow v) ` by A2, A27, WAYBEL_0:13; hence v <= u by A28, YELLOW_9:1; ::_thesis: verum end; then A29: u >= y by A13, YELLOW_0:32; y in Z by A25, A11, A12; hence contradiction by A29, A9, A23, WAYBEL_0:def_20; ::_thesis: verum end; then X << X by WAYBEL_7:31; then X is compact by WAYBEL_3:def_2; hence T is compact by WAYBEL_3:37; ::_thesis: verum end; end; registration cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete continuous Lawson -> Hausdorff complete continuous for TopRelStr ; coherence for b1 being complete continuous TopLattice st b1 is Lawson holds b1 is Hausdorff proof let T be complete continuous TopLattice; ::_thesis: ( T is Lawson implies T is Hausdorff ) assume A1: T is Lawson ; ::_thesis: T is Hausdorff let x, y be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( x = y or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 ) ) assume A2: x <> y ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 ) reconsider x9 = x, y9 = y as Element of T ; A3: for x being Element of T holds ( not waybelow x is empty & waybelow x is directed ) ; percases ( not y9 <= x9 or not x9 <= y9 ) by A2, ORDERS_2:2; suppose not y9 <= x9 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 ) then consider u being Element of T such that A4: u << y9 and A5: not u <= x9 by A3, WAYBEL_3:24; take V = (uparrow u) ` ; ::_thesis: ex b1 being Element of bool the carrier of T st ( V is open & b1 is open & x in V & y in b1 & V misses b1 ) take W = wayabove u; ::_thesis: ( V is open & W is open & x in V & y in W & V misses W ) thus ( V is open & W is open ) by A1, Th39, Th40; ::_thesis: ( x in V & y in W & V misses W ) thus x in V by A5, YELLOW_9:1; ::_thesis: ( y in W & V misses W ) thus y in W by A4; ::_thesis: V misses W A6: V ` = uparrow u ; W c= uparrow u by WAYBEL_3:11; hence V misses W by A6, SUBSET_1:23; ::_thesis: verum end; suppose not x9 <= y9 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 ) then consider u being Element of T such that A7: u << x9 and A8: not u <= y9 by A3, WAYBEL_3:24; take W = wayabove u; ::_thesis: ex b1 being Element of bool the carrier of T st ( W is open & b1 is open & x in W & y in b1 & W misses b1 ) take V = (uparrow u) ` ; ::_thesis: ( W is open & V is open & x in W & y in V & W misses V ) thus ( W is open & V is open ) by A1, Th39, Th40; ::_thesis: ( x in W & y in V & W misses V ) thus x in W by A7; ::_thesis: ( y in V & W misses V ) thus y in V by A8, YELLOW_9:1; ::_thesis: W misses V A9: V ` = uparrow u ; W c= uparrow u by WAYBEL_3:11; hence W misses V by A9, SUBSET_1:23; ::_thesis: verum end; end; end; end;