:: 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;