:: WAYBEL29 semantic presentation begin theorem Th1: :: WAYBEL29:1 for X, Y being non empty set for Z being non empty RelStr for S being non empty SubRelStr of Z |^ [:X,Y:] for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f " is uncurrying proof let X, Y be non empty set ; ::_thesis: for Z being non empty RelStr for S being non empty SubRelStr of Z |^ [:X,Y:] for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f " is uncurrying let Z be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of Z |^ [:X,Y:] for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f " is uncurrying let S be non empty SubRelStr of Z |^ [:X,Y:]; ::_thesis: for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f " is uncurrying let T be non empty SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of S,T st f is currying & f is V7() & f is onto holds f " is uncurrying let f be Function of S,T; ::_thesis: ( f is currying & f is V7() & f is onto implies f " is uncurrying ) assume A1: ( f is currying & f is V7() & f is onto ) ; ::_thesis: f " is uncurrying then A2: rng f = the carrier of T by FUNCT_2:def_3; A3: f " = f " by A1, TOPS_2:def_4; A4: ( Funcs (X, the carrier of (Z |^ Y)) = the carrier of ((Z |^ Y) |^ X) & Funcs (Y, the carrier of Z) = the carrier of (Z |^ Y) ) by YELLOW_1:28; hereby :: according to WAYBEL27:def_1 ::_thesis: for b1 being set holds ( not b1 in proj1 (f ") or (f ") . b1 = uncurry b1 ) let x be set ; ::_thesis: ( x in dom (f ") implies x is Function-yielding Function ) assume x in dom (f ") ; ::_thesis: x is Function-yielding Function then x is Element of ((Z |^ Y) |^ X) by YELLOW_0:58; then x is Function of X,(Funcs (Y, the carrier of Z)) by A4, FUNCT_2:66; hence x is Function-yielding Function ; ::_thesis: verum end; let g be Function; ::_thesis: ( not g in proj1 (f ") or (f ") . g = uncurry g ) assume g in dom (f ") ; ::_thesis: (f ") . g = uncurry g then consider h being set such that A5: h in dom f and A6: g = f . h by A2, FUNCT_1:def_3; reconsider h = h as Function by A5; ( Funcs ([:X,Y:], the carrier of Z) = the carrier of (Z |^ [:X,Y:]) & h is Element of (Z |^ [:X,Y:]) ) by A5, YELLOW_0:58, YELLOW_1:28; then h is Function of [:X,Y:], the carrier of Z by FUNCT_2:66; then A7: dom h = [:X,Y:] by FUNCT_2:def_1; g = curry h by A1, A5, A6, WAYBEL27:def_2; then uncurry g = h by A7, FUNCT_5:49; hence (f ") . g = uncurry g by A1, A3, A5, A6, FUNCT_1:32; ::_thesis: verum end; theorem Th2: :: WAYBEL29:2 for X, Y being non empty set for Z being non empty RelStr for S being non empty SubRelStr of Z |^ [:X,Y:] for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds f " is currying proof let X, Y be non empty set ; ::_thesis: for Z being non empty RelStr for S being non empty SubRelStr of Z |^ [:X,Y:] for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds f " is currying let Z be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of Z |^ [:X,Y:] for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds f " is currying let S be non empty SubRelStr of Z |^ [:X,Y:]; ::_thesis: for T being non empty SubRelStr of (Z |^ Y) |^ X for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds f " is currying let T be non empty SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds f " is currying let f be Function of T,S; ::_thesis: ( f is uncurrying & f is V7() & f is onto implies f " is currying ) A1: ( Funcs (X, the carrier of (Z |^ Y)) = the carrier of ((Z |^ Y) |^ X) & Funcs (Y, the carrier of Z) = the carrier of (Z |^ Y) ) by YELLOW_1:28; assume A2: ( f is uncurrying & f is V7() & f is onto ) ; ::_thesis: f " is currying then A3: rng f = the carrier of S by FUNCT_2:def_3; A4: f " = f " by A2, TOPS_2:def_4; A5: Funcs ([:X,Y:], the carrier of Z) = the carrier of (Z |^ [:X,Y:]) by YELLOW_1:28; hereby :: according to WAYBEL27:def_2 ::_thesis: for b1 being set holds ( not b1 in proj1 (f ") or (f ") . b1 = curry b1 ) let x be set ; ::_thesis: ( x in dom (f ") implies ( x is Function & proj1 x is Relation ) ) assume x in dom (f ") ; ::_thesis: ( x is Function & proj1 x is Relation ) then x is Element of (Z |^ [:X,Y:]) by YELLOW_0:58; then reconsider g = x as Function of [:X,Y:], the carrier of Z by A5, FUNCT_2:66; dom g = proj1 g ; hence ( x is Function & proj1 x is Relation ) ; ::_thesis: verum end; let g be Function; ::_thesis: ( not g in proj1 (f ") or (f ") . g = curry g ) assume g in dom (f ") ; ::_thesis: (f ") . g = curry g then consider h being set such that A6: h in dom f and A7: g = f . h by A3, FUNCT_1:def_3; reconsider h = h as Function by A6; h is Element of ((Z |^ Y) |^ X) by A6, YELLOW_0:58; then h is Function of X,(Funcs (Y, the carrier of Z)) by A1, FUNCT_2:66; then A8: rng h c= Funcs (Y, the carrier of Z) by RELAT_1:def_19; g = uncurry h by A2, A6, A7, WAYBEL27:def_1; then curry g = h by A8, FUNCT_5:48; hence (f ") . g = curry g by A2, A4, A6, A7, FUNCT_1:32; ::_thesis: verum end; theorem :: WAYBEL29:3 for X, Y being non empty set for Z being non empty Poset for S being non empty full SubRelStr of Z |^ [:X,Y:] for T being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f is isomorphic proof let X, Y be non empty set ; ::_thesis: for Z being non empty Poset for S being non empty full SubRelStr of Z |^ [:X,Y:] for T being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f is isomorphic let Z be non empty Poset; ::_thesis: for S being non empty full SubRelStr of Z |^ [:X,Y:] for T being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f is isomorphic let S be non empty full SubRelStr of Z |^ [:X,Y:]; ::_thesis: for T being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is currying & f is V7() & f is onto holds f is isomorphic let T be non empty full SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of S,T st f is currying & f is V7() & f is onto holds f is isomorphic let f be Function of S,T; ::_thesis: ( f is currying & f is V7() & f is onto implies f is isomorphic ) assume A1: ( f is currying & f is V7() & f is onto ) ; ::_thesis: f is isomorphic then A2: ( f * (f ") = id T & (f ") * f = id S ) by GRCAT_1:41; ( f is monotone & f " is monotone ) by A1, Th1, WAYBEL27:20, WAYBEL27:21; hence f is isomorphic by A2, YELLOW16:15; ::_thesis: verum end; theorem :: WAYBEL29:4 for X, Y being non empty set for Z being non empty Poset for T being non empty full SubRelStr of Z |^ [:X,Y:] for S being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds f is isomorphic proof let X, Y be non empty set ; ::_thesis: for Z being non empty Poset for T being non empty full SubRelStr of Z |^ [:X,Y:] for S being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds f is isomorphic let Z be non empty Poset; ::_thesis: for T being non empty full SubRelStr of Z |^ [:X,Y:] for S being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds f is isomorphic let T be non empty full SubRelStr of Z |^ [:X,Y:]; ::_thesis: for S being non empty full SubRelStr of (Z |^ Y) |^ X for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds f is isomorphic let S be non empty full SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds f is isomorphic let f be Function of S,T; ::_thesis: ( f is uncurrying & f is V7() & f is onto implies f is isomorphic ) assume A1: ( f is uncurrying & f is V7() & f is onto ) ; ::_thesis: f is isomorphic then A2: ( f * (f ") = id T & (f ") * f = id S ) by GRCAT_1:41; ( f is monotone & f " is monotone ) by A1, Th2, WAYBEL27:20, WAYBEL27:21; hence f is isomorphic by A2, YELLOW16:15; ::_thesis: verum end; theorem Th5: :: WAYBEL29:5 for S1, S2, T1, T2 being RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds for f being Function of S1,T1 st f is isomorphic holds for g being Function of S2,T2 st g = f holds g is isomorphic proof let S1, S2, T1, T2 be RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f being Function of S1,T1 st f is isomorphic holds for g being Function of S2,T2 st g = f holds g is isomorphic ) assume that A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f being Function of S1,T1 st f is isomorphic holds for g being Function of S2,T2 st g = f holds g is isomorphic let f be Function of S1,T1; ::_thesis: ( f is isomorphic implies for g being Function of S2,T2 st g = f holds g is isomorphic ) assume A3: f is isomorphic ; ::_thesis: for g being Function of S2,T2 st g = f holds g is isomorphic let g be Function of S2,T2; ::_thesis: ( g = f implies g is isomorphic ) assume A4: g = f ; ::_thesis: g is isomorphic percases ( S1 is empty or not S1 is empty ) ; supposeA5: S1 is empty ; ::_thesis: g is isomorphic then T1 is empty by A3, WAYBEL_0:def_38; then A6: T2 is empty by A2; S2 is empty by A1, A5; hence g is isomorphic by A6, WAYBEL_0:def_38; ::_thesis: verum end; suppose not S1 is empty ; ::_thesis: g is isomorphic then reconsider S1 = S1, T1 = T1 as non empty RelStr by A3, WAYBEL_0:def_38; reconsider f = f as Function of S1,T1 ; ( the carrier of S1 <> {} & the carrier of T1 <> {} ) ; then reconsider S2 = S2, T2 = T2 as non empty RelStr by A1, A2; reconsider g = g as Function of S2,T2 ; A7: now__::_thesis:_for_x,_y_being_Element_of_S2_holds_ (_x_<=_y_iff_g_._x_<=_g_._y_) let x, y be Element of S2; ::_thesis: ( x <= y iff g . x <= g . y ) reconsider a = x, b = y as Element of S1 by A1; A8: ( x <= y iff a <= b ) by A1, YELLOW_0:1; ( g . x <= g . y iff f . a <= f . b ) by A2, A4, YELLOW_0:1; hence ( x <= y iff g . x <= g . y ) by A3, A8, WAYBEL_0:66; ::_thesis: verum end; rng f = the carrier of T1 by A3, WAYBEL_0:66; hence g is isomorphic by A2, A3, A4, A7, WAYBEL_0:66; ::_thesis: verum end; end; end; theorem Th6: :: WAYBEL29:6 for R, S, T being RelStr for f being Function of R,S st f is isomorphic holds for g being Function of S,T st g is isomorphic holds for h being Function of R,T st h = g * f holds h is isomorphic proof let L1, L2, L3 be RelStr ; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds for g being Function of L2,L3 st g is isomorphic holds for h being Function of L1,L3 st h = g * f holds h is isomorphic let f1 be Function of L1,L2; ::_thesis: ( f1 is isomorphic implies for g being Function of L2,L3 st g is isomorphic holds for h being Function of L1,L3 st h = g * f1 holds h is isomorphic ) assume A1: f1 is isomorphic ; ::_thesis: for g being Function of L2,L3 st g is isomorphic holds for h being Function of L1,L3 st h = g * f1 holds h is isomorphic let f2 be Function of L2,L3; ::_thesis: ( f2 is isomorphic implies for h being Function of L1,L3 st h = f2 * f1 holds h is isomorphic ) assume A2: f2 is isomorphic ; ::_thesis: for h being Function of L1,L3 st h = f2 * f1 holds h is isomorphic let h be Function of L1,L3; ::_thesis: ( h = f2 * f1 implies h is isomorphic ) assume A3: h = f2 * f1 ; ::_thesis: h is isomorphic percases ( ( not L1 is empty & not L2 is empty & not L3 is empty ) or L1 is empty or L2 is empty or L3 is empty ) ; suppose ( not L1 is empty & not L2 is empty & not L3 is empty ) ; ::_thesis: h is isomorphic then reconsider L1 = L1, L2 = L2, L3 = L3 as non empty RelStr ; reconsider f1 = f1 as Function of L1,L2 ; reconsider f2 = f2 as Function of L2,L3 ; consider g1 being Function of L2,L1 such that A4: ( g1 = f1 " & g1 is monotone ) by A1, WAYBEL_0:def_38; consider g2 being Function of L3,L2 such that A5: ( g2 = f2 " & g2 is monotone ) by A2, WAYBEL_0:def_38; A6: f2 * f1 is monotone by A1, A2, YELLOW_2:12; ( g1 * g2 is monotone & g1 * g2 = (f2 * f1) " ) by A1, A2, A4, A5, FUNCT_1:44, YELLOW_2:12; hence h is isomorphic by A1, A2, A3, A6, WAYBEL_0:def_38; ::_thesis: verum end; supposeA7: L1 is empty ; ::_thesis: h is isomorphic then L2 is empty by A1, WAYBEL_0:def_38; then L3 is empty by A2, WAYBEL_0:def_38; hence h is isomorphic by A7, WAYBEL_0:def_38; ::_thesis: verum end; suppose L2 is empty ; ::_thesis: h is isomorphic then ( L1 is empty & L3 is empty ) by A1, A2, WAYBEL_0:def_38; hence h is isomorphic by WAYBEL_0:def_38; ::_thesis: verum end; supposeA8: L3 is empty ; ::_thesis: h is isomorphic then L2 is empty by A2, WAYBEL_0:def_38; then L1 is empty by A1, WAYBEL_0:def_38; hence h is isomorphic by A8, WAYBEL_0:def_38; ::_thesis: verum end; end; end; theorem Th7: :: WAYBEL29:7 for X, Y, X1, Y1 being TopSpace st TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) holds [:X,Y:] = [:X1,Y1:] proof let X, Y, X1, Y1 be TopSpace; ::_thesis: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) implies [:X,Y:] = [:X1,Y1:] ) assume A1: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ) ; ::_thesis: [:X,Y:] = [:X1,Y1:] set U2 = { (union A) where A is Subset-Family of [:X1,Y1:] : A c= { [:X2,Y2:] where X2 is Subset of X1, Y2 is Subset of Y1 : ( X2 in the topology of X1 & Y2 in the topology of Y1 ) } } ; A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by BORSUK_1:def_2 .= the carrier of [:X1,Y1:] by A1, BORSUK_1:def_2 ; then the topology of [:X,Y:] = { (union A) where A is Subset-Family of [:X1,Y1:] : A c= { [:X2,Y2:] where X2 is Subset of X1, Y2 is Subset of Y1 : ( X2 in the topology of X1 & Y2 in the topology of Y1 ) } } by A1, BORSUK_1:def_2 .= the topology of [:X1,Y1:] by BORSUK_1:def_2 ; hence [:X,Y:] = [:X1,Y1:] by A2; ::_thesis: verum end; theorem Th8: :: WAYBEL29:8 for X being non empty TopSpace for L being non empty up-complete Scott TopPoset for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L proof let X be non empty TopSpace; ::_thesis: for L being non empty up-complete Scott TopPoset for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L let L be non empty up-complete Scott TopPoset; ::_thesis: for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L let F be non empty directed Subset of (ContMaps (X,L)); ::_thesis: "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L set sF = "\/" (F,(L |^ the carrier of X)); Funcs ( the carrier of X, the carrier of L) = the carrier of (L |^ the carrier of X) by YELLOW_1:28; then reconsider sF = "\/" (F,(L |^ the carrier of X)) as Function of X,L by FUNCT_2:66; ContMaps (X,L) is full SubRelStr of L |^ the carrier of X by WAYBEL24:def_3; then reconsider aF = F as non empty directed Subset of (L |^ the carrier of X) by YELLOW_2:7; A1: now__::_thesis:_for_A_being_Subset_of_L_st_A_is_open_holds_ sF_"_A_is_open let A be Subset of L; ::_thesis: ( A is open implies sF " A is open ) assume A2: A is open ; ::_thesis: sF " A is open now__::_thesis:_for_x_being_set_holds_ (_(_x_in_sF_"_A_implies_ex_Q_being_Element_of_bool_the_carrier_of_X_st_ (_Q_is_open_&_Q_c=_sF_"_A_&_x_in_Q_)_)_&_(_ex_Q_being_Subset_of_X_st_ (_Q_is_open_&_Q_c=_sF_"_A_&_x_in_Q_)_implies_x_in_sF_"_A_)_) let x be set ; ::_thesis: ( ( x in sF " A implies ex Q being Element of bool the carrier of X st ( Q is open & Q c= sF " A & x in Q ) ) & ( ex Q being Subset of X st ( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) ) hereby ::_thesis: ( ex Q being Subset of X st ( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) assume A3: x in sF " A ; ::_thesis: ex Q being Element of bool the carrier of X st ( Q is open & Q c= sF " A & x in Q ) then A4: sF . x in A by FUNCT_1:def_7; reconsider y = x as Element of X by A3; A5: the carrier of X -POS_prod ( the carrier of X => L) = L |^ the carrier of X by YELLOW_1:def_5; A6: ( the carrier of X => L) . y = L by FUNCOP_1:7; then A7: ( pi (aF,y) is directed & not pi (aF,y) is empty ) by A5, YELLOW16:35; A8: ex_sup_of aF,L |^ the carrier of X by WAYBEL_0:75; then (sup aF) . y = sup (pi (aF,y)) by A6, A5, YELLOW16:33; then pi (aF,y) meets A by A2, A4, A7, WAYBEL11:def_1; then consider a being set such that A9: a in pi (aF,y) and A10: a in A by XBOOLE_0:3; consider f being Function such that A11: f in aF and A12: a = f . y by A9, CARD_3:def_6; reconsider f = f as continuous Function of X,L by A11, WAYBEL24:21; take Q = f " A; ::_thesis: ( Q is open & Q c= sF " A & x in Q ) [#] L <> {} ; hence Q is open by A2, TOPS_2:43; ::_thesis: ( Q c= sF " A & x in Q ) A13: dom sF = the carrier of X by FUNCT_2:def_1; thus Q c= sF " A ::_thesis: x in Q proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Q or b in sF " A ) assume A14: b in Q ; ::_thesis: b in sF " A then A15: f . b in A by FUNCT_1:def_7; reconsider b = b as Element of X by A14; A16: ( the carrier of X => L) . b = L by FUNCOP_1:7; then ( pi (aF,b) is directed & not pi (aF,b) is empty ) by A5, YELLOW16:35; then A17: ex_sup_of pi (aF,b),L by WAYBEL_0:75; sF . b = sup (pi (aF,b)) by A8, A5, A16, YELLOW16:33; then A18: sF . b is_>=_than pi (aF,b) by A17, YELLOW_0:30; f . b in pi (aF,b) by A11, CARD_3:def_6; then f . b <= sF . b by A18, LATTICE3:def_9; then sF . b in A by A2, A15, WAYBEL_0:def_20; hence b in sF " A by A13, FUNCT_1:def_7; ::_thesis: verum end; dom f = the carrier of X by FUNCT_2:def_1; hence x in Q by A10, A12, FUNCT_1:def_7; ::_thesis: verum end; thus ( ex Q being Subset of X st ( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) ; ::_thesis: verum end; hence sF " A is open by TOPS_1:25; ::_thesis: verum end; [#] L <> {} ; hence "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L by A1, TOPS_2:43; ::_thesis: verum end; theorem Th9: :: WAYBEL29:9 for X being non empty TopSpace for L being non empty up-complete Scott TopPoset holds ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X proof let X be non empty TopSpace; ::_thesis: for L being non empty up-complete Scott TopPoset holds ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X let L be non empty up-complete Scott TopPoset; ::_thesis: ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X reconsider XL = ContMaps (X,L) as non empty full SubRelStr of L |^ the carrier of X by WAYBEL24:def_3; XL is directed-sups-inheriting proof let A be directed Subset of XL; :: according to WAYBEL_0:def_4 ::_thesis: ( A = {} or not ex_sup_of A,L |^ the carrier of X or "\/" (A,(L |^ the carrier of X)) in the carrier of XL ) assume that A1: A <> {} and ex_sup_of A,L |^ the carrier of X ; ::_thesis: "\/" (A,(L |^ the carrier of X)) in the carrier of XL reconsider A = A as non empty directed Subset of XL by A1; "\/" (A,(L |^ the carrier of X)) is continuous Function of X,L by Th8; hence "\/" (A,(L |^ the carrier of X)) in the carrier of XL by WAYBEL24:def_3; ::_thesis: verum end; hence ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X ; ::_thesis: verum end; theorem Th10: :: WAYBEL29:10 for S1, S2 being TopStruct st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) holds for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds ContMaps (S1,T1) = ContMaps (S2,T2) proof let S1, S2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) implies for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds ContMaps (S1,T1) = ContMaps (S2,T2) ) assume A1: TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) ; ::_thesis: for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds ContMaps (S1,T1) = ContMaps (S2,T2) let T1, T2 be non empty TopRelStr ; ::_thesis: ( TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) implies ContMaps (S1,T1) = ContMaps (S2,T2) ) assume A2: TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) ; ::_thesis: ContMaps (S1,T1) = ContMaps (S2,T2) then RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; then T1 |^ the carrier of S1 = T2 |^ the carrier of S2 by A1, WAYBEL27:15; then reconsider C2 = ContMaps (S2,T2) as full SubRelStr of T1 |^ the carrier of S1 by WAYBEL24:def_3; reconsider C1 = ContMaps (S1,T1) as full SubRelStr of T1 |^ the carrier of S1 by WAYBEL24:def_3; the carrier of (ContMaps (S1,T1)) = the carrier of (ContMaps (S2,T2)) proof thus the carrier of (ContMaps (S1,T1)) c= the carrier of (ContMaps (S2,T2)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (ContMaps (S2,T2)) c= the carrier of (ContMaps (S1,T1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ContMaps (S1,T1)) or x in the carrier of (ContMaps (S2,T2)) ) assume x in the carrier of (ContMaps (S1,T1)) ; ::_thesis: x in the carrier of (ContMaps (S2,T2)) then consider f being Function of S1,T1 such that A3: x = f and A4: f is continuous by WAYBEL24:def_3; reconsider f2 = f as Function of S2,T2 by A1, A2; f2 is continuous proof let P2 be Subset of T2; :: according to PRE_TOPC:def_6 ::_thesis: ( not P2 is closed or f2 " P2 is closed ) reconsider P1 = P2 as Subset of T1 by A2; assume P2 is closed ; ::_thesis: f2 " P2 is closed then ([#] T2) \ P2 is open by PRE_TOPC:def_3; then ([#] T2) \ P2 in the topology of T2 by PRE_TOPC:def_2; then ([#] T1) \ P1 is open by A2, PRE_TOPC:def_2; then P1 is closed by PRE_TOPC:def_3; then f " P1 is closed by A4, PRE_TOPC:def_6; then ([#] S1) \ (f " P1) is open by PRE_TOPC:def_3; then ([#] S1) \ (f2 " P2) in the topology of S2 by A1, PRE_TOPC:def_2; then ([#] S2) \ (f2 " P2) is open by A1, PRE_TOPC:def_2; hence f2 " P2 is closed by PRE_TOPC:def_3; ::_thesis: verum end; hence x in the carrier of (ContMaps (S2,T2)) by A3, WAYBEL24:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ContMaps (S2,T2)) or x in the carrier of (ContMaps (S1,T1)) ) assume x in the carrier of (ContMaps (S2,T2)) ; ::_thesis: x in the carrier of (ContMaps (S1,T1)) then consider f being Function of S2,T2 such that A5: x = f and A6: f is continuous by WAYBEL24:def_3; reconsider f1 = f as Function of S1,T1 by A1, A2; f1 is continuous proof let P1 be Subset of T1; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f1 " P1 is closed ) reconsider P2 = P1 as Subset of T2 by A2; assume P1 is closed ; ::_thesis: f1 " P1 is closed then ([#] T1) \ P1 is open by PRE_TOPC:def_3; then ([#] T1) \ P2 in the topology of T2 by A2, PRE_TOPC:def_2; then ([#] T2) \ P2 is open by A2, PRE_TOPC:def_2; then P2 is closed by PRE_TOPC:def_3; then f " P2 is closed by A6, PRE_TOPC:def_6; then ([#] S2) \ (f " P2) is open by PRE_TOPC:def_3; then ([#] S2) \ (f1 " P1) in the topology of S1 by A1, PRE_TOPC:def_2; then ([#] S1) \ (f1 " P1) is open by A1, PRE_TOPC:def_2; hence f1 " P1 is closed by PRE_TOPC:def_3; ::_thesis: verum end; hence x in the carrier of (ContMaps (S1,T1)) by A5, WAYBEL24:def_3; ::_thesis: verum end; then RelStr(# the carrier of C1, the InternalRel of C1 #) = RelStr(# the carrier of C2, the InternalRel of C2 #) by YELLOW_0:57; hence ContMaps (S1,T1) = ContMaps (S2,T2) ; ::_thesis: verum end; registration cluster TopSpace-like reflexive transitive antisymmetric Scott continuous with_suprema with_infima complete -> T_0 continuous injective complete for TopRelStr ; coherence for b1 being continuous complete TopLattice st b1 is Scott holds ( b1 is injective & b1 is T_0 ) proof let T be continuous complete TopLattice; ::_thesis: ( T is Scott implies ( T is injective & T is T_0 ) ) assume T is Scott ; ::_thesis: ( T is injective & T is T_0 ) then T is Scott TopAugmentation of T by YELLOW_9:44; hence ( T is injective & T is T_0 ) ; ::_thesis: verum end; end; registration cluster non empty TopSpace-like reflexive transitive antisymmetric Scott continuous non void with_suprema with_infima complete for TopRelStr ; existence ex b1 being TopLattice st ( b1 is Scott & b1 is continuous & b1 is complete ) proof set L = the continuous complete LATTICE; set T = the Scott TopAugmentation of the continuous complete LATTICE; take the Scott TopAugmentation of the continuous complete LATTICE ; ::_thesis: ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete ) thus ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete ) ; ::_thesis: verum end; end; registration let X be non empty TopSpace; let L be non empty up-complete Scott TopPoset; cluster ContMaps (X,L) -> up-complete ; coherence ContMaps (X,L) is up-complete proof ContMaps (X,L) is full directed-sups-inheriting SubRelStr of L |^ the carrier of X by Th9, WAYBEL24:def_3; hence ContMaps (X,L) is up-complete by YELLOW16:5; ::_thesis: verum end; end; theorem Th11: :: WAYBEL29:11 for I being non empty set for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds I -POS_prod J is up-complete proof let I be non empty set ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds I -POS_prod J is up-complete let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is up-complete ) implies I -POS_prod J is up-complete ) assume A1: for i being Element of I holds J . i is up-complete ; ::_thesis: I -POS_prod J is up-complete set L = I -POS_prod J; now__::_thesis:_for_A_being_non_empty_directed_Subset_of_(I_-POS_prod_J)_holds_ex_sup_of_A,I_-POS_prod_J let A be non empty directed Subset of (I -POS_prod J); ::_thesis: ex_sup_of A,I -POS_prod J now__::_thesis:_for_x_being_Element_of_I_holds_ex_sup_of_pi_(A,x),J_._x let x be Element of I; ::_thesis: ex_sup_of pi (A,x),J . x ( J . x is non empty up-complete Poset & pi (A,x) is directed & not pi (A,x) is empty ) by A1, YELLOW16:35; hence ex_sup_of pi (A,x),J . x by WAYBEL_0:75; ::_thesis: verum end; hence ex_sup_of A,I -POS_prod J by YELLOW16:31; ::_thesis: verum end; hence I -POS_prod J is up-complete by WAYBEL_0:75; ::_thesis: verum end; theorem :: WAYBEL29:12 for I being non empty set for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds ( J . i is up-complete & J . i is lower-bounded ) ) holds for x, y being Element of (product J) holds ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) ) ) proof let I be non empty set ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds ( J . i is up-complete & J . i is lower-bounded ) ) holds for x, y being Element of (product J) holds ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) ) ) let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds ( J . i is up-complete & J . i is lower-bounded ) ) implies for x, y being Element of (product J) holds ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) ) ) ) set L = product J; assume A1: for i being Element of I holds ( J . i is up-complete & J . i is lower-bounded ) ; ::_thesis: for x, y being Element of (product J) holds ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) ) ) then reconsider L9 = product J as non empty up-complete Poset by Th11; let x, y be Element of (product J); ::_thesis: ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) ) ) hereby ::_thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) implies x << y ) assume A2: x << y ; ::_thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) ) hereby ::_thesis: ex K being finite Subset of I st for i being Element of I st not i in K holds x . i = Bottom (J . i) let i be Element of I; ::_thesis: x . i << y . i thus x . i << y . i ::_thesis: verum proof let Di be non empty directed Subset of (J . i); :: according to WAYBEL_3:def_1 ::_thesis: ( not y . i <= "\/" (Di,(J . i)) or ex b1 being Element of the carrier of (J . i) st ( b1 in Di & x . i <= b1 ) ) assume A3: y . i <= sup Di ; ::_thesis: ex b1 being Element of the carrier of (J . i) st ( b1 in Di & x . i <= b1 ) set di = the Element of Di; set D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } ; reconsider di = the Element of Di as Element of (J . i) ; A4: dom y = I by WAYBEL_3:27; { (y +* (i,z)) where z is Element of (J . i) : z in Di } c= the carrier of (product J) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } or a in the carrier of (product J) ) assume a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } ; ::_thesis: a in the carrier of (product J) then consider z being Element of (J . i) such that A5: a = y +* (i,z) and z in Di ; A6: now__::_thesis:_for_j_being_Element_of_I_holds_(y_+*_(i,z))_._j_is_Element_of_(J_._j) let j be Element of I; ::_thesis: (y +* (i,z)) . j is Element of (J . j) ( i = j or i <> j ) ; then ( ( (y +* (i,z)) . j = z & i = j ) or (y +* (i,z)) . j = y . j ) by A4, FUNCT_7:31, FUNCT_7:32; hence (y +* (i,z)) . j is Element of (J . j) ; ::_thesis: verum end; dom (y +* (i,z)) = I by A4, FUNCT_7:30; then a is Element of (product J) by A5, A6, WAYBEL_3:27; hence a in the carrier of (product J) ; ::_thesis: verum end; then reconsider D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } as Subset of (product J) ; A7: y +* (i,di) in D ; then reconsider D = D as non empty Subset of (product J) ; D is directed proof let z1, z2 be Element of (product J); :: according to WAYBEL_0:def_1 ::_thesis: ( not z1 in D or not z2 in D or ex b1 being Element of the carrier of (product J) st ( b1 in D & z1 <= b1 & z2 <= b1 ) ) assume z1 in D ; ::_thesis: ( not z2 in D or ex b1 being Element of the carrier of (product J) st ( b1 in D & z1 <= b1 & z2 <= b1 ) ) then consider a1 being Element of (J . i) such that A8: z1 = y +* (i,a1) and A9: a1 in Di ; assume z2 in D ; ::_thesis: ex b1 being Element of the carrier of (product J) st ( b1 in D & z1 <= b1 & z2 <= b1 ) then consider a2 being Element of (J . i) such that A10: z2 = y +* (i,a2) and A11: a2 in Di ; consider a being Element of (J . i) such that A12: a in Di and A13: a >= a1 and A14: a >= a2 by A9, A11, WAYBEL_0:def_1; y +* (i,a) in D by A12; then reconsider z = y +* (i,a) as Element of (product J) ; take z ; ::_thesis: ( z in D & z1 <= z & z2 <= z ) thus z in D by A12; ::_thesis: ( z1 <= z & z2 <= z ) A15: dom y = I by WAYBEL_3:27; now__::_thesis:_for_j_being_Element_of_I_holds_z_._j_>=_z1_._j let j be Element of I; ::_thesis: z . j >= z1 . j ( i = j or i <> j ) ; then ( ( z . j = a & z1 . j = a1 & i = j ) or ( z . j = y . j & z1 . j = y . j ) ) by A8, A15, FUNCT_7:31, FUNCT_7:32; hence z . j >= z1 . j by A13, YELLOW_0:def_1; ::_thesis: verum end; hence z >= z1 by WAYBEL_3:28; ::_thesis: z2 <= z now__::_thesis:_for_j_being_Element_of_I_holds_z_._j_>=_z2_._j let j be Element of I; ::_thesis: z . j >= z2 . j ( i = j or i <> j ) ; then ( ( z . j = a & z2 . j = a2 & i = j ) or ( z . j = y . j & z2 . j = y . j ) ) by A10, A15, FUNCT_7:31, FUNCT_7:32; hence z . j >= z2 . j by A14, YELLOW_0:def_1; ::_thesis: verum end; hence z2 <= z by WAYBEL_3:28; ::_thesis: verum end; then reconsider D = D as non empty directed Subset of (product J) ; A16: dom y = I by WAYBEL_3:27; now__::_thesis:_for_j_being_Element_of_I_holds_(sup_D)_._j_>=_y_._j A17: Di c= pi (D,i) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Di or a in pi (D,i) ) assume A18: a in Di ; ::_thesis: a in pi (D,i) then reconsider a = a as Element of (J . i) ; y +* (i,a) in D by A18; then (y +* (i,a)) . i in pi (D,i) by CARD_3:def_6; hence a in pi (D,i) by A16, FUNCT_7:31; ::_thesis: verum end; let j be Element of I; ::_thesis: (sup D) . j >= y . j A19: ( J . i is non empty up-complete Poset & J . j is non empty up-complete Poset ) by A1; ( not pi (D,i) is empty & pi (D,i) is directed ) by YELLOW16:35; then A20: ex_sup_of pi (D,i),J . i by A19, WAYBEL_0:75; ex_sup_of Di,J . i by A19, WAYBEL_0:75; then A21: sup Di <= sup (pi (D,i)) by A20, A17, YELLOW_0:34; ex_sup_of D,L9 by WAYBEL_0:75; then A22: (sup D) . j = sup (pi (D,j)) by YELLOW16:33; A23: now__::_thesis:_(_j_<>_i_implies_y_._j_in_pi_(D,j)_) assume j <> i ; ::_thesis: y . j in pi (D,j) then (y +* (i,di)) . j = y . j by FUNCT_7:32; hence y . j in pi (D,j) by A7, CARD_3:def_6; ::_thesis: verum end; ( not pi (D,j) is empty & pi (D,j) is directed ) by YELLOW16:35; then ex_sup_of pi (D,j),J . j by A19, WAYBEL_0:75; then (sup D) . j is_>=_than pi (D,j) by A22, YELLOW_0:30; hence (sup D) . j >= y . j by A3, A21, A22, A23, LATTICE3:def_9, YELLOW_0:def_2; ::_thesis: verum end; then sup D >= y by WAYBEL_3:28; then consider d being Element of (product J) such that A24: d in D and A25: d >= x by A2, WAYBEL_3:def_1; consider z being Element of (J . i) such that A26: d = y +* (i,z) and A27: z in Di by A24; take z ; ::_thesis: ( z in Di & x . i <= z ) d . i = z by A4, A26, FUNCT_7:31; hence ( z in Di & x . i <= z ) by A25, A27, WAYBEL_3:28; ::_thesis: verum end; end; set K = { i where i is Element of I : x . i <> Bottom (J . i) } ; { i where i is Element of I : x . i <> Bottom (J . i) } c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : x . i <> Bottom (J . i) } or a in I ) assume a in { i where i is Element of I : x . i <> Bottom (J . i) } ; ::_thesis: a in I then ex i being Element of I st ( a = i & x . i <> Bottom (J . i) ) ; hence a in I ; ::_thesis: verum end; then reconsider K = { i where i is Element of I : x . i <> Bottom (J . i) } as Subset of I ; deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = Bottom (J . \$1); consider f being ManySortedSet of I such that A28: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5(); A29: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i) let i be Element of I; ::_thesis: f . i is Element of (J . i) f . i = Bottom (J . i) by A28; hence f . i is Element of (J . i) ; ::_thesis: verum end; A30: dom f = I by PARTFUN1:def_2; then reconsider f = f as Element of (product J) by A29, WAYBEL_3:27; set X = { (f +* (y | a)) where a is finite Subset of I : verum } ; { (f +* (y | a)) where a is finite Subset of I : verum } c= the carrier of (product J) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f +* (y | a)) where a is finite Subset of I : verum } or a in the carrier of (product J) ) assume a in { (f +* (y | a)) where a is finite Subset of I : verum } ; ::_thesis: a in the carrier of (product J) then consider b being finite Subset of I such that A31: a = f +* (y | b) ; dom y = I by WAYBEL_3:27; then A32: dom (y | b) = b by RELAT_1:62; A33: now__::_thesis:_for_i_being_Element_of_I_holds_(f_+*_(y_|_b))_._i_is_Element_of_(J_._i) let i be Element of I; ::_thesis: (f +* (y | b)) . i is Element of (J . i) ( (f +* (y | b)) . i = f . i or ( (f +* (y | b)) . i = (y | b) . i & (y | b) . i = y . i ) ) by A32, FUNCT_1:47, FUNCT_4:11, FUNCT_4:13; hence (f +* (y | b)) . i is Element of (J . i) ; ::_thesis: verum end; I = I \/ (dom (y | b)) by A32, XBOOLE_1:12 .= dom (f +* (y | b)) by A30, FUNCT_4:def_1 ; then a is Element of (product J) by A31, A33, WAYBEL_3:27; hence a in the carrier of (product J) ; ::_thesis: verum end; then reconsider X = { (f +* (y | a)) where a is finite Subset of I : verum } as Subset of (product J) ; f +* (y | ({} I)) in X ; then reconsider X = X as non empty Subset of (product J) ; X is directed proof let z1, z2 be Element of (product J); :: according to WAYBEL_0:def_1 ::_thesis: ( not z1 in X or not z2 in X or ex b1 being Element of the carrier of (product J) st ( b1 in X & z1 <= b1 & z2 <= b1 ) ) assume z1 in X ; ::_thesis: ( not z2 in X or ex b1 being Element of the carrier of (product J) st ( b1 in X & z1 <= b1 & z2 <= b1 ) ) then consider a1 being finite Subset of I such that A34: z1 = f +* (y | a1) ; assume z2 in X ; ::_thesis: ex b1 being Element of the carrier of (product J) st ( b1 in X & z1 <= b1 & z2 <= b1 ) then consider a2 being finite Subset of I such that A35: z2 = f +* (y | a2) ; reconsider a = a1 \/ a2 as finite Subset of I ; f +* (y | a) in X ; then reconsider z = f +* (y | a) as Element of (product J) ; take z ; ::_thesis: ( z in X & z1 <= z & z2 <= z ) thus z in X ; ::_thesis: ( z1 <= z & z2 <= z ) A36: dom y = I by WAYBEL_3:27; then A37: dom (y | a) = a by RELAT_1:62; A38: dom (y | a1) = a1 by A36, RELAT_1:62; now__::_thesis:_for_i_being_Element_of_I_holds_z_._i_>=_z1_._i let i be Element of I; ::_thesis: z . b1 >= z1 . b1 A39: f . i = Bottom (J . i) by A28; J . i is non empty lower-bounded up-complete Poset by A1; then A40: Bottom (J . i) <= y . i by YELLOW_0:44; percases ( ( not i in a1 & i in a ) or ( not i in a & not i in a1 ) or ( i in a1 & i in a ) ) by XBOOLE_0:def_3; supposeA41: ( not i in a1 & i in a ) ; ::_thesis: z . b1 >= z1 . b1 then ( z . i = (y | a) . i & (y | a) . i = y . i ) by A37, FUNCT_1:47, FUNCT_4:13; hence z . i >= z1 . i by A34, A38, A40, A39, A41, FUNCT_4:11; ::_thesis: verum end; suppose ( not i in a & not i in a1 ) ; ::_thesis: z . b1 >= z1 . b1 then ( z . i = f . i & z1 . i = f . i ) by A34, A37, A38, FUNCT_4:11; hence z . i >= z1 . i by YELLOW_0:def_1; ::_thesis: verum end; supposeA42: ( i in a1 & i in a ) ; ::_thesis: z . b1 >= z1 . b1 then A43: ( z . i = (y | a) . i & (y | a) . i = y . i ) by A37, FUNCT_1:47, FUNCT_4:13; ( z1 . i = (y | a1) . i & (y | a1) . i = y . i ) by A34, A38, A42, FUNCT_1:47, FUNCT_4:13; hence z . i >= z1 . i by A43, YELLOW_0:def_1; ::_thesis: verum end; end; end; hence z >= z1 by WAYBEL_3:28; ::_thesis: z2 <= z A44: dom (y | a2) = a2 by A36, RELAT_1:62; now__::_thesis:_for_i_being_Element_of_I_holds_z_._i_>=_z2_._i let i be Element of I; ::_thesis: z . b1 >= z2 . b1 A45: f . i = Bottom (J . i) by A28; J . i is non empty lower-bounded up-complete Poset by A1; then A46: Bottom (J . i) <= y . i by YELLOW_0:44; percases ( ( not i in a2 & i in a ) or ( not i in a & not i in a2 ) or ( i in a2 & i in a ) ) by XBOOLE_0:def_3; supposeA47: ( not i in a2 & i in a ) ; ::_thesis: z . b1 >= z2 . b1 then ( z . i = (y | a) . i & (y | a) . i = y . i ) by A37, FUNCT_1:47, FUNCT_4:13; hence z . i >= z2 . i by A35, A44, A46, A45, A47, FUNCT_4:11; ::_thesis: verum end; suppose ( not i in a & not i in a2 ) ; ::_thesis: z . b1 >= z2 . b1 then ( z . i = f . i & z2 . i = f . i ) by A35, A37, A44, FUNCT_4:11; hence z . i >= z2 . i by YELLOW_0:def_1; ::_thesis: verum end; supposeA48: ( i in a2 & i in a ) ; ::_thesis: z . b1 >= z2 . b1 then A49: ( z . i = (y | a) . i & (y | a) . i = y . i ) by A37, FUNCT_1:47, FUNCT_4:13; ( z2 . i = (y | a2) . i & (y | a2) . i = y . i ) by A35, A44, A48, FUNCT_1:47, FUNCT_4:13; hence z . i >= z2 . i by A49, YELLOW_0:def_1; ::_thesis: verum end; end; end; hence z2 <= z by WAYBEL_3:28; ::_thesis: verum end; then reconsider X = X as non empty directed Subset of (product J) ; now__::_thesis:_for_i_being_Element_of_I_holds_(sup_X)_._i_>=_y_._i let i be Element of I; ::_thesis: (sup X) . i >= y . i reconsider a = {i} as finite Subset of I by ZFMISC_1:31; A50: f +* (y | a) in X ; then reconsider z = f +* (y | a) as Element of (product J) ; ex_sup_of X,L9 by WAYBEL_0:75; then sup X is_>=_than X by YELLOW_0:30; then A51: z <= sup X by A50, LATTICE3:def_9; dom y = I by WAYBEL_3:27; then A52: dom (y | a) = a by RELAT_1:62; A53: i in a by TARSKI:def_1; then (y | a) . i = y . i by FUNCT_1:49; then z . i = y . i by A53, A52, FUNCT_4:13; hence (sup X) . i >= y . i by A51, WAYBEL_3:28; ::_thesis: verum end; then y <= sup X by WAYBEL_3:28; then consider d being Element of (product J) such that A54: d in X and A55: x <= d by A2, WAYBEL_3:def_1; consider a being finite Subset of I such that A56: d = f +* (y | a) by A54; K c= a proof dom y = I by WAYBEL_3:27; then A57: dom (y | a) = a by RELAT_1:62; let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in K or j in a ) assume j in K ; ::_thesis: j in a then consider i being Element of I such that A58: j = i and A59: x . i <> Bottom (J . i) ; J . i is non empty lower-bounded up-complete Poset by A1; then A60: x . i >= Bottom (J . i) by YELLOW_0:44; assume not j in a ; ::_thesis: contradiction then A61: d . i = f . i by A56, A58, A57, FUNCT_4:11 .= Bottom (J . i) by A28 ; x . i <= d . i by A55, WAYBEL_3:28; hence contradiction by A59, A61, A60, ORDERS_2:2; ::_thesis: verum end; then reconsider K = K as finite Subset of I ; take K = K; ::_thesis: for i being Element of I st not i in K holds x . i = Bottom (J . i) thus for i being Element of I st not i in K holds x . i = Bottom (J . i) ; ::_thesis: verum end; defpred S1[ set , set ] means ex i being Element of I ex z being Element of (product J) st ( \$1 = i & \$2 = z & z . i >= x . i ); assume A62: for i being Element of I holds x . i << y . i ; ::_thesis: ( for K being finite Subset of I ex i being Element of I st ( not i in K & not x . i = Bottom (J . i) ) or x << y ) given K being finite Subset of I such that A63: for i being Element of I st not i in K holds x . i = Bottom (J . i) ; ::_thesis: x << y let D be non empty directed Subset of (product J); :: according to WAYBEL_3:def_1 ::_thesis: ( not y <= "\/" (D,(product J)) or ex b1 being Element of the carrier of (product J) st ( b1 in D & x <= b1 ) ) assume A64: y <= sup D ; ::_thesis: ex b1 being Element of the carrier of (product J) st ( b1 in D & x <= b1 ) A65: now__::_thesis:_for_k_being_set_st_k_in_K_holds_ ex_a_being_set_st_ (_a_in_D_&_S1[k,a]_) let k be set ; ::_thesis: ( k in K implies ex a being set st ( a in D & S1[k,a] ) ) assume k in K ; ::_thesis: ex a being set st ( a in D & S1[k,a] ) then reconsider i = k as Element of I ; A66: pi (D,i) is directed proof let a, b be Element of (J . i); :: according to WAYBEL_0:def_1 ::_thesis: ( not a in pi (D,i) or not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st ( b1 in pi (D,i) & a <= b1 & b <= b1 ) ) assume a in pi (D,i) ; ::_thesis: ( not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st ( b1 in pi (D,i) & a <= b1 & b <= b1 ) ) then consider f being Function such that A67: f in D and A68: a = f . i by CARD_3:def_6; assume b in pi (D,i) ; ::_thesis: ex b1 being Element of the carrier of (J . i) st ( b1 in pi (D,i) & a <= b1 & b <= b1 ) then consider g being Function such that A69: g in D and A70: b = g . i by CARD_3:def_6; reconsider f = f, g = g as Element of (product J) by A67, A69; consider h being Element of (product J) such that A71: ( h in D & h >= f & h >= g ) by A67, A69, WAYBEL_0:def_1; take h . i ; ::_thesis: ( h . i in pi (D,i) & a <= h . i & b <= h . i ) thus ( h . i in pi (D,i) & a <= h . i & b <= h . i ) by A68, A70, A71, CARD_3:def_6, WAYBEL_3:28; ::_thesis: verum end; ex_sup_of D,L9 by WAYBEL_0:75; then A72: (sup D) . i = sup (pi (D,i)) by YELLOW16:33; ( x . i << y . i & y . i <= (sup D) . i ) by A62, A64, WAYBEL_3:28; then consider zi being Element of (J . i) such that A73: zi in pi (D,i) and A74: zi >= x . i by A66, A72, WAYBEL_3:def_1; consider a being Function such that A75: a in D and A76: zi = a . i by A73, CARD_3:def_6; reconsider a = a as set ; take a = a; ::_thesis: ( a in D & S1[k,a] ) thus a in D by A75; ::_thesis: S1[k,a] thus S1[k,a] by A74, A75, A76; ::_thesis: verum end; consider F being Function such that A77: ( dom F = K & rng F c= D ) and A78: for k being set st k in K holds S1[k,F . k] from FUNCT_1:sch_5(A65); reconsider Y = rng F as finite Subset of D by A77, FINSET_1:8; consider d being Element of (product J) such that A79: d in D and A80: d is_>=_than Y by WAYBEL_0:1; take d ; ::_thesis: ( d in D & x <= d ) thus d in D by A79; ::_thesis: x <= d now__::_thesis:_for_i_being_Element_of_I_holds_d_._i_>=_x_._i let i be Element of I; ::_thesis: d . b1 >= x . b1 A81: J . i is non empty lower-bounded up-complete Poset by A1; percases ( i in K or not i in K ) ; supposeA82: i in K ; ::_thesis: d . b1 >= x . b1 then consider j being Element of I, z being Element of (product J) such that A83: i = j and A84: F . i = z and A85: z . j >= x . j by A78; z in Y by A77, A82, A84, FUNCT_1:def_3; then d >= z by A80, LATTICE3:def_9; then d . i >= z . i by WAYBEL_3:28; hence d . i >= x . i by A81, A83, A85, YELLOW_0:def_2; ::_thesis: verum end; suppose not i in K ; ::_thesis: d . b1 >= x . b1 then x . i = Bottom (J . i) by A63; hence d . i >= x . i by A81, YELLOW_0:44; ::_thesis: verum end; end; end; hence x <= d by WAYBEL_3:28; ::_thesis: verum end; registration let X be set ; let L be non empty reflexive antisymmetric lower-bounded RelStr ; clusterL |^ X -> lower-bounded ; coherence L |^ X is lower-bounded proof A1: rng (X --> (Bottom L)) c= the carrier of L ; ( the carrier of (L |^ X) = Funcs (X, the carrier of L) & dom (X --> (Bottom L)) = X ) by FUNCT_2:def_1, YELLOW_1:28; then reconsider f = X --> (Bottom L) as Element of (L |^ X) by A1, FUNCT_2:def_2; take f ; :: according to YELLOW_0:def_4 ::_thesis: f is_<=_than the carrier of (L |^ X) let g be Element of (L |^ X); :: according to LATTICE3:def_8 ::_thesis: ( not g in the carrier of (L |^ X) or f <= g ) percases ( X is empty or not X is empty ) ; supposeA2: X is empty ; ::_thesis: ( not g in the carrier of (L |^ X) or f <= g ) A3: f <= f ; ( L |^ X = RelStr(# {{}},(id {{}}) #) & f = {} ) by A2, YELLOW_1:27; hence ( not g in the carrier of (L |^ X) or f <= g ) by A3, TARSKI:def_1; ::_thesis: verum end; suppose not X is empty ; ::_thesis: ( not g in the carrier of (L |^ X) or f <= g ) then reconsider X = X as non empty set ; reconsider f = f, g = g as Element of (L |^ X) ; now__::_thesis:_for_x_being_Element_of_X_holds_f_._x_<=_g_._x let x be Element of X; ::_thesis: f . x <= g . x f . x = Bottom L by FUNCOP_1:7; hence f . x <= g . x by YELLOW_0:44; ::_thesis: verum end; hence ( not g in the carrier of (L |^ X) or f <= g ) by WAYBEL27:14; ::_thesis: verum end; end; end; end; registration let X be non empty TopSpace; let L be non empty lower-bounded TopPoset; cluster ContMaps (X,L) -> lower-bounded ; coherence ContMaps (X,L) is lower-bounded proof reconsider f = X --> (Bottom L) as Element of (ContMaps (X,L)) by WAYBEL24:21; take f ; :: according to YELLOW_0:def_4 ::_thesis: f is_<=_than the carrier of (ContMaps (X,L)) let g be Element of (ContMaps (X,L)); :: according to LATTICE3:def_8 ::_thesis: ( not g in the carrier of (ContMaps (X,L)) or f <= g ) A1: ContMaps (X,L) is full SubRelStr of L |^ the carrier of X by WAYBEL24:def_3; then reconsider a = g as Element of (L |^ the carrier of X) by YELLOW_0:58; A2: TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) = TopStruct(# the carrier of X, the topology of X #) by WAYBEL25:def_2; then (Omega X) --> (Bottom L) = the carrier of X --> (Bottom L) .= X --> (Bottom L) ; then ( a >= Bottom (L |^ the carrier of X) & Bottom (L |^ the carrier of X) = f ) by A2, WAYBEL24:33, YELLOW_0:44; hence ( not g in the carrier of (ContMaps (X,L)) or f <= g ) by A1, YELLOW_0:60; ::_thesis: verum end; end; registration let L be non empty up-complete Poset; cluster -> up-complete for TopAugmentation of L; coherence for b1 being TopAugmentation of L holds b1 is up-complete proof let S be TopAugmentation of L; ::_thesis: S is up-complete RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; hence S is up-complete by WAYBEL_8:15; ::_thesis: verum end; cluster Scott -> correct for TopAugmentation of L; coherence for b1 being TopAugmentation of L st b1 is Scott holds b1 is correct proof let IT be TopAugmentation of L; ::_thesis: ( IT is Scott implies IT is correct ) assume A1: IT is Scott ; ::_thesis: IT is correct then [#] IT is open ; hence the carrier of IT in the topology of IT by PRE_TOPC:def_2; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of IT) holds ( not b1 c= the topology of IT or union b1 in the topology of IT ) ) & ( for b1, b2 being Element of bool the carrier of IT holds ( not b1 in the topology of IT or not b2 in the topology of IT or b1 /\ b2 in the topology of IT ) ) ) thus for a being Subset-Family of IT st a c= the topology of IT holds union a in the topology of IT ::_thesis: for b1, b2 being Element of bool the carrier of IT holds ( not b1 in the topology of IT or not b2 in the topology of IT or b1 /\ b2 in the topology of IT ) proof let a be Subset-Family of IT; ::_thesis: ( a c= the topology of IT implies union a in the topology of IT ) assume A2: a c= the topology of IT ; ::_thesis: union a in the topology of IT A3: union a is inaccessible proof let D be non empty directed Subset of IT; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,IT) in union a or not D misses union a ) assume sup D in union a ; ::_thesis: not D misses union a then consider A being set such that A4: sup D in A and A5: A in a by TARSKI:def_4; reconsider A = A as Subset of IT by A5; A is open by A2, A5, PRE_TOPC:def_2; then D meets A by A1, A4, WAYBEL11:def_1; then consider x being set such that A6: x in D and A7: x in A by XBOOLE_0:3; x in union a by A5, A7, TARSKI:def_4; hence not D misses union a by A6, XBOOLE_0:3; ::_thesis: verum end; now__::_thesis:_for_X_being_Subset_of_IT_st_X_in_a_holds_ X_is_upper let X be Subset of IT; ::_thesis: ( X in a implies X is upper ) assume X in a ; ::_thesis: X is upper then X is open by A2, PRE_TOPC:def_2; hence X is upper by A1; ::_thesis: verum end; then union a is upper by WAYBEL_0:28; hence union a in the topology of IT by A1, A3, PRE_TOPC:def_2; ::_thesis: verum end; thus for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds a /\ b in the topology of IT ::_thesis: verum proof let a, b be Subset of IT; ::_thesis: ( a in the topology of IT & b in the topology of IT implies a /\ b in the topology of IT ) assume that A8: a in the topology of IT and A9: b in the topology of IT ; ::_thesis: a /\ b in the topology of IT reconsider a1 = a, b1 = b as Subset of IT ; A10: b1 is open by A9, PRE_TOPC:def_2; A11: a1 is open by A8, PRE_TOPC:def_2; A12: a /\ b is inaccessible proof let D be non empty directed Subset of IT; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,IT) in a /\ b or not D misses a /\ b ) assume A13: sup D in a /\ b ; ::_thesis: not D misses a /\ b then sup D in a1 by XBOOLE_0:def_4; then D meets a1 by A1, A11, WAYBEL11:def_1; then consider d1 being set such that A14: d1 in D and A15: d1 in a1 by XBOOLE_0:3; sup D in b1 by A13, XBOOLE_0:def_4; then D meets b1 by A1, A10, WAYBEL11:def_1; then consider d2 being set such that A16: d2 in D and A17: d2 in b1 by XBOOLE_0:3; reconsider d1 = d1, d2 = d2 as Element of IT by A14, A16; consider z being Element of IT such that A18: z in D and A19: d1 <= z and A20: d2 <= z by A14, A16, WAYBEL_0:def_1; A21: z in b1 by A1, A10, A17, A20, WAYBEL_0:def_20; z in a1 by A1, A11, A15, A19, WAYBEL_0:def_20; then z in a /\ b by A21, XBOOLE_0:def_4; hence not D misses a /\ b by A18, XBOOLE_0:3; ::_thesis: verum end; a /\ b is upper by A1, A11, A10, WAYBEL_0:29; hence a /\ b in the topology of IT by A1, A12, PRE_TOPC:def_2; ::_thesis: verum end; end; end; registration let L be non empty up-complete Poset; cluster non empty reflexive transitive antisymmetric up-complete strict Scott non void for TopAugmentation of L; existence ex b1 being TopAugmentation of L st ( b1 is strict & b1 is Scott ) proof set T = { S where S is Subset of L : ( S is upper & S is inaccessible ) } ; { S where S is Subset of L : ( S is upper & S is inaccessible ) } c= bool the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } or x in bool the carrier of L ) assume x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } ; ::_thesis: x in bool the carrier of L then ex S being Subset of L st ( x = S & S is upper & S is inaccessible ) ; hence x in bool the carrier of L ; ::_thesis: verum end; then reconsider T = { S where S is Subset of L : ( S is upper & S is inaccessible ) } as Subset-Family of L ; set SL = TopRelStr(# the carrier of L, the InternalRel of L,T #); A1: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,T #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,T #) #) ; then reconsider SL = TopRelStr(# the carrier of L, the InternalRel of L,T #) as TopAugmentation of L by YELLOW_9:def_4; take SL ; ::_thesis: ( SL is strict & SL is Scott ) for S being Subset of SL holds ( S is open iff ( S is inaccessible & S is upper ) ) proof let S be Subset of SL; ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) ) thus ( S is open implies ( S is inaccessible & S is upper ) ) ::_thesis: ( S is inaccessible & S is upper implies S is open ) proof assume S is open ; ::_thesis: ( S is inaccessible & S is upper ) then S in T by PRE_TOPC:def_2; then ex S1 being Subset of L st ( S1 = S & S1 is upper & S1 is inaccessible ) ; hence ( S is inaccessible & S is upper ) by A1, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum end; thus ( S is inaccessible & S is upper implies S is open ) ::_thesis: verum proof reconsider S1 = S as Subset of L ; assume ( S is inaccessible & S is upper ) ; ::_thesis: S is open then ( S1 is inaccessible & S1 is upper ) by A1, WAYBEL_0:25, YELLOW_9:47; then S in the topology of SL ; hence S is open by PRE_TOPC:def_2; ::_thesis: verum end; end; hence ( SL is strict & SL is Scott ) by WAYBEL11:def_4; ::_thesis: verum end; end; theorem Th13: :: WAYBEL29:13 for L being non empty up-complete Poset for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2 proof let L be non empty up-complete Poset; ::_thesis: for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2 let S1, S2 be Scott TopAugmentation of L; ::_thesis: the topology of S1 = the topology of S2 A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4 .= RelStr(# the carrier of S2, the InternalRel of S2 #) by YELLOW_9:def_4 ; thus the topology of S1 c= the topology of S2 :: according to XBOOLE_0:def_10 ::_thesis: the topology of S2 c= the topology of S1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of S1 or x in the topology of S2 ) assume x in the topology of S1 ; ::_thesis: x in the topology of S2 then reconsider y = x as open Subset of S1 by PRE_TOPC:def_2; reconsider z = y as Subset of S2 by A1; ( z is inaccessible & z is upper ) by A1, WAYBEL_0:25, YELLOW_9:47; hence x in the topology of S2 by PRE_TOPC:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of S2 or x in the topology of S1 ) assume x in the topology of S2 ; ::_thesis: x in the topology of S1 then reconsider y = x as open Subset of S2 by PRE_TOPC:def_2; reconsider z = y as Subset of S1 by A1; ( z is inaccessible & z is upper ) by A1, WAYBEL_0:25, YELLOW_9:47; hence x in the topology of S1 by PRE_TOPC:def_2; ::_thesis: verum end; theorem Th14: :: WAYBEL29:14 for S1, S2 being non empty reflexive antisymmetric up-complete TopRelStr st TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) & S1 is Scott holds S2 is Scott proof let S1, S2 be non empty reflexive antisymmetric up-complete TopRelStr ; ::_thesis: ( TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) & S1 is Scott implies S2 is Scott ) assume A1: TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) ; ::_thesis: ( not S1 is Scott or S2 is Scott ) assume A2: S1 is Scott ; ::_thesis: S2 is Scott let T be Subset of S2; :: according to WAYBEL11:def_4 ::_thesis: ( ( not T is open or ( T is inaccessible_by_directed_joins & T is upper ) ) & ( not T is inaccessible_by_directed_joins or not T is upper or T is open ) ) reconsider T1 = T as Subset of S1 by A1; A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) by A1; thus ( T is open implies ( T is inaccessible & T is upper ) ) ::_thesis: ( not T is inaccessible_by_directed_joins or not T is upper or T is open ) proof assume T is open ; ::_thesis: ( T is inaccessible & T is upper ) then T in the topology of S2 by PRE_TOPC:def_2; then T1 is open by A1, PRE_TOPC:def_2; hence ( T is inaccessible & T is upper ) by A3, A2, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum end; thus ( T is inaccessible & T is upper implies T is open ) ::_thesis: verum proof assume ( T is inaccessible & T is upper ) ; ::_thesis: T is open then ( T1 is inaccessible & T1 is upper ) by A3, WAYBEL_0:25, YELLOW_9:47; then T1 in the topology of S1 by A2, PRE_TOPC:def_2; hence T is open by A1, PRE_TOPC:def_2; ::_thesis: verum end; end; definition let L be non empty up-complete Poset; func Sigma L -> strict Scott TopAugmentation of L means :Def1: :: WAYBEL29:def 1 verum; uniqueness for b1, b2 being strict Scott TopAugmentation of L holds b1 = b2 proof let S1, S2 be strict Scott TopAugmentation of L; ::_thesis: S1 = S2 ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4; hence S1 = S2 by Th13; ::_thesis: verum end; existence ex b1 being strict Scott TopAugmentation of L st verum ; end; :: deftheorem Def1 defines Sigma WAYBEL29:def_1_:_ for L being non empty up-complete Poset for b2 being strict Scott TopAugmentation of L holds ( b2 = Sigma L iff verum ); theorem Th15: :: WAYBEL29:15 for S being non empty up-complete Scott TopPoset holds Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) proof let S be non empty up-complete Scott TopPoset; ::_thesis: Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) RelStr(# the carrier of TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #), the InternalRel of TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) #) = RelStr(# the carrier of S, the InternalRel of S #) ; then reconsider T = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) as TopAugmentation of S by YELLOW_9:def_4; T is Scott by Th14; hence Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by Def1; ::_thesis: verum end; theorem Th16: :: WAYBEL29:16 for L1, L2 being non empty up-complete Poset st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds Sigma L1 = Sigma L2 proof let L1, L2 be non empty up-complete Poset; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies Sigma L1 = Sigma L2 ) assume RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: Sigma L1 = Sigma L2 then A1: RelStr(# the carrier of (Sigma L2), the InternalRel of (Sigma L2) #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4; then ( RelStr(# the carrier of (Sigma L1), the InternalRel of (Sigma L1) #) = RelStr(# the carrier of L1, the InternalRel of L1 #) & Sigma L2 is TopAugmentation of L1 ) by YELLOW_9:def_4; hence Sigma L1 = Sigma L2 by A1, Th13; ::_thesis: verum end; definition let S, T be non empty up-complete Poset; let f be Function of S,T; func Sigma f -> Function of (Sigma S),(Sigma T) equals :: WAYBEL29:def 2 f; coherence f is Function of (Sigma S),(Sigma T) proof ( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def_4; hence f is Function of (Sigma S),(Sigma T) ; ::_thesis: verum end; end; :: deftheorem defines Sigma WAYBEL29:def_2_:_ for S, T being non empty up-complete Poset for f being Function of S,T holds Sigma f = f; registration let S, T be non empty up-complete Poset; let f be directed-sups-preserving Function of S,T; cluster Sigma f -> continuous ; coherence Sigma f is continuous proof ( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def_4; hence Sigma f is continuous by WAYBEL17:29, WAYBEL21:6; ::_thesis: verum end; end; theorem :: WAYBEL29:17 for S, T being non empty up-complete Poset for f being Function of S,T holds ( f is isomorphic iff Sigma f is isomorphic ) proof let S, T be non empty up-complete Poset; ::_thesis: for f being Function of S,T holds ( f is isomorphic iff Sigma f is isomorphic ) let f be Function of S,T; ::_thesis: ( f is isomorphic iff Sigma f is isomorphic ) ( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def_4; hence ( f is isomorphic iff Sigma f is isomorphic ) by Th5; ::_thesis: verum end; theorem Th18: :: WAYBEL29:18 for X being non empty TopSpace for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S) proof let X be non empty TopSpace; ::_thesis: for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S) let S be Scott complete TopLattice; ::_thesis: oContMaps (X,S) = ContMaps (X,S) A1: ( Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ) by WAYBEL25:15; thus oContMaps (X,S) = ContMaps (X,(Omega S)) by WAYBEL26:def_1 .= ContMaps (X,S) by A1, Th10 ; ::_thesis: verum end; definition let X, Y be non empty TopSpace; func Theta (X,Y) -> Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) means :Def3: :: WAYBEL29:def 3 for W being open Subset of [:X,Y:] holds it . W = (W, the carrier of X) *graph ; existence ex b1 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph proof Omega (Sigma (InclPoset the topology of Y)) = Sigma (InclPoset the topology of Y) by WAYBEL25:15; then ( ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,(Sigma (InclPoset the topology of Y)))) st ( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) ) & oContMaps (X,(Sigma (InclPoset the topology of Y))) = ContMaps (X,(Sigma (InclPoset the topology of Y))) ) by WAYBEL26:45, WAYBEL26:def_1; hence ex b1 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st ( for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds b2 . W = (W, the carrier of X) *graph ) holds b1 = b2; proof let F, G be Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))); ::_thesis: ( ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds G . W = (W, the carrier of X) *graph ) implies F = G ) assume that A1: for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph and A2: for W being open Subset of [:X,Y:] holds G . W = (W, the carrier of X) *graph ; ::_thesis: F = G now__::_thesis:_for_x_being_Element_of_(InclPoset_the_topology_of_[:X,Y:])_holds_F_._x_=_G_._x let x be Element of (InclPoset the topology of [:X,Y:]); ::_thesis: F . x = G . x the carrier of (InclPoset the topology of [:X,Y:]) = the topology of [:X,Y:] by YELLOW_1:1; then x in the topology of [:X,Y:] ; then reconsider W = x as open Subset of [:X,Y:] by PRE_TOPC:def_2; thus F . x = (W, the carrier of X) *graph by A1 .= G . x by A2 ; ::_thesis: verum end; hence F = G by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines Theta WAYBEL29:def_3_:_ for X, Y being non empty TopSpace for b3 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds ( b3 = Theta (X,Y) iff for W being open Subset of [:X,Y:] holds b3 . W = (W, the carrier of X) *graph ); defpred S1[ T_0-TopSpace] means for X being non empty TopSpace for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps (\$1,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,\$1:],L)) ex g being Function of (ContMaps ([:X,\$1:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ); defpred S2[ T_0-TopSpace] means for X being non empty TopSpace for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps (\$1,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,\$1:],L)) ex g being Function of (ContMaps ([:X,\$1:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ); defpred S3[ T_0-TopSpace] means for X being non empty TopSpace holds Theta (X,\$1) is isomorphic ; defpred S4[ T_0-TopSpace] means for X being non empty TopSpace for T being Scott TopAugmentation of InclPoset the topology of \$1 for f being continuous Function of X,T holds *graph f is open Subset of [:X,\$1:]; defpred S5[ T_0-TopSpace] means for T being Scott TopAugmentation of InclPoset the topology of \$1 holds { [W,y] where W is open Subset of \$1, y is Element of \$1 : y in W } is open Subset of [:T,\$1:]; defpred S6[ T_0-TopSpace] means for S being Scott TopAugmentation of InclPoset the topology of \$1 for y being Element of \$1 for V being open a_neighborhood of y ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ); Lm1: for T being T_0-TopSpace holds ( S1[T] iff S2[T] ) proof let T be T_0-TopSpace; ::_thesis: ( S1[T] iff S2[T] ) thus ( S1[T] implies S2[T] ) ::_thesis: ( S2[T] implies S1[T] ) proof assume A1: S1[T] ; ::_thesis: S2[T] let X be non empty TopSpace; ::_thesis: for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) let L be Scott continuous complete TopLattice; ::_thesis: for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) let S be Scott TopAugmentation of ContMaps (T,L); ::_thesis: ex f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) consider f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)), g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) such that A2: ( f is uncurrying & f is V7() & f is onto ) and A3: ( g is currying & g is V7() & g is onto ) by A1; A4: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (ContMaps (T,L)), the InternalRel of (ContMaps (T,L)) #) by YELLOW_9:def_4; A5: ContMaps (T,L) is non empty full SubRelStr of L |^ the carrier of T by WAYBEL24:def_3; then A6: the InternalRel of (ContMaps (T,L)) = the InternalRel of (L |^ the carrier of T) |_2 the carrier of (ContMaps (T,L)) by YELLOW_0:def_14; ( the carrier of (ContMaps (T,L)) c= the carrier of (L |^ the carrier of T) & the InternalRel of (ContMaps (T,L)) c= the InternalRel of (L |^ the carrier of T) ) by A5, YELLOW_0:def_13; then S is non empty full SubRelStr of L |^ the carrier of T by A4, A6, YELLOW_0:def_13, YELLOW_0:def_14; then A7: S |^ the carrier of X is non empty full SubRelStr of (L |^ the carrier of T) |^ the carrier of X by YELLOW16:39; L |^ the carrier of [:X,T:] = L |^ [: the carrier of X, the carrier of T:] by BORSUK_1:def_2; then A8: ContMaps ([:X,T:],L) is non empty full SubRelStr of L |^ [: the carrier of X, the carrier of T:] by WAYBEL24:def_3; ContMaps (X,S) is non empty full SubRelStr of S |^ the carrier of X by WAYBEL24:def_3; then ContMaps (X,S) is non empty full SubRelStr of (L |^ the carrier of T) |^ the carrier of X by A7, WAYBEL15:1; then A9: ( f is monotone & g is monotone ) by A2, A3, A8, WAYBEL27:20, WAYBEL27:21; take f ; ::_thesis: ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) take g ; ::_thesis: ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ContMaps (T,L) is non empty full SubRelStr of L |^ the carrier of T by WAYBEL24:def_3; then (ContMaps (T,L)) |^ the carrier of X is full SubRelStr of (L |^ the carrier of T) |^ the carrier of X by YELLOW16:39; then A10: the carrier of ((ContMaps (T,L)) |^ the carrier of X) c= the carrier of ((L |^ the carrier of T) |^ the carrier of X) by YELLOW_0:def_13; A11: rng f = the carrier of (ContMaps ([:X,T:],L)) by A2, FUNCT_2:def_3 .= dom g by FUNCT_2:def_1 ; ContMaps (X,S) is non empty full SubRelStr of S |^ the carrier of X by WAYBEL24:def_3; then the carrier of (ContMaps (X,S)) c= the carrier of (S |^ the carrier of X) by YELLOW_0:def_13; then dom f c= the carrier of (S |^ the carrier of X) by FUNCT_2:def_1; then dom f c= the carrier of ((ContMaps (T,L)) |^ the carrier of X) by A4, WAYBEL27:15; then dom f c= the carrier of ((L |^ the carrier of T) |^ the carrier of X) by A10, XBOOLE_1:1; then dom f c= Funcs ( the carrier of X, the carrier of (L |^ the carrier of T)) by YELLOW_1:28; then dom f c= Funcs ( the carrier of X,(Funcs ( the carrier of T, the carrier of L))) by YELLOW_1:28; then g * f = id (dom f) by A2, A3, A11, WAYBEL27:4; then g = f " by A2, A11, FUNCT_1:41; hence ( f is uncurrying & f is isomorphic ) by A2, A9, WAYBEL_0:def_38; ::_thesis: ( g is currying & g is isomorphic ) A12: rng g = the carrier of (ContMaps (X,S)) by A3, FUNCT_2:def_3 .= dom f by FUNCT_2:def_1 ; ContMaps ([:X,T:],L) is non empty full SubRelStr of L |^ the carrier of [:X,T:] by WAYBEL24:def_3; then the carrier of (ContMaps ([:X,T:],L)) c= the carrier of (L |^ the carrier of [:X,T:]) by YELLOW_0:def_13; then dom g c= the carrier of (L |^ the carrier of [:X,T:]) by FUNCT_2:def_1; then dom g c= Funcs ( the carrier of [:X,T:], the carrier of L) by YELLOW_1:28; then dom g c= Funcs ([: the carrier of X, the carrier of T:], the carrier of L) by BORSUK_1:def_2; then f * g = id (dom g) by A2, A3, A12, WAYBEL27:5; then f = g " by A3, A12, FUNCT_1:41; hence ( g is currying & g is isomorphic ) by A3, A9, WAYBEL_0:def_38; ::_thesis: verum end; assume A13: S2[T] ; ::_thesis: S1[T] let X be non empty TopSpace; ::_thesis: for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) let L be Scott continuous complete TopLattice; ::_thesis: for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) let S be Scott TopAugmentation of ContMaps (T,L); ::_thesis: ex f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) consider f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)), g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) such that A14: ( f is uncurrying & f is isomorphic ) and A15: ( g is currying & g is isomorphic ) by A13; take f ; ::_thesis: ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) take g ; ::_thesis: ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) thus ( f is uncurrying & f is V7() & f is onto ) by A14; ::_thesis: ( g is currying & g is V7() & g is onto ) thus ( g is currying & g is V7() & g is onto ) by A15; ::_thesis: verum end; begin definition let X be non empty TopSpace; func alpha X -> Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) means :Def4: :: WAYBEL29:def 4 for g being continuous Function of X,Sierpinski_Space holds it . g = g " {1}; existence ex b1 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st for g being continuous Function of X,Sierpinski_Space holds b1 . g = g " {1} proof deffunc H1( Function) -> set = \$1 " {1}; consider f being Function such that A1: dom f = the carrier of (oContMaps (X,Sierpinski_Space)) and A2: for x being Element of (oContMaps (X,Sierpinski_Space)) holds f . x = H1(x) from FUNCT_1:sch_4(); rng f c= the topology of X proof the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9; then {1} in the topology of Sierpinski_Space by ENUMSET1:def_1; then reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def_2; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the topology of X ) assume y in rng f ; ::_thesis: y in the topology of X then consider x being set such that A3: x in dom f and A4: y = f . x by FUNCT_1:def_3; reconsider x = x as Element of (oContMaps (X,Sierpinski_Space)) by A1, A3; reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2; [#] Sierpinski_Space <> {} ; then A5: g " A is open by TOPS_2:43; y = g " A by A2, A4; hence y in the topology of X by A5, PRE_TOPC:def_2; ::_thesis: verum end; then rng f c= the carrier of (InclPoset the topology of X) by YELLOW_1:1; then reconsider f = f as Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) by A1, FUNCT_2:2; take f ; ::_thesis: for g being continuous Function of X,Sierpinski_Space holds f . g = g " {1} let g be continuous Function of X,Sierpinski_Space; ::_thesis: f . g = g " {1} g is Element of (oContMaps (X,Sierpinski_Space)) by WAYBEL26:2; hence f . g = g " {1} by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st ( for g being continuous Function of X,Sierpinski_Space holds b1 . g = g " {1} ) & ( for g being continuous Function of X,Sierpinski_Space holds b2 . g = g " {1} ) holds b1 = b2 proof let f1, f2 be Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X); ::_thesis: ( ( for g being continuous Function of X,Sierpinski_Space holds f1 . g = g " {1} ) & ( for g being continuous Function of X,Sierpinski_Space holds f2 . g = g " {1} ) implies f1 = f2 ) assume that A6: for g being continuous Function of X,Sierpinski_Space holds f1 . g = g " {1} and A7: for g being continuous Function of X,Sierpinski_Space holds f2 . g = g " {1} ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_Element_of_(oContMaps_(X,Sierpinski_Space))_holds_f1_._x_=_f2_._x let x be Element of (oContMaps (X,Sierpinski_Space)); ::_thesis: f1 . x = f2 . x reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2; thus f1 . x = g " {1} by A6 .= f2 . x by A7 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines alpha WAYBEL29:def_4_:_ for X being non empty TopSpace for b2 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) holds ( b2 = alpha X iff for g being continuous Function of X,Sierpinski_Space holds b2 . g = g " {1} ); theorem :: WAYBEL29:19 for X being non empty TopSpace for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X) proof A1: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9; the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9; then {1} in the topology of Sierpinski_Space by ENUMSET1:def_1; then reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def_2; let X be non empty TopSpace; ::_thesis: for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X) consider f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) such that A2: f is isomorphic and A3: for V being open Subset of X holds f . V = chi (V, the carrier of X) by WAYBEL26:5; A4: the carrier of (InclPoset the topology of X) = the topology of X by YELLOW_1:1; A5: rng f = [#] (oContMaps (X,Sierpinski_Space)) by A2, WAYBEL_0:66; A6: f " = f " by A2, TOPS_2:def_4; now__::_thesis:_for_x_being_Element_of_(oContMaps_(X,Sierpinski_Space))_holds_(alpha_X)_._x_=_(f_")_._x let x be Element of (oContMaps (X,Sierpinski_Space)); ::_thesis: (alpha X) . x = (f ") . x reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2; [#] Sierpinski_Space <> {} ; then A7: g " A is open by TOPS_2:43; then A8: g " A in the topology of X by PRE_TOPC:def_2; A9: f . (g " A) = chi ((g " A), the carrier of X) by A3, A7 .= x by A1, FUNCT_3:40 ; thus (alpha X) . x = g " A by Def4 .= (f ") . x by A2, A6, A4, A8, A9, FUNCT_2:26 ; ::_thesis: verum end; then alpha X = f " by FUNCT_2:63; then (alpha X) " = f by A2, A5, TOPS_2:51; hence for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X) by A3; ::_thesis: verum end; registration let X be non empty TopSpace; cluster alpha X -> isomorphic ; coherence alpha X is isomorphic proof the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9; then {1} in the topology of Sierpinski_Space by ENUMSET1:def_1; then reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def_2; consider f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) such that A1: f is isomorphic and A2: for V being open Subset of X holds f . V = chi (V, the carrier of X) by WAYBEL26:5; A3: f " = f " by A1, TOPS_2:def_4; A4: the carrier of (InclPoset the topology of X) = the topology of X by YELLOW_1:1; A5: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9; now__::_thesis:_for_x_being_Element_of_(oContMaps_(X,Sierpinski_Space))_holds_(alpha_X)_._x_=_(f_")_._x let x be Element of (oContMaps (X,Sierpinski_Space)); ::_thesis: (alpha X) . x = (f ") . x reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2; [#] Sierpinski_Space <> {} ; then A6: g " A is open by TOPS_2:43; then A7: g " A in the topology of X by PRE_TOPC:def_2; A8: f . (g " A) = chi ((g " A), the carrier of X) by A2, A6 .= x by A5, FUNCT_3:40 ; thus (alpha X) . x = g " A by Def4 .= (f ") . x by A1, A3, A4, A7, A8, FUNCT_2:26 ; ::_thesis: verum end; hence alpha X is isomorphic by A1, A3, FUNCT_2:63, WAYBEL_0:68; ::_thesis: verum end; end; registration let X be non empty TopSpace; cluster(alpha X) " -> isomorphic ; coherence (alpha X) " is isomorphic by YELLOW14:10; end; registration let S be injective T_0-TopSpace; cluster Omega S -> Scott ; coherence Omega S is Scott proof set T = the strict Scott TopAugmentation of Omega S; A1: TopStruct(# the carrier of the strict Scott TopAugmentation of Omega S, the topology of the strict Scott TopAugmentation of Omega S #) = TopStruct(# the carrier of S, the topology of S #) by WAYBEL25:37 .= TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) by WAYBEL25:def_2 ; RelStr(# the carrier of the strict Scott TopAugmentation of Omega S, the InternalRel of the strict Scott TopAugmentation of Omega S #) = RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) by YELLOW_9:def_4; hence Omega S is Scott by A1; ::_thesis: verum end; end; registration let X be non empty TopSpace; cluster oContMaps (X,Sierpinski_Space) -> complete ; coherence oContMaps (X,Sierpinski_Space) is complete proof InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by WAYBEL26:6; hence oContMaps (X,Sierpinski_Space) is complete by WAYBEL20:18; ::_thesis: verum end; end; theorem :: WAYBEL29:20 Omega Sierpinski_Space = Sigma (BoolePoset 1) proof set S = Sigma (BoolePoset 1); reconsider T = Omega Sierpinski_Space as strict Scott TopAugmentation of BoolePoset 1 by WAYBEL26:4; A1: the topology of T = sigma (BoolePoset 1) by YELLOW_9:51 .= the topology of (Sigma (BoolePoset 1)) by YELLOW_9:51 ; RelStr(# the carrier of T, the InternalRel of T #) = BoolePoset 1 by YELLOW_9:def_4 .= RelStr(# the carrier of (Sigma (BoolePoset 1)), the InternalRel of (Sigma (BoolePoset 1)) #) by YELLOW_9:def_4 ; hence Omega Sierpinski_Space = Sigma (BoolePoset 1) by A1; ::_thesis: verum end; registration let M be non empty set ; let S be injective T_0-TopSpace; cluster product (M => S) -> injective ; coherence M -TOP_prod (M => S) is injective proof for m being Element of M holds (M => S) . m is injective by FUNCOP_1:7; hence M -TOP_prod (M => S) is injective by WAYBEL18:7; ::_thesis: verum end; end; theorem :: WAYBEL29:21 for M being non empty set for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L)) proof let M be non empty set ; ::_thesis: for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L)) let L be continuous complete LATTICE; ::_thesis: Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L)) A1: RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; reconsider S = Sigma L as injective T_0-TopSpace ; Omega (Sigma L) = Sigma L by WAYBEL25:15; then RelStr(# the carrier of (Omega (M -TOP_prod (M => (Sigma L)))), the InternalRel of (Omega (M -TOP_prod (M => (Sigma L)))) #) = M -POS_prod (M => (Sigma L)) by WAYBEL25:14 .= (Sigma L) |^ M by YELLOW_1:def_5 .= L |^ M by A1, WAYBEL27:15 ; then Sigma (L |^ M) = Sigma (Omega (M -TOP_prod (M => S))) by Th16 .= Omega (M -TOP_prod (M => (Sigma L))) by Th15 ; hence Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L)) by YELLOW_1:def_5; ::_thesis: verum end; theorem :: WAYBEL29:22 for M being non empty set for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T))) proof let M be non empty set ; ::_thesis: for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T))) let T be injective T_0-TopSpace; ::_thesis: Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T))) set L = Omega T; RelStr(# the carrier of (Omega (M -TOP_prod (M => T))), the InternalRel of (Omega (M -TOP_prod (M => T))) #) = M -POS_prod (M => (Omega T)) by WAYBEL25:14; then Sigma (Omega (M -TOP_prod (M => T))) = Sigma (M -POS_prod (M => (Omega T))) by Th16; hence Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T))) by Th15; ::_thesis: verum end; definition let M be non empty set ; let X, Y be non empty TopSpace; func commute (X,M,Y) -> Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) means :Def5: :: WAYBEL29:def 5 for f being continuous Function of X,(M -TOP_prod (M => Y)) holds it . f = commute f; uniqueness for b1, b2 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b2 . f = commute f ) holds b1 = b2 proof let F1, F2 be Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M); ::_thesis: ( ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F1 . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F2 . f = commute f ) implies F1 = F2 ) assume that A1: for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F1 . f = commute f and A2: for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F2 . f = commute f ; ::_thesis: F1 = F2 now__::_thesis:_for_f_being_Element_of_(oContMaps_(X,(M_-TOP_prod_(M_=>_Y))))_holds_F1_._f_=_F2_._f let f be Element of (oContMaps (X,(M -TOP_prod (M => Y)))); ::_thesis: F1 . f = F2 . f reconsider g = f as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:2; thus F1 . f = commute g by A1 .= F2 . f by A2 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; existence ex b1 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f proof deffunc H1( Function) -> set = commute \$1; consider F being Function such that A3: dom F = the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) and A4: for f being Element of (oContMaps (X,(M -TOP_prod (M => Y)))) holds F . f = H1(f) from FUNCT_1:sch_4(); rng F c= the carrier of ((oContMaps (X,Y)) |^ M) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of ((oContMaps (X,Y)) |^ M) ) assume y in rng F ; ::_thesis: y in the carrier of ((oContMaps (X,Y)) |^ M) then consider x being set such that A5: x in dom F and A6: y = F . x by FUNCT_1:def_3; reconsider x = x as Element of (oContMaps (X,(M -TOP_prod (M => Y)))) by A3, A5; reconsider f = x as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:2; ( commute f is Function of M, the carrier of (oContMaps (X,Y)) & y = commute x ) by A4, A6, WAYBEL26:31; then y in Funcs (M, the carrier of (oContMaps (X,Y))) by FUNCT_2:8; hence y in the carrier of ((oContMaps (X,Y)) |^ M) by YELLOW_1:28; ::_thesis: verum end; then reconsider F = F as Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) by A3, FUNCT_2:2; take F ; ::_thesis: for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F . f = commute f let f be continuous Function of X,(M -TOP_prod (M => Y)); ::_thesis: F . f = commute f f is Element of (oContMaps (X,(M -TOP_prod (M => Y)))) by WAYBEL26:2; hence F . f = commute f by A4; ::_thesis: verum end; end; :: deftheorem Def5 defines commute WAYBEL29:def_5_:_ for M being non empty set for X, Y being non empty TopSpace for b4 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) holds ( b4 = commute (X,M,Y) iff for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b4 . f = commute f ); registration let M be non empty set ; let X, Y be non empty TopSpace; cluster commute (X,M,Y) -> V7() onto ; correctness coherence ( commute (X,M,Y) is one-to-one & commute (X,M,Y) is onto ); proof set f = commute (X,M,Y); Carrier (M => Y) = M => the carrier of Y by WAYBEL26:30; then the carrier of (M -TOP_prod (M => Y)) = product (M => the carrier of Y) by WAYBEL18:def_3 .= Funcs (M, the carrier of Y) by CARD_3:11 ; then A1: the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) c= Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by WAYBEL26:32; now__::_thesis:_(_the_carrier_of_((oContMaps_(X,Y))_|^_M)_<>_{}_&_(_for_x1,_x2_being_set_st_x1_in_the_carrier_of_(oContMaps_(X,(M_-TOP_prod_(M_=>_Y))))_&_x2_in_the_carrier_of_(oContMaps_(X,(M_-TOP_prod_(M_=>_Y))))_&_(commute_(X,M,Y))_._x1_=_(commute_(X,M,Y))_._x2_holds_ x1_=_x2_)_) thus the carrier of ((oContMaps (X,Y)) |^ M) <> {} ; ::_thesis: for x1, x2 being set st x1 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & x2 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 holds x1 = x2 let x1, x2 be set ; ::_thesis: ( x1 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & x2 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 implies x1 = x2 ) assume that A2: x1 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) and A3: x2 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) ; ::_thesis: ( (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 implies x1 = x2 ) reconsider a1 = x1, a2 = x2 as Element of (oContMaps (X,(M -TOP_prod (M => Y)))) by A2, A3; reconsider f1 = a1, f2 = a2 as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:2; assume (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 ; ::_thesis: x1 = x2 then commute f1 = (commute (X,M,Y)) . x2 by Def5 .= commute f2 by Def5 ; then f1 = commute (commute f2) by A1, A2, FUNCT_6:57; hence x1 = x2 by A1, A3, FUNCT_6:57; ::_thesis: verum end; hence commute (X,M,Y) is V7() by FUNCT_2:19; ::_thesis: commute (X,M,Y) is onto rng (commute (X,M,Y)) = the carrier of ((oContMaps (X,Y)) |^ M) proof thus rng (commute (X,M,Y)) c= the carrier of ((oContMaps (X,Y)) |^ M) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((oContMaps (X,Y)) |^ M) c= rng (commute (X,M,Y)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((oContMaps (X,Y)) |^ M) or x in rng (commute (X,M,Y)) ) assume A4: x in the carrier of ((oContMaps (X,Y)) |^ M) ; ::_thesis: x in rng (commute (X,M,Y)) then reconsider x = x as Element of ((oContMaps (X,Y)) |^ M) ; A5: the carrier of ((oContMaps (X,Y)) |^ M) = Funcs (M, the carrier of (oContMaps (X,Y))) by YELLOW_1:28; then reconsider x = x as Function of M, the carrier of (oContMaps (X,Y)) by FUNCT_2:66; reconsider g = commute x as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:33; reconsider y = g as Element of (oContMaps (X,(M -TOP_prod (M => Y)))) by WAYBEL26:2; the carrier of ((oContMaps (X,Y)) |^ M) c= Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by A5, FUNCT_5:56, WAYBEL26:32; then commute (commute x) = x by A4, FUNCT_6:57; then A6: (commute (X,M,Y)) . y = x by Def5; dom (commute (X,M,Y)) = the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) by FUNCT_2:def_1; hence x in rng (commute (X,M,Y)) by A6, FUNCT_1:def_3; ::_thesis: verum end; hence commute (X,M,Y) is onto by FUNCT_2:def_3; ::_thesis: verum end; end; registration let M be non empty set ; let X be non empty TopSpace; cluster commute (X,M,Sierpinski_Space) -> isomorphic ; correctness coherence commute (X,M,Sierpinski_Space) is isomorphic ; proof M -POS_prod (M => (oContMaps (X,Sierpinski_Space))) = (oContMaps (X,Sierpinski_Space)) |^ M by YELLOW_1:def_5; then ex f1 being Function of (oContMaps (X,(M -TOP_prod (M => Sierpinski_Space)))),((oContMaps (X,Sierpinski_Space)) |^ M) st ( f1 is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M => Sierpinski_Space)) holds f1 . f = commute f ) ) by WAYBEL26:34; hence commute (X,M,Sierpinski_Space) is isomorphic by Def5; ::_thesis: verum end; end; Lm2: for T being T_0-TopSpace st S3[T] holds S4[T] proof let Y be T_0-TopSpace; ::_thesis: ( S3[Y] implies S4[Y] ) assume A1: S3[Y] ; ::_thesis: S4[Y] set S = Sigma (InclPoset the topology of Y); let X be non empty TopSpace; ::_thesis: for T being Scott TopAugmentation of InclPoset the topology of Y for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:] let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:] A2: the topology of T = sigma (InclPoset the topology of Y) by YELLOW_9:51; let f be continuous Function of X,T; ::_thesis: *graph f is open Subset of [:X,Y:] ( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def_4; then A3: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) & TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) = TopRelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by A2, YELLOW_9:51; then reconsider F = Theta (X,Y) as Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,T)) by Th10; ContMaps (X,T) = ContMaps (X,(Sigma (InclPoset the topology of Y))) by A3, Th10; then F is isomorphic by A1; then ( f in the carrier of (ContMaps (X,T)) & rng F = the carrier of (ContMaps (X,T)) ) by WAYBEL24:def_3, WAYBEL_0:66; then consider W being set such that A4: W in dom F and A5: f = F . W by FUNCT_1:def_3; dom F = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def_1 .= the topology of [:X,Y:] by YELLOW_1:1 ; then reconsider W = W as open Subset of [:X,Y:] by A4, PRE_TOPC:def_2; reconsider R = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def_2; A6: dom R c= the carrier of X ; f = (W, the carrier of X) *graph by A5, Def3; hence *graph f is open Subset of [:X,Y:] by A6, WAYBEL26:41; ::_thesis: verum end; theorem Th23: :: WAYBEL29:23 for X, Y being non empty TopSpace for S being Scott TopAugmentation of InclPoset the topology of Y for f1, f2 being Element of (ContMaps (X,S)) st f1 <= f2 holds *graph f1 c= *graph f2 proof let X, Y be non empty TopSpace; ::_thesis: for S being Scott TopAugmentation of InclPoset the topology of Y for f1, f2 being Element of (ContMaps (X,S)) st f1 <= f2 holds *graph f1 c= *graph f2 let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f1, f2 being Element of (ContMaps (X,S)) st f1 <= f2 holds *graph f1 c= *graph f2 let f1, f2 be Element of (ContMaps (X,S)); ::_thesis: ( f1 <= f2 implies *graph f1 c= *graph f2 ) assume A1: f1 <= f2 ; ::_thesis: *graph f1 c= *graph f2 reconsider F1 = f1, F2 = f2 as Function of X,S by WAYBEL24:21; let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in *graph f1 or [a,b] in *graph f2 ) A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4; f2 is Function of X,S by WAYBEL24:21; then A3: dom f2 = the carrier of X by FUNCT_2:def_1; assume A4: [a,b] in *graph f1 ; ::_thesis: [a,b] in *graph f2 then A5: ( a in dom f1 & b in f1 . a ) by WAYBEL26:38; f1 is Function of X,S by WAYBEL24:21; then A6: dom f1 = the carrier of X by FUNCT_2:def_1; then reconsider a9 = a as Element of X by A4, WAYBEL26:38; F1 . a9 is Element of S ; then f1 . a in the carrier of (InclPoset the topology of Y) by A2; then A7: f1 . a in the topology of Y by YELLOW_1:1; F2 . a9 is Element of S ; then f2 . a in the carrier of (InclPoset the topology of Y) by A2; then A8: f2 . a in the topology of Y by YELLOW_1:1; [(f1 . a9),(f2 . a9)] in the InternalRel of S by A1, WAYBEL24:20; then [(f1 . a),(f2 . a)] in RelIncl the topology of Y by A2, YELLOW_1:1; then f1 . a c= f2 . a by A7, A8, WELLORD2:def_1; hence [a,b] in *graph f2 by A6, A3, A5, WAYBEL26:38; ::_thesis: verum end; Lm3: for T being T_0-TopSpace st S4[T] holds S3[T] proof deffunc H1( Function) -> set = *graph \$1; let Y be T_0-TopSpace; ::_thesis: ( S4[Y] implies S3[Y] ) assume A1: S4[Y] ; ::_thesis: S3[Y] set T = Sigma (InclPoset the topology of Y); let X be non empty TopSpace; ::_thesis: Theta (X,Y) is isomorphic consider G being Function such that A2: dom G = the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) and A3: for f being Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds G . f = H1(f) from FUNCT_1:sch_4(); rng G c= the carrier of (InclPoset the topology of [:X,Y:]) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of (InclPoset the topology of [:X,Y:]) ) assume x in rng G ; ::_thesis: x in the carrier of (InclPoset the topology of [:X,Y:]) then consider a being set such that A4: a in dom G and A5: x = G . a by FUNCT_1:def_3; reconsider a = a as Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by A2, A4; reconsider a = a as continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL24:21; x = *graph a by A3, A5; then x is open Subset of [:X,Y:] by A1; then x in the topology of [:X,Y:] by PRE_TOPC:def_2; hence x in the carrier of (InclPoset the topology of [:X,Y:]) by YELLOW_1:1; ::_thesis: verum end; then reconsider G = G as Function of (ContMaps (X,(Sigma (InclPoset the topology of Y)))),(InclPoset the topology of [:X,Y:]) by A2, FUNCT_2:2; consider F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,(Sigma (InclPoset the topology of Y)))) such that A6: F is monotone and A7: for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph by WAYBEL26:45; A8: G is monotone proof let f1, f2 be Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))); :: according to WAYBEL_1:def_2 ::_thesis: ( not f1 <= f2 or G . f1 <= G . f2 ) assume f1 <= f2 ; ::_thesis: G . f1 <= G . f2 then *graph f1 c= *graph f2 by Th23; then G . f1 c= *graph f2 by A3; then G . f1 c= G . f2 by A3; hence G . f1 <= G . f2 by YELLOW_1:3; ::_thesis: verum end; reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) by Th18; dom F = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def_1; then rng G c= dom F ; then A9: dom (F * G) = the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by A2, RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(ContMaps_(X,(Sigma_(InclPoset_the_topology_of_Y))))_holds_ (F_*_G)_._x_=_x let x be set ; ::_thesis: ( x in the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) implies (F * G) . x = x ) assume A10: x in the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) ; ::_thesis: (F * G) . x = x then reconsider x1 = x as continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL24:21; reconsider gx = *graph x1 as open Subset of [:X,Y:] by A1; A11: dom x1 = the carrier of X by FUNCT_2:def_1; A12: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_X_holds_ x1_._i_=_Im_(gx,i) let i be set ; ::_thesis: ( i in the carrier of X implies x1 . i = Im (gx,i) ) assume i in the carrier of X ; ::_thesis: x1 . i = Im (gx,i) then A13: i in dom x1 by FUNCT_2:def_1; A14: i in {i} by TARSKI:def_1; thus x1 . i = Im (gx,i) ::_thesis: verum proof thus x1 . i c= Im (gx,i) :: according to XBOOLE_0:def_10 ::_thesis: Im (gx,i) c= x1 . i proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in x1 . i or b in Im (gx,i) ) assume b in x1 . i ; ::_thesis: b in Im (gx,i) then [i,b] in gx by A13, WAYBEL26:38; hence b in Im (gx,i) by A14, RELAT_1:def_13; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Im (gx,i) or b in x1 . i ) assume b in Im (gx,i) ; ::_thesis: b in x1 . i then ex j being set st ( [j,b] in gx & j in {i} ) by RELAT_1:def_13; then [i,b] in gx by TARSKI:def_1; hence b in x1 . i by WAYBEL26:38; ::_thesis: verum end; end; (F * G) . x = F . (G . x1) by A9, A10, FUNCT_1:12 .= F . gx by A3, A10 .= (gx, the carrier of X) *graph by A7 ; hence (F * G) . x = x by A11, A12, WAYBEL26:def_5; ::_thesis: verum end; then A15: F * G = id (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by A9, FUNCT_1:17; A16: dom (G * F) = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(InclPoset_the_topology_of_[:X,Y:])_holds_ (G_*_F)_._x_=_x let x be set ; ::_thesis: ( x in the carrier of (InclPoset the topology of [:X,Y:]) implies (G * F) . x = x ) assume A17: x in the carrier of (InclPoset the topology of [:X,Y:]) ; ::_thesis: (G * F) . x = x then x in the topology of [:X,Y:] by YELLOW_1:1; then reconsider x1 = x as open Subset of [:X,Y:] by PRE_TOPC:def_2; (x1, the carrier of X) *graph is continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL26:43; then reconsider x1X = (x1, the carrier of X) *graph as Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by WAYBEL24:21; x1 c= the carrier of [:X,Y:] ; then A18: x1 c= [: the carrier of X, the carrier of Y:] by BORSUK_1:def_2; A19: dom x1 c= the carrier of X proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in dom x1 or d in the carrier of X ) assume d in dom x1 ; ::_thesis: d in the carrier of X then ex e being set st [d,e] in x1 by XTUPLE_0:def_12; hence d in the carrier of X by A18, ZFMISC_1:87; ::_thesis: verum end; thus (G * F) . x = G . (F . x1) by A16, A17, FUNCT_1:12 .= G . x1X by A7 .= *graph x1X by A3 .= x by A19, WAYBEL26:41 ; ::_thesis: verum end; then A20: G * F = id (InclPoset the topology of [:X,Y:]) by A16, FUNCT_1:17; ContMaps (X,(Sigma (InclPoset the topology of Y))) = oContMaps (X,(Sigma (InclPoset the topology of Y))) by Th18; then F is isomorphic by A6, A8, A15, A20, YELLOW16:15; hence Theta (X,Y) is isomorphic by A7, Def3; ::_thesis: verum end; Lm4: for T being T_0-TopSpace st S4[T] holds S5[T] proof let Y be T_0-TopSpace; ::_thesis: ( S4[Y] implies S5[Y] ) assume A1: S4[Y] ; ::_thesis: S5[Y] let X be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:X,Y:] reconsider f = id X as continuous Function of X,X ; A2: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4; *graph f = { [W,y] where W is open Subset of Y, y is Element of Y : y in W } proof thus *graph f c= { [W,y] where W is open Subset of Y, y is Element of Y : y in W } :: according to XBOOLE_0:def_10 ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } c= *graph f proof let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in *graph f or [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } ) assume A3: [a,b] in *graph f ; ::_thesis: [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } then A4: a in dom f by WAYBEL26:38; A5: b in f . a by A3, WAYBEL26:38; dom f = the carrier of (InclPoset the topology of Y) by A2, FUNCT_2:def_1 .= the topology of Y by YELLOW_1:1 ; then reconsider a = a as open Subset of Y by A4, PRE_TOPC:def_2; f . a = a by A4, FUNCT_1:18; then reconsider b = b as Element of Y by A5; b in a by A4, A5, FUNCT_1:18; hence [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } ; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } or e in *graph f ) assume e in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } ; ::_thesis: e in *graph f then consider W being open Subset of Y, y being Element of Y such that A6: ( e = [W,y] & y in W ) ; W in the topology of Y by PRE_TOPC:def_2; then W in the carrier of (InclPoset the topology of Y) by YELLOW_1:1; then ( W in dom f & f . W = W ) by A2, FUNCT_1:18, FUNCT_2:def_1; hence e in *graph f by A6, WAYBEL26:38; ::_thesis: verum end; hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:X,Y:] by A1; ::_thesis: verum end; Lm5: for T being T_0-TopSpace st S5[T] holds S6[T] proof let Y be T_0-TopSpace; ::_thesis: ( S5[Y] implies S6[Y] ) assume A1: S5[Y] ; ::_thesis: S6[Y] let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ) reconsider A = { [W,z] where W is open Subset of Y, z is Element of Y : z in W } as open Subset of [:S,Y:] by A1; let y be Element of Y; ::_thesis: for V being open a_neighborhood of y ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ) let V be open a_neighborhood of y; ::_thesis: ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ) ( the topology of S is Basis of S & the topology of Y is Basis of Y ) by CANTOR_1:2; then reconsider B = { [:a,b:] where a is Subset of S, b is Subset of Y : ( a in the topology of S & b in the topology of Y ) } as Basis of [:S,Y:] by YELLOW_9:40; y in V by CONNSP_2:4; then [V,y] in A ; then consider ab being Subset of [:S,Y:] such that A2: ab in B and A3: [V,y] in ab and A4: ab c= A by YELLOW_9:31; consider H being Subset of S, W being Subset of Y such that A5: ab = [:H,W:] and A6: H in the topology of S and A7: W in the topology of Y by A2; reconsider H = H as open Subset of S by A6, PRE_TOPC:def_2; A8: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4; meet H c= the carrier of Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet H or x in the carrier of Y ) H <> {} by A3, A5; then consider A being set such that A9: A in H by XBOOLE_0:def_1; A in the carrier of S by A9; then A10: A in the topology of Y by A8, YELLOW_1:1; assume x in meet H ; ::_thesis: x in the carrier of Y then x in A by A9, SETFAM_1:def_1; hence x in the carrier of Y by A10; ::_thesis: verum end; then reconsider mH = meet H as Subset of Y ; reconsider W = W as open Subset of Y by A7, PRE_TOPC:def_2; W c= mH proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in W or w in mH ) assume A11: w in W ; ::_thesis: w in mH A12: now__::_thesis:_for_a_being_set_st_a_in_H_holds_ w_in_a let a be set ; ::_thesis: ( a in H implies w in a ) assume a in H ; ::_thesis: w in a then [a,w] in ab by A5, A11, ZFMISC_1:87; then [a,w] in A by A4; then consider a1 being open Subset of Y, w1 being Element of Y such that A13: [a,w] = [a1,w1] and A14: w1 in a1 ; a = a1 by A13, XTUPLE_0:1; hence w in a by A13, A14, XTUPLE_0:1; ::_thesis: verum end; H <> {} by A3, A5; hence w in mH by A12, SETFAM_1:def_1; ::_thesis: verum end; then A15: W c= Int mH by TOPS_1:24; take H ; ::_thesis: ( V in H & meet H is a_neighborhood of y ) thus V in H by A3, A5, ZFMISC_1:87; ::_thesis: meet H is a_neighborhood of y y in W by A3, A5, ZFMISC_1:87; hence meet H is a_neighborhood of y by A15, CONNSP_2:def_1; ::_thesis: verum end; Lm6: for T being T_0-TopSpace st S6[T] holds S4[T] proof let Y be T_0-TopSpace; ::_thesis: ( S6[Y] implies S4[Y] ) assume A1: S6[Y] ; ::_thesis: S4[Y] let X be non empty TopSpace; ::_thesis: for T being Scott TopAugmentation of InclPoset the topology of Y for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:] let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:] let f be continuous Function of X,T; ::_thesis: *graph f is open Subset of [:X,Y:] ( the topology of X is Basis of X & the topology of Y is Basis of Y ) by CANTOR_1:2; then reconsider B = { [:a,b:] where a is Subset of X, b is Subset of Y : ( a in the topology of X & b in the topology of Y ) } as Basis of [:X,Y:] by YELLOW_9:40; A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4; now__::_thesis:_for_s_being_set_st_s_in_*graph_f_holds_ s_in_the_carrier_of_[:X,Y:] let s be set ; ::_thesis: ( s in *graph f implies s in the carrier of [:X,Y:] ) assume A3: s in *graph f ; ::_thesis: s in the carrier of [:X,Y:] then consider s1, s2 being set such that A4: s = [s1,s2] by RELAT_1:def_1; A5: s1 in dom f by A3, A4, WAYBEL26:38; then f . s1 in rng f by FUNCT_1:def_3; then f . s1 in the carrier of T ; then A6: f . s1 in the topology of Y by A2, YELLOW_1:1; s2 in f . s1 by A3, A4, WAYBEL26:38; then s in [: the carrier of X, the carrier of Y:] by A4, A5, A6, ZFMISC_1:87; hence s in the carrier of [:X,Y:] by BORSUK_1:def_2; ::_thesis: verum end; then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def_3; now__::_thesis:_for_p_being_Point_of_[:X,Y:]_st_p_in_A_holds_ ex_a_being_Subset_of_[:X,Y:]_st_ (_a_in_B_&_p_in_a_&_a_c=_A_) let p be Point of [:X,Y:]; ::_thesis: ( p in A implies ex a being Subset of [:X,Y:] st ( a in B & p in a & a c= A ) ) assume A7: p in A ; ::_thesis: ex a being Subset of [:X,Y:] st ( a in B & p in a & a c= A ) then consider x, y being set such that A8: p = [x,y] by RELAT_1:def_1; A9: y in f . x by A7, A8, WAYBEL26:38; A10: x in dom f by A7, A8, WAYBEL26:38; then reconsider x = x as Element of X ; f . x in the carrier of (InclPoset the topology of Y) by A2; then A11: f . x in the topology of Y by YELLOW_1:1; then reconsider y = y as Element of Y by A9; reconsider W = f . x as open Subset of Y by A11, PRE_TOPC:def_2; y in Int W by A9, TOPS_1:23; then reconsider W = W as open a_neighborhood of y by CONNSP_2:def_1; consider H being open Subset of T such that A12: W in H and A13: meet H is a_neighborhood of y by A1; [#] T <> {} ; then reconsider fH = f " H as open Subset of X by TOPS_2:43; reconsider mH = meet H as a_neighborhood of y by A13; Int (Int mH) = Int mH ; then reconsider V = Int mH as open a_neighborhood of y by CONNSP_2:def_1; reconsider a = [:fH,V:] as Subset of [:X,Y:] ; take a = a; ::_thesis: ( a in B & p in a & a c= A ) ( V in the topology of Y & fH in the topology of X ) by PRE_TOPC:def_2; hence a in B ; ::_thesis: ( p in a & a c= A ) ( y in Int mH & x in fH ) by A10, A12, CONNSP_2:def_1, FUNCT_1:def_7; hence p in a by A8, ZFMISC_1:87; ::_thesis: a c= A thus a c= A ::_thesis: verum proof let s1, s2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [s1,s2] in a or [s1,s2] in A ) A14: V c= mH by TOPS_1:16; assume A15: [s1,s2] in a ; ::_thesis: [s1,s2] in A then A16: s1 in fH by ZFMISC_1:87; then A17: f . s1 in H by FUNCT_1:def_7; A18: s1 in dom f by A16, FUNCT_1:def_7; s2 in V by A15, ZFMISC_1:87; then s2 in f . s1 by A17, A14, SETFAM_1:def_1; hence [s1,s2] in A by A18, WAYBEL26:38; ::_thesis: verum end; end; hence *graph f is open Subset of [:X,Y:] by YELLOW_9:31; ::_thesis: verum end; Lm7: for T being T_0-TopSpace st S6[T] holds InclPoset the topology of T is continuous proof let Y be T_0-TopSpace; ::_thesis: ( S6[Y] implies InclPoset the topology of Y is continuous ) assume A1: S6[Y] ; ::_thesis: InclPoset the topology of Y is continuous set L = InclPoset the topology of Y; set S = the Scott TopAugmentation of InclPoset the topology of Y; thus for x being Element of (InclPoset the topology of Y) holds ( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( InclPoset the topology of Y is up-complete & InclPoset the topology of Y is satisfying_axiom_of_approximation ) thus InclPoset the topology of Y is up-complete ; ::_thesis: InclPoset the topology of Y is satisfying_axiom_of_approximation let A be Element of (InclPoset the topology of Y); :: according to WAYBEL_3:def_5 ::_thesis: A = "\/" ((waybelow A),(InclPoset the topology of Y)) the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1; then A in the topology of Y ; then reconsider B = A as open Subset of Y by PRE_TOPC:def_2; A2: RelStr(# the carrier of the Scott TopAugmentation of InclPoset the topology of Y, the InternalRel of the Scott TopAugmentation of InclPoset the topology of Y #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4; thus A c= sup (waybelow A) :: according to XBOOLE_0:def_10 ::_thesis: "\/" ((waybelow A),(InclPoset the topology of Y)) c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in sup (waybelow A) ) assume A3: x in A ; ::_thesis: x in sup (waybelow A) then x in B ; then reconsider x9 = x as Element of Y ; reconsider B = B as open a_neighborhood of x9 by A3, CONNSP_2:3; consider H being open Subset of the Scott TopAugmentation of InclPoset the topology of Y such that A4: B in H and A5: meet H is a_neighborhood of x9 by A1; reconsider mH = meet H as a_neighborhood of x9 by A5; reconsider H1 = H as Subset of (InclPoset the topology of Y) by A2; Int mH in the topology of Y by PRE_TOPC:def_2; then reconsider ImH = Int mH as Element of (InclPoset the topology of Y) by YELLOW_1:1; ImH << A proof let D be non empty directed Subset of (InclPoset the topology of Y); :: according to WAYBEL_3:def_1 ::_thesis: ( not A <= "\/" (D,(InclPoset the topology of Y)) or ex b1 being Element of the carrier of (InclPoset the topology of Y) st ( b1 in D & ImH <= b1 ) ) A6: ( H1 is inaccessible & H1 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47; assume A <= sup D ; ::_thesis: ex b1 being Element of the carrier of (InclPoset the topology of Y) st ( b1 in D & ImH <= b1 ) then sup D in H1 by A4, A6, WAYBEL_0:def_20; then D meets H1 by A6, WAYBEL11:def_1; then consider d being set such that A7: d in D and A8: d in H1 by XBOOLE_0:3; reconsider d = d as Element of (InclPoset the topology of Y) by A7; take d ; ::_thesis: ( d in D & ImH <= d ) thus d in D by A7; ::_thesis: ImH <= d ( Int mH c= mH & mH c= d ) by A8, SETFAM_1:3, TOPS_1:16; then ImH c= d by XBOOLE_1:1; hence ImH <= d by YELLOW_1:3; ::_thesis: verum end; then ( x in Int mH & Int mH in waybelow A ) by CONNSP_2:def_1; then x in union (waybelow A) by TARSKI:def_4; hence x in sup (waybelow A) by YELLOW_1:22; ::_thesis: verum end; union (waybelow A) c= union (downarrow A) by WAYBEL_3:11, ZFMISC_1:77; then sup (waybelow A) c= union (downarrow A) by YELLOW_1:22; then sup (waybelow A) c= sup (downarrow A) by YELLOW_1:22; hence "\/" ((waybelow A),(InclPoset the topology of Y)) c= A by WAYBEL_0:34; ::_thesis: verum end; Lm8: for T being T_0-TopSpace st InclPoset the topology of T is continuous holds S6[T] proof let T be T_0-TopSpace; ::_thesis: ( InclPoset the topology of T is continuous implies S6[T] ) assume A1: InclPoset the topology of T is continuous ; ::_thesis: S6[T] let S be Scott TopAugmentation of InclPoset the topology of T; ::_thesis: for y being Element of T for V being open a_neighborhood of y ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ) let y be Element of T; ::_thesis: for V being open a_neighborhood of y ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ) let V be open a_neighborhood of y; ::_thesis: ex H being open Subset of S st ( V in H & meet H is a_neighborhood of y ) A2: ( Int V c= V & y in Int V ) by CONNSP_2:def_1, TOPS_1:16; V in the topology of T by PRE_TOPC:def_2; then reconsider W = V as Element of (InclPoset the topology of T) by YELLOW_1:1; W = sup (waybelow W) by A1, WAYBEL_3:def_5 .= union (waybelow W) by YELLOW_1:22 ; then consider Z being set such that A3: y in Z and A4: Z in waybelow W by A2, TARSKI:def_4; reconsider Z = Z as Element of (InclPoset the topology of T) by A4; A5: RelStr(# the carrier of (InclPoset the topology of T), the InternalRel of (InclPoset the topology of T) #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then reconsider Z1 = Z as Element of S ; Z in the carrier of (InclPoset the topology of T) ; then Z in the topology of T by YELLOW_1:1; then reconsider Z2 = Z as open Subset of T by PRE_TOPC:def_2; A6: Z c= meet (uparrow Z) proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Z or s in meet (uparrow Z) ) assume A7: s in Z ; ::_thesis: s in meet (uparrow Z) now__::_thesis:_for_z_being_set_st_z_in_uparrow_Z_holds_ s_in_z let z be set ; ::_thesis: ( z in uparrow Z implies s in z ) assume A8: z in uparrow Z ; ::_thesis: s in z then reconsider z1 = z as Element of (InclPoset the topology of T) ; Z <= z1 by A8, WAYBEL_0:18; then Z c= z by YELLOW_1:3; hence s in z by A7; ::_thesis: verum end; hence s in meet (uparrow Z) by SETFAM_1:def_1; ::_thesis: verum end; reconsider H = wayabove Z1 as open Subset of S by A1, WAYBEL11:36; take H ; ::_thesis: ( V in H & meet H is a_neighborhood of y ) Z << W by A4, WAYBEL_3:7; then A9: V in wayabove Z ; hence A10: V in H by A5, YELLOW12:13; ::_thesis: meet H is a_neighborhood of y meet H c= the carrier of T proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in meet H or s in the carrier of T ) assume s in meet H ; ::_thesis: s in the carrier of T then s in V by A10, SETFAM_1:def_1; hence s in the carrier of T ; ::_thesis: verum end; then reconsider mH = meet H as Subset of T ; meet (uparrow Z) c= meet (wayabove Z) by A9, SETFAM_1:6, WAYBEL_3:11; then meet (uparrow Z) c= meet (wayabove Z1) by A5, YELLOW12:13; then Z2 c= mH by A6, XBOOLE_1:1; then Z2 c= Int mH by TOPS_1:24; hence meet H is a_neighborhood of y by A3, CONNSP_2:def_1; ::_thesis: verum end; begin theorem :: WAYBEL29:24 for Y being T_0-TopSpace holds ( ( for X being non empty TopSpace for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) ) iff for X being non empty TopSpace for L being Scott continuous complete TopLattice for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1; theorem :: WAYBEL29:25 for Y being T_0-TopSpace holds ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta (X,Y) is isomorphic ) proof let Y be T_0-TopSpace; ::_thesis: ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta (X,Y) is isomorphic ) hereby ::_thesis: ( ( for X being non empty TopSpace holds Theta (X,Y) is isomorphic ) implies InclPoset the topology of Y is continuous ) assume InclPoset the topology of Y is continuous ; ::_thesis: S3[Y] then S6[Y] by Lm8; then S4[Y] by Lm6; hence S3[Y] by Lm3; ::_thesis: verum end; assume S3[Y] ; ::_thesis: InclPoset the topology of Y is continuous then S4[Y] by Lm2; then S5[Y] by Lm4; then S6[Y] by Lm5; hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum end; theorem :: WAYBEL29:26 for Y being T_0-TopSpace holds ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ) proof let Y be T_0-TopSpace; ::_thesis: ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ) hereby ::_thesis: ( ( for X being non empty TopSpace for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ) implies InclPoset the topology of Y is continuous ) assume InclPoset the topology of Y is continuous ; ::_thesis: for X being non empty TopSpace for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] then S6[Y] by Lm8; hence for X being non empty TopSpace for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] by Lm6; ::_thesis: verum end; assume A1: for X being non empty TopSpace for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ; ::_thesis: InclPoset the topology of Y is continuous S4[Y] proof let X be non empty TopSpace; ::_thesis: for T being Scott TopAugmentation of InclPoset the topology of Y for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:] let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:] let f be continuous Function of X,T; ::_thesis: *graph f is open Subset of [:X,Y:] A2: ( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def_4; then reconsider g = f as Function of X,(Sigma (InclPoset the topology of Y)) ; ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) & TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by A2, Th13; then g is continuous by YELLOW12:36; hence *graph f is open Subset of [:X,Y:] by A1; ::_thesis: verum end; then S5[Y] by Lm4; then S6[Y] by Lm5; hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum end; theorem :: WAYBEL29:27 for Y being T_0-TopSpace holds ( InclPoset the topology of Y is continuous iff { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] ) proof let Y be T_0-TopSpace; ::_thesis: ( InclPoset the topology of Y is continuous iff { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] ) hereby ::_thesis: ( { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] implies InclPoset the topology of Y is continuous ) assume InclPoset the topology of Y is continuous ; ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] then S6[Y] by Lm8; then S4[Y] by Lm6; hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] by Lm4; ::_thesis: verum end; assume A1: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] ; ::_thesis: InclPoset the topology of Y is continuous S5[Y] proof let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:] ( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def_4; then ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y, the topology of Y #) & TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by Th13; then [:T,Y:] = [:(Sigma (InclPoset the topology of Y)),Y:] by Th7; hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:] by A1; ::_thesis: verum end; then S6[Y] by Lm5; hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum end; theorem :: WAYBEL29:28 for Y being T_0-TopSpace holds ( InclPoset the topology of Y is continuous iff for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st ( V in H & meet H is a_neighborhood of y ) ) proof let Y be T_0-TopSpace; ::_thesis: ( InclPoset the topology of Y is continuous iff for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st ( V in H & meet H is a_neighborhood of y ) ) thus ( InclPoset the topology of Y is continuous implies for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st ( V in H & meet H is a_neighborhood of y ) ) by Lm8; ::_thesis: ( ( for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st ( V in H & meet H is a_neighborhood of y ) ) implies InclPoset the topology of Y is continuous ) assume A1: for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st ( V in H & meet H is a_neighborhood of y ) ; ::_thesis: InclPoset the topology of Y is continuous S6[Y] proof let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for y being Element of Y for V being open a_neighborhood of y ex H being open Subset of T st ( V in H & meet H is a_neighborhood of y ) let y be Element of Y; ::_thesis: for V being open a_neighborhood of y ex H being open Subset of T st ( V in H & meet H is a_neighborhood of y ) let V be open a_neighborhood of y; ::_thesis: ex H being open Subset of T st ( V in H & meet H is a_neighborhood of y ) consider H being open Subset of (Sigma (InclPoset the topology of Y)) such that A2: ( V in H & meet H is a_neighborhood of y ) by A1; ( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def_4; then reconsider G = H as Subset of T ; the topology of T = the topology of (Sigma (InclPoset the topology of Y)) by Th13; then G in the topology of T by PRE_TOPC:def_2; then H is open Subset of T by PRE_TOPC:def_2; hence ex H being open Subset of T st ( V in H & meet H is a_neighborhood of y ) by A2; ::_thesis: verum end; hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum end; defpred S7[ complete LATTICE] means InclPoset (sigma \$1) is continuous ; defpred S8[ complete LATTICE] means for SL being Scott TopAugmentation of \$1 for S being complete LATTICE for SS being Scott TopAugmentation of S holds sigma [:S,\$1:] = the topology of [:SS,SL:]; defpred S9[ complete LATTICE] means for SL being Scott TopAugmentation of \$1 for S being complete LATTICE for SS being Scott TopAugmentation of S for SSL being Scott TopAugmentation of [:S,\$1:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]; Lm9: for L being complete LATTICE holds ( S8[L] iff S9[L] ) proof let L be complete LATTICE; ::_thesis: ( S8[L] iff S9[L] ) thus ( S8[L] implies S9[L] ) ::_thesis: ( S9[L] implies S8[L] ) proof assume A1: S8[L] ; ::_thesis: S9[L] let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE for SS being Scott TopAugmentation of S for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] let SS be Scott TopAugmentation of S; ::_thesis: for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] let SSL be Scott TopAugmentation of [:S,L:]; ::_thesis: TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] A2: the topology of [:SS,SL:] = sigma [:S,L:] by A1 .= the topology of SSL by YELLOW_9:51 ; A3: RelStr(# the carrier of SSL, the InternalRel of SSL #) = RelStr(# the carrier of [:S,L:], the InternalRel of [:S,L:] #) by YELLOW_9:def_4; ( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def_4; then the carrier of SSL = [: the carrier of SS, the carrier of SL:] by A3, YELLOW_3:def_2 .= the carrier of [:SS,SL:] by BORSUK_1:def_2 ; hence TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] by A2; ::_thesis: verum end; assume A4: S9[L] ; ::_thesis: S8[L] let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:] now__::_thesis:_for_SSL_being_Scott_TopAugmentation_of_[:S,L:]_holds_sigma_[:S,L:]_=_the_topology_of_[:SS,SL:] let SSL be Scott TopAugmentation of [:S,L:]; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:] TopStruct(# the carrier of SSL, the topology of SSL #) = TopStruct(# the carrier of [:SS,SL:], the topology of [:SS,SL:] #) by A4; hence sigma [:S,L:] = the topology of [:SS,SL:] by YELLOW_9:51; ::_thesis: verum end; hence sigma [:S,L:] = the topology of [:SS,SL:] ; ::_thesis: verum end; begin theorem :: WAYBEL29:29 for R1, R2, R3 being non empty RelStr for f1 being Function of R1,R3 st f1 is isomorphic holds for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) proof let R1, R2, R3 be non empty RelStr ; ::_thesis: for f1 being Function of R1,R3 st f1 is isomorphic holds for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) let f1 be Function of R1,R3; ::_thesis: ( f1 is isomorphic implies for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ) assume A1: f1 is isomorphic ; ::_thesis: for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) let f2 be Function of R2,R3; ::_thesis: ( f2 = f1 & f2 is isomorphic implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ) assume that A2: f2 = f1 and A3: f2 is isomorphic ; ::_thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) A4: the carrier of R1 = rng (f2 ") by A1, A2, WAYBEL_0:67 .= the carrier of R2 by A3, WAYBEL_0:67 ; A5: the InternalRel of R2 c= the InternalRel of R1 proof let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in the InternalRel of R2 or [x1,x2] in the InternalRel of R1 ) assume A6: [x1,x2] in the InternalRel of R2 ; ::_thesis: [x1,x2] in the InternalRel of R1 then reconsider x19 = x1, x29 = x2 as Element of R2 by ZFMISC_1:87; reconsider y1 = x19, y2 = x29 as Element of R1 by A4; x19 <= x29 by A6, ORDERS_2:def_5; then f2 . x19 <= f2 . x29 by A3, WAYBEL_0:66; then y1 <= y2 by A1, A2, WAYBEL_0:66; hence [x1,x2] in the InternalRel of R1 by ORDERS_2:def_5; ::_thesis: verum end; the InternalRel of R1 c= the InternalRel of R2 proof let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in the InternalRel of R1 or [x1,x2] in the InternalRel of R2 ) assume A7: [x1,x2] in the InternalRel of R1 ; ::_thesis: [x1,x2] in the InternalRel of R2 then reconsider x19 = x1, x29 = x2 as Element of R1 by ZFMISC_1:87; reconsider y1 = x19, y2 = x29 as Element of R2 by A4; x19 <= x29 by A7, ORDERS_2:def_5; then f1 . x19 <= f1 . x29 by A1, WAYBEL_0:66; then y1 <= y2 by A2, A3, WAYBEL_0:66; hence [x1,x2] in the InternalRel of R2 by ORDERS_2:def_5; ::_thesis: verum end; hence RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A4, A5, XBOOLE_0:def_10; ::_thesis: verum end; Lm10: for L being complete LATTICE st S7[L] holds S8[L] proof let L be complete LATTICE; ::_thesis: ( S7[L] implies S8[L] ) assume A1: S7[L] ; ::_thesis: S8[L] let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:] A2: RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; UPS (L,(BoolePoset 1)) is non empty full SubRelStr of (BoolePoset 1) |^ the carrier of L by WAYBEL27:def_4; then A3: (UPS (L,(BoolePoset 1))) |^ the carrier of S is non empty full SubRelStr of ((BoolePoset 1) |^ the carrier of L) |^ the carrier of S by YELLOW16:39; UPS (S,(UPS (L,(BoolePoset 1)))) is non empty full SubRelStr of (UPS (L,(BoolePoset 1))) |^ the carrier of S by WAYBEL27:def_4; then A4: UPS (S,(UPS (L,(BoolePoset 1)))) is non empty full SubRelStr of ((BoolePoset 1) |^ the carrier of L) |^ the carrier of S by A3, WAYBEL15:1; consider f5 being Function of (UPS (L,(BoolePoset 1))),(InclPoset (sigma L)) such that A5: f5 is isomorphic and A6: for f being directed-sups-preserving Function of L,(BoolePoset 1) holds f5 . f = f " {1} by WAYBEL27:33; set f6 = UPS ((id S),f5); consider f3 being Function of (UPS (S,(UPS (L,(BoolePoset 1))))),(UPS ([:S,L:],(BoolePoset 1))) such that A7: ( f3 is uncurrying & f3 is isomorphic ) by WAYBEL27:47; set f4 = f3 " ; set T = Sigma (InclPoset the topology of SL); consider f1 being Function of (UPS ([:S,L:],(BoolePoset 1))),(InclPoset (sigma [:S,L:])) such that A8: f1 is isomorphic and A9: for f being directed-sups-preserving Function of [:S,L:],(BoolePoset 1) holds f1 . f = f " {1} by WAYBEL27:33; A10: f3 " is isomorphic by A7, YELLOW14:10; set f2 = f1 " ; set G = ((UPS ((id S),f5)) * (f3 ")) * (f1 "); A11: the topology of SL = sigma L by YELLOW_9:51; then A12: RelStr(# the carrier of (Sigma (InclPoset the topology of SL)), the InternalRel of (Sigma (InclPoset the topology of SL)) #) = RelStr(# the carrier of (InclPoset (sigma L)), the InternalRel of (InclPoset (sigma L)) #) by YELLOW_9:def_4; A13: the carrier of (UPS (S,(InclPoset (sigma L)))) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) proof thus the carrier of (UPS (S,(InclPoset (sigma L)))) c= the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) c= the carrier of (UPS (S,(InclPoset (sigma L)))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (UPS (S,(InclPoset (sigma L)))) or x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ) assume A14: x in the carrier of (UPS (S,(InclPoset (sigma L)))) ; ::_thesis: x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) then reconsider x1 = x as Function of SS,(Sigma (InclPoset the topology of SL)) by A2, A12, WAYBEL27:def_4; x is directed-sups-preserving Function of S,(InclPoset (sigma L)) by A14, WAYBEL27:def_4; then x1 is directed-sups-preserving by A2, A12, WAYBEL21:6; then x1 is continuous by WAYBEL17:22; hence x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by WAYBEL24:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) or x in the carrier of (UPS (S,(InclPoset (sigma L)))) ) assume x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ; ::_thesis: x in the carrier of (UPS (S,(InclPoset (sigma L)))) then consider x1 being Function of SS,(Sigma (InclPoset the topology of SL)) such that A15: x1 = x and A16: x1 is continuous by WAYBEL24:def_3; reconsider x2 = x1 as Function of S,(InclPoset (sigma L)) by A2, A12; x1 is directed-sups-preserving by A16, WAYBEL17:22; then x2 is directed-sups-preserving by A2, A12, WAYBEL21:6; hence x in the carrier of (UPS (S,(InclPoset (sigma L)))) by A15, WAYBEL27:def_4; ::_thesis: verum end; then reconsider G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ") as Function of (InclPoset (sigma [:S,L:])),(ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ; set F = Theta (SS,SL); A17: RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; ( (BoolePoset 1) |^ the carrier of [:S,L:] = (BoolePoset 1) |^ [: the carrier of S, the carrier of L:] & UPS ([:S,L:],(BoolePoset 1)) is non empty full SubRelStr of (BoolePoset 1) |^ the carrier of [:S,L:] ) by WAYBEL27:def_4, YELLOW_3:def_2; then A18: f3 " is currying by A7, A4, Th2; A19: for V being Element of (InclPoset (sigma [:S,L:])) for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V } proof let V be Element of (InclPoset (sigma [:S,L:])); ::_thesis: for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V } let s be Element of S; ::_thesis: (G . V) . s = { y where y is Element of L : [s,y] in V } reconsider fff = (f3 ") . ((f1 ") . V) as directed-sups-preserving Function of S,(UPS (L,(BoolePoset 1))) by WAYBEL27:def_4; reconsider f2V = (f1 ") . V as directed-sups-preserving Function of [:S,L:],(BoolePoset 1) by WAYBEL27:def_4; A20: ( f5 is sups-preserving & (f5 * fff) * (id the carrier of S) = f5 * fff ) by A5, FUNCT_2:17, WAYBEL13:20; A21: ((f3 ") . ((f1 ") . V)) . s is directed-sups-preserving Function of L,(BoolePoset 1) by WAYBEL27:def_4; then A22: dom (((f3 ") . ((f1 ") . V)) . s) = the carrier of L by FUNCT_2:def_1; G . V = ((UPS ((id S),f5)) * (f3 ")) . ((f1 ") . V) by FUNCT_2:15 .= (UPS ((id S),f5)) . ((f3 ") . ((f1 ") . V)) by FUNCT_2:15 .= f5 * fff by A20, WAYBEL27:def_5 ; then A23: (G . V) . s = f5 . (fff . s) by FUNCT_2:15 .= (((f3 ") . ((f1 ") . V)) . s) " {1} by A6, A21 ; A24: rng f1 = [#] (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def_3; dom (f3 ") = the carrier of (UPS ([:S,L:],(BoolePoset 1))) by FUNCT_2:def_1; then A25: (f3 ") . ((f1 ") . V) = curry ((f1 ") . V) by A18, WAYBEL27:def_2; rng f1 = the carrier of (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def_3; then A26: V = (id (rng f1)) . V by FUNCT_1:18 .= (f1 * (f1 ")) . V by A8, A24, TOPS_2:52 .= f1 . ((f1 ") . V) by FUNCT_2:15 .= f2V " {1} by A9 ; thus (G . V) . s c= { y where y is Element of L : [s,y] in V } :: according to XBOOLE_0:def_10 ::_thesis: { y where y is Element of L : [s,y] in V } c= (G . V) . s proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (G . V) . s or x in { y where y is Element of L : [s,y] in V } ) assume A27: x in (G . V) . s ; ::_thesis: x in { y where y is Element of L : [s,y] in V } then x in dom (((f3 ") . ((f1 ") . V)) . s) by A23, FUNCT_1:def_7; then reconsider y = x as Element of L by A21, FUNCT_2:def_1; (((f3 ") . ((f1 ") . V)) . s) . x in {1} by A23, A27, FUNCT_1:def_7; then A28: (((f3 ") . ((f1 ") . V)) . s) . y = 1 by TARSKI:def_1; A29: dom f2V = the carrier of [:S,L:] by FUNCT_2:def_1; then [s,y] in dom ((f1 ") . V) ; then ((f1 ") . V) . (s,y) = 1 by A25, A28, FUNCT_5:20; then ((f1 ") . V) . (s,y) in {1} by TARSKI:def_1; then [s,y] in ((f1 ") . V) " {1} by A29, FUNCT_1:def_7; hence x in { y where y is Element of L : [s,y] in V } by A26; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Element of L : [s,y] in V } or x in (G . V) . s ) assume x in { y where y is Element of L : [s,y] in V } ; ::_thesis: x in (G . V) . s then consider y being Element of L such that A30: y = x and A31: [s,y] in V ; dom f2V = the carrier of [:S,L:] by FUNCT_2:def_1; then A32: [s,y] in dom ((f1 ") . V) ; then reconsider cs = (curry ((f1 ") . V)) . s as Function by FUNCT_5:19; ((f1 ") . V) . (s,y) in {1} by A26, A31, FUNCT_1:def_7; then ((f1 ") . V) . (s,y) = 1 by TARSKI:def_1; then cs . y = 1 by A32, FUNCT_5:20; then (((f3 ") . ((f1 ") . V)) . s) . y in {1} by A25, TARSKI:def_1; hence x in (G . V) . s by A23, A30, A22, FUNCT_1:def_7; ::_thesis: verum end; S6[SL] by A1, A11, Lm8; then S4[SL] by Lm6; then A33: Theta (SS,SL) is isomorphic by Lm3; A34: the carrier of (InclPoset (sigma [:S,L:])) c= the carrier of (InclPoset the topology of [:SS,SL:]) proof let V be set ; :: according to TARSKI:def_3 ::_thesis: ( not V in the carrier of (InclPoset (sigma [:S,L:])) or V in the carrier of (InclPoset the topology of [:SS,SL:]) ) assume V in the carrier of (InclPoset (sigma [:S,L:])) ; ::_thesis: V in the carrier of (InclPoset the topology of [:SS,SL:]) then reconsider V1 = V as Element of (InclPoset (sigma [:S,L:])) ; rng (Theta (SS,SL)) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by A33, FUNCT_2:def_3; then consider W being set such that A35: W in dom (Theta (SS,SL)) and A36: (Theta (SS,SL)) . W = G . V1 by FUNCT_1:def_3; reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) by A35; dom (Theta (SS,SL)) = the carrier of (InclPoset the topology of [:SS,SL:]) by FUNCT_2:def_1; then W in the topology of [:SS,SL:] by A35, YELLOW_1:1; then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def_2; A37: V c= W proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in V or v in W ) assume A38: v in V ; ::_thesis: v in W V1 in the carrier of (InclPoset (sigma [:S,L:])) ; then V in sigma [:S,L:] by YELLOW_1:1; then V c= the carrier of [:S,L:] ; then V c= [: the carrier of S, the carrier of L:] by YELLOW_3:def_2; then consider v1, v2 being set such that A39: v1 in the carrier of S and A40: v2 in the carrier of L and A41: v = [v1,v2] by A38, ZFMISC_1:84; reconsider v2 = v2 as Element of L by A40; reconsider v1 = v1 as Element of S by A39; v2 in { y where y is Element of L : [v1,y] in V } by A38, A41; then v2 in (G . V1) . v1 by A19; then v2 in ((W1, the carrier of S) *graph) . v1 by A2, A36, Def3; then v2 in Im (W1,v1) by WAYBEL26:def_5; then ex v19 being set st ( [v19,v2] in W & v19 in {v1} ) by RELAT_1:def_13; hence v in W by A41, TARSKI:def_1; ::_thesis: verum end; W c= V proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in W or w in V ) assume A42: w in W ; ::_thesis: w in V W1 c= the carrier of [:SS,SL:] ; then W1 c= [: the carrier of SS, the carrier of SL:] by BORSUK_1:def_2; then consider w1, w2 being set such that A43: w1 in the carrier of S and A44: w2 in the carrier of L and A45: w = [w1,w2] by A2, A17, A42, ZFMISC_1:84; reconsider w2 = w2 as Element of L by A44; reconsider w1 = w1 as Element of S by A43; w1 in {w1} by TARSKI:def_1; then w2 in Im (W1,w1) by A42, A45, RELAT_1:def_13; then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def_5; then w2 in ((Theta (SS,SL)) . W2) . w1 by A2, Def3; then w2 in { y where y is Element of L : [w1,y] in V } by A19, A36; then ex w29 being Element of L st ( w29 = w2 & [w1,w29] in V ) ; hence w in V by A45; ::_thesis: verum end; then W2 = V by A37, XBOOLE_0:def_10; hence V in the carrier of (InclPoset the topology of [:SS,SL:]) ; ::_thesis: verum end; InclPoset (sigma L) = InclPoset the topology of SL by YELLOW_9:51; then UPS ((id S),f5) is isomorphic by A5, WAYBEL27:35; then A46: (UPS ((id S),f5)) * (f3 ") is isomorphic by A10, Th6; A47: f1 " is isomorphic by A8, YELLOW14:10; the carrier of (InclPoset the topology of [:SS,SL:]) c= the carrier of (InclPoset (sigma [:S,L:])) proof let W be set ; :: according to TARSKI:def_3 ::_thesis: ( not W in the carrier of (InclPoset the topology of [:SS,SL:]) or W in the carrier of (InclPoset (sigma [:S,L:])) ) assume A48: W in the carrier of (InclPoset the topology of [:SS,SL:]) ; ::_thesis: W in the carrier of (InclPoset (sigma [:S,L:])) then reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) ; W in the topology of [:SS,SL:] by A48, YELLOW_1:1; then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def_2; G is onto by A47, A46, A13, Th6, YELLOW14:9; then rng G = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by FUNCT_2:def_3; then consider V being set such that A49: V in dom G and A50: G . V = (Theta (SS,SL)) . W2 by FUNCT_1:def_3; reconsider V = V as Element of (InclPoset (sigma [:S,L:])) by A49; A51: V c= W proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in V or v in W ) assume A52: v in V ; ::_thesis: v in W V in the carrier of (InclPoset (sigma [:S,L:])) ; then V in sigma [:S,L:] by YELLOW_1:1; then V c= the carrier of [:S,L:] ; then V c= [: the carrier of S, the carrier of L:] by YELLOW_3:def_2; then consider v1, v2 being set such that A53: v1 in the carrier of S and A54: v2 in the carrier of L and A55: v = [v1,v2] by A52, ZFMISC_1:84; reconsider v2 = v2 as Element of L by A54; reconsider v1 = v1 as Element of S by A53; v2 in { y where y is Element of L : [v1,y] in V } by A52, A55; then v2 in (G . V) . v1 by A19; then v2 in ((W1, the carrier of S) *graph) . v1 by A2, A50, Def3; then v2 in Im (W1,v1) by WAYBEL26:def_5; then ex v19 being set st ( [v19,v2] in W & v19 in {v1} ) by RELAT_1:def_13; hence v in W by A55, TARSKI:def_1; ::_thesis: verum end; W c= V proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in W or w in V ) assume A56: w in W ; ::_thesis: w in V W1 c= the carrier of [:SS,SL:] ; then W1 c= [: the carrier of SS, the carrier of SL:] by BORSUK_1:def_2; then consider w1, w2 being set such that A57: w1 in the carrier of S and A58: w2 in the carrier of L and A59: w = [w1,w2] by A2, A17, A56, ZFMISC_1:84; reconsider w2 = w2 as Element of L by A58; reconsider w1 = w1 as Element of S by A57; w1 in {w1} by TARSKI:def_1; then w2 in Im (W1,w1) by A56, A59, RELAT_1:def_13; then w2 in ((W1, the carrier of S) *graph) . w1 by WAYBEL26:def_5; then w2 in ((Theta (SS,SL)) . W2) . w1 by A2, Def3; then w2 in { y where y is Element of L : [w1,y] in V } by A19, A50; then ex w29 being Element of L st ( w29 = w2 & [w1,w29] in V ) ; hence w in V by A59; ::_thesis: verum end; then W = V by A51, XBOOLE_0:def_10; hence W in the carrier of (InclPoset (sigma [:S,L:])) ; ::_thesis: verum end; then the carrier of (InclPoset (sigma [:S,L:])) = the carrier of (InclPoset the topology of [:SS,SL:]) by A34, XBOOLE_0:def_10; hence sigma [:S,L:] = the carrier of (InclPoset the topology of [:SS,SL:]) by YELLOW_1:1 .= the topology of [:SS,SL:] by YELLOW_1:1 ; ::_thesis: verum end; Lm11: for L being complete LATTICE st S8[L] holds S7[L] proof let L be complete LATTICE; ::_thesis: ( S8[L] implies S7[L] ) set SL = the Scott TopAugmentation of L; A1: RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) = ConvergenceSpace (Scott-Convergence the Scott TopAugmentation of L) by WAYBEL11:32; then A2: the topology of the Scott TopAugmentation of L = sigma the Scott TopAugmentation of L ; then A3: InclPoset (sigma L) = InclPoset the topology of the Scott TopAugmentation of L by A1, YELLOW_9:52; then reconsider S = InclPoset (sigma L) as complete LATTICE ; set SS = the Scott TopAugmentation of S; assume S8[L] ; ::_thesis: S7[L] then A4: sigma [:S,L:] = the topology of [: the Scott TopAugmentation of S, the Scott TopAugmentation of L:] ; A5: S5[ the Scott TopAugmentation of L] proof set Wy = { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } ; let T be Scott TopAugmentation of InclPoset the topology of the Scott TopAugmentation of L; ::_thesis: { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } is open Subset of [:T, the Scott TopAugmentation of L:] { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } c= the carrier of [:T, the Scott TopAugmentation of L:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } or x in the carrier of [:T, the Scott TopAugmentation of L:] ) A6: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of the Scott TopAugmentation of L), the InternalRel of (InclPoset the topology of the Scott TopAugmentation of L) #) by YELLOW_9:def_4; assume x in { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } ; ::_thesis: x in the carrier of [:T, the Scott TopAugmentation of L:] then consider W being open Subset of the Scott TopAugmentation of L, y being Element of the Scott TopAugmentation of L such that A7: x = [W,y] and y in W ; W in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2; then W in the carrier of (InclPoset the topology of the Scott TopAugmentation of L) by YELLOW_1:1; then [W,y] in [: the carrier of T, the carrier of the Scott TopAugmentation of L:] by A6, ZFMISC_1:87; hence x in the carrier of [:T, the Scott TopAugmentation of L:] by A7, BORSUK_1:def_2; ::_thesis: verum end; then reconsider WY = { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } as Subset of [:T, the Scott TopAugmentation of L:] ; A8: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of (InclPoset the topology of the Scott TopAugmentation of L), the InternalRel of (InclPoset the topology of the Scott TopAugmentation of L) #) by A3, YELLOW_9:def_4 .= RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4 ; reconsider T1 = T as Scott TopAugmentation of S by A1, A2, YELLOW_9:52; A9: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; the carrier of [:T, the Scott TopAugmentation of L:] = [: the carrier of T, the carrier of the Scott TopAugmentation of L:] by BORSUK_1:def_2 .= the carrier of [:S,L:] by A1, A8, A9, YELLOW_3:def_2 ; then reconsider wy = WY as Subset of [:S,L:] ; A10: wy is inaccessible proof let D be non empty directed Subset of [:S,L:]; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,[:S,L:]) in wy or not D misses wy ) assume sup D in wy ; ::_thesis: not D misses wy then [(sup (proj1 D)),(sup (proj2 D))] in wy by YELLOW_3:46; then consider sp1D being open Subset of the Scott TopAugmentation of L, sp2D being Element of the Scott TopAugmentation of L such that A11: [(sup (proj1 D)),(sup (proj2 D))] = [sp1D,sp2D] and A12: sp2D in sp1D ; reconsider sp1D9 = sp1D as Subset of L by A1; reconsider sp1D9 = sp1D9 as upper inaccessible Subset of L by A1, WAYBEL_0:25, YELLOW_9:47; reconsider pD = proj1 D as Subset of (InclPoset the topology of the Scott TopAugmentation of L) by A1, A2, YELLOW_9:52; reconsider proj2D = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22; A13: sup (proj1 D) = union pD by A3, YELLOW_1:22; sup proj2D in sp1D9 by A11, A12, XTUPLE_0:1; then proj2 D meets sp1D by WAYBEL11:def_1; then consider d being set such that A14: d in proj2 D and A15: d in sp1D by XBOOLE_0:3; reconsider d = d as Element of L by A14; d in sup (proj1 D) by A11, A15, XTUPLE_0:1; then consider V being set such that A16: d in V and A17: V in proj1 D by A13, TARSKI:def_4; consider Y being set such that A18: [Y,d] in D by A14, XTUPLE_0:def_13; reconsider V = V as Element of S by A17; consider e being set such that A19: [V,e] in D by A17, XTUPLE_0:def_12; A20: Y in proj1 D by A18, XTUPLE_0:def_12; A21: e in proj2 D by A19, XTUPLE_0:def_13; reconsider Y = Y as Element of S by A20; reconsider e = e as Element of L by A21; consider DD being Element of [:S,L:] such that A22: DD in D and A23: [V,e] <= DD and A24: [Y,d] <= DD by A18, A19, WAYBEL_0:def_1; D c= the carrier of [:S,L:] ; then D c= [: the carrier of S, the carrier of L:] by YELLOW_3:def_2; then consider DD1, DD2 being set such that A25: DD = [DD1,DD2] by A22, RELAT_1:def_1; A26: DD2 in proj2 D by A22, A25, XTUPLE_0:def_13; A27: DD1 in proj1 D by A22, A25, XTUPLE_0:def_12; reconsider DD2 = DD2 as Element of L by A26; reconsider DD1 = DD1 as Element of S by A27; [V,e] <= [DD1,DD2] by A23, A25; then V <= DD1 by YELLOW_3:11; then A28: V c= DD1 by YELLOW_1:3; DD1 in the carrier of S ; then DD1 in sigma L by YELLOW_1:1; then DD1 in the topology of the Scott TopAugmentation of L by A1, A2, YELLOW_9:52; then DD1 is open Subset of the Scott TopAugmentation of L by PRE_TOPC:def_2; then A29: DD1 is upper Subset of L by A1, WAYBEL_0:25; [Y,d] <= [DD1,DD2] by A24, A25; then d <= DD2 by YELLOW_3:11; then A30: DD2 in DD1 by A16, A28, A29, WAYBEL_0:def_20; DD1 in the carrier of S ; then DD1 in sigma L by YELLOW_1:1; then DD1 in the topology of the Scott TopAugmentation of L by A1, A2, YELLOW_9:52; then reconsider DD1 = DD1 as open Subset of the Scott TopAugmentation of L by PRE_TOPC:def_2; reconsider DD2 = DD2 as Element of the Scott TopAugmentation of L by A1; [DD1,DD2] in wy by A30; hence not D misses wy by A22, A25, XBOOLE_0:3; ::_thesis: verum end; wy is upper proof let x, y be Element of [:S,L:]; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in wy or not x <= y or y in wy ) assume that A31: x in wy and A32: x <= y ; ::_thesis: y in wy consider x1 being open Subset of the Scott TopAugmentation of L, x2 being Element of the Scott TopAugmentation of L such that A33: x = [x1,x2] and A34: x2 in x1 by A31; reconsider u2 = x2 as Element of L by A1; x1 in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2; then x1 in sigma L by A1, A2, YELLOW_9:52; then reconsider u1 = x1 as Element of S by YELLOW_1:1; the carrier of [:S,L:] = [: the carrier of S, the carrier of L:] by YELLOW_3:def_2; then consider y1, y2 being set such that A35: y1 in the carrier of S and A36: y2 in the carrier of L and A37: y = [y1,y2] by ZFMISC_1:def_2; y1 in sigma L by A35, YELLOW_1:1; then y1 in the topology of the Scott TopAugmentation of L by A1, A2, YELLOW_9:52; then reconsider y1 = y1 as open Subset of the Scott TopAugmentation of L by PRE_TOPC:def_2; reconsider y2 = y2 as Element of the Scott TopAugmentation of L by A1, A36; reconsider v2 = y2 as Element of L by A36; y1 in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2; then y1 in sigma L by A1, A2, YELLOW_9:52; then reconsider v1 = y1 as Element of S by YELLOW_1:1; A38: [u1,u2] <= [v1,v2] by A32, A37, A33; then u2 <= v2 by YELLOW_3:11; then x2 <= y2 by A1, YELLOW_0:1; then A39: y2 in x1 by A34, WAYBEL_0:def_20; u1 <= v1 by A38, YELLOW_3:11; then x1 c= y1 by YELLOW_1:3; hence y in wy by A37, A39; ::_thesis: verum end; then A40: wy in the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) by A10, WAYBEL11:31; the topology of the Scott TopAugmentation of S = sigma S by YELLOW_9:51 .= the topology of T1 by YELLOW_9:51 .= the topology of T ; then A41: TopStruct(# the carrier of the Scott TopAugmentation of S, the topology of the Scott TopAugmentation of S #) = TopStruct(# the carrier of T, the topology of T #) by A8; TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) = TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) ; then [: the Scott TopAugmentation of S, the Scott TopAugmentation of L:] = [:T, the Scott TopAugmentation of L:] by A41, Th7; hence { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } is open Subset of [:T, the Scott TopAugmentation of L:] by A4, A40, PRE_TOPC:def_2; ::_thesis: verum end; ( S5[ the Scott TopAugmentation of L] implies InclPoset the topology of the Scott TopAugmentation of L is continuous ) proof assume S5[ the Scott TopAugmentation of L] ; ::_thesis: InclPoset the topology of the Scott TopAugmentation of L is continuous then S6[ the Scott TopAugmentation of L] by Lm5; hence InclPoset the topology of the Scott TopAugmentation of L is continuous by Lm7; ::_thesis: verum end; hence S7[L] by A1, A2, A5, YELLOW_9:52; ::_thesis: verum end; theorem Th30: :: WAYBEL29:30 for L being complete LATTICE holds ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) proof let L be complete LATTICE; ::_thesis: ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) thus ( InclPoset (sigma L) is continuous implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) by Lm10; ::_thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) implies InclPoset (sigma L) is continuous ) assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; ::_thesis: InclPoset (sigma L) is continuous now__::_thesis:_for_SL_being_Scott_TopAugmentation_of_L for_S_being_complete_LATTICE for_SS_being_Scott_TopAugmentation_of_S_holds_sigma_[:S,L:]_=_the_topology_of_[:SS,SL:] let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:] ( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4; then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13; ( RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def_4; then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13; then [:SS,SL:] = [:(Sigma S),(Sigma L):] by A2, Th7; hence sigma [:S,L:] = the topology of [:SS,SL:] by A1; ::_thesis: verum end; hence InclPoset (sigma L) is continuous by Lm11; ::_thesis: verum end; theorem Th31: :: WAYBEL29:31 for L being complete LATTICE holds ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ) proof let L be complete LATTICE; ::_thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ) hereby ::_thesis: ( ( for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] S8[L] proof let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:] let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:] ( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4; then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13; ( RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def_4; then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13; then [:SS,SL:] = [:(Sigma S),(Sigma L):] by A2, Th7; hence sigma [:S,L:] = the topology of [:SS,SL:] by A1; ::_thesis: verum end; hence for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by Lm9; ::_thesis: verum end; assume A3: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] let S be complete LATTICE; ::_thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by A3; hence sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] by YELLOW_9:51; ::_thesis: verum end; theorem Th32: :: WAYBEL29:32 for L being complete LATTICE holds ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) proof let L be complete LATTICE; ::_thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) hereby ::_thesis: ( ( for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] let S be complete LATTICE; ::_thesis: Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by A1, Th31; then Omega (Sigma [:S,L:]) = Omega [:(Sigma S),(Sigma L):] by WAYBEL25:13; hence Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by WAYBEL25:15; ::_thesis: verum end; assume A2: for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] let S be complete LATTICE; ::_thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by A2; then TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by WAYBEL25:def_2; hence sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] by YELLOW_9:51; ::_thesis: verum end; theorem :: WAYBEL29:33 for L being complete LATTICE holds ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) proof let L be complete LATTICE; ::_thesis: ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) by Th30; hence ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) by Th32; ::_thesis: verum end;