:: WAYBEL30 semantic presentation begin theorem Th1: :: WAYBEL30:1 for x being set for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum } proof let x be set ; ::_thesis: for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum } let D be non empty set ; ::_thesis: x /\ (union D) = union { (x /\ d) where d is Element of D : verum } hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (x /\ d) where d is Element of D : verum } c= x /\ (union D) let a be set ; ::_thesis: ( a in x /\ (union D) implies a in union { (x /\ d) where d is Element of D : verum } ) assume A1: a in x /\ (union D) ; ::_thesis: a in union { (x /\ d) where d is Element of D : verum } then a in union D by XBOOLE_0:def_4; then consider Z being set such that A2: a in Z and A3: Z in D by TARSKI:def_4; A4: x /\ Z in { (x /\ d) where d is Element of D : verum } by A3; a in x by A1, XBOOLE_0:def_4; then a in x /\ Z by A2, XBOOLE_0:def_4; hence a in union { (x /\ d) where d is Element of D : verum } by A4, TARSKI:def_4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (x /\ d) where d is Element of D : verum } or a in x /\ (union D) ) assume a in union { (x /\ d) where d is Element of D : verum } ; ::_thesis: a in x /\ (union D) then consider Z being set such that A5: a in Z and A6: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def_4; consider d being Element of D such that A7: Z = x /\ d and verum by A6; a in d by A5, A7, XBOOLE_0:def_4; then A8: a in union D by TARSKI:def_4; a in x by A5, A7, XBOOLE_0:def_4; hence a in x /\ (union D) by A8, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th2: :: WAYBEL30:2 for R being non empty reflexive transitive RelStr for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R proof let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: union D is Ideal of R set d = the Element of D; D c= the carrier of (InclPoset (Ids R)) ; then A1: D c= Ids R by YELLOW_1:1; A2: D c= bool the carrier of R proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in D or d in bool the carrier of R ) assume d in D ; ::_thesis: d in bool the carrier of R then d in Ids R by A1; then ex I being Ideal of R st d = I ; hence d in bool the carrier of R ; ::_thesis: verum end; the Element of D in D ; then the Element of D in Ids R by A1; then consider I being Ideal of R such that A3: the Element of D = I and verum ; A4: for X being Subset of R st X in D holds X is directed proof let X be Subset of R; ::_thesis: ( X in D implies X is directed ) assume X in D ; ::_thesis: X is directed then X in Ids R by A1; then ex I being Ideal of R st X = I ; hence X is directed ; ::_thesis: verum end; A5: for X, Y being Subset of R st X in D & Y in D holds ex Z being Subset of R st ( Z in D & X \/ Y c= Z ) proof let X, Y be Subset of R; ::_thesis: ( X in D & Y in D implies ex Z being Subset of R st ( Z in D & X \/ Y c= Z ) ) assume that A6: X in D and A7: Y in D ; ::_thesis: ex Z being Subset of R st ( Z in D & X \/ Y c= Z ) reconsider X1 = X, Y1 = Y as Element of (InclPoset (Ids R)) by A6, A7; consider Z1 being Element of (InclPoset (Ids R)) such that A8: Z1 in D and A9: X1 <= Z1 and A10: Y1 <= Z1 by A6, A7, WAYBEL_0:def_1; Z1 in Ids R by A1, A8; then ex I being Ideal of R st Z1 = I ; then reconsider Z = Z1 as Subset of R ; take Z ; ::_thesis: ( Z in D & X \/ Y c= Z ) thus Z in D by A8; ::_thesis: X \/ Y c= Z A11: Y1 c= Z1 by A10, YELLOW_1:3; X1 c= Z1 by A9, YELLOW_1:3; hence X \/ Y c= Z by A11, XBOOLE_1:8; ::_thesis: verum end; A12: for X being Subset of R st X in D holds X is lower proof let X be Subset of R; ::_thesis: ( X in D implies X is lower ) assume X in D ; ::_thesis: X is lower then X in Ids R by A1; then ex I being Ideal of R st X = I ; hence X is lower ; ::_thesis: verum end; set i = the Element of I; the Element of I in the Element of D by A3; hence union D is Ideal of R by A12, A2, A4, A5, TARSKI:def_4, WAYBEL_0:26, WAYBEL_0:46; ::_thesis: verum end; Lm1: now__::_thesis:_for_R_being_non_empty_reflexive_transitive_RelStr_ for_D_being_non_empty_directed_Subset_of_(InclPoset_(Ids_R)) for_UD_being_Element_of_(InclPoset_(Ids_R))_st_UD_=_union_D_holds_ D_is_<=_than_UD let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) for UD being Element of (InclPoset (Ids R)) st UD = union D holds D is_<=_than UD let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds D is_<=_than UD let UD be Element of (InclPoset (Ids R)); ::_thesis: ( UD = union D implies D is_<=_than UD ) assume A1: UD = union D ; ::_thesis: D is_<=_than UD thus D is_<=_than UD ::_thesis: verum proof let d be Element of (InclPoset (Ids R)); :: according to LATTICE3:def_9 ::_thesis: ( not d in D or d <= UD ) assume A2: d in D ; ::_thesis: d <= UD d c= UD proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in d or a in UD ) assume a in d ; ::_thesis: a in UD hence a in UD by A1, A2, TARSKI:def_4; ::_thesis: verum end; hence d <= UD by YELLOW_1:3; ::_thesis: verum end; end; Lm2: now__::_thesis:_for_R_being_non_empty_reflexive_transitive_RelStr_ for_D_being_non_empty_directed_Subset_of_(InclPoset_(Ids_R)) for_UD_being_Element_of_(InclPoset_(Ids_R))_st_UD_=_union_D_holds_ for_b_being_Element_of_(InclPoset_(Ids_R))_st_b_is_>=_than_D_holds_ UD_<=_b let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) for UD being Element of (InclPoset (Ids R)) st UD = union D holds for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds UD <= b let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds UD <= b let UD be Element of (InclPoset (Ids R)); ::_thesis: ( UD = union D implies for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds UD <= b ) assume A1: UD = union D ; ::_thesis: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds UD <= b thus for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds UD <= b ::_thesis: verum proof let b be Element of (InclPoset (Ids R)); ::_thesis: ( b is_>=_than D implies UD <= b ) assume A2: for a being Element of (InclPoset (Ids R)) st a in D holds b >= a ; :: according to LATTICE3:def_9 ::_thesis: UD <= b UD c= b proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UD or x in b ) assume x in UD ; ::_thesis: x in b then consider Z being set such that A3: x in Z and A4: Z in D by A1, TARSKI:def_4; reconsider Z = Z as Element of (InclPoset (Ids R)) by A4; b >= Z by A2, A4; then Z c= b by YELLOW_1:3; hence x in b by A3; ::_thesis: verum end; hence UD <= b by YELLOW_1:3; ::_thesis: verum end; end; registration let R be non empty reflexive transitive RelStr ; cluster InclPoset (Ids R) -> up-complete ; coherence InclPoset (Ids R) is up-complete proof set I = InclPoset (Ids R); let D be non empty directed Subset of (InclPoset (Ids R)); :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids R)) st ( D is_<=_than b1 & ( for b2 being Element of the carrier of (InclPoset (Ids R)) holds ( not D is_<=_than b2 or b1 <= b2 ) ) ) reconsider UD = union D as Ideal of R by Th2; UD in Ids R ; then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1; take UD ; ::_thesis: ( D is_<=_than UD & ( for b1 being Element of the carrier of (InclPoset (Ids R)) holds ( not D is_<=_than b1 or UD <= b1 ) ) ) thus ( D is_<=_than UD & ( for b1 being Element of the carrier of (InclPoset (Ids R)) holds ( not D is_<=_than b1 or UD <= b1 ) ) ) by Lm1, Lm2; ::_thesis: verum end; end; theorem Th3: :: WAYBEL30:3 for R being non empty reflexive transitive RelStr for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D proof let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: sup D = union D reconsider UD = union D as Ideal of R by Th2; A1: ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75; UD in Ids R ; then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1; A2: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds UD <= b by Lm2; D is_<=_than UD by Lm1; hence sup D = union D by A2, A1, YELLOW_0:def_9; ::_thesis: verum end; theorem Th4: :: WAYBEL30:4 for R being Semilattice for D being non empty directed Subset of (InclPoset (Ids R)) for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum } proof let R be Semilattice; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum } let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum } let x be Element of (InclPoset (Ids R)); ::_thesis: sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum } set I = InclPoset (Ids R); set A = { (x /\ d) where d is Element of D : verum } ; set xD = { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } ; { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } c= the carrier of (InclPoset (Ids R)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } or a in the carrier of (InclPoset (Ids R)) ) assume a in { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } ; ::_thesis: a in the carrier of (InclPoset (Ids R)) then ex d being Element of (InclPoset (Ids R)) st ( a = x "/\" d & d in D ) ; hence a in the carrier of (InclPoset (Ids R)) ; ::_thesis: verum end; then reconsider xD = { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } as Subset of (InclPoset (Ids R)) ; A1: ex_sup_of {x} "/\" D, InclPoset (Ids R) by WAYBEL_2:1; then ex_sup_of xD, InclPoset (Ids R) by YELLOW_4:42; then A2: sup xD is_>=_than xD by YELLOW_0:def_9; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (x /\ d) where d is Element of D : verum } c= sup ({x} "/\" D) set A = { (x /\ w) where w is Element of D : verum } ; let a be set ; ::_thesis: ( a in sup ({x} "/\" D) implies a in union { (x /\ w) where w is Element of D : verum } ) ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75; then sup ({x} "/\" D) <= x "/\" (sup D) by A1, YELLOW_4:53; then A3: sup ({x} "/\" D) c= x "/\" (sup D) by YELLOW_1:3; assume a in sup ({x} "/\" D) ; ::_thesis: a in union { (x /\ w) where w is Element of D : verum } then a in x "/\" (sup D) by A3; then A4: a in x /\ (sup D) by YELLOW_2:43; then a in sup D by XBOOLE_0:def_4; then a in union D by Th3; then consider d being set such that A5: a in d and A6: d in D by TARSKI:def_4; reconsider d = d as Element of (InclPoset (Ids R)) by A6; A7: x /\ d in { (x /\ w) where w is Element of D : verum } by A6; a in x by A4, XBOOLE_0:def_4; then a in x /\ d by A5, XBOOLE_0:def_4; hence a in union { (x /\ w) where w is Element of D : verum } by A7, TARSKI:def_4; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (x /\ d) where d is Element of D : verum } or a in sup ({x} "/\" D) ) assume a in union { (x /\ d) where d is Element of D : verum } ; ::_thesis: a in sup ({x} "/\" D) then consider Z being set such that A8: a in Z and A9: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def_4; consider d being Element of D such that A10: Z = x /\ d and verum by A9; reconsider d = d as Element of (InclPoset (Ids R)) ; A11: xD = {x} "/\" D by YELLOW_4:42; then x "/\" d in {x} "/\" D ; then sup xD >= x "/\" d by A2, A11, LATTICE3:def_9; then A12: x "/\" d c= sup xD by YELLOW_1:3; x /\ d = x "/\" d by YELLOW_2:43; then a in sup xD by A12, A8, A10; hence a in sup ({x} "/\" D) by YELLOW_4:42; ::_thesis: verum end; registration let R be Semilattice; cluster InclPoset (Ids R) -> satisfying_MC ; coherence InclPoset (Ids R) is satisfying_MC proof set I = InclPoset (Ids R); let x be Element of (InclPoset (Ids R)); :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of bool the carrier of (InclPoset (Ids R)) holds x "/\" ("\/" (b1,(InclPoset (Ids R)))) = "\/" (({x} "/\" b1),(InclPoset (Ids R))) let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: x "/\" ("\/" (D,(InclPoset (Ids R)))) = "\/" (({x} "/\" D),(InclPoset (Ids R))) thus x "/\" (sup D) = x /\ (sup D) by YELLOW_2:43 .= x /\ (union D) by Th3 .= union { (x /\ d) where d is Element of D : verum } by Th1 .= sup ({x} "/\" D) by Th4 ; ::_thesis: verum end; end; registration let R be 1 -element RelStr ; cluster -> trivial for TopAugmentation of R; coherence for b1 being TopAugmentation of R holds b1 is trivial proof let T be TopAugmentation of R; ::_thesis: T is trivial RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4; hence T is trivial ; ::_thesis: verum end; end; theorem :: WAYBEL30:5 for S being complete Scott TopLattice for T being complete LATTICE for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) proof let S be complete Scott TopLattice; ::_thesis: for T being complete LATTICE for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) let T be complete LATTICE; ::_thesis: for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) let A be Scott TopAugmentation of T; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) ) assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) A2: the topology of S = sigma S by WAYBEL14:23 .= sigma T by A1, YELLOW_9:52 .= the topology of A by YELLOW_9:51 ; RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of S, the InternalRel of S #) by A1, YELLOW_9:def_4; hence TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by A2; ::_thesis: verum end; theorem :: WAYBEL30:6 for N being complete Lawson TopLattice for T being complete LATTICE for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) proof let N be complete Lawson TopLattice; ::_thesis: for T being complete LATTICE for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) let T be complete LATTICE; ::_thesis: for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) let A be correct Lawson TopAugmentation of T; ::_thesis: ( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) ) assume A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) A2: omega T = omega N by A1, WAYBEL19:3; set S = the correct Scott TopAugmentation of T; set l = the correct lower TopAugmentation of T; A3: 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; A4: RelStr(# the carrier of the correct Scott TopAugmentation of T, the InternalRel of the correct Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4; the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T c= bool the carrier of N proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T or a in bool the carrier of N ) assume a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T ; ::_thesis: a in bool the carrier of N then ( a in the topology of the correct Scott TopAugmentation of T or a in the topology of the correct lower TopAugmentation of T ) by XBOOLE_0:def_3; hence a in bool the carrier of N by A1, A4, A3; ::_thesis: verum end; then reconsider X = the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T as Subset-Family of N ; reconsider X = X as Subset-Family of N ; A5: the topology of the correct lower TopAugmentation of T = omega T by WAYBEL19:def_2; (sigma N) \/ (omega N) is prebasis of N by WAYBEL19:def_3; then A6: (sigma T) \/ (omega N) is prebasis of N by A1, YELLOW_9:52; A7: the topology of the correct Scott TopAugmentation of T = sigma T by YELLOW_9:51; the carrier of N = the carrier of the correct Scott TopAugmentation of T \/ the carrier of the correct lower TopAugmentation of T by A1, A4, A3; then N is Refinement of the correct Scott TopAugmentation of T, the correct lower TopAugmentation of T by A2, A6, A5, A7, YELLOW_9:def_6; then A8: the topology of N = UniCl (FinMeetCl X) by YELLOW_9:56 .= lambda T by A1, A5, A7, WAYBEL19:33 .= the topology of A by WAYBEL19:def_4 ; RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, YELLOW_9:def_4; hence TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) by A8; ::_thesis: verum end; theorem :: WAYBEL30:7 for N being complete Lawson TopLattice for S being Scott TopAugmentation of N for A being Subset of N for J being Subset of S st A = J & J is closed holds A is closed proof let N be complete Lawson TopLattice; ::_thesis: for S being Scott TopAugmentation of N for A being Subset of N for J being Subset of S st A = J & J is closed holds A is closed let S be Scott TopAugmentation of N; ::_thesis: for A being Subset of N for J being Subset of S st A = J & J is closed holds A is closed let A be Subset of N; ::_thesis: for J being Subset of S st A = J & J is closed holds A is closed let J be Subset of S; ::_thesis: ( A = J & J is closed implies A is closed ) assume A1: A = J ; ::_thesis: ( not J is closed or A is closed ) assume J is closed ; ::_thesis: A is closed then A2: ([#] S) \ J is open by PRE_TOPC:def_3; A3: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then N is correct Lawson TopAugmentation of S by YELLOW_9:def_4; hence ([#] N) \ A is open by A1, A3, A2, WAYBEL19:37; :: according to PRE_TOPC:def_3 ::_thesis: verum end; registration let A be complete LATTICE; cluster lambda A -> non empty ; coherence not lambda A is empty proof set S = the correct Lawson TopAugmentation of A; not InclPoset the topology of the correct Lawson TopAugmentation of A is trivial ; hence not lambda A is empty by WAYBEL19:def_4; ::_thesis: verum end; end; registration let S be complete Scott TopLattice; cluster InclPoset (sigma S) -> non trivial complete ; coherence ( InclPoset (sigma S) is complete & not InclPoset (sigma S) is trivial ) ; end; registration let N be complete Lawson TopLattice; cluster InclPoset (sigma N) -> non trivial complete ; coherence ( InclPoset (sigma N) is complete & not InclPoset (sigma N) is trivial ) ; cluster InclPoset (lambda N) -> non trivial complete ; coherence ( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial ) proof set S = the correct Lawson TopAugmentation of N; ( InclPoset the topology of the correct Lawson TopAugmentation of N is complete & not InclPoset the topology of the correct Lawson TopAugmentation of N is trivial ) ; hence ( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial ) by WAYBEL19:def_4; ::_thesis: verum end; end; theorem Th8: :: WAYBEL30:8 for T being non empty reflexive RelStr holds sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } proof let T be non empty reflexive RelStr ; ::_thesis: sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in sigma T or s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ) A1: s \ (uparrow ({} T)) = s ; assume s in sigma T ; ::_thesis: s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } hence s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A1; ::_thesis: verum end; theorem Th9: :: WAYBEL30:9 for N being complete Lawson TopLattice holds lambda N = the topology of N proof let N be complete Lawson TopLattice; ::_thesis: lambda N = the topology of N N is correct Lawson TopAugmentation of N by YELLOW_9:44; hence lambda N = the topology of N by WAYBEL19:def_4; ::_thesis: verum end; theorem Th10: :: WAYBEL30:10 for N being complete Lawson TopLattice holds sigma N c= lambda N proof let N be complete Lawson TopLattice; ::_thesis: sigma N c= lambda N set Z = { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } ; { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } is Basis of N by WAYBEL19:32; then { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } c= the topology of N by TOPS_2:64; then A1: { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } c= lambda N by Th9; sigma N c= { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } by Th8; hence sigma N c= lambda N by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: WAYBEL30:11 for M, N being complete LATTICE st RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) holds lambda M = lambda N proof let M, N be complete LATTICE; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) implies lambda M = lambda N ) assume A1: RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) ; ::_thesis: lambda M = lambda N A2: lambda N = UniCl (FinMeetCl ((sigma N) \/ (omega N))) by WAYBEL19:33; A3: lambda M = UniCl (FinMeetCl ((sigma M) \/ (omega M))) by WAYBEL19:33; sigma M = sigma N by A1, YELLOW_9:52; hence lambda M = lambda N by A1, A3, A2, WAYBEL19:3; ::_thesis: verum end; theorem Th12: :: WAYBEL30:12 for N being complete Lawson TopLattice for X being Subset of N holds ( X in lambda N iff X is open ) proof let N be complete Lawson TopLattice; ::_thesis: for X being Subset of N holds ( X in lambda N iff X is open ) let X be Subset of N; ::_thesis: ( X in lambda N iff X is open ) lambda N = the topology of N by Th9; hence ( X in lambda N iff X is open ) by PRE_TOPC:def_2; ::_thesis: verum end; registration cluster1 -element TopSpace-like reflexive -> 1 -element reflexive Scott for TopRelStr ; coherence for b1 being 1 -element reflexive TopRelStr st b1 is TopSpace-like holds b1 is Scott proof let T be 1 -element reflexive TopRelStr ; ::_thesis: ( T is TopSpace-like implies T is Scott ) assume T is TopSpace-like ; ::_thesis: T is Scott then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ; W is Scott proof let S be Subset of W; :: according to WAYBEL11:def_5 ::_thesis: ( ( not S is open or S is upper ) & ( not S is upper or S is open ) ) thus ( S is open implies S is upper ) ; ::_thesis: ( not S is upper or S is open ) thus ( not S is upper or S is open ) by TDLAT_3:15; ::_thesis: verum end; hence T is Scott ; ::_thesis: verum end; end; registration cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete -> complete Lawson for TopRelStr ; coherence for b1 being complete TopLattice st b1 is trivial holds b1 is Lawson proof let T be complete TopLattice; ::_thesis: ( T is trivial implies T is Lawson ) assume T is trivial ; ::_thesis: T is Lawson then the carrier of T is 1 -element ; then reconsider W = T as 1 -element complete TopLattice by STRUCT_0:def_19; set N = the correct Lawson TopAugmentation of W; A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of the correct Lawson TopAugmentation of W, the InternalRel of the correct Lawson TopAugmentation of W #) by YELLOW_9:def_4; the topology of W = {{}, the carrier of W} by TDLAT_3:def_2; then the topology of T = the topology of the correct Lawson TopAugmentation of W by A1, TDLAT_3:def_2 .= lambda T by WAYBEL19:def_4 .= UniCl (FinMeetCl ((sigma T) \/ (omega T))) by WAYBEL19:33 ; then FinMeetCl ((omega T) \/ (sigma T)) is Basis of T by YELLOW_9:22; hence (omega T) \/ (sigma T) is prebasis of T by YELLOW_9:23; :: according to WAYBEL19:def_3 ::_thesis: verum end; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Scott continuous non void meet-continuous for TopRelStr ; existence ex b1 being complete TopLattice st ( b1 is strict & b1 is continuous & b1 is lower-bounded & b1 is meet-continuous & b1 is Scott ) proof set A = the 1 -element strict TopLattice; take the 1 -element strict TopLattice ; ::_thesis: ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is continuous & the 1 -element strict TopLattice is lower-bounded & the 1 -element strict TopLattice is meet-continuous & the 1 -element strict TopLattice is Scott ) thus ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is continuous & the 1 -element strict TopLattice is lower-bounded & the 1 -element strict TopLattice is meet-continuous & the 1 -element strict TopLattice is Scott ) ; ::_thesis: verum end; end; registration cluster non empty TopSpace-like Hausdorff reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Lawson continuous non void compact for TopRelStr ; existence ex b1 being complete TopLattice st ( b1 is strict & b1 is continuous & b1 is compact & b1 is Hausdorff & b1 is Lawson ) proof set R = the trivial complete strict TopLattice; take the trivial complete strict TopLattice ; ::_thesis: ( the trivial complete strict TopLattice is strict & the trivial complete strict TopLattice is continuous & the trivial complete strict TopLattice is compact & the trivial complete strict TopLattice is Hausdorff & the trivial complete strict TopLattice is Lawson ) thus ( the trivial complete strict TopLattice is strict & the trivial complete strict TopLattice is continuous & the trivial complete strict TopLattice is compact & the trivial complete strict TopLattice is Hausdorff & the trivial complete strict TopLattice is Lawson ) ; ::_thesis: verum end; end; scheme :: WAYBEL30:sch 1 EmptySch{ F1() -> Scott TopLattice, F2() -> set , F3( set ) -> set } : { F3(w) where w is Element of F1() : w in {} } = {} proof thus { F3(w) where w is Element of F1() : w in {} } c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= { F3(w) where w is Element of F1() : w in {} } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F3(w) where w is Element of F1() : w in {} } or a in {} ) assume a in { F3(w) where w is Element of F1() : w in {} } ; ::_thesis: a in {} then A1: ex w being Element of F1() st ( a = F3(w) & w in {} ) ; assume not a in {} ; ::_thesis: contradiction thus contradiction by A1; ::_thesis: verum end; thus {} c= { F3(w) where w is Element of F1() : w in {} } by XBOOLE_1:2; ::_thesis: verum end; theorem Th13: :: WAYBEL30:13 for N being meet-continuous LATTICE for A being Subset of N st A is property(S) holds uparrow A is property(S) proof let N be meet-continuous LATTICE; ::_thesis: for A being Subset of N st A is property(S) holds uparrow A is property(S) let A be Subset of N; ::_thesis: ( A is property(S) implies uparrow A is property(S) ) assume A1: for D being non empty directed Subset of N st sup D in A holds ex y being Element of N st ( y in D & ( for x being Element of N st x in D & x >= y holds x in A ) ) ; :: according to WAYBEL11:def_3 ::_thesis: uparrow A is property(S) let D be non empty directed Subset of N; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,N) in uparrow A or ex b1 being Element of the carrier of N st ( b1 in D & ( for b2 being Element of the carrier of N holds ( not b2 in D or not b1 <= b2 or b2 in uparrow A ) ) ) ) assume sup D in uparrow A ; ::_thesis: ex b1 being Element of the carrier of N st ( b1 in D & ( for b2 being Element of the carrier of N holds ( not b2 in D or not b1 <= b2 or b2 in uparrow A ) ) ) then consider a being Element of N such that A2: a <= sup D and A3: a in A by WAYBEL_0:def_16; reconsider aa = {a} as non empty directed Subset of N by WAYBEL_0:5; a = sup ({a} "/\" D) by A2, WAYBEL_2:52; then consider y being Element of N such that A4: y in aa "/\" D and A5: for x being Element of N st x in aa "/\" D & x >= y holds x in A by A1, A3; aa "/\" D = { (a "/\" d) where d is Element of N : d in D } by YELLOW_4:42; then consider d being Element of N such that A6: y = a "/\" d and A7: d in D by A4; take d ; ::_thesis: ( d in D & ( for b1 being Element of the carrier of N holds ( not b1 in D or not d <= b1 or b1 in uparrow A ) ) ) thus d in D by A7; ::_thesis: for b1 being Element of the carrier of N holds ( not b1 in D or not d <= b1 or b1 in uparrow A ) let x be Element of N; ::_thesis: ( not x in D or not d <= x or x in uparrow A ) assume that x in D and A8: x >= d ; ::_thesis: x in uparrow A d >= y by A6, YELLOW_0:23; then A9: x >= y by A8, ORDERS_2:3; y in A by A4, A5, ORDERS_2:1; hence x in uparrow A by A9, WAYBEL_0:def_16; ::_thesis: verum end; registration let N be meet-continuous LATTICE; let A be property(S) Subset of N; cluster uparrow A -> property(S) ; coherence uparrow A is property(S) by Th13; end; theorem Th14: :: WAYBEL30:14 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N for A being Subset of N st A in lambda N holds uparrow A in sigma S proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N for A being Subset of N st A in lambda N holds uparrow A in sigma S let S be Scott TopAugmentation of N; ::_thesis: for A being Subset of N st A in lambda N holds uparrow A in sigma S let A be Subset of N; ::_thesis: ( A in lambda N implies uparrow A in sigma S ) assume A in lambda N ; ::_thesis: uparrow A in sigma S then A1: A is open by Th12; A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then reconsider Y = A as Subset of S ; A3: S is meet-continuous by A2, YELLOW12:14; reconsider UA = uparrow A as Subset of S by A2; A4: uparrow A = uparrow Y by A2, WAYBEL_0:13; Y is property(S) by A1, A2, WAYBEL19:36, YELLOW12:19; then UA is open by A3, A4, WAYBEL11:15; then uparrow A in the topology of S by PRE_TOPC:def_2; hence uparrow A in sigma S by WAYBEL14:23; ::_thesis: verum end; theorem Th15: :: WAYBEL30:15 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N for A being Subset of N for J being Subset of S st A = J & A is open holds uparrow J is open proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N for A being Subset of N for J being Subset of S st A = J & A is open holds uparrow J is open let S be Scott TopAugmentation of N; ::_thesis: for A being Subset of N for J being Subset of S st A = J & A is open holds uparrow J is open let A be Subset of N; ::_thesis: for J being Subset of S st A = J & A is open holds uparrow J is open let J be Subset of S; ::_thesis: ( A = J & A is open implies uparrow J is open ) assume A1: A = J ; ::_thesis: ( not A is open or uparrow J is open ) assume A is open ; ::_thesis: uparrow J is open then A in lambda N by Th12; then A2: uparrow A in sigma S by Th14; RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then uparrow J in sigma S by A2, A1, WAYBEL_0:13; hence uparrow J is open by WAYBEL14:24; ::_thesis: verum end; theorem Th16: :: WAYBEL30:16 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N for x being Point of S for y being Point of N for J being Basis of y st x = y holds { (uparrow A) where A is Subset of N : A in J } is Basis of x proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N for x being Point of S for y being Point of N for J being Basis of y st x = y holds { (uparrow A) where A is Subset of N : A in J } is Basis of x let S be Scott TopAugmentation of N; ::_thesis: for x being Point of S for y being Point of N for J being Basis of y st x = y holds { (uparrow A) where A is Subset of N : A in J } is Basis of x let x be Point of S; ::_thesis: for y being Point of N for J being Basis of y st x = y holds { (uparrow A) where A is Subset of N : A in J } is Basis of x let y be Point of N; ::_thesis: for J being Basis of y st x = y holds { (uparrow A) where A is Subset of N : A in J } is Basis of x let J be Basis of y; ::_thesis: ( x = y implies { (uparrow A) where A is Subset of N : A in J } is Basis of x ) assume A1: x = y ; ::_thesis: { (uparrow A) where A is Subset of N : A in J } is Basis of x set Z = { (uparrow A) where A is Subset of N : A in J } ; set K = { (uparrow A) where A is Subset of N : A in J } ; A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; { (uparrow A) where A is Subset of N : A in J } c= bool the carrier of S proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (uparrow A) where A is Subset of N : A in J } or k in bool the carrier of S ) assume k in { (uparrow A) where A is Subset of N : A in J } ; ::_thesis: k in bool the carrier of S then ex A being Subset of N st ( k = uparrow A & A in J ) ; hence k in bool the carrier of S by A2; ::_thesis: verum end; then reconsider K = { (uparrow A) where A is Subset of N : A in J } as Subset-Family of S ; K is Basis of x proof A3: K is open proof let k be Subset of S; :: according to TOPS_2:def_1 ::_thesis: ( not k in K or k is open ) assume k in K ; ::_thesis: k is open then consider A being Subset of N such that A4: k = uparrow A and A5: A in J ; reconsider A9 = A as Subset of S by A2; uparrow A9 is open by A5, Th15, YELLOW_8:12; then uparrow A9 in the topology of S by PRE_TOPC:def_2; then uparrow A in the topology of S by A2, WAYBEL_0:13; hence k is open by A4, PRE_TOPC:def_2; ::_thesis: verum end; K is x -quasi_basis proof for k being set st k in K holds x in k proof let k be set ; ::_thesis: ( k in K implies x in k ) assume k in K ; ::_thesis: x in k then consider A being Subset of N such that A6: k = uparrow A and A7: A in J ; A8: A c= uparrow A by WAYBEL_0:16; y in Intersect J by YELLOW_8:def_1; then y in A by A7, SETFAM_1:43; hence x in k by A8, A1, A6; ::_thesis: verum end; hence x in Intersect K by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of S holds ( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of S st ( b2 in K & b2 c= b1 ) ) let sA be Subset of S; ::_thesis: ( not sA is open or not x in sA or ex b1 being Element of bool the carrier of S st ( b1 in K & b1 c= sA ) ) assume that A9: sA is open and A10: x in sA ; ::_thesis: ex b1 being Element of bool the carrier of S st ( b1 in K & b1 c= sA ) sA is upper by A9, WAYBEL11:def_4; then A11: uparrow sA c= sA by WAYBEL_0:24; reconsider lA = sA as Subset of N by A2; N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def_4; then lA is open by A9, WAYBEL19:37; then lA in lambda N by Th12; then A12: uparrow lA in sigma S by Th14; A13: lA c= uparrow lA by WAYBEL_0:16; sigma N c= lambda N by Th10; then sigma S c= lambda N by A2, YELLOW_9:52; then uparrow lA is open by A12, Th12; then consider lV1 being Subset of N such that A14: lV1 in J and A15: lV1 c= uparrow lA by A13, A1, A10, YELLOW_8:def_1; reconsider sUV = uparrow lV1 as Subset of S by A2; take sUV ; ::_thesis: ( sUV in K & sUV c= sA ) thus sUV in K by A14; ::_thesis: sUV c= sA A16: lV1 is_coarser_than uparrow lA by A15, WAYBEL12:16; sA c= uparrow sA by WAYBEL_0:16; then A17: sA = uparrow sA by A11, XBOOLE_0:def_10; uparrow sA = uparrow lA by A2, WAYBEL_0:13; hence sUV c= sA by A16, A17, YELLOW12:28; ::_thesis: verum end; hence K is Basis of x by A3; ::_thesis: verum end; hence { (uparrow A) where A is Subset of N : A in J } is Basis of x ; ::_thesis: verum end; theorem Th17: :: WAYBEL30:17 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N for X being upper Subset of N for Y being Subset of S st X = Y holds Int X = Int Y proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N for X being upper Subset of N for Y being Subset of S st X = Y holds Int X = Int Y let S be Scott TopAugmentation of N; ::_thesis: for X being upper Subset of N for Y being Subset of S st X = Y holds Int X = Int Y let X be upper Subset of N; ::_thesis: for Y being Subset of S st X = Y holds Int X = Int Y let Y be Subset of S; ::_thesis: ( X = Y implies Int X = Int Y ) assume A1: X = Y ; ::_thesis: Int X = Int Y A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then reconsider K = uparrow (Int X) as Subset of S ; reconsider sX = Int X as Subset of S by A2; A3: K c= Y proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in K or a in Y ) A4: Int X c= X by TOPS_1:16; assume A5: a in K ; ::_thesis: a in Y then reconsider x = a as Element of N ; A6: X c= uparrow X by WAYBEL_0:16; uparrow X c= X by WAYBEL_0:24; then A7: uparrow X = X by A6, XBOOLE_0:def_10; ex y being Element of N st ( y <= x & y in Int X ) by A5, WAYBEL_0:def_16; hence a in Y by A7, A1, A4, WAYBEL_0:def_16; ::_thesis: verum end; A8: Int X c= uparrow (Int X) by WAYBEL_0:16; uparrow sX is open by Th15; then K is open by A2, WAYBEL_0:13; then uparrow (Int X) c= Int Y by A3, TOPS_1:24; hence Int X c= Int Y by A8, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: Int Y c= Int X reconsider A = Int Y as Subset of N by A2; N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def_4; then A is open by WAYBEL19:37; hence Int Y c= Int X by A1, TOPS_1:16, TOPS_1:24; ::_thesis: verum end; theorem :: WAYBEL30:18 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N for X being lower Subset of N for Y being Subset of S st X = Y holds Cl X = Cl Y proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N for X being lower Subset of N for Y being Subset of S st X = Y holds Cl X = Cl Y let S be Scott TopAugmentation of N; ::_thesis: for X being lower Subset of N for Y being Subset of S st X = Y holds Cl X = Cl Y let X be lower Subset of N; ::_thesis: for Y being Subset of S st X = Y holds Cl X = Cl Y let Y be Subset of S; ::_thesis: ( X = Y implies Cl X = Cl Y ) assume A1: X = Y ; ::_thesis: Cl X = Cl Y A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then reconsider A = Cl Y as Subset of N ; (Cl X) ` = (Cl ((X `) `)) ` .= Int (X `) by TOPS_1:def_1 .= Int (Y `) by A1, A2, Th17 .= (Cl ((Y `) `)) ` by TOPS_1:def_1 .= A ` by A2 ; hence Cl X = Cl Y by TOPS_1:1; ::_thesis: verum end; theorem Th19: :: WAYBEL30:19 for M, N being complete LATTICE for LM being correct Lawson TopAugmentation of M for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds the topology of [:LM,LN:] = lambda [:M,N:] proof let M, N be complete LATTICE; ::_thesis: for LM being correct Lawson TopAugmentation of M for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds the topology of [:LM,LN:] = lambda [:M,N:] let LM be correct Lawson TopAugmentation of M; ::_thesis: for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds the topology of [:LM,LN:] = lambda [:M,N:] let LN be correct Lawson TopAugmentation of N; ::_thesis: ( InclPoset (sigma N) is continuous implies the topology of [:LM,LN:] = lambda [:M,N:] ) assume A1: InclPoset (sigma N) is continuous ; ::_thesis: the topology of [:LM,LN:] = lambda [:M,N:] set SMN = the non empty correct Scott TopAugmentation of [:M,N:]; set lMN = the non empty correct lower TopAugmentation of [:M,N:]; set LMN = the non empty correct Lawson TopAugmentation of [:M,N:]; A2: [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) proof set lN = the non empty correct lower TopAugmentation of N; set lM = the non empty correct lower TopAugmentation of M; set SN = the non empty correct Scott TopAugmentation of N; set SM = the non empty correct Scott TopAugmentation of M; A3: LN is Refinement of the non empty correct Scott TopAugmentation of N, the non empty correct lower TopAugmentation of N by WAYBEL19:29; A4: RelStr(# the carrier of the non empty correct lower TopAugmentation of N, the InternalRel of the non empty correct lower TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; (omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of the non empty correct Lawson TopAugmentation of [:M,N:] by WAYBEL19:def_3; then A5: (omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by YELLOW12:33; A6: RelStr(# the carrier of LM, the InternalRel of LM #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4; A7: RelStr(# the carrier of LN, the InternalRel of LN #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; A8: RelStr(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the InternalRel of the non empty correct Lawson TopAugmentation of [:M,N:] #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def_4; A9: the carrier of [:LM,LN:] = [: the carrier of LM, the carrier of LN:] by BORSUK_1:def_2 .= the carrier of the non empty correct Lawson TopAugmentation of [:M,N:] by A6, A7, A8, YELLOW_3:def_2 ; A10: the topology of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] = omega [:M,N:] by WAYBEL19:15 .= omega the non empty correct Lawson TopAugmentation of [:M,N:] by A8, WAYBEL19:3 ; A11: RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4 .= RelStr(# the carrier of (Sigma M), the InternalRel of (Sigma M) #) by YELLOW_9:def_4 ; then A12: TopStruct(# the carrier of the non empty correct Scott TopAugmentation of M, the topology of the non empty correct Scott TopAugmentation of M #) = TopStruct(# the carrier of (Sigma M), the topology of (Sigma M) #) by WAYBEL29:13; A13: RelStr(# the carrier of the non empty correct lower TopAugmentation of M, the InternalRel of the non empty correct lower TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4; RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4 .= RelStr(# the carrier of (Sigma N), the InternalRel of (Sigma N) #) by YELLOW_9:def_4 ; then TopStruct(# the carrier of the non empty correct Scott TopAugmentation of N, the topology of the non empty correct Scott TopAugmentation of N #) = TopStruct(# the carrier of (Sigma N), the topology of (Sigma N) #) by WAYBEL29:13; then A14: the topology of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] = the topology of [:(Sigma M),(Sigma N):] by A12, WAYBEL29:7 .= sigma [:M,N:] by A1, WAYBEL29:30 .= sigma the non empty correct Lawson TopAugmentation of [:M,N:] by A8, YELLOW_9:52 ; A15: RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4; A16: LM is Refinement of the non empty correct Scott TopAugmentation of M, the non empty correct lower TopAugmentation of M by WAYBEL19:29; then [:LM,LN:] is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A3, A15, A11, A13, A4, YELLOW12:50; then the carrier of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) = the carrier of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] \/ the carrier of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A9, YELLOW_9:def_6; then TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A5, A14, A10, YELLOW_9:def_6; hence [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by A16, A3, A15, A11, A13, A4, A9, YELLOW12:49; ::_thesis: verum end; the non empty correct Lawson TopAugmentation of [:M,N:] is Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:] by WAYBEL19:29; then reconsider R = [:LM,LN:] as Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:] by A2, YELLOW12:47; the topology of [:LM,LN:] = the topology of R ; hence the topology of [:LM,LN:] = lambda [:M,N:] by WAYBEL19:34; ::_thesis: verum end; theorem Th20: :: WAYBEL30:20 for M, N being complete LATTICE for P being correct Lawson TopAugmentation of [:M,N:] for Q being correct Lawson TopAugmentation of M for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] proof let M, N be complete LATTICE; ::_thesis: for P being correct Lawson TopAugmentation of [:M,N:] for Q being correct Lawson TopAugmentation of M for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] let P be correct Lawson TopAugmentation of [:M,N:]; ::_thesis: for Q being correct Lawson TopAugmentation of M for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] let Q be correct Lawson TopAugmentation of M; ::_thesis: for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] let R be correct Lawson TopAugmentation of N; ::_thesis: ( InclPoset (sigma N) is continuous implies TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] ) assume A1: InclPoset (sigma N) is continuous ; ::_thesis: TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] A2: the topology of P = lambda [:M,N:] by WAYBEL19:def_4 .= the topology of [:Q,R:] by A1, Th19 ; A3: RelStr(# the carrier of Q, the InternalRel of Q #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4; A4: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; RelStr(# the carrier of P, the InternalRel of P #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def_4; then the carrier of P = [: the carrier of Q, the carrier of N:] by A3, YELLOW_3:def_2 .= the carrier of [:Q,R:] by A4, BORSUK_1:def_2 ; hence TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] by A2; ::_thesis: verum end; theorem Th21: :: WAYBEL30:21 for N being complete Lawson meet-continuous TopLattice for x being Element of N holds x "/\" is continuous proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for x being Element of N holds x "/\" is continuous let x be Element of N; ::_thesis: x "/\" is continuous for X being non empty Subset of N holds x "/\" preserves_inf_of X by YELLOW13:11; hence x "/\" is continuous by WAYBEL21:45; ::_thesis: verum end; registration let N be complete Lawson meet-continuous TopLattice; let x be Element of N; clusterx "/\" -> continuous ; coherence x "/\" is continuous by Th21; end; theorem Th22: :: WAYBEL30:22 for N being complete Lawson meet-continuous TopLattice st InclPoset (sigma N) is continuous holds N is topological_semilattice proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( InclPoset (sigma N) is continuous implies N is topological_semilattice ) assume A1: InclPoset (sigma N) is continuous ; ::_thesis: N is topological_semilattice set NN = the correct Lawson TopAugmentation of [:N,N:]; N is TopAugmentation of N by YELLOW_9:44; then A2: TopStruct(# the carrier of the correct Lawson TopAugmentation of [:N,N:], the topology of the correct Lawson TopAugmentation of [:N,N:] #) = [:N,N:] by A1, Th20; A3: RelStr(# the carrier of the correct Lawson TopAugmentation of [:N,N:], the InternalRel of the correct Lawson TopAugmentation of [:N,N:] #) = RelStr(# the carrier of [:N,N:], the InternalRel of [:N,N:] #) by YELLOW_9:def_4; then reconsider h = inf_op N as Function of the correct Lawson TopAugmentation of [:N,N:],N ; A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N, the InternalRel of N #) ; A5: h is directed-sups-preserving proof let X be Subset of the correct Lawson TopAugmentation of [:N,N:]; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or h preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: h preserves_sup_of X then reconsider X1 = X as non empty directed Subset of [:N,N:] by A3, WAYBEL_0:3; inf_op N preserves_sup_of X1 by WAYBEL_0:def_37; hence h preserves_sup_of X by A3, A4, WAYBEL_0:65; ::_thesis: verum end; A6: h is infs-preserving proof let X be Subset of the correct Lawson TopAugmentation of [:N,N:]; :: according to WAYBEL_0:def_32 ::_thesis: h preserves_inf_of X reconsider X1 = X as Subset of [:N,N:] by A3; inf_op N preserves_inf_of X1 by WAYBEL_0:def_32; hence h preserves_inf_of X by A3, A4, WAYBEL_0:65; ::_thesis: verum end; then h is SemilatticeHomomorphism of the correct Lawson TopAugmentation of [:N,N:],N by WAYBEL21:5; then A7: h is continuous by A5, A6, WAYBEL21:46; A8: TopStruct(# the carrier of N, the topology of N #) = TopStruct(# the carrier of N, the topology of N #) ; let g be Function of [:N,N:],N; :: according to YELLOW13:def_5 ::_thesis: ( not R16( the carrier of [:N,N:], the carrier of N, the carrier of [:N,N:], the carrier of N,g, inf_op N) or g is continuous ) assume g = inf_op N ; ::_thesis: g is continuous hence g is continuous by A2, A7, A8, YELLOW12:36; ::_thesis: verum end; Lm3: now__::_thesis:_for_S,_T,_x1,_x2_being_set_st_x1_in_S_&_x2_in_T_holds_ <:(pr2_(S,T)),(pr1_(S,T)):>_._[x1,x2]_=_[x2,x1] let S, T, x1, x2 be set ; ::_thesis: ( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1] ) assume that A1: x1 in S and A2: x2 in T ; ::_thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1] A3: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def_7 .= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def_4 .= [:S,T:] /\ [:S,T:] by FUNCT_3:def_5 .= [:S,T:] ; [x1,x2] in [:S,T:] by A1, A2, ZFMISC_1:87; hence <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A3, FUNCT_3:def_7 .= [x2,((pr1 (S,T)) . (x1,x2))] by A1, A2, FUNCT_3:def_5 .= [x2,x1] by A1, A2, FUNCT_3:def_4 ; ::_thesis: verum end; theorem :: WAYBEL30:23 for N being complete Lawson meet-continuous TopLattice st InclPoset (sigma N) is continuous holds ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed ) proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( InclPoset (sigma N) is continuous implies ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed ) ) assume A1: InclPoset (sigma N) is continuous ; ::_thesis: ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed ) A2: [: the carrier of N, the carrier of N:] = the carrier of [:N,N:] by BORSUK_1:def_2; hereby ::_thesis: ( ( for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed ) implies N is Hausdorff ) reconsider D = id the carrier of N as Subset of [:N,N:] by BORSUK_1:def_2; set INF = inf_op N; set f = <:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):>; assume N is Hausdorff ; ::_thesis: for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed then A3: D is closed by YELLOW12:46; A4: the carrier of [:N,N:] = [: the carrier of N, the carrier of N:] by YELLOW_3:def_2; then reconsider f = <:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):> as Function of [:N,N:],[:N,N:] by A2, FUNCT_3:58; let X be Subset of [:N,N:]; ::_thesis: ( X = the InternalRel of N implies X is closed ) assume A5: X = the InternalRel of N ; ::_thesis: X is closed A6: for x, y being Element of N holds f . [x,y] = [x,(x "/\" y)] proof let x, y be Element of N; ::_thesis: f . [x,y] = [x,(x "/\" y)] A7: dom (pr1 ( the carrier of N, the carrier of N)) = [: the carrier of N, the carrier of N:] by FUNCT_2:def_1; A8: [x,y] in [: the carrier of N, the carrier of N:] by ZFMISC_1:87; dom (inf_op N) = [: the carrier of N, the carrier of N:] by A4, FUNCT_2:def_1; hence f . [x,y] = [((pr1 ( the carrier of N, the carrier of N)) . (x,y)),((inf_op N) . (x,y))] by A8, A7, FUNCT_3:49 .= [x,((inf_op N) . (x,y))] by FUNCT_3:def_4 .= [x,(x "/\" y)] by WAYBEL_2:def_4 ; ::_thesis: verum end; A9: X = f " D proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f " D c= X let a be set ; ::_thesis: ( a in X implies a in f " D ) assume A10: a in X ; ::_thesis: a in f " D then consider s, t being set such that A11: s in the carrier of N and A12: t in the carrier of N and A13: a = [s,t] by A5, ZFMISC_1:def_2; reconsider s = s, t = t as Element of N by A11, A12; s <= t by A5, A10, A13, ORDERS_2:def_5; then s "/\" t = s by YELLOW_0:25; then f . [s,t] = [s,s] by A6; then A14: f . a in D by A13, RELAT_1:def_10; dom f = the carrier of [:N,N:] by FUNCT_2:def_1; then a in dom f by A2, A11, A12, A13, ZFMISC_1:87; hence a in f " D by A14, FUNCT_1:def_7; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f " D or a in X ) assume A15: a in f " D ; ::_thesis: a in X then A16: f . a in D by FUNCT_1:def_7; consider s, t being set such that A17: s in the carrier of N and A18: t in the carrier of N and A19: a = [s,t] by A2, A15, ZFMISC_1:def_2; reconsider s = s, t = t as Element of N by A17, A18; f . a = [s,(s "/\" t)] by A6, A19; then s = s "/\" t by A16, RELAT_1:def_10; then s <= t by YELLOW_0:25; hence a in X by A5, A19, ORDERS_2:def_5; ::_thesis: verum end; reconsider INF = inf_op N as Function of [:N,N:],N by A2, A4; N is topological_semilattice by A1, Th22; then A20: INF is continuous by YELLOW13:def_5; pr1 ( the carrier of N, the carrier of N) is continuous Function of [:N,N:],N by YELLOW12:39; then f is continuous by A20, YELLOW12:41; hence X is closed by A9, A3, PRE_TOPC:def_6; ::_thesis: verum end; assume A21: for X being Subset of [:N,N:] st X = the InternalRel of N holds X is closed ; ::_thesis: N is Hausdorff A22: the InternalRel of N /\ the InternalRel of (N ~) c= id the carrier of N by YELLOW12:23; id the carrier of N c= the InternalRel of N /\ the InternalRel of (N ~) by YELLOW12:22; then A23: id the carrier of N = the InternalRel of N /\ the InternalRel of (N ~) by A22, XBOOLE_0:def_10; for A being Subset of [:N,N:] st A = id the carrier of N holds A is closed proof reconsider f = <:(pr2 ( the carrier of N, the carrier of N)),(pr1 ( the carrier of N, the carrier of N)):> as continuous Function of [:N,N:],[:N,N:] by YELLOW12:42; reconsider X = the InternalRel of N, Y = the InternalRel of (N ~) as Subset of [:N,N:] by BORSUK_1:def_2; let A be Subset of [:N,N:]; ::_thesis: ( A = id the carrier of N implies A is closed ) assume A24: A = id the carrier of N ; ::_thesis: A is closed reconsider X = X, Y = Y as Subset of [:N,N:] ; A25: X is closed by A21; A26: dom f = [: the carrier of N, the carrier of N:] by YELLOW12:4; A27: f .: X = Y proof thus f .: X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= f .: X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in Y ) assume y in f .: X ; ::_thesis: y in Y then consider x being set such that x in dom f and A28: x in X and A29: y = f . x by FUNCT_1:def_6; consider x1, x2 being set such that A30: x1 in the carrier of N and A31: x2 in the carrier of N and A32: x = [x1,x2] by A28, ZFMISC_1:def_2; f . x = [x2,x1] by A30, A31, A32, Lm3; hence y in Y by A28, A29, A32, RELAT_1:def_7; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in f .: X ) assume A33: y in Y ; ::_thesis: y in f .: X then consider y1, y2 being set such that A34: y1 in the carrier of N and A35: y2 in the carrier of N and A36: y = [y1,y2] by ZFMISC_1:def_2; A37: [y2,y1] in X by A33, A36, RELAT_1:def_7; f . [y2,y1] = y by A34, A35, A36, Lm3; hence y in f .: X by A26, A37, FUNCT_1:def_6; ::_thesis: verum end; f is being_homeomorphism by YELLOW12:43; then Y is closed by A25, A27, TOPS_2:58; hence A is closed by A23, A24, A25; ::_thesis: verum end; hence N is Hausdorff by YELLOW12:46; ::_thesis: verum end; definition let N be non empty reflexive RelStr ; let X be Subset of N; funcX ^0 -> Subset of N equals :: WAYBEL30:def 1 { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds X meets D } ; coherence { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds X meets D } is Subset of N proof defpred S1[ Element of N] means for D being non empty directed Subset of N st $1 <= sup D holds X meets D; thus { u where u is Element of N : S1[u] } is Subset of N from DOMAIN_1:sch_7(); ::_thesis: verum end; end; :: deftheorem defines ^0 WAYBEL30:def_1_:_ for N being non empty reflexive RelStr for X being Subset of N holds X ^0 = { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds X meets D } ; registration let N be non empty reflexive antisymmetric RelStr ; let X be empty Subset of N; clusterX ^0 -> empty ; coherence X ^0 is empty proof X ^0 c= {} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X ^0 or a in {} ) assume that A1: a in X ^0 and not a in {} ; ::_thesis: contradiction consider u being Element of N such that a = u and A2: for D being non empty directed Subset of N st u <= sup D holds X meets D by A1; reconsider D = {u} as non empty directed Subset of N by WAYBEL_0:5; A3: X misses D by XBOOLE_1:65; u <= sup D by YELLOW_0:39; hence contradiction by A3, A2; ::_thesis: verum end; hence X ^0 is empty ; ::_thesis: verum end; end; theorem :: WAYBEL30:24 for N being non empty reflexive RelStr for A, J being Subset of N st A c= J holds A ^0 c= J ^0 proof let N be non empty reflexive RelStr ; ::_thesis: for A, J being Subset of N st A c= J holds A ^0 c= J ^0 let A, J be Subset of N; ::_thesis: ( A c= J implies A ^0 c= J ^0 ) assume A1: A c= J ; ::_thesis: A ^0 c= J ^0 let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A ^0 or a in J ^0 ) assume a in A ^0 ; ::_thesis: a in J ^0 then consider u being Element of N such that A2: a = u and A3: for D being non empty directed Subset of N st u <= sup D holds A meets D ; for D being non empty directed Subset of N st u <= sup D holds J meets D by A1, A3, XBOOLE_1:63; hence a in J ^0 by A2; ::_thesis: verum end; theorem Th25: :: WAYBEL30:25 for N being non empty reflexive RelStr for x being Element of N holds (uparrow x) ^0 = wayabove x proof let N be non empty reflexive RelStr ; ::_thesis: for x being Element of N holds (uparrow x) ^0 = wayabove x let x be Element of N; ::_thesis: (uparrow x) ^0 = wayabove x thus (uparrow x) ^0 c= wayabove x :: according to XBOOLE_0:def_10 ::_thesis: wayabove x c= (uparrow x) ^0 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (uparrow x) ^0 or a in wayabove x ) assume a in (uparrow x) ^0 ; ::_thesis: a in wayabove x then consider u being Element of N such that A1: a = u and A2: for D being non empty directed Subset of N st u <= sup D holds uparrow x meets D ; u >> x proof let D be non empty directed Subset of N; :: according to WAYBEL_3:def_1 ::_thesis: ( not u <= "\/" (D,N) or ex b1 being Element of the carrier of N st ( b1 in D & x <= b1 ) ) assume u <= sup D ; ::_thesis: ex b1 being Element of the carrier of N st ( b1 in D & x <= b1 ) then uparrow x meets D by A2; then consider d being set such that A3: d in (uparrow x) /\ D by XBOOLE_0:4; reconsider d = d as Element of N by A3; take d ; ::_thesis: ( d in D & x <= d ) thus d in D by A3, XBOOLE_0:def_4; ::_thesis: x <= d d in uparrow x by A3, XBOOLE_0:def_4; hence x <= d by WAYBEL_0:18; ::_thesis: verum end; hence a in wayabove x by A1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in wayabove x or a in (uparrow x) ^0 ) assume A4: a in wayabove x ; ::_thesis: a in (uparrow x) ^0 then reconsider b = a as Element of N ; now__::_thesis:_for_D_being_non_empty_directed_Subset_of_N_st_b_<=_sup_D_holds_ uparrow_x_meets_D A5: b >> x by A4, WAYBEL_3:8; let D be non empty directed Subset of N; ::_thesis: ( b <= sup D implies uparrow x meets D ) assume b <= sup D ; ::_thesis: uparrow x meets D then consider d being Element of N such that A6: d in D and A7: x <= d by A5, WAYBEL_3:def_1; d in uparrow x by A7, WAYBEL_0:18; hence uparrow x meets D by A6, XBOOLE_0:3; ::_thesis: verum end; hence a in (uparrow x) ^0 ; ::_thesis: verum end; theorem Th26: :: WAYBEL30:26 for N being Scott TopLattice for X being upper Subset of N holds Int X c= X ^0 proof let N be Scott TopLattice; ::_thesis: for X being upper Subset of N holds Int X c= X ^0 let X be upper Subset of N; ::_thesis: Int X c= X ^0 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int X or x in X ^0 ) assume A1: x in Int X ; ::_thesis: x in X ^0 then reconsider y = x as Element of N ; now__::_thesis:_for_D_being_non_empty_directed_Subset_of_N_st_y_<=_sup_D_holds_ X_meets_D A2: ( Int X is upper & Int X is inaccessible ) by WAYBEL11:def_4; let D be non empty directed Subset of N; ::_thesis: ( y <= sup D implies X meets D ) assume y <= sup D ; ::_thesis: X meets D then sup D in Int X by A2, A1, WAYBEL_0:def_20; then D meets Int X by A2, WAYBEL11:def_1; hence X meets D by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum end; hence x in X ^0 ; ::_thesis: verum end; theorem Th27: :: WAYBEL30:27 for N being non empty reflexive RelStr for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0 proof let N be non empty reflexive RelStr ; ::_thesis: for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0 let X, Y be Subset of N; ::_thesis: (X ^0) \/ (Y ^0) c= (X \/ Y) ^0 let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (X ^0) \/ (Y ^0) or a in (X \/ Y) ^0 ) assume A1: a in (X ^0) \/ (Y ^0) ; ::_thesis: a in (X \/ Y) ^0 then reconsider b = a as Element of N ; now__::_thesis:_for_D_being_non_empty_directed_Subset_of_N_st_b_<=_sup_D_holds_ X_\/_Y_meets_D let D be non empty directed Subset of N; ::_thesis: ( b <= sup D implies X \/ Y meets D ) assume A2: b <= sup D ; ::_thesis: X \/ Y meets D now__::_thesis:_(X_\/_Y)_/\_D_<>_{} percases ( a in X ^0 or a in Y ^0 ) by A1, XBOOLE_0:def_3; suppose a in X ^0 ; ::_thesis: (X \/ Y) /\ D <> {} then ex x being Element of N st ( a = x & ( for D being non empty directed Subset of N st x <= sup D holds X meets D ) ) ; then X meets D by A2; then X /\ D <> {} by XBOOLE_0:def_7; then (X /\ D) \/ (Y /\ D) <> {} ; hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; ::_thesis: verum end; suppose a in Y ^0 ; ::_thesis: (X \/ Y) /\ D <> {} then ex y being Element of N st ( a = y & ( for D being non empty directed Subset of N st y <= sup D holds Y meets D ) ) ; then Y meets D by A2; then Y /\ D <> {} by XBOOLE_0:def_7; then (X /\ D) \/ (Y /\ D) <> {} ; hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; ::_thesis: verum end; end; end; hence X \/ Y meets D by XBOOLE_0:def_7; ::_thesis: verum end; hence a in (X \/ Y) ^0 ; ::_thesis: verum end; theorem Th28: :: WAYBEL30:28 for N being meet-continuous LATTICE for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0 proof let N be meet-continuous LATTICE; ::_thesis: for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0 let X, Y be upper Subset of N; ::_thesis: (X ^0) \/ (Y ^0) = (X \/ Y) ^0 thus (X ^0) \/ (Y ^0) c= (X \/ Y) ^0 by Th27; :: according to XBOOLE_0:def_10 ::_thesis: (X \/ Y) ^0 c= (X ^0) \/ (Y ^0) assume not (X \/ Y) ^0 c= (X ^0) \/ (Y ^0) ; ::_thesis: contradiction then consider s being set such that A1: s in (X \/ Y) ^0 and A2: not s in (X ^0) \/ (Y ^0) by TARSKI:def_3; A3: not s in X ^0 by A2, XBOOLE_0:def_3; A4: not s in Y ^0 by A2, XBOOLE_0:def_3; reconsider s = s as Element of N by A1; consider D being non empty directed Subset of N such that A5: s <= sup D and A6: X misses D by A3; consider E being non empty directed Subset of N such that A7: s <= sup E and A8: Y misses E by A4; s "/\" s = s by YELLOW_0:25; then s <= (sup D) "/\" (sup E) by A5, A7, YELLOW_3:2; then A9: s <= sup (D "/\" E) by WAYBEL_2:51; ex xy being Element of N st ( s = xy & ( for D being non empty directed Subset of N st xy <= sup D holds X \/ Y meets D ) ) by A1; then X \/ Y meets D "/\" E by A9; then A10: (X \/ Y) /\ (D "/\" E) <> {} by XBOOLE_0:def_7; X misses D "/\" E by A6, YELLOW12:21; then A11: X /\ (D "/\" E) = {} by XBOOLE_0:def_7; Y misses D "/\" E by A8, YELLOW12:21; then (X /\ (D "/\" E)) \/ (Y /\ (D "/\" E)) = {} by A11, XBOOLE_0:def_7; hence contradiction by A10, XBOOLE_1:23; ::_thesis: verum end; theorem Th29: :: WAYBEL30:29 for S being Scott meet-continuous TopLattice for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } proof let S be Scott meet-continuous TopLattice; ::_thesis: for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } let F be finite Subset of S; ::_thesis: Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } defpred S1[ set ] means ex UU being Subset-Family of S st ( UU = { (uparrow x) where x is Element of S : x in $1 } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in $1 } ); A1: for b, J being set st b in F & J c= F & S1[J] holds S1[J \/ {b}] proof let b, J be set ; ::_thesis: ( b in F & J c= F & S1[J] implies S1[J \/ {b}] ) assume that A2: b in F and J c= F ; ::_thesis: ( not S1[J] or S1[J \/ {b}] ) reconsider bb = b as Element of S by A2; A3: (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } proof { ((uparrow x) ^0) where x is Element of S : x in J } c= { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) ^0) where x is Element of S : x in J } or a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } ) assume a in { ((uparrow x) ^0) where x is Element of S : x in J } ; ::_thesis: a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } then A4: ex y being Element of S st ( a = (uparrow y) ^0 & y in J ) ; J c= J \/ {b} by XBOOLE_1:7; hence a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A4; ::_thesis: verum end; then A5: union { ((uparrow x) ^0) where x is Element of S : x in J } c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:77; A6: {b} c= J \/ {b} by XBOOLE_1:7; b in {b} by TARSKI:def_1; then (uparrow bb) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A6; then (uparrow bb) ^0 c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:74; hence (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A5, XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } or a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) ) assume a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } ; ::_thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) then consider A being set such that A7: a in A and A8: A in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by TARSKI:def_4; consider y being Element of S such that A9: A = (uparrow y) ^0 and A10: y in J \/ {b} by A8; percases ( y in J or y in {b} ) by A10, XBOOLE_0:def_3; suppose y in J ; ::_thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) then (uparrow y) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J } ; then A11: a in union { ((uparrow x) ^0) where x is Element of S : x in J } by A7, A9, TARSKI:def_4; union { ((uparrow x) ^0) where x is Element of S : x in J } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7; hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A11; ::_thesis: verum end; supposeA12: y in {b} ; ::_thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) A13: (uparrow bb) ^0 c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7; y = b by A12, TARSKI:def_1; hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A13, A7, A9; ::_thesis: verum end; end; end; assume S1[J] ; ::_thesis: S1[J \/ {b}] then consider UU being Subset-Family of S such that A14: UU = { (uparrow x) where x is Element of S : x in J } and A15: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J } ; reconsider I = UU \/ {(uparrow bb)} as Subset-Family of S ; take I ; ::_thesis: ( I = { (uparrow x) where x is Element of S : x in J \/ {b} } & (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } ) thus I = { (uparrow x) where x is Element of S : x in J \/ {b} } ::_thesis: (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } proof thus I c= { (uparrow x) where x is Element of S : x in J \/ {b} } :: according to XBOOLE_0:def_10 ::_thesis: { (uparrow x) where x is Element of S : x in J \/ {b} } c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in I or a in { (uparrow x) where x is Element of S : x in J \/ {b} } ) assume A16: a in I ; ::_thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} } percases ( a in UU or a in {(uparrow bb)} ) by A16, XBOOLE_0:def_3; supposeA17: a in UU ; ::_thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} } A18: J c= J \/ {b} by XBOOLE_1:7; ex x being Element of S st ( a = uparrow x & x in J ) by A17, A14; hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A18; ::_thesis: verum end; supposeA19: a in {(uparrow bb)} ; ::_thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} } A20: b in {b} by TARSKI:def_1; A21: {b} c= J \/ {b} by XBOOLE_1:7; a = uparrow bb by A19, TARSKI:def_1; hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A20, A21; ::_thesis: verum end; end; end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (uparrow x) where x is Element of S : x in J \/ {b} } or a in I ) assume a in { (uparrow x) where x is Element of S : x in J \/ {b} } ; ::_thesis: a in I then consider x being Element of S such that A22: a = uparrow x and A23: x in J \/ {b} ; percases ( x in J or x in {b} ) by A23, XBOOLE_0:def_3; supposeA24: x in J ; ::_thesis: a in I A25: UU c= UU \/ {(uparrow bb)} by XBOOLE_1:7; uparrow x in UU by A24, A14; hence a in I by A25, A22; ::_thesis: verum end; supposeA26: x in {b} ; ::_thesis: a in I A27: {(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7; A28: a in {(uparrow x)} by A22, TARSKI:def_1; x = b by A26, TARSKI:def_1; hence a in I by A27, A28; ::_thesis: verum end; end; end; A29: (union UU) \/ (uparrow bb) = union I proof thus (union UU) \/ (uparrow bb) c= union I :: according to XBOOLE_0:def_10 ::_thesis: union I c= (union UU) \/ (uparrow bb) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union UU) \/ (uparrow bb) or a in union I ) assume A30: a in (union UU) \/ (uparrow bb) ; ::_thesis: a in union I percases ( a in union UU or a in uparrow bb ) by A30, XBOOLE_0:def_3; supposeA31: a in union UU ; ::_thesis: a in union I A32: UU c= I by XBOOLE_1:7; ex A being set st ( a in A & A in UU ) by A31, TARSKI:def_4; hence a in union I by A32, TARSKI:def_4; ::_thesis: verum end; supposeA33: a in uparrow bb ; ::_thesis: a in union I A34: uparrow bb in {(uparrow bb)} by TARSKI:def_1; {(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7; hence a in union I by A34, A33, TARSKI:def_4; ::_thesis: verum end; end; end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union I or a in (union UU) \/ (uparrow bb) ) assume a in union I ; ::_thesis: a in (union UU) \/ (uparrow bb) then consider A being set such that A35: a in A and A36: A in I by TARSKI:def_4; percases ( A in UU or A in {(uparrow bb)} ) by A36, XBOOLE_0:def_3; suppose A in UU ; ::_thesis: a in (union UU) \/ (uparrow bb) then A c= union UU by ZFMISC_1:74; then A37: a in union UU by A35; union UU c= (union UU) \/ (uparrow bb) by XBOOLE_1:7; hence a in (union UU) \/ (uparrow bb) by A37; ::_thesis: verum end; supposeA38: A in {(uparrow bb)} ; ::_thesis: a in (union UU) \/ (uparrow bb) A39: uparrow bb c= (union UU) \/ (uparrow bb) by XBOOLE_1:7; A = uparrow bb by A38, TARSKI:def_1; hence a in (union UU) \/ (uparrow bb) by A39, A35; ::_thesis: verum end; end; end; for X being Subset of S st X in UU holds X is upper proof let X be Subset of S; ::_thesis: ( X in UU implies X is upper ) assume X in UU ; ::_thesis: X is upper then ex x being Element of S st ( X = uparrow x & x in J ) by A14; hence X is upper ; ::_thesis: verum end; then union UU is upper by WAYBEL_0:28; hence (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A3, A15, A29, Th28; ::_thesis: verum end; A40: S1[ {} ] proof deffunc H1( Element of S) -> Subset of S = (uparrow $1) ^0 ; reconsider UU = {} as Subset-Family of S by XBOOLE_1:2; take UU ; ::_thesis: ( UU = { (uparrow x) where x is Element of S : x in {} } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } ) reconsider K = union UU as empty Subset of S ; A41: K ^0 is empty ; thus UU = { (uparrow x) where x is Element of S : x in {} } ::_thesis: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } proof deffunc H2( Element of S) -> Element of bool the carrier of S = uparrow $1; { H2(x) where x is Element of S : x in {} } = {} from WAYBEL30:sch_1(); hence UU = { (uparrow x) where x is Element of S : x in {} } ; ::_thesis: verum end; { H1(x) where x is Element of S : x in {} } = {} from WAYBEL30:sch_1(); hence (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } by A41; ::_thesis: verum end; A42: { ((uparrow x) ^0) where x is Element of S : x in F } = { (wayabove x) where x is Element of S : x in F } proof thus { ((uparrow x) ^0) where x is Element of S : x in F } c= { (wayabove x) where x is Element of S : x in F } :: according to XBOOLE_0:def_10 ::_thesis: { (wayabove x) where x is Element of S : x in F } c= { ((uparrow x) ^0) where x is Element of S : x in F } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) ^0) where x is Element of S : x in F } or a in { (wayabove x) where x is Element of S : x in F } ) assume a in { ((uparrow x) ^0) where x is Element of S : x in F } ; ::_thesis: a in { (wayabove x) where x is Element of S : x in F } then consider x being Element of S such that A43: a = (uparrow x) ^0 and A44: x in F ; (uparrow x) ^0 = wayabove x by Th25; hence a in { (wayabove x) where x is Element of S : x in F } by A43, A44; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (wayabove x) where x is Element of S : x in F } or a in { ((uparrow x) ^0) where x is Element of S : x in F } ) assume a in { (wayabove x) where x is Element of S : x in F } ; ::_thesis: a in { ((uparrow x) ^0) where x is Element of S : x in F } then consider x being Element of S such that A45: a = wayabove x and A46: x in F ; (uparrow x) ^0 = wayabove x by Th25; hence a in { ((uparrow x) ^0) where x is Element of S : x in F } by A45, A46; ::_thesis: verum end; A47: F is finite ; S1[F] from FINSET_1:sch_2(A47, A40, A1); then (uparrow F) ^0 = union { (wayabove x) where x is Element of S : x in F } by A42, YELLOW_9:4; hence Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } by Th26; ::_thesis: verum end; theorem Th30: :: WAYBEL30:30 for N being complete Lawson TopLattice holds ( N is continuous iff ( N is meet-continuous & N is Hausdorff ) ) proof let N be complete Lawson TopLattice; ::_thesis: ( N is continuous iff ( N is meet-continuous & N is Hausdorff ) ) thus ( N is continuous implies ( N is meet-continuous & N is Hausdorff ) ) ; ::_thesis: ( N is meet-continuous & N is Hausdorff implies N is continuous ) assume A1: ( N is meet-continuous & N is Hausdorff ) ; ::_thesis: N is continuous thus A2: for x being Element of N holds ( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( N is up-complete & N is satisfying_axiom_of_approximation ) thus N is up-complete ; ::_thesis: N is satisfying_axiom_of_approximation for x, y being Element of N st not x <= y holds ex u being Element of N st ( u << x & not u <= y ) proof reconsider J = { (O \ (uparrow F)) where O, F is Subset of N : ( O in sigma N & F is finite ) } as Basis of N by WAYBEL19:32; set S = the Scott TopAugmentation of N; A3: for N being Semilattice for x, y being Element of N st ex u being Element of N st ( u << x & not u <= x "/\" y ) holds ex u being Element of N st ( u << x & not u <= y ) proof let N be Semilattice; ::_thesis: for x, y being Element of N st ex u being Element of N st ( u << x & not u <= x "/\" y ) holds ex u being Element of N st ( u << x & not u <= y ) let x, y be Element of N; ::_thesis: ( ex u being Element of N st ( u << x & not u <= x "/\" y ) implies ex u being Element of N st ( u << x & not u <= y ) ) given u being Element of N such that A4: u << x and A5: not u <= x "/\" y ; ::_thesis: ex u being Element of N st ( u << x & not u <= y ) take u ; ::_thesis: ( u << x & not u <= y ) thus u << x by A4; ::_thesis: not u <= y assume A6: u <= y ; ::_thesis: contradiction u <= x by A4, WAYBEL_3:1; then u "/\" u <= x "/\" y by A6, YELLOW_3:2; hence contradiction by A5, YELLOW_0:25; ::_thesis: verum end; let x, y be Element of N; ::_thesis: ( not x <= y implies ex u being Element of N st ( u << x & not u <= y ) ) assume not x <= y ; ::_thesis: ex u being Element of N st ( u << x & not u <= y ) then x "/\" y <> x by YELLOW_0:23; then consider W, V being Subset of N such that A7: W is open and A8: V is open and A9: x in W and A10: x "/\" y in V and A11: W misses V by A1, PRE_TOPC:def_10; V = union { G where G is Subset of N : ( G in J & G c= V ) } by A8, YELLOW_8:9; then consider K being set such that A12: x "/\" y in K and A13: K in { G where G is Subset of N : ( G in J & G c= V ) } by A10, TARSKI:def_4; consider V1 being Subset of N such that A14: K = V1 and A15: V1 in J and A16: V1 c= V by A13; consider U2, F being Subset of N such that A17: V1 = U2 \ (uparrow F) and A18: U2 in sigma N and A19: F is finite by A15; A20: RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; then reconsider x1 = x, y1 = y as Element of the Scott TopAugmentation of N ; A21: ex_inf_of {x1,y1}, the Scott TopAugmentation of N by YELLOW_0:21; reconsider U1 = U2 as Subset of the Scott TopAugmentation of N by A20; reconsider WU1 = W /\ U2 as Subset of N ; reconsider W1 = WU1 as Subset of the Scott TopAugmentation of N by A20; A22: uparrow W1 = uparrow WU1 by A20, WAYBEL_0:13; U2 in sigma the Scott TopAugmentation of N by A20, A18, YELLOW_9:52; then A23: U1 is open by WAYBEL14:24; then A24: U1 is upper by WAYBEL11:def_4; WU1 c= uparrow F proof A25: W misses V1 by A11, A16, XBOOLE_1:63; A26: WU1 \ (uparrow F) c= U1 \ (uparrow F) by XBOOLE_1:17, XBOOLE_1:33; let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in WU1 or w in uparrow F ) assume that A27: w in WU1 and A28: not w in uparrow F ; ::_thesis: contradiction A29: w in W by A27, XBOOLE_0:def_4; w in WU1 \ (uparrow F) by A27, A28, XBOOLE_0:def_5; hence contradiction by A26, A17, A29, A25, XBOOLE_0:3; ::_thesis: verum end; then WU1 is_coarser_than uparrow F by WAYBEL12:16; then A30: uparrow WU1 c= uparrow F by YELLOW12:28; A31: x1 "/\" y1 <= x1 by YELLOW_0:23; x "/\" y = inf {x,y} by YELLOW_0:40 .= "/\" ({x1,y1}, the Scott TopAugmentation of N) by A20, A21, YELLOW_0:27 .= x1 "/\" y1 by YELLOW_0:40 ; then x1 "/\" y1 in U1 by A12, A14, A17, XBOOLE_0:def_5; then x1 in U1 by A24, A31, WAYBEL_0:def_20; then A32: x in W1 by A9, XBOOLE_0:def_4; W1 c= uparrow W1 by WAYBEL_0:16; then A33: x in uparrow W1 by A32; reconsider F1 = F as finite Subset of the Scott TopAugmentation of N by A20, A19; A34: uparrow F1 = uparrow F by A20, WAYBEL_0:13; N is correct Lawson TopAugmentation of the Scott TopAugmentation of N by A20, YELLOW_9:def_4; then U2 is open by A23, WAYBEL19:37; then uparrow W1 c= Int (uparrow F1) by A7, A1, A30, A22, A34, Th15, TOPS_1:24; then A35: x in Int (uparrow F1) by A33; the Scott TopAugmentation of N is meet-continuous by A1, A20, YELLOW12:14; then Int (uparrow F1) c= union { (wayabove u) where u is Element of the Scott TopAugmentation of N : u in F1 } by Th29; then consider A being set such that A36: x in A and A37: A in { (wayabove u) where u is Element of the Scott TopAugmentation of N : u in F1 } by A35, TARSKI:def_4; consider u being Element of the Scott TopAugmentation of N such that A38: A = wayabove u and A39: u in F1 by A37; reconsider u1 = u as Element of N by A20; A40: wayabove u1 = wayabove u by A20, YELLOW12:13; now__::_thesis:_ex_u1_being_Element_of_N_st_ (_u1_<<_x_&_not_u1_<=_x_"/\"_y_) take u1 = u1; ::_thesis: ( u1 << x & not u1 <= x "/\" y ) thus u1 << x by A36, A38, A40, WAYBEL_3:8; ::_thesis: not u1 <= x "/\" y uparrow u1 c= uparrow F by A39, YELLOW12:30; then not x "/\" y in uparrow u1 by A12, A14, A17, XBOOLE_0:def_5; hence not u1 <= x "/\" y by WAYBEL_0:18; ::_thesis: verum end; then consider u2 being Element of N such that A41: u2 << x and A42: not u2 <= y by A3; take u2 ; ::_thesis: ( u2 << x & not u2 <= y ) thus ( u2 << x & not u2 <= y ) by A41, A42; ::_thesis: verum end; hence N is satisfying_axiom_of_approximation by A2, WAYBEL_3:24; ::_thesis: verum end; registration cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous -> Hausdorff complete for TopRelStr ; coherence for b1 being complete TopLattice st b1 is continuous & b1 is Lawson holds b1 is Hausdorff ; cluster TopSpace-like Hausdorff reflexive transitive antisymmetric with_suprema with_infima complete Lawson meet-continuous -> complete continuous for TopRelStr ; coherence for b1 being complete TopLattice st b1 is meet-continuous & b1 is Lawson & b1 is Hausdorff holds b1 is continuous by Th30; end; definition let N be non empty TopRelStr ; attrN is with_small_semilattices means :: WAYBEL30:def 2 for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting ; attrN is with_compact_semilattices means :: WAYBEL30:def 3 for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds ( subrelstr A is meet-inheriting & A is compact ); attrN is with_open_semilattices means :Def4: :: WAYBEL30:def 4 for x being Point of N ex J being Basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting ; end; :: deftheorem defines with_small_semilattices WAYBEL30:def_2_:_ for N being non empty TopRelStr holds ( N is with_small_semilattices iff for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting ); :: deftheorem defines with_compact_semilattices WAYBEL30:def_3_:_ for N being non empty TopRelStr holds ( N is with_compact_semilattices iff for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds ( subrelstr A is meet-inheriting & A is compact ) ); :: deftheorem Def4 defines with_open_semilattices WAYBEL30:def_4_:_ for N being non empty TopRelStr holds ( N is with_open_semilattices iff for x being Point of N ex J being Basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting ); registration cluster non empty TopSpace-like with_open_semilattices -> non empty TopSpace-like with_small_semilattices for TopRelStr ; coherence for b1 being non empty TopSpace-like TopRelStr st b1 is with_open_semilattices holds b1 is with_small_semilattices proof let N be non empty TopSpace-like TopRelStr ; ::_thesis: ( N is with_open_semilattices implies N is with_small_semilattices ) assume A1: for x being Point of N ex J being Basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting ; :: according to WAYBEL30:def_4 ::_thesis: N is with_small_semilattices let x be Point of N; :: according to WAYBEL30:def_2 ::_thesis: ex J being basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting consider J being Basis of x such that A2: for A being Subset of N st A in J holds subrelstr A is meet-inheriting by A1; reconsider J = J as basis of x by YELLOW13:23; take J ; ::_thesis: for A being Subset of N st A in J holds subrelstr A is meet-inheriting thus for A being Subset of N st A in J holds subrelstr A is meet-inheriting by A2; ::_thesis: verum end; cluster non empty TopSpace-like with_compact_semilattices -> non empty TopSpace-like with_small_semilattices for TopRelStr ; coherence for b1 being non empty TopSpace-like TopRelStr st b1 is with_compact_semilattices holds b1 is with_small_semilattices proof let N be non empty TopSpace-like TopRelStr ; ::_thesis: ( N is with_compact_semilattices implies N is with_small_semilattices ) assume A3: for x being Point of N ex J being basis of x st for A being Subset of N st A in J holds ( subrelstr A is meet-inheriting & A is compact ) ; :: according to WAYBEL30:def_3 ::_thesis: N is with_small_semilattices let x be Point of N; :: according to WAYBEL30:def_2 ::_thesis: ex J being basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting consider J being basis of x such that A4: for A being Subset of N st A in J holds ( subrelstr A is meet-inheriting & A is compact ) by A3; take J ; ::_thesis: for A being Subset of N st A in J holds subrelstr A is meet-inheriting thus for A being Subset of N st A in J holds subrelstr A is meet-inheriting by A4; ::_thesis: verum end; cluster non empty anti-discrete -> non empty with_small_semilattices with_open_semilattices for TopRelStr ; coherence for b1 being non empty TopRelStr st b1 is anti-discrete holds ( b1 is with_small_semilattices & b1 is with_open_semilattices ) proof let T be non empty TopRelStr ; ::_thesis: ( T is anti-discrete implies ( T is with_small_semilattices & T is with_open_semilattices ) ) assume T is anti-discrete ; ::_thesis: ( T is with_small_semilattices & T is with_open_semilattices ) then reconsider W = T as non empty anti-discrete TopRelStr ; set J = { the carrier of W}; A5: now__::_thesis:_for_A_being_Subset_of_W_st_A_in_{_the_carrier_of_W}_holds_ subrelstr_A_is_meet-inheriting let A be Subset of W; ::_thesis: ( A in { the carrier of W} implies subrelstr A is meet-inheriting ) A6: subrelstr ([#] W) is infs-inheriting ; assume A in { the carrier of W} ; ::_thesis: subrelstr A is meet-inheriting then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A6, TARSKI:def_1; K is meet-inheriting ; hence subrelstr A is meet-inheriting ; ::_thesis: verum end; A7: W is with_open_semilattices proof let x be Point of W; :: according to WAYBEL30:def_4 ::_thesis: ex J being Basis of x st for A being Subset of W st A in J holds subrelstr A is meet-inheriting reconsider J = { the carrier of W} as Basis of x by YELLOW13:13; take J ; ::_thesis: for A being Subset of W st A in J holds subrelstr A is meet-inheriting let A be Subset of W; ::_thesis: ( A in J implies subrelstr A is meet-inheriting ) assume A in J ; ::_thesis: subrelstr A is meet-inheriting hence subrelstr A is meet-inheriting by A5; ::_thesis: verum end; W is with_small_semilattices proof let x be Point of W; :: according to WAYBEL30:def_2 ::_thesis: ex J being basis of x st for A being Subset of W st A in J holds subrelstr A is meet-inheriting reconsider J = { the carrier of W} as basis of x by YELLOW13:21; take J ; ::_thesis: for A being Subset of W st A in J holds subrelstr A is meet-inheriting let A be Subset of W; ::_thesis: ( A in J implies subrelstr A is meet-inheriting ) assume A in J ; ::_thesis: subrelstr A is meet-inheriting hence subrelstr A is meet-inheriting by A5; ::_thesis: verum end; hence ( T is with_small_semilattices & T is with_open_semilattices ) by A7; ::_thesis: verum end; cluster1 -element TopSpace-like reflexive -> 1 -element with_compact_semilattices for TopRelStr ; coherence for b1 being 1 -element TopRelStr st b1 is reflexive & b1 is TopSpace-like holds b1 is with_compact_semilattices proof let T be 1 -element TopRelStr ; ::_thesis: ( T is reflexive & T is TopSpace-like implies T is with_compact_semilattices ) assume ( T is reflexive & T is TopSpace-like ) ; ::_thesis: T is with_compact_semilattices then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ; W is with_compact_semilattices proof let x be Point of W; :: according to WAYBEL30:def_3 ::_thesis: ex J being basis of x st for A being Subset of W st A in J holds ( subrelstr A is meet-inheriting & A is compact ) reconsider J = { the carrier of W} as basis of x by YELLOW13:21; take J ; ::_thesis: for A being Subset of W st A in J holds ( subrelstr A is meet-inheriting & A is compact ) let A be Subset of W; ::_thesis: ( A in J implies ( subrelstr A is meet-inheriting & A is compact ) ) assume A8: A in J ; ::_thesis: ( subrelstr A is meet-inheriting & A is compact ) subrelstr ([#] W) is infs-inheriting ; then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A8, TARSKI:def_1; K is meet-inheriting ; hence subrelstr A is meet-inheriting ; ::_thesis: A is compact A = [#] W by A8, TARSKI:def_1; hence A is compact ; ::_thesis: verum end; hence T is with_compact_semilattices ; ::_thesis: verum end; end; registration cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima strict lower non void for TopRelStr ; existence ex b1 being TopLattice st ( b1 is strict & b1 is trivial & b1 is lower ) proof set T = the 1 -element strict TopLattice; take the 1 -element strict TopLattice ; ::_thesis: ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is trivial & the 1 -element strict TopLattice is lower ) thus ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is trivial & the 1 -element strict TopLattice is lower ) ; ::_thesis: verum end; end; theorem Th31: :: WAYBEL30:31 for N being with_infima topological_semilattice TopPoset for C being Subset of N st subrelstr C is meet-inheriting holds subrelstr (Cl C) is meet-inheriting proof let N be with_infima topological_semilattice TopPoset; ::_thesis: for C being Subset of N st subrelstr C is meet-inheriting holds subrelstr (Cl C) is meet-inheriting let C be Subset of N; ::_thesis: ( subrelstr C is meet-inheriting implies subrelstr (Cl C) is meet-inheriting ) assume A1: subrelstr C is meet-inheriting ; ::_thesis: subrelstr (Cl C) is meet-inheriting set A = Cl C; set S = subrelstr (Cl C); let x, y be Element of N; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (subrelstr (Cl C)) or not y in the carrier of (subrelstr (Cl C)) or not ex_inf_of {x,y},N or "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) ) assume that A2: x in the carrier of (subrelstr (Cl C)) and A3: y in the carrier of (subrelstr (Cl C)) and ex_inf_of {x,y},N ; ::_thesis: "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) A4: the carrier of (subrelstr (Cl C)) = Cl C by YELLOW_0:def_15; for V being a_neighborhood of x "/\" y holds V meets C proof set NN = [:N,N:]; let V be a_neighborhood of x "/\" y; ::_thesis: V meets C A5: the carrier of [:N,N:] = [: the carrier of N, the carrier of N:] by BORSUK_1:def_2; then reconsider xy = [x,y] as Point of [:N,N:] by YELLOW_3:def_2; the carrier of [:N,N:] = [: the carrier of N, the carrier of N:] by YELLOW_3:def_2; then reconsider f = inf_op N as Function of [:N,N:],N by A5; A6: f . xy = f . (x,y) .= x "/\" y by WAYBEL_2:def_4 ; f is continuous by YELLOW13:def_5; then consider H being a_neighborhood of xy such that A7: f .: H c= V by A6, BORSUK_1:def_1; consider A being Subset-Family of [:N,N:] such that A8: Int H = union A and A9: for e being set st e in A holds ex X1, Y1 being Subset of N st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; xy in union A by A8, CONNSP_2:def_1; then consider K being set such that A10: xy in K and A11: K in A by TARSKI:def_4; consider Ix, Iy being Subset of N such that A12: K = [:Ix,Iy:] and A13: Ix is open and A14: Iy is open by A9, A11; A15: x in Ix by A10, A12, ZFMISC_1:87; A16: y in Iy by A10, A12, ZFMISC_1:87; A17: Ix = Int Ix by A13, TOPS_1:23; Iy = Int Iy by A14, TOPS_1:23; then reconsider Iy = Iy as a_neighborhood of y by A16, CONNSP_2:def_1; Iy meets C by A3, A4, CONNSP_2:27; then consider iy being set such that A18: iy in Iy and A19: iy in C by XBOOLE_0:3; reconsider Ix = Ix as a_neighborhood of x by A15, A17, CONNSP_2:def_1; Ix meets C by A2, A4, CONNSP_2:27; then consider ix being set such that A20: ix in Ix and A21: ix in C by XBOOLE_0:3; reconsider ix = ix, iy = iy as Element of N by A20, A18; now__::_thesis:_ex_a_being_Element_of_the_carrier_of_N_st_ (_a_in_V_&_a_in_C_) [ix,iy] in K by A12, A20, A18, ZFMISC_1:87; then A22: [ix,iy] in Int H by A8, A11, TARSKI:def_4; take a = ix "/\" iy; ::_thesis: ( a in V & a in C ) A23: dom f = the carrier of [:N,N:] by FUNCT_2:def_1; A24: Int H c= H by TOPS_1:16; f . (ix,iy) = ix "/\" iy by WAYBEL_2:def_4; then ix "/\" iy in f .: H by A24, A23, A22, FUNCT_1:def_6; hence a in V by A7; ::_thesis: a in C A25: ex_inf_of {ix,iy},N by YELLOW_0:21; the carrier of (subrelstr C) = C by YELLOW_0:def_15; then inf {ix,iy} in C by A25, A1, A21, A19, YELLOW_0:def_16; hence a in C by YELLOW_0:40; ::_thesis: verum end; hence V meets C by XBOOLE_0:3; ::_thesis: verum end; then x "/\" y in Cl C by CONNSP_2:27; hence "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) by A4, YELLOW_0:40; ::_thesis: verum end; theorem Th32: :: WAYBEL30:32 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N holds ( ( for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S ) iff N is with_open_semilattices ) proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N holds ( ( for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S ) iff N is with_open_semilattices ) let S be Scott TopAugmentation of N; ::_thesis: ( ( for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S ) iff N is with_open_semilattices ) A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; hereby ::_thesis: ( N is with_open_semilattices implies for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S ) assume A2: for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S ; ::_thesis: N is with_open_semilattices thus N is with_open_semilattices ::_thesis: verum proof let x be Point of N; :: according to WAYBEL30:def_4 ::_thesis: ex J being Basis of x st for A being Subset of N st A in J holds subrelstr A is meet-inheriting defpred S1[ set ] means ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st ( $1 = W1 & U1 \ (uparrow F) = $1 & x in $1 & W1 is open ); consider SF being Subset-Family of N such that A3: for W being Subset of N holds ( W in SF iff S1[W] ) from SUBSET_1:sch_3(); reconsider SF = SF as Subset-Family of N ; A4: now__::_thesis:_for_W_being_Subset_of_N_st_W_is_open_&_x_in_W_holds_ ex_U2_being_Filter_of_N_ex_F_being_finite_Subset_of_N_ex_IT_being_Subset_of_N_st_ (_IT_=_U2_\_(uparrow_F)_&_x_in_IT_&_IT_is_open_&_IT_c=_W_) reconsider BL = { (O \ (uparrow F)) where O, F is Subset of N : ( O in sigma N & F is finite ) } as Basis of N by WAYBEL19:32; A5: BL c= the topology of N by TOPS_2:64; reconsider y = x as Point of S by A1; let W be Subset of N; ::_thesis: ( W is open & x in W implies ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) ) assume that A6: W is open and A7: x in W ; ::_thesis: ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) consider By being Basis of y such that A8: for A being Subset of S st A in By holds A is Filter of S by A2; W = union { G where G is Subset of N : ( G in BL & G c= W ) } by A6, YELLOW_8:9; then consider K being set such that A9: x in K and A10: K in { G where G is Subset of N : ( G in BL & G c= W ) } by A7, TARSKI:def_4; consider G being Subset of N such that A11: K = G and A12: G in BL and A13: G c= W by A10; consider V, F being Subset of N such that A14: G = V \ (uparrow F) and A15: V in sigma N and A16: F is finite by A12; reconsider F = F as finite Subset of N by A16; A17: not x in uparrow F by A9, A11, A14, XBOOLE_0:def_5; reconsider V = V as Subset of S by A1; A18: y in V by A9, A11, A14, XBOOLE_0:def_5; A19: sigma N = sigma S by A1, YELLOW_9:52; then V is open by A15, WAYBEL14:24; then consider U1 being Subset of S such that A20: U1 in By and A21: U1 c= V by A18, YELLOW_8:13; reconsider U2 = U1 as Subset of N by A1; U1 is Filter of S by A8, A20; then reconsider U2 = U2 as Filter of N by A1, WAYBEL_0:4, WAYBEL_0:25; U2 \ (uparrow F) is Subset of N ; then reconsider IT = U1 \ (uparrow F) as Subset of N ; take U2 = U2; ::_thesis: ex F being finite Subset of N ex IT being Subset of N st ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) take F = F; ::_thesis: ex IT being Subset of N st ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) take IT = IT; ::_thesis: ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) thus IT = U2 \ (uparrow F) ; ::_thesis: ( x in IT & IT is open & IT c= W ) y in U1 by A20, YELLOW_8:12; hence x in IT by A17, XBOOLE_0:def_5; ::_thesis: ( IT is open & IT c= W ) U1 is open by A20, YELLOW_8:12; then U1 in sigma S by WAYBEL14:24; then IT in BL by A19; hence IT is open by A5, PRE_TOPC:def_2; ::_thesis: IT c= W IT c= G by A14, A21, XBOOLE_1:33; hence IT c= W by A13, XBOOLE_1:1; ::_thesis: verum end; SF is Basis of x proof A22: SF is open proof let a be Subset of N; :: according to TOPS_2:def_1 ::_thesis: ( not a in SF or a is open ) assume A23: a in SF ; ::_thesis: a is open reconsider W = a as Subset of N ; ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st ( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A23; hence a is open ; ::_thesis: verum end; SF is x -quasi_basis proof for a being set st a in SF holds x in a proof let a be set ; ::_thesis: ( a in SF implies x in a ) assume A24: a in SF ; ::_thesis: x in a then reconsider W = a as Subset of N ; ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st ( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A24; hence x in a ; ::_thesis: verum end; hence x in Intersect SF by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of N holds ( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of N st ( b2 in SF & b2 c= b1 ) ) let W be Subset of N; ::_thesis: ( not W is open or not x in W or ex b1 being Element of bool the carrier of N st ( b1 in SF & b1 c= W ) ) assume that A25: W is open and A26: x in W ; ::_thesis: ex b1 being Element of bool the carrier of N st ( b1 in SF & b1 c= W ) consider U2 being Filter of N, F being finite Subset of N, IT being Subset of N such that A27: IT = U2 \ (uparrow F) and A28: x in IT and A29: IT is open and A30: IT c= W by A25, A26, A4; take IT ; ::_thesis: ( IT in SF & IT c= W ) thus ( IT in SF & IT c= W ) by A3, A27, A28, A29, A30; ::_thesis: verum end; hence SF is Basis of x by A22; ::_thesis: verum end; then reconsider SF = SF as Basis of x ; take SF ; ::_thesis: for A being Subset of N st A in SF holds subrelstr A is meet-inheriting let W be Subset of N; ::_thesis: ( W in SF implies subrelstr W is meet-inheriting ) assume W in SF ; ::_thesis: subrelstr W is meet-inheriting then consider U1 being Filter of N, F being finite Subset of N, W1 being Subset of N such that W1 = W and A31: U1 \ (uparrow F) = W and x in W and W1 is open by A3; set SW = subrelstr W; thus subrelstr W is meet-inheriting ::_thesis: verum proof let a, b be Element of N; :: according to YELLOW_0:def_16 ::_thesis: ( not a in the carrier of (subrelstr W) or not b in the carrier of (subrelstr W) or not ex_inf_of {a,b},N or "/\" ({a,b},N) in the carrier of (subrelstr W) ) assume that A32: a in the carrier of (subrelstr W) and A33: b in the carrier of (subrelstr W) and ex_inf_of {a,b},N ; ::_thesis: "/\" ({a,b},N) in the carrier of (subrelstr W) A34: the carrier of (subrelstr W) = W by YELLOW_0:def_15; then A35: b in U1 by A31, A33, XBOOLE_0:def_5; A36: not a in uparrow F by A34, A31, A32, XBOOLE_0:def_5; for y being Element of N st y <= a "/\" b holds not y in F proof A37: a "/\" b <= a by YELLOW_0:23; let y be Element of N; ::_thesis: ( y <= a "/\" b implies not y in F ) assume y <= a "/\" b ; ::_thesis: not y in F then y <= a by A37, ORDERS_2:3; hence not y in F by A36, WAYBEL_0:def_16; ::_thesis: verum end; then A38: not a "/\" b in uparrow F by WAYBEL_0:def_16; a in U1 by A34, A31, A32, XBOOLE_0:def_5; then consider z being Element of N such that A39: z in U1 and A40: z <= a and A41: z <= b by A35, WAYBEL_0:def_2; z "/\" z <= a "/\" b by A40, A41, YELLOW_3:2; then z <= a "/\" b by YELLOW_0:25; then a "/\" b in U1 by A39, WAYBEL_0:def_20; then a "/\" b in W by A38, A31, XBOOLE_0:def_5; hence "/\" ({a,b},N) in the carrier of (subrelstr W) by A34, YELLOW_0:40; ::_thesis: verum end; end; end; assume A42: N is with_open_semilattices ; ::_thesis: for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S let x be Point of S; ::_thesis: ex J being Basis of x st for W being Subset of S st W in J holds W is Filter of S reconsider y = x as Point of N by A1; consider J being Basis of y such that A43: for A being Subset of N st A in J holds subrelstr A is meet-inheriting by A42, Def4; reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16; take J9 ; ::_thesis: for W being Subset of S st W in J9 holds W is Filter of S let W be Subset of S; ::_thesis: ( W in J9 implies W is Filter of S ) assume W in J9 ; ::_thesis: W is Filter of S then consider V being Subset of N such that A44: W = uparrow V and A45: V in J ; subrelstr V is meet-inheriting by A43, A45; then A46: V is filtered by YELLOW12:26; x in V by A45, YELLOW_8:12; hence W is Filter of S by A46, A1, A44, WAYBEL_0:4, WAYBEL_0:25; ::_thesis: verum end; theorem Th33: :: WAYBEL30:33 for N being complete Lawson TopLattice for S being Scott TopAugmentation of N for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } proof let N be complete Lawson TopLattice; ::_thesis: for S being Scott TopAugmentation of N for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } let S be Scott TopAugmentation of N; ::_thesis: for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } let x be Element of N; ::_thesis: { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } set s = { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } ; let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } or k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } ) assume k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } ; ::_thesis: k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } then consider J being Subset of S such that A1: k = inf J and A2: x in J and A3: J in sigma S ; A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then reconsider A = J as Subset of N ; sigma N c= lambda N by Th10; then A5: sigma S c= lambda N by A4, YELLOW_9:52; inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27; hence k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } by A5, A1, A2, A3; ::_thesis: verum end; theorem Th34: :: WAYBEL30:34 for N being complete Lawson meet-continuous TopLattice for S being Scott TopAugmentation of N for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } let S be Scott TopAugmentation of N; ::_thesis: for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } let x be Element of N; ::_thesis: { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } set l = { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ; set s = { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } ; thus { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } c= { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } by Th33; :: according to XBOOLE_0:def_10 ::_thesis: { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } c= { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } or k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } ) assume k in { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ; ::_thesis: k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } then consider A being Subset of N such that A1: k = inf A and A2: x in A and A3: A in lambda N ; A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then reconsider J = A as Subset of S ; A is open by A3, Th12; then uparrow J is open by Th15; then A5: uparrow J in sigma S by WAYBEL14:24; A6: J c= uparrow J by WAYBEL_0:16; inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27 .= inf (uparrow J) by WAYBEL_0:38, YELLOW_0:17 ; hence k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } by A5, A1, A2, A6; ::_thesis: verum end; theorem Th35: :: WAYBEL30:35 for N being complete Lawson meet-continuous TopLattice holds ( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) ) proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) ) set S = the Scott TopAugmentation of N; A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) by YELLOW_9:def_4; hereby ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous implies N is continuous ) assume A2: N is continuous ; ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) for x being Point of the Scott TopAugmentation of N ex J being Basis of x st for W being Subset of the Scott TopAugmentation of N st W in J holds W is Filter of the Scott TopAugmentation of N proof let x be Point of the Scott TopAugmentation of N; ::_thesis: ex J being Basis of x st for W being Subset of the Scott TopAugmentation of N st W in J holds W is Filter of the Scott TopAugmentation of N consider J being Basis of x such that A3: for W being Subset of the Scott TopAugmentation of N st W in J holds ( W is open & W is filtered ) by A2, WAYBEL14:35; take J ; ::_thesis: for W being Subset of the Scott TopAugmentation of N st W in J holds W is Filter of the Scott TopAugmentation of N let W be Subset of the Scott TopAugmentation of N; ::_thesis: ( W in J implies W is Filter of the Scott TopAugmentation of N ) assume A4: W in J ; ::_thesis: W is Filter of the Scott TopAugmentation of N then W is open by A3; hence W is Filter of the Scott TopAugmentation of N by A3, A4, WAYBEL11:def_4, YELLOW_8:12; ::_thesis: verum end; hence N is with_open_semilattices by Th32; ::_thesis: InclPoset (sigma N) is continuous InclPoset (sigma the Scott TopAugmentation of N) is continuous by A2, WAYBEL14:36; hence InclPoset (sigma N) is continuous by A1, YELLOW_9:52; ::_thesis: verum end; assume that A5: N is with_open_semilattices and A6: InclPoset (sigma N) is continuous ; ::_thesis: N is continuous A7: for x being Element of the Scott TopAugmentation of N ex J being Basis of x st for Y being Subset of the Scott TopAugmentation of N st Y in J holds ( Y is open & Y is filtered ) proof let x be Element of the Scott TopAugmentation of N; ::_thesis: ex J being Basis of x st for Y being Subset of the Scott TopAugmentation of N st Y in J holds ( Y is open & Y is filtered ) reconsider y = x as Element of N by A1; consider J being Basis of y such that A8: for A being Subset of N st A in J holds subrelstr A is meet-inheriting by A5, Def4; reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16; take J9 ; ::_thesis: for Y being Subset of the Scott TopAugmentation of N st Y in J9 holds ( Y is open & Y is filtered ) let Y be Subset of the Scott TopAugmentation of N; ::_thesis: ( Y in J9 implies ( Y is open & Y is filtered ) ) assume A9: Y in J9 ; ::_thesis: ( Y is open & Y is filtered ) then consider A being Subset of N such that A10: Y = uparrow A and A11: A in J ; subrelstr A is meet-inheriting by A8, A11; then A is filtered by YELLOW12:26; hence ( Y is open & Y is filtered ) by A1, A9, A10, WAYBEL_0:4, YELLOW_8:12; ::_thesis: verum end; sigma the Scott TopAugmentation of N = sigma N by A1, YELLOW_9:52; then for x being Element of the Scott TopAugmentation of N holds x = "\/" ( { (inf X) where X is Subset of the Scott TopAugmentation of N : ( x in X & X in sigma the Scott TopAugmentation of N ) } , the Scott TopAugmentation of N) by A7, A6, WAYBEL14:37; then the Scott TopAugmentation of N is continuous by WAYBEL14:38; hence N is continuous by A1, YELLOW12:15; ::_thesis: verum end; registration cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous -> complete Lawson with_open_semilattices for TopRelStr ; coherence for b1 being complete Lawson TopLattice st b1 is continuous holds b1 is with_open_semilattices by Th35; end; registration let N be complete Lawson continuous TopLattice; cluster InclPoset (sigma N) -> continuous ; coherence InclPoset (sigma N) is continuous by Th35; end; theorem :: WAYBEL30:36 for N being complete Lawson continuous TopLattice holds ( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices ) proof let N be complete Lawson continuous TopLattice; ::_thesis: ( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices ) thus ( N is compact & N is Hausdorff ) ; ::_thesis: ( N is topological_semilattice & N is with_open_semilattices ) InclPoset (sigma N) is continuous ; hence N is topological_semilattice by Th22; ::_thesis: N is with_open_semilattices thus N is with_open_semilattices ; ::_thesis: verum end; theorem :: WAYBEL30:37 for N being Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice holds N is with_compact_semilattices proof let N be Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice; ::_thesis: N is with_compact_semilattices let x be Point of N; :: according to WAYBEL30:def_3 ::_thesis: ex J being basis of x st for A being Subset of N st A in J holds ( subrelstr A is meet-inheriting & A is compact ) consider BO being Basis of x such that A1: for A being Subset of N st A in BO holds subrelstr A is meet-inheriting by Def4; set BC = { (Cl A) where A is Subset of N : A in BO } ; { (Cl A) where A is Subset of N : A in BO } c= bool the carrier of N proof let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (Cl A) where A is Subset of N : A in BO } or k in bool the carrier of N ) assume k in { (Cl A) where A is Subset of N : A in BO } ; ::_thesis: k in bool the carrier of N then ex A being Subset of N st ( k = Cl A & A in BO ) ; hence k in bool the carrier of N ; ::_thesis: verum end; then reconsider BC = { (Cl A) where A is Subset of N : A in BO } as Subset-Family of N ; BC is basis of x proof let S be a_neighborhood of x; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of x st ( b1 in BC & b1 c= S ) A2: Int S c= S by TOPS_1:16; x in Int S by CONNSP_2:def_1; then consider W being Subset of N such that A3: W in BO and A4: W c= Int S by YELLOW_8:13; A5: W is open by A3, YELLOW_8:12; x in W by A3, YELLOW_8:12; then x in Int W by A5, TOPS_1:23; then reconsider T = W as a_neighborhood of x by CONNSP_2:def_1; percases ( W <> [#] N or W = [#] N ) ; supposeA6: W <> [#] N ; ::_thesis: ex b1 being a_neighborhood of x st ( b1 in BC & b1 c= S ) x in W by A3, YELLOW_8:12; then {x} c= W by ZFMISC_1:31; then consider G being Subset of N such that A7: G is open and A8: {x} c= G and A9: Cl G c= W by A5, A6, CONNSP_2:20; x in G by A8, ZFMISC_1:31; then consider K being Subset of N such that A10: K in BO and A11: K c= G by A7, YELLOW_8:13; A12: K is open by A10, YELLOW_8:12; A13: Int K c= Int (Cl K) by PRE_TOPC:18, TOPS_1:19; x in K by A10, YELLOW_8:12; then x in Int K by A12, TOPS_1:23; then reconsider KK = Cl K as a_neighborhood of x by A13, CONNSP_2:def_1; take KK ; ::_thesis: ( KK in BC & KK c= S ) thus KK in BC by A10; ::_thesis: KK c= S Cl K c= Cl G by A11, PRE_TOPC:19; then Cl K c= W by A9, XBOOLE_1:1; then KK c= Int S by A4, XBOOLE_1:1; hence KK c= S by A2, XBOOLE_1:1; ::_thesis: verum end; supposeA14: W = [#] N ; ::_thesis: ex b1 being a_neighborhood of x st ( b1 in BC & b1 c= S ) take T ; ::_thesis: ( T in BC & T c= S ) Cl ([#] N) = [#] N by TOPS_1:2; hence T in BC by A3, A14; ::_thesis: T c= S thus T c= S by A4, A2, XBOOLE_1:1; ::_thesis: verum end; end; end; then reconsider BC = BC as basis of x ; take BC ; ::_thesis: for A being Subset of N st A in BC holds ( subrelstr A is meet-inheriting & A is compact ) let A be Subset of N; ::_thesis: ( A in BC implies ( subrelstr A is meet-inheriting & A is compact ) ) assume A in BC ; ::_thesis: ( subrelstr A is meet-inheriting & A is compact ) then consider C being Subset of N such that A15: A = Cl C and A16: C in BO ; subrelstr C is meet-inheriting by A1, A16; hence subrelstr A is meet-inheriting by A15, Th31; ::_thesis: A is compact thus A is compact by A15, COMPTS_1:8; ::_thesis: verum end; theorem :: WAYBEL30:38 for N being Hausdorff complete Lawson meet-continuous TopLattice for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) proof let N be Hausdorff complete Lawson meet-continuous TopLattice; ::_thesis: for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) let x be Element of N; ::_thesis: x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) set S = the complete Scott TopAugmentation of N; A1: InclPoset (sigma the complete Scott TopAugmentation of N) is continuous by WAYBEL14:36; A2: RelStr(# the carrier of the complete Scott TopAugmentation of N, the InternalRel of the complete Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; then reconsider y = x as Element of the complete Scott TopAugmentation of N ; for y being Element of the complete Scott TopAugmentation of N ex J being Basis of y st for X being Subset of the complete Scott TopAugmentation of N st X in J holds ( X is open & X is filtered ) by WAYBEL14:35; hence x = "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( y in X & X in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A1, WAYBEL14:37 .= "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } ,N) by A2, YELLOW_0:17, YELLOW_0:26 .= "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by Th34 ; ::_thesis: verum end; theorem :: WAYBEL30:39 for N being complete Lawson meet-continuous TopLattice holds ( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) ) proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) ) set S = the complete Scott TopAugmentation of N; A1: RelStr(# the carrier of the complete Scott TopAugmentation of N, the InternalRel of the complete Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; hereby ::_thesis: ( ( for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) ) implies N is continuous ) assume A2: N is continuous ; ::_thesis: for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) then A3: for x being Element of the complete Scott TopAugmentation of N ex J being Basis of x st for Y being Subset of the complete Scott TopAugmentation of N st Y in J holds ( Y is open & Y is filtered ) by WAYBEL14:35; let x be Element of N; ::_thesis: x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) InclPoset (sigma the complete Scott TopAugmentation of N) is continuous by A2, WAYBEL14:36; hence x = "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A3, A1, WAYBEL14:37 .= "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } ,N) by A1, YELLOW_0:17, YELLOW_0:26 .= "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by Th34 ; ::_thesis: verum end; assume A4: for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) ; ::_thesis: N is continuous now__::_thesis:_for_x_being_Element_of_the_complete_Scott_TopAugmentation_of_N_holds_x_=_"\/"_(_{__(inf_V)_where_V_is_Subset_of_the_complete_Scott_TopAugmentation_of_N_:_(_x_in_V_&_V_in_sigma_the_complete_Scott_TopAugmentation_of_N_)__}__,_the_complete_Scott_TopAugmentation_of_N) let x be Element of the complete Scott TopAugmentation of N; ::_thesis: x = "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) thus x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by A1, A4 .= "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } ,N) by A1, Th34 .= "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A1, YELLOW_0:17, YELLOW_0:26 ; ::_thesis: verum end; then the complete Scott TopAugmentation of N is continuous by WAYBEL14:38; hence N is continuous by A1, YELLOW12:15; ::_thesis: verum end; theorem Th40: :: WAYBEL30:40 for N being complete Lawson meet-continuous TopLattice holds ( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) ) proof let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) ) set S = the Scott TopAugmentation of N; A1: RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4; hereby ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic implies N is algebraic ) assume A2: N is algebraic ; ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) then reconsider M = N as algebraic LATTICE ; M is continuous ; hence N is with_open_semilattices ; ::_thesis: InclPoset (sigma N) is algebraic the Scott TopAugmentation of N is algebraic by A1, A2, WAYBEL_8:17; then ex K being Basis of the Scott TopAugmentation of N st K = { (uparrow x) where x is Element of the Scott TopAugmentation of N : x in the carrier of (CompactSublatt the Scott TopAugmentation of N) } by WAYBEL14:42; then InclPoset (sigma the Scott TopAugmentation of N) is algebraic by WAYBEL14:43; hence InclPoset (sigma N) is algebraic by A1, YELLOW_9:52; ::_thesis: verum end; assume that A3: N is with_open_semilattices and A4: InclPoset (sigma N) is algebraic ; ::_thesis: N is algebraic reconsider T = InclPoset (sigma N) as algebraic LATTICE by A4; T is continuous ; then N is continuous by A3, Th35; then for x being Element of the Scott TopAugmentation of N ex K being Basis of x st for Y being Subset of the Scott TopAugmentation of N st Y in K holds ( Y is open & Y is filtered ) by WAYBEL14:35; then A5: for V being Element of (InclPoset (sigma the Scott TopAugmentation of N)) ex VV being Subset of (InclPoset (sigma the Scott TopAugmentation of N)) st ( V = sup VV & ( for W being Element of (InclPoset (sigma the Scott TopAugmentation of N)) st W in VV holds W is co-prime ) ) by WAYBEL14:39; InclPoset (sigma the Scott TopAugmentation of N) is algebraic by A1, A4, YELLOW_9:52; then ex K being Basis of the Scott TopAugmentation of N st K = { (uparrow x) where x is Element of the Scott TopAugmentation of N : x in the carrier of (CompactSublatt the Scott TopAugmentation of N) } by A5, WAYBEL14:44; then the Scott TopAugmentation of N is algebraic by WAYBEL14:45; hence N is algebraic by A1, WAYBEL_8:17; ::_thesis: verum end; registration let N be complete algebraic Lawson meet-continuous TopLattice; cluster InclPoset (sigma N) -> algebraic ; coherence InclPoset (sigma N) is algebraic by Th40; end;