:: WAYBEL25 semantic presentation

begin

theorem :: WAYBEL25:1
for p being Point of Sierpinski_Space st p = 0 holds
{p} is closed
proof
set S = Sierpinski_Space ;
let p be Point of Sierpinski_Space; ::_thesis: ( p = 0 implies {p} is closed )
A1: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9;
assume A2: p = 0 ; ::_thesis: {p} is closed
A3: ([#] Sierpinski_Space) \ {p} = {1}
proof
thus  ([#] Sierpinski_Space) \ {p} c= {1} :: according to XBOOLE_0:def_10 ::_thesis: {1} c= ([#] Sierpinski_Space) \ {p}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ([#] Sierpinski_Space) \ {p} or a in {1} )
assume A4: a in ([#] Sierpinski_Space) \ {p} ; ::_thesis: a in {1}
then  not a in {p} by XBOOLE_0:def_5;
then  a <> 0 by A2, TARSKI:def_1;
then  a = 1 by A1, A4, TARSKI:def_2;
hence  a in {1} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {1} or a in ([#] Sierpinski_Space) \ {p} )
assume  a in {1} ; ::_thesis: a in ([#] Sierpinski_Space) \ {p}
then A5: a = 1 by TARSKI:def_1;
then A6: not a in {p} by A2, TARSKI:def_1;
 a in [#] Sierpinski_Space by A1, A5, TARSKI:def_2;
hence  a in ([#] Sierpinski_Space) \ {p} by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
 the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9;
hence  ([#] Sierpinski_Space) \ {p} in the topology of Sierpinski_Space by A3, ENUMSET1:def_1; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum
end;

theorem Th2: :: WAYBEL25:2
for p being Point of Sierpinski_Space st p = 1 holds
not {p} is closed
proof
set S = Sierpinski_Space ;
let p be Point of Sierpinski_Space; ::_thesis: ( p = 1 implies not {p} is closed )
A1: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9;
assume A2: p = 1 ; ::_thesis: not {p} is closed
A3: ([#] Sierpinski_Space) \ {p} = {0}
proof
thus  ([#] Sierpinski_Space) \ {p} c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= ([#] Sierpinski_Space) \ {p}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ([#] Sierpinski_Space) \ {p} or a in {0} )
assume A4: a in ([#] Sierpinski_Space) \ {p} ; ::_thesis: a in {0}
then  not a in {p} by XBOOLE_0:def_5;
then  a <> 1 by A2, TARSKI:def_1;
then  a = 0 by A1, A4, TARSKI:def_2;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in ([#] Sierpinski_Space) \ {p} )
assume  a in {0} ; ::_thesis: a in ([#] Sierpinski_Space) \ {p}
then A5: a = 0 by TARSKI:def_1;
then A6: not a in {p} by A2, TARSKI:def_1;
 a in [#] Sierpinski_Space by A1, A5, TARSKI:def_2;
hence  a in ([#] Sierpinski_Space) \ {p} by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
A7: {0} <> {1} by ZFMISC_1:3;
A8: {0} <> {0,1} by ZFMISC_1:5;
 the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9;
hence  not ([#] Sierpinski_Space) \ {p} in the topology of Sierpinski_Space by A7, A8, A3, ENUMSET1:def_1; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum
end;

registration
cluster Sierpinski_Space  ->  non T_1 ;
coherence
 not Sierpinski_Space is T_1
proof
set S = Sierpinski_Space ;
 ex p being Point of Sierpinski_Space st Cl {p} <> {p}
proof
 the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9;
then reconsider p = 1 as Point of Sierpinski_Space by TARSKI:def_2;
take  p ; ::_thesis: Cl {p} <> {p}
thus  Cl {p} <> {p} by Th2; ::_thesis: verum
end;
hence  not Sierpinski_Space is T_1 by YELLOW_8:26; ::_thesis: verum
end;
end;

registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott  ->  T_0 for TopRelStr ;
coherence
 for b1 being TopLattice st b1 is complete & b1 is Scott holds
b1 is T_0 by WAYBEL11:10;
end;

registration
cluster non empty strict TopSpace-like T_0 injective for TopStruct ;
existence
 ex b1 being T_0-TopSpace st
( b1 is injective & b1 is strict )
proof
take  Sierpinski_Space ; ::_thesis: ( Sierpinski_Space is injective & Sierpinski_Space is strict )
thus  ( Sierpinski_Space is injective & Sierpinski_Space is strict ) ; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is complete & b1 is Scott & b1 is strict )
proof
set T = the complete strict Scott TopLattice;
take  the complete strict Scott TopLattice ; ::_thesis: ( the complete strict Scott TopLattice is complete & the complete strict Scott TopLattice is Scott & the complete strict Scott TopLattice is strict )
thus  ( the complete strict Scott TopLattice is complete & the complete strict Scott TopLattice is Scott & the complete strict Scott TopLattice is strict ) ; ::_thesis: verum
end;
end;

theorem Th3: :: WAYBEL25:3
for I being non empty set
for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space))
proof
set S = Sierpinski_Space ;
set B = BoolePoset 1;
let I be non empty set ; ::_thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space))
let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); ::_thesis: the carrier of T = the carrier of (product (I --> Sierpinski_Space))
A1: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def_2;
A2: dom (Carrier (I --> Sierpinski_Space)) = I by PARTFUN1:def_2;
A3: for x being set st x in dom (Carrier (I --> Sierpinski_Space)) holds
(Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x
proof
let x be set ; ::_thesis: ( x in dom (Carrier (I --> Sierpinski_Space)) implies (Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x )
assume A4: x in dom (Carrier (I --> Sierpinski_Space)) ; ::_thesis: (Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x
then A5: ex T being 1-sorted st
( T = (I --> Sierpinski_Space) . x & (Carrier (I --> Sierpinski_Space)) . x = the carrier of T ) by PRALG_1:def_13;
 ex R being 1-sorted st
( R = (I --> (BoolePoset 1)) . x & (Carrier (I --> (BoolePoset 1))) . x = the carrier of R ) by A4, PRALG_1:def_13;
hence (Carrier (I --> (BoolePoset 1))) . x = the carrier of (BoolePoset 1) by A4, FUNCOP_1:7
.= bool 1 by WAYBEL_7:2
.= the carrier of Sierpinski_Space by WAYBEL18:def_9, YELLOW14:1
.= (Carrier (I --> Sierpinski_Space)) . x by A4, A5, FUNCOP_1:7 ;
::_thesis: verum
end;
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (product (I --> (BoolePoset 1))), the InternalRel of (product (I --> (BoolePoset 1))) #) by YELLOW_9:def_4;
hence  the carrier of T = product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def_4
.= product (Carrier (I --> Sierpinski_Space)) by A1, A2, A3, FUNCT_1:2
.= the carrier of (product (I --> Sierpinski_Space)) by WAYBEL18:def_3 ;
::_thesis: verum
end;

theorem Th4: :: WAYBEL25:4
for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2
for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
proof
let L1, L2 be complete LATTICE; ::_thesis: for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2
for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being Scott TopAugmentation of L2
for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let T2 be Scott TopAugmentation of L2; ::_thesis: for h being Function of L1,L2
for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let h be Function of L1,L2; ::_thesis: for H being Function of T1,T2 st h = H & h is isomorphic holds
H is being_homeomorphism
let H be Function of T1,T2; ::_thesis: ( h = H & h is isomorphic implies H is being_homeomorphism )
assume that
A1: h = H and
A2: h is isomorphic ; ::_thesis: H is being_homeomorphism
A3: RelStr(# the carrier of L2, the InternalRel of L2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) by YELLOW_9:def_4;
A4: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by YELLOW_9:def_4;
then reconsider H9 = h " as Function of T2,T1 by A3;
consider g being Function of L2,L1 such that
A5: g = h " ;
 g = h " by A2, A5, TOPS_2:def_4;
then  g is isomorphic by A2, WAYBEL_0:68;
then reconsider h2 = h " as sups-preserving Function of L2,L1 by A5, WAYBEL13:20;
A6: rng H = [#] T2 by A1, A2, A3, WAYBEL_0:66;
A7: for x being set st x in dom H9 holds
H9 . x = (H ") . x
proof
let x be set ; ::_thesis: ( x in dom H9 implies H9 . x = (H ") . x )
assume  x in dom H9 ; ::_thesis: H9 . x = (H ") . x
A8: H is onto by A6, FUNCT_2:def_3;
thus H9 . x = (h ") . x by A2, TOPS_2:def_4
.= (H ") . x by A1, A2, A8, TOPS_2:def_4 ; ::_thesis: verum
end;
 h2 is directed-sups-preserving ;
then A9: H9 is directed-sups-preserving by A4, A3, WAYBEL21:6;
dom (H ") = the carrier of T2 by FUNCT_2:def_1
.= dom H9 by FUNCT_2:def_1 ;
then A10: H " = H9 by A7, FUNCT_1:2;
reconsider h1 = h as sups-preserving Function of L1,L2 by A2, WAYBEL13:20;
 h1 is directed-sups-preserving ;
then A11: H is directed-sups-preserving by A1, A4, A3, WAYBEL21:6;
 dom H = [#] T1 by FUNCT_2:def_1;
hence  H is being_homeomorphism by A1, A2, A11, A9, A6, A10, TOPS_2:def_5; ::_thesis: verum
end;

theorem Th5: :: WAYBEL25:5
for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic
proof
let L1, L2 be complete LATTICE; ::_thesis: for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic
let T1 be Scott TopAugmentation of L1; ::_thesis: for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic
let T2 be Scott TopAugmentation of L2; ::_thesis: ( L1,L2 are_isomorphic implies T1,T2 are_homeomorphic )
given h being Function of L1,L2 such that A1: h is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: T1,T2 are_homeomorphic
A2: RelStr(# the carrier of L2, the InternalRel of L2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) by YELLOW_9:def_4;
 RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by YELLOW_9:def_4;
then reconsider H = h as Function of T1,T2 by A2;
take  H ; :: according to T_0TOPSP:def_1 ::_thesis: H is being_homeomorphism
thus  H is being_homeomorphism by A1, Th4; ::_thesis: verum
end;

theorem Th6: :: WAYBEL25:6
for S, T being non empty TopSpace st S is injective & S,T are_homeomorphic holds
T is injective
proof
let S, T be non empty TopSpace; ::_thesis: ( S is injective & S,T are_homeomorphic implies T is injective )
assume that
A1: S is injective and
A2: S,T are_homeomorphic ; ::_thesis: T is injective
consider p being Function of S,T such that
A3: p is being_homeomorphism by A2, T_0TOPSP:def_1;
let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for b1 being Element of bool [: the carrier of X, the carrier of T:] holds
( not b1 is continuous or for b2 being TopStruct holds
( not X is SubSpace of b2 or ex b3 being Element of bool [: the carrier of b2, the carrier of T:] st
( b3 is continuous & b3 | the carrier of X = b1 ) ) )
let f be Function of X,T; ::_thesis: ( not f is continuous or for b1 being TopStruct holds
( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st
( b2 is continuous & b2 | the carrier of X = f ) ) )
assume A4: f is continuous ; ::_thesis: for b1 being TopStruct holds
( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st
( b2 is continuous & b2 | the carrier of X = f ) )
let Y be non empty TopSpace; ::_thesis: ( not X is SubSpace of Y or ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st
( b1 is continuous & b1 | the carrier of X = f ) )
assume A5: X is SubSpace of Y ; ::_thesis: ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st
( b1 is continuous & b1 | the carrier of X = f )
then A6: [#] X c= [#] Y by PRE_TOPC:def_4;
A7: p is V7() by A3, TOPS_2:58;
set F = (p ") * f;
 p " is continuous by A3, TOPS_2:def_5;
then consider G being Function of Y,S such that
A8: G is continuous and
A9: G | the carrier of X = (p ") * f by A1, A4, A5, WAYBEL18:def_5;
take g = p * G; ::_thesis: ( g is continuous & g | the carrier of X = f )
A10: rng p = [#] T by A3, TOPS_2:58;
A11: for x being set st x in dom f holds
g . x = f . x
proof
let x be set ; ::_thesis: ( x in dom f implies g . x = f . x )
assume A12: x in dom f ; ::_thesis: g . x = f . x
then A13: f . x in rng f by FUNCT_1:def_3;
then  f . x in the carrier of T ;
then A14: f . x in dom (p ") by FUNCT_2:def_1;
 x in the carrier of X by A12;
then  x in the carrier of Y by A6;
then  x in dom G by FUNCT_2:def_1;
hence g . x = p . (G . x) by FUNCT_1:13
.= p . (((p ") * f) . x) by A9, A12, FUNCT_1:49
.= p . ((p ") . (f . x)) by A12, FUNCT_1:13
.= (p * (p ")) . (f . x) by A14, FUNCT_1:13
.= (id the carrier of T) . (f . x) by A10, A7, TOPS_2:52
.= f . x by A13, FUNCT_1:17 ;
::_thesis: verum
end;
 p is continuous by A3, TOPS_2:def_5;
hence  g is continuous by A8; ::_thesis: g | the carrier of X = f
dom f = the carrier of X by FUNCT_2:def_1
.= the carrier of Y /\ the carrier of X by A6, XBOOLE_1:28
.= (dom g) /\ the carrier of X by FUNCT_2:def_1 ;
hence  g | the carrier of X = f by A11, FUNCT_1:46; ::_thesis: verum
end;

theorem :: WAYBEL25:7
for L1, L2 being complete LATTICE
for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic & T1 is injective holds
T2 is injective by Th5, Th6;

definition
let X, Y be non empty TopSpace;
redefine pred X is_Retract_of Y means :Def1: :: WAYBEL25:def 1
 ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X;
compatibility
 ( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X )
proof
thus  ( X is_Retract_of Y implies ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X ) ::_thesis: ( ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X implies X is_Retract_of Y )
proof
given f being Function of Y,Y such that A1: f is continuous and
A2: f * f = f and
A3: Image f,X are_homeomorphic ; :: according to WAYBEL18:def_8 ::_thesis: ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X
consider h being Function of (Image f),X such that
A4: h is being_homeomorphism by A3, T_0TOPSP:def_1;
A5: corestr f is continuous by A1, WAYBEL18:10;
 h " is continuous by A4, TOPS_2:def_5;
then reconsider c = (incl (Image f)) * (h ") as continuous Function of X,Y ;
 h is continuous by A4, TOPS_2:def_5;
then reconsider r = h * (corestr f) as continuous Function of Y,X by A5;
take  c ; ::_thesis: ex r being continuous Function of Y,X st r * c = id X
take  r ; ::_thesis: r * c = id X
A6: rng h = [#] X by A4, TOPS_2:def_5;
A7: h is V7() by A4, TOPS_2:def_5;
thus r * c = h * ((corestr f) * ((incl (Image f)) * (h "))) by RELAT_1:36
.= h * (((corestr f) * (incl (Image f))) * (h ")) by RELAT_1:36
.= h * ((id (Image f)) * (h ")) by A2, YELLOW14:35
.= h * (h ") by FUNCT_2:17
.= id X by A6, A7, TOPS_2:52 ; ::_thesis: verum
end;
given c being continuous Function of X,Y, r being continuous Function of Y,X such that A8: r * c = id X ; ::_thesis: X is_Retract_of Y
take f = c * r; :: according to WAYBEL18:def_8 ::_thesis: ( f is continuous & f * f = f & Image f,X are_homeomorphic )
A9: dom c = the carrier of X by FUNCT_2:def_1
.= rng r by A8, FUNCT_2:18 ;
then reconsider cf = corestr c as Function of X,(Image f) by RELAT_1:28;
A10: Image f = Image c by A9, RELAT_1:28;
 the carrier of (Image c) c= the carrier of Y by BORSUK_1:1;
then  id (Image c) is Function of the carrier of (Image c), the carrier of Y by FUNCT_2:7;
then reconsider q = r * (id (Image c)) as Function of (Image f),X by A10;
A11: [#] X <> {} ;
A12: for P being Subset of X st P is open holds
q " P is open
proof
let P be Subset of X; ::_thesis: ( P is open implies q " P is open )
A13: dom (id (Image c)) = [#] (Image c) by FUNCT_2:def_1;
A14: (id (Image c)) " (r " P) = (r " P) /\ ([#] (Image c))
proof
thus  (id (Image c)) " (r " P) c= (r " P) /\ ([#] (Image c)) :: according to XBOOLE_0:def_10 ::_thesis: (r " P) /\ ([#] (Image c)) c= (id (Image c)) " (r " P)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (id (Image c)) " (r " P) or a in (r " P) /\ ([#] (Image c)) )
assume A15: a in (id (Image c)) " (r " P) ; ::_thesis: a in (r " P) /\ ([#] (Image c))
then  (id (Image c)) . a in r " P by FUNCT_1:def_7;
then  a in r " P by A15, FUNCT_1:18;
hence  a in (r " P) /\ ([#] (Image c)) by A15, XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (r " P) /\ ([#] (Image c)) or a in (id (Image c)) " (r " P) )
assume A16: a in (r " P) /\ ([#] (Image c)) ; ::_thesis: a in (id (Image c)) " (r " P)
then  a in r " P by XBOOLE_0:def_4;
then  (id (Image c)) . a in r " P by A16, FUNCT_1:18;
hence  a in (id (Image c)) " (r " P) by A13, A16, FUNCT_1:def_7; ::_thesis: verum
end;
assume  P is open ; ::_thesis: q " P is open
then  r " P is open by A11, TOPS_2:43;
then A17: r " P in the topology of Y by PRE_TOPC:def_2;
 q " P = (id (Image c)) " (r " P) by RELAT_1:146;
hence  q " P in the topology of (Image f) by A10, A17, A14, PRE_TOPC:def_4; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
A18: r * (cf * (cf ")) = (id X) * (cf ") by A8, RELAT_1:36;
thus  f is continuous ; ::_thesis: ( f * f = f & Image f,X are_homeomorphic )
thus f * f = c * (r * (c * r)) by RELAT_1:36
.= c * ((id X) * r) by A8, RELAT_1:36
.= f by FUNCT_2:17 ; ::_thesis: Image f,X are_homeomorphic
take h = cf " ; :: according to T_0TOPSP:def_1 ::_thesis: h is being_homeomorphism
thus  dom h = [#] (Image f) by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng h = [#] X & h is one-to-one & h is continuous & h " is continuous )
A19: rng (corestr c) = [#] (Image c) by FUNCT_2:def_3;
A20: c is V7() by A8, FUNCT_2:23;
hence  rng h = [#] X by A10, A19, TOPS_2:49; ::_thesis: ( h is one-to-one & h is continuous & h " is continuous )
 (corestr c) " is one-to-one by A20;
hence  h is V7() by A10, A20, TOPS_2:def_4; ::_thesis: ( h is continuous & h " is continuous )
 corestr c is V7() by A8, FUNCT_2:23;
then  r * (id the carrier of (Image c)) = (id X) * (cf ") by A10, A19, A18, TOPS_2:52;
then  r * (id (Image c)) = cf " by FUNCT_2:17;
hence  h is continuous by A11, A12, TOPS_2:43; ::_thesis: h " is continuous
 corestr c is continuous by WAYBEL18:10;
hence  h " is continuous by A10, A19, A20, TOPS_2:51; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines is_Retract_of WAYBEL25:def_1_:_
 for X, Y being non empty TopSpace holds
( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X );

theorem :: WAYBEL25:8
for S, T, X, Y being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) & S is_Retract_of X holds
T is_Retract_of Y
proof
let S, T, X, Y be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) & S is_Retract_of X implies T is_Retract_of Y )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) ; ::_thesis: ( not S is_Retract_of X or T is_Retract_of Y )
given c being continuous Function of S,X, r being continuous Function of X,S such that A3: r * c = id S ; :: according to WAYBEL25:def_1 ::_thesis: T is_Retract_of Y
reconsider rr = r as continuous Function of Y,T by A1, A2, YELLOW12:36;
reconsider cc = c as continuous Function of T,Y by A1, A2, YELLOW12:36;
take  cc ; :: according to WAYBEL25:def_1 ::_thesis: ex r being continuous Function of Y,T st r * cc = id T
take  rr ; ::_thesis: rr * cc = id T
thus  rr * cc = id T by A1, A3; ::_thesis: verum
end;

theorem :: WAYBEL25:9
for T, S1, S2 being non empty TopStruct st S1,S2 are_homeomorphic & S1 is_Retract_of T holds
S2 is_Retract_of T
proof
let T, S1, S2 be non empty TopStruct ; ::_thesis: ( S1,S2 are_homeomorphic & S1 is_Retract_of T implies S2 is_Retract_of T )
assume that
A1: S1,S2 are_homeomorphic and
A2: S1 is_Retract_of T ; ::_thesis: S2 is_Retract_of T
consider G being Function of S1,S2 such that
A3: G is being_homeomorphism by A1, T_0TOPSP:def_1;
consider H being Function of T,T such that
A4: H is continuous and
A5: H * H = H and
A6: Image H,S1 are_homeomorphic by A2, WAYBEL18:def_8;
take  H ; :: according to WAYBEL18:def_8 ::_thesis: ( H is continuous & H * H = H & Image H,S2 are_homeomorphic )
consider F being Function of (Image H),S1 such that
A7: F is being_homeomorphism by A6, T_0TOPSP:def_1;
 G * F is being_homeomorphism by A3, A7, TOPS_2:57;
hence  ( H is continuous & H * H = H & Image H,S2 are_homeomorphic ) by A4, A5, T_0TOPSP:def_1; ::_thesis: verum
end;

theorem :: WAYBEL25:10
for S, T being non empty TopSpace st T is injective & S is_Retract_of T holds
S is injective
proof
let S, T be non empty TopSpace; ::_thesis: ( T is injective & S is_Retract_of T implies S is injective )
assume that
A1: T is injective and
A2: S is_Retract_of T ; ::_thesis: S is injective
consider h being Function of T,T such that
A3: h is continuous and
A4: h * h = h and
A5: Image h,S are_homeomorphic by A2, WAYBEL18:def_8;
set F = corestr h;
 for W being Point of T st W in the carrier of (Image h) holds
(corestr h) . W = W
proof
let W be Point of T; ::_thesis: ( W in the carrier of (Image h) implies (corestr h) . W = W )
assume  W in the carrier of (Image h) ; ::_thesis: (corestr h) . W = W
then  W in rng h by WAYBEL18:9;
then  ex x being set st
( x in dom h & W = h . x ) by FUNCT_1:def_3;
hence  (corestr h) . W = W by A4, FUNCT_1:13; ::_thesis: verum
end;
then A6: corestr h is being_a_retraction by BORSUK_1:def_16;
 corestr h is continuous by A3, WAYBEL18:10;
then  Image h is_a_retract_of T by A6, BORSUK_1:def_17;
then  Image h is injective by A1, WAYBEL18:8;
hence  S is injective by A5, Th6; ::_thesis: verum
end;

theorem :: WAYBEL25:11
for J being non empty injective TopSpace
for Y being non empty TopSpace st J is SubSpace of Y holds
J is_Retract_of Y
proof
let J be non empty injective TopSpace; ::_thesis: for Y being non empty TopSpace st J is SubSpace of Y holds
J is_Retract_of Y
let Y be non empty TopSpace; ::_thesis: ( J is SubSpace of Y implies J is_Retract_of Y )
assume A1: J is SubSpace of Y ; ::_thesis: J is_Retract_of Y
then consider f being Function of Y,J such that
A2: f is continuous and
A3: f | the carrier of J = id J by WAYBEL18:def_5;
A4: the carrier of J c= the carrier of Y by A1, BORSUK_1:1;
then reconsider ff = f as Function of Y,Y by FUNCT_2:7;
 ex ff being Function of Y,Y st
( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )
proof
reconsider M = [#] J as non empty Subset of Y by A1, BORSUK_1:1;
take  ff ; ::_thesis: ( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )
thus  ff is continuous by A1, A2, PRE_TOPC:26; ::_thesis: ( ff * ff = ff & Image ff,J are_homeomorphic )
A5: dom f = the carrier of Y by FUNCT_2:def_1;
A6: for x being set st x in the carrier of Y holds
(f * f) . x = f . x
proof
let x be set ; ::_thesis: ( x in the carrier of Y implies (f * f) . x = f . x )
assume A7: x in the carrier of Y ; ::_thesis: (f * f) . x = f . x
hence (f * f) . x = f . (f . x) by A5, FUNCT_1:13
.= (id J) . (f . x) by A3, A7, FUNCT_1:49, FUNCT_2:5
.= f . x by A7, FUNCT_1:18, FUNCT_2:5 ;
::_thesis: verum
end;
 dom (ff * ff) = the carrier of Y by FUNCT_2:def_1;
hence  ff * ff = ff by A5, A6, FUNCT_1:2; ::_thesis: Image ff,J are_homeomorphic
A8: rng f = the carrier of J
proof
thus  rng f c= the carrier of J ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of J c= rng f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of J or y in rng f )
assume A9: y in the carrier of J ; ::_thesis: y in rng f
then  y in the carrier of Y by A4;
then A10: y in dom f by FUNCT_2:def_1;
f . y = (f | the carrier of J) . y by A9, FUNCT_1:49
.= y by A3, A9, FUNCT_1:18 ;
hence  y in rng f by A10, FUNCT_1:def_3; ::_thesis: verum
end;
the carrier of (Y | M) = [#] (Y | M)
.= the carrier of J by PRE_TOPC:def_5 ;
then  Image ff = TopStruct(# the carrier of J, the topology of J #) by A1, A8, TSEP_1:5;
hence  Image ff,J are_homeomorphic by YELLOW14:19; ::_thesis: verum
end;
hence  J is_Retract_of Y by WAYBEL18:def_8; ::_thesis: verum
end;

theorem Th12: :: WAYBEL25:12
for L being complete continuous LATTICE
for T being Scott TopAugmentation of L holds T is injective
proof
let L be complete continuous LATTICE; ::_thesis: for T being Scott TopAugmentation of L holds T is injective
let T be Scott TopAugmentation of L; ::_thesis: T is injective
let X be non empty TopSpace; :: according to WAYBEL18:def_5 ::_thesis: for b1 being Element of bool [: the carrier of X, the carrier of T:] holds
( not b1 is continuous or for b2 being TopStruct holds
( not X is SubSpace of b2 or ex b3 being Element of bool [: the carrier of b2, the carrier of T:] st
( b3 is continuous & b3 | the carrier of X = b1 ) ) )
let f be Function of X,T; ::_thesis: ( not f is continuous or for b1 being TopStruct holds
( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st
( b2 is continuous & b2 | the carrier of X = f ) ) )
assume A1: f is continuous ; ::_thesis: for b1 being TopStruct holds
( not X is SubSpace of b1 or ex b2 being Element of bool [: the carrier of b1, the carrier of T:] st
( b2 is continuous & b2 | the carrier of X = f ) )
let Y be non empty TopSpace; ::_thesis: ( not X is SubSpace of Y or ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st
( b1 is continuous & b1 | the carrier of X = f ) )
assume A2: X is SubSpace of Y ; ::_thesis: ex b1 being Element of bool [: the carrier of Y, the carrier of T:] st
( b1 is continuous & b1 | the carrier of X = f )
deffunc H1( set ) ->  Element of the carrier of T = "\/" ( {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : $1 in V  }  ,T);
consider g being Function of the carrier of Y, the carrier of T such that
A3: for x being Element of Y holds g . x = H1(x) from FUNCT_2:sch_4();
reconsider g = g as Function of Y,T ;
take  g ; ::_thesis: ( g is continuous & g | the carrier of X = f )
A4: dom f = the carrier of X by FUNCT_2:def_1;
A5: for P being Subset of T st P is open holds
g " P is open
proof
let P be Subset of T; ::_thesis: ( P is open implies g " P is open )
assume  P is open ; ::_thesis: g " P is open
then reconsider P = P as open Subset of T ;
 for x being set holds
( x in g " P iff ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) )
proof
let x be set ; ::_thesis: ( x in g " P iff ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) )
thus  ( x in g " P implies ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) ) ::_thesis: ( ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) implies x in g " P )
proof
assume A6: x in g " P ; ::_thesis: ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q )
then reconsider y = x as Point of Y ;
set A =  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  ;
  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  c= the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  or a in the carrier of T )
assume  a in  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  ; ::_thesis: a in the carrier of T
then  ex V being open Subset of Y st
( a = inf (f .: (V /\ the carrier of X)) & y in V ) ;
hence  a in the carrier of T ; ::_thesis: verum
end;
then reconsider A =  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  as Subset of T ;
A7: inf (f .: (([#] Y) /\ the carrier of X)) in A ;
A8: A is directed
proof
let a, b be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not a in A or not b in A or ex b1 being Element of the carrier of T st
( b1 in A & a <= b1 & b <= b1 ) )
assume  a in A ; ::_thesis: ( not b in A or ex b1 being Element of the carrier of T st
( b1 in A & a <= b1 & b <= b1 ) )
then consider Va being open Subset of Y such that
A9: a = inf (f .: (Va /\ the carrier of X)) and
A10: y in Va ;
assume  b in A ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in A & a <= b1 & b <= b1 )
then consider Vb being open Subset of Y such that
A11: b = inf (f .: (Vb /\ the carrier of X)) and
A12: y in Vb ;
take  inf (f .: ((Va /\ Vb) /\ the carrier of X)) ; ::_thesis: ( inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A & a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) )
 y in Va /\ Vb by A10, A12, XBOOLE_0:def_4;
hence  inf (f .: ((Va /\ Vb) /\ the carrier of X)) in A ; ::_thesis: ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) )
 (Va /\ Vb) /\ the carrier of X c= Vb /\ the carrier of X by XBOOLE_1:17, XBOOLE_1:26;
then A13: f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Vb /\ the carrier of X) by RELAT_1:123;
 (Va /\ Vb) /\ the carrier of X c= Va /\ the carrier of X by XBOOLE_1:17, XBOOLE_1:26;
then  f .: ((Va /\ Vb) /\ the carrier of X) c= f .: (Va /\ the carrier of X) by RELAT_1:123;
hence  ( a <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) & b <= inf (f .: ((Va /\ Vb) /\ the carrier of X)) ) by A9, A11, A13, WAYBEL_7:1; ::_thesis: verum
end;
A14: g . y = sup A by A3;
 g . y in P by A6, FUNCT_2:38;
then  A meets P by A14, A7, A8, WAYBEL11:def_1;
then consider b being set  such that
A15: b in A and
A16: b in P by XBOOLE_0:3;
consider B being open Subset of Y such that
A17: b = inf (f .: (B /\ the carrier of X)) and
A18: y in B by A15;
reconsider b = b as Element of T by A17;
take  B ; ::_thesis: ( B is open & B c= g " P & x in B )
thus  B is open ; ::_thesis: ( B c= g " P & x in B )
thus  B c= g " P ::_thesis: x in B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in g " P )
assume A19: a in B ; ::_thesis: a in g " P
then reconsider a = a as Point of Y ;
A20: g . a = H1(a) by A3;
 b in  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : a in V  }  by A17, A19;
then  b <= g . a by A20, YELLOW_2:22;
then  g . a in P by A16, WAYBEL_0:def_20;
hence  a in g " P by FUNCT_2:38; ::_thesis: verum
end;
thus  x in B by A18; ::_thesis: verum
end;
thus  ( ex Q being Subset of Y st
( Q is open & Q c= g " P & x in Q ) implies x in g " P ) ; ::_thesis: verum
end;
hence  g " P is open by TOPS_1:25; ::_thesis: verum
end;
set gX = g | the carrier of X;
A21: the carrier of X c= the carrier of Y by A2, BORSUK_1:1;
A22: for a being set st a in the carrier of X holds
(g | the carrier of X) . a = f . a
proof
let a be set ; ::_thesis: ( a in the carrier of X implies (g | the carrier of X) . a = f . a )
assume A23: a in the carrier of X ; ::_thesis: (g | the carrier of X) . a = f . a
then reconsider x = a as Point of X ;
reconsider y = x as Point of Y by A21, A23;
set A =  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  ;
  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  c= the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  or a in the carrier of T )
assume  a in  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  ; ::_thesis: a in the carrier of T
then  ex V being open Subset of Y st
( a = inf (f .: (V /\ the carrier of X)) & y in V ) ;
hence  a in the carrier of T ; ::_thesis: verum
end;
then reconsider A =  {  (inf (f .: (V /\ the carrier of X))) where V is open Subset of Y : y in V  }  as Subset of T ;
A24: f . x is_>=_than A
proof
let z be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not z in A or z <= f . x )
assume  z in A ; ::_thesis: z <= f . x
then consider V being open Subset of Y such that
A25: z = inf (f .: (V /\ the carrier of X)) and
A26: y in V ;
A27: ex_inf_of f .: (V /\ the carrier of X),T by YELLOW_0:17;
 y in V /\ the carrier of X by A26, XBOOLE_0:def_4;
hence  z <= f . x by A25, A27, FUNCT_2:35, YELLOW_4:2; ::_thesis: verum
end;
A28: for b being Element of T st b is_>=_than A holds
f . x <= b
proof
let b be Element of T; ::_thesis: ( b is_>=_than A implies f . x <= b )
assume A29: for k being Element of T st k in A holds
k <= b ; :: according to LATTICE3:def_9 ::_thesis: f . x <= b
A30: for V being open Subset of X st x in V holds
inf (f .: V) <= b
proof
let V be open Subset of X; ::_thesis: ( x in V implies inf (f .: V) <= b )
 V in the topology of X by PRE_TOPC:def_2;
then consider Q being Subset of Y such that
A31: Q in the topology of Y and
A32: V = Q /\ ([#] X) by A2, PRE_TOPC:def_4;
reconsider Q = Q as open Subset of Y by A31, PRE_TOPC:def_2;
assume  x in V ; ::_thesis: inf (f .: V) <= b
then  y in Q by A32, XBOOLE_0:def_4;
then  inf (f .: (Q /\ the carrier of X)) in A ;
hence  inf (f .: V) <= b by A29, A32; ::_thesis: verum
end;
A33: b is_>=_than waybelow (f . x)
proof
let w be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not w in waybelow (f . x) or w <= b )
A34: wayabove w is open by WAYBEL11:36;
A35: ex_inf_of f .: (f " (wayabove w)),T by YELLOW_0:17;
A36: w <= inf (wayabove w) by WAYBEL14:9;
 ex_inf_of wayabove w,T by YELLOW_0:17;
then  inf (wayabove w) <= inf (f .: (f " (wayabove w))) by A35, FUNCT_1:75, YELLOW_0:35;
then A37: w <= inf (f .: (f " (wayabove w))) by A36, ORDERS_2:3;
assume  w in waybelow (f . x) ; ::_thesis: w <= b
then  w << f . x by WAYBEL_3:7;
then  f . x in wayabove w by WAYBEL_3:8;
then A38: x in f " (wayabove w) by FUNCT_2:38;
 [#] T <> {} ;
then  f " (wayabove w) is open by A1, A34, TOPS_2:43;
then  inf (f .: (f " (wayabove w))) <= b by A30, A38;
hence  w <= b by A37, ORDERS_2:3; ::_thesis: verum
end;
 f . x = sup (waybelow (f . x)) by WAYBEL_3:def_5;
hence  f . x <= b by A33, YELLOW_0:32; ::_thesis: verum
end;
thus (g | the carrier of X) . a = g . y by FUNCT_1:49
.= H1(y) by A3
.= f . a by A24, A28, YELLOW_0:30 ; ::_thesis: verum
end;
 [#] T <> {} ;
hence  g is continuous by A5, TOPS_2:43; ::_thesis: g | the carrier of X = f
dom (g | the carrier of X) = (dom g) /\ the carrier of X by RELAT_1:61
.= the carrier of Y /\ the carrier of X by FUNCT_2:def_1
.= the carrier of X by A2, BORSUK_1:1, XBOOLE_1:28 ;
hence  g | the carrier of X = f by A4, A22, FUNCT_1:2; ::_thesis: verum
end;

registration
let L be complete continuous LATTICE;
cluster Scott  ->  injective for TopAugmentation of L;
coherence
 for b1 being TopAugmentation of L st b1 is Scott holds
b1 is injective by Th12;
end;

registration
let T be non empty injective TopSpace;
cluster TopStruct(# the carrier of T, the topology of T #) ->  injective ;
coherence
 TopStruct(# the carrier of T, the topology of T #) is injective by WAYBEL18:16;
end;

begin

definition
let T be TopStruct ;
func Omega T ->  strict TopRelStr  means :Def2: :: WAYBEL25:def 2
( TopStruct(# the carrier of it, the topology of it #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of it holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) );
existence
 ex b1 being strict TopRelStr st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) )
proof
defpred S1[ set , set ] means  ex Y being Subset of T st
( Y = {$2} & $1 in Cl Y );
consider R being Relation of the carrier of T such that
A1: for x, y being set holds
( [x,y] in R iff ( x in the carrier of T & y in the carrier of T & S1[x,y] ) ) from RELSET_1:sch_1();
take G = TopRelStr(# the carrier of T,R, the topology of T #); ::_thesis: ( TopStruct(# the carrier of G, the topology of G #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of G holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) )
thus  TopStruct(# the carrier of G, the topology of G #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: for x, y being Element of G holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
thus  for x, y being Element of G holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ::_thesis: verum
proof
let x, y be Element of G; ::_thesis: ( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) )
hereby  ::_thesis: ( ex Y being Subset of T st
( Y = {y} & x in Cl Y ) implies x <= y )
assume  x <= y ; ::_thesis: ex Y being Subset of T st
( Y = {y} & x in Cl Y )
then  [x,y] in R by ORDERS_2:def_5;
hence  ex Y being Subset of T st
( Y = {y} & x in Cl Y ) by A1; ::_thesis: verum
end;
given Y being Subset of T such that A2: Y = {y} and
A3: x in Cl Y ; ::_thesis: x <= y
 [x,y] in R by A1, A2, A3;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being strict TopRelStr st TopStruct(# the carrier of b1, the topology of b1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of b2, the topology of b2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) holds
b1 = b2
proof
let R1, R2 be strict TopRelStr ; ::_thesis: ( TopStruct(# the carrier of R1, the topology of R1 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of R1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of R2, the topology of R2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of R2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) implies R1 = R2 )
assume that
A4: TopStruct(# the carrier of R1, the topology of R1 #) = TopStruct(# the carrier of T, the topology of T #) and
A5: for x, y being Element of R1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) and
A6: TopStruct(# the carrier of R2, the topology of R2 #) = TopStruct(# the carrier of T, the topology of T #) and
A7: for x, y being Element of R2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ; ::_thesis: R1 = R2
 the InternalRel of R1 = the InternalRel of R2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of R1 or [x,y] in the InternalRel of R2 ) & ( not [x,y] in the InternalRel of R2 or [x,y] in the InternalRel of R1 ) )
hereby  ::_thesis: ( not [x,y] in the InternalRel of R2 or [x,y] in the InternalRel of R1 )
assume A8: [x,y] in the InternalRel of R1 ; ::_thesis: [x,y] in the InternalRel of R2
then reconsider x1 = x, y1 = y as Element of R1 by ZFMISC_1:87;
reconsider x2 = x, y2 = y as Element of R2 by A4, A6, A8, ZFMISC_1:87;
 x1 <= y1 by A8, ORDERS_2:def_5;
then  ex Y being Subset of T st
( Y = {y1} & x1 in Cl Y ) by A5;
then  x2 <= y2 by A7;
hence  [x,y] in the InternalRel of R2 by ORDERS_2:def_5; ::_thesis: verum
end;
assume A9: [x,y] in the InternalRel of R2 ; ::_thesis: [x,y] in the InternalRel of R1
then reconsider x2 = x, y2 = y as Element of R2 by ZFMISC_1:87;
reconsider x1 = x, y1 = y as Element of R1 by A4, A6, A9, ZFMISC_1:87;
 x2 <= y2 by A9, ORDERS_2:def_5;
then  ex Y being Subset of T st
( Y = {y2} & x2 in Cl Y ) by A7;
then  x1 <= y1 by A5;
hence  [x,y] in the InternalRel of R1 by ORDERS_2:def_5; ::_thesis: verum
end;
hence  R1 = R2 by A4, A6; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Omega WAYBEL25:def_2_:_
 for T being TopStruct
for b2 being strict TopRelStr holds
( b2 = Omega T iff ( TopStruct(# the carrier of b2, the topology of b2 #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) ) );

Lm1:  for T being TopStruct holds the carrier of T = the carrier of (Omega T)
proof
let T be TopStruct ; ::_thesis: the carrier of T = the carrier of (Omega T)
 TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
hence  the carrier of T = the carrier of (Omega T) ; ::_thesis: verum
end;

registration
let T be empty TopStruct ;
cluster Omega T ->  empty strict ;
coherence
 Omega T is empty
proof
 the carrier of (Omega T) = the carrier of T by Lm1;
hence  the carrier of (Omega T) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let T be non empty TopStruct ;
cluster Omega T ->  non empty strict ;
coherence
 not Omega T is empty
proof
 the carrier of (Omega T) = the carrier of T by Lm1;
hence  not the carrier of (Omega T) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster Omega T ->  TopSpace-like strict ;
coherence
 Omega T is TopSpace-like
proof
A1: TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2;
hence  the carrier of (Omega T) in the topology of (Omega T) by PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of (Omega T)) holds
( not b1 c= the topology of (Omega T) or K252( the carrier of (Omega T),b1) in the topology of (Omega T) ) ) & ( for b1, b2 being Element of bool the carrier of (Omega T) holds
( not b1 in the topology of (Omega T) or not b2 in the topology of (Omega T) or b1 /\ b2 in the topology of (Omega T) ) ) )
thus  ( ( for b1 being Element of bool (bool the carrier of (Omega T)) holds
( not b1 c= the topology of (Omega T) or K252( the carrier of (Omega T),b1) in the topology of (Omega T) ) ) & ( for b1, b2 being Element of bool the carrier of (Omega T) holds
( not b1 in the topology of (Omega T) or not b2 in the topology of (Omega T) or b1 /\ b2 in the topology of (Omega T) ) ) ) by A1, PRE_TOPC:def_1; ::_thesis: verum
end;
end;

registration
let T be TopStruct ;
cluster Omega T ->  reflexive strict ;
coherence
 Omega T is reflexive
proof
let x be set ; :: according to ORDERS_2:def_2,RELAT_2:def_1 ::_thesis: ( not x in the carrier of (Omega T) or [x,x] in the InternalRel of (Omega T) )
assume A1: x in the carrier of (Omega T) ; ::_thesis: [x,x] in the InternalRel of (Omega T)
then reconsider T9 = T as non empty TopStruct ;
reconsider a = x as Element of (Omega T) by A1;
reconsider t9 = x as Element of T9 by A1, Lm1;
consider Y being Subset of T such that
A2: Y = {t9} ;
A3: Y c= Cl Y by PRE_TOPC:18;
 a in Y by A2, TARSKI:def_1;
then  a <= a by A2, A3, Def2;
hence  [x,x] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum
end;
end;

Lm2:  for T being TopStruct
for x, y being Element of T
for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
proof
let T be TopStruct ; ::_thesis: for x, y being Element of T
for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
let x, y be Element of T; ::_thesis: for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
let X, Y be Subset of T; ::_thesis: ( X = {x} & Y = {y} implies ( x in Cl Y iff Cl X c= Cl Y ) )
assume that
A1: X = {x} and
A2: Y = {y} ; ::_thesis: ( x in Cl Y iff Cl X c= Cl Y )
hereby  ::_thesis: ( Cl X c= Cl Y implies x in Cl Y )
assume  x in Cl Y ; ::_thesis: Cl X c= Cl Y
then  for V being Subset of T st V is open & x in V holds
y in V by A2, YELLOW14:21;
hence  Cl X c= Cl Y by A1, A2, YELLOW14:22; ::_thesis: verum
end;
assume  Cl X c= Cl Y ; ::_thesis: x in Cl Y
hence  x in Cl Y by A1, YELLOW14:20; ::_thesis: verum
end;

registration
let T be TopStruct ;
cluster Omega T ->  transitive strict ;
coherence
 Omega T is transitive
proof
let x, y, z be set ; :: according to ORDERS_2:def_3,RELAT_2:def_8 ::_thesis: ( not x in the carrier of (Omega T) or not y in the carrier of (Omega T) or not z in the carrier of (Omega T) or not [x,y] in the InternalRel of (Omega T) or not [y,z] in the InternalRel of (Omega T) or [x,z] in the InternalRel of (Omega T) )
assume that
A1: x in the carrier of (Omega T) and
A2: y in the carrier of (Omega T) and
A3: z in the carrier of (Omega T) and
A4: [x,y] in the InternalRel of (Omega T) and
A5: [y,z] in the InternalRel of (Omega T) ; ::_thesis: [x,z] in the InternalRel of (Omega T)
reconsider a = x, b = y, c = z as Element of (Omega T) by A1, A2, A3;
 a <= b by A4, ORDERS_2:def_5;
then consider Y2 being Subset of T such that
A6: Y2 = {b} and
A7: a in Cl Y2 by Def2;
 TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2;
then reconsider t3 = z as Element of T by A3;
 b <= c by A5, ORDERS_2:def_5;
then consider Y3 being Subset of T such that
A8: Y3 = {c} and
A9: b in Cl Y3 by Def2;
 Y3 = {t3} by A8;
then  Cl Y2 c= Cl Y3 by A6, A9, Lm2;
then  a <= c by A7, A8, Def2;
hence  [x,z] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum
end;
end;

registration
let T be T_0-TopSpace;
cluster Omega T ->  antisymmetric strict ;
coherence
 Omega T is antisymmetric
proof
let x, y be set ; :: according to ORDERS_2:def_4,RELAT_2:def_4 ::_thesis: ( not x in the carrier of (Omega T) or not y in the carrier of (Omega T) or not [x,y] in the InternalRel of (Omega T) or not [y,x] in the InternalRel of (Omega T) or x = y )
assume that
A1: x in the carrier of (Omega T) and
A2: y in the carrier of (Omega T) and
A3: [x,y] in the InternalRel of (Omega T) and
A4: [y,x] in the InternalRel of (Omega T) ; ::_thesis: x = y
reconsider a = x, b = y as Element of (Omega T) by A1, A2;
 b <= a by A4, ORDERS_2:def_5;
then A5: ex Y1 being Subset of T st
( Y1 = {a} & b in Cl Y1 ) by Def2;
 TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2;
then reconsider t1 = x, t2 = y as Element of T by A1, A2;
 a <= b by A3, ORDERS_2:def_5;
then  ex Y2 being Subset of T st
( Y2 = {b} & a in Cl Y2 ) by Def2;
then  for V being Subset of T holds
( not V is open or ( ( t1 in V implies t2 in V ) & ( t2 in V implies t1 in V ) ) ) by A5, YELLOW14:21;
hence  x = y by T_0TOPSP:def_7; ::_thesis: verum
end;
end;

theorem Th13: :: WAYBEL25:13
for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
Omega S = Omega T
proof
let S, T be TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies Omega S = Omega T )
assume A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: Omega S = Omega T
A2: TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) = TopStruct(# the carrier of S, the topology of S #) by Def2
.= TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by A1, Def2 ;
 the InternalRel of (Omega S) = the InternalRel of (Omega T)
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of (Omega S) or [a,b] in the InternalRel of (Omega T) ) & ( not [a,b] in the InternalRel of (Omega T) or [a,b] in the InternalRel of (Omega S) ) )
thus  ( [a,b] in the InternalRel of (Omega S) implies [a,b] in the InternalRel of (Omega T) ) ::_thesis: ( not [a,b] in the InternalRel of (Omega T) or [a,b] in the InternalRel of (Omega S) )
proof
assume A3: [a,b] in the InternalRel of (Omega S) ; ::_thesis: [a,b] in the InternalRel of (Omega T)
then reconsider s1 = a, s2 = b as Element of (Omega S) by ZFMISC_1:87;
reconsider t1 = s1, t2 = s2 as Element of (Omega T) by A2;
 s1 <= s2 by A3, ORDERS_2:def_5;
then consider Y being Subset of S such that
A4: Y = {s2} and
A5: s1 in Cl Y by Def2;
reconsider Z = Y as Subset of T by A1;
 t1 in Cl Z by A1, A5, TOPS_3:80;
then  t1 <= t2 by A4, Def2;
hence  [a,b] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum
end;
assume A6: [a,b] in the InternalRel of (Omega T) ; ::_thesis: [a,b] in the InternalRel of (Omega S)
then reconsider s1 = a, s2 = b as Element of (Omega T) by ZFMISC_1:87;
reconsider t1 = s1, t2 = s2 as Element of (Omega S) by A2;
 s1 <= s2 by A6, ORDERS_2:def_5;
then consider Y being Subset of T such that
A7: Y = {s2} and
A8: s1 in Cl Y by Def2;
reconsider Z = Y as Subset of S by A1;
 t1 in Cl Z by A1, A8, TOPS_3:80;
then  t1 <= t2 by A7, Def2;
hence  [a,b] in the InternalRel of (Omega S) by ORDERS_2:def_5; ::_thesis: verum
end;
hence  Omega S = Omega T by A2; ::_thesis: verum
end;

theorem :: WAYBEL25:14
for M being non empty set
for T being non empty TopSpace holds RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #)
proof
let M be non empty set ; ::_thesis: for T being non empty TopSpace holds RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #)
let T be non empty TopSpace; ::_thesis: RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #)
A1: dom (Carrier (M --> T)) = M by PARTFUN1:def_2
.= dom (Carrier (M --> (Omega T))) by PARTFUN1:def_2 ;
A2: for i being set st i in dom (Carrier (M --> T)) holds
(Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i
proof
let i be set ; ::_thesis: ( i in dom (Carrier (M --> T)) implies (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i )
assume  i in dom (Carrier (M --> T)) ; ::_thesis: (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i
then A3: i in M ;
then consider R1 being 1-sorted  such that
A4: R1 = (M --> T) . i and
A5: (Carrier (M --> T)) . i = the carrier of R1 by PRALG_1:def_13;
consider R2 being 1-sorted  such that
A6: R2 = (M --> (Omega T)) . i and
A7: (Carrier (M --> (Omega T))) . i = the carrier of R2 by A3, PRALG_1:def_13;
the carrier of R1 = the carrier of T by A3, A4, FUNCOP_1:7
.= the carrier of (Omega T) by Lm1
.= the carrier of R2 by A3, A6, FUNCOP_1:7 ;
hence  (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i by A5, A7; ::_thesis: verum
end;
A8: the carrier of (Omega (product (M --> T))) = the carrier of (product (M --> T)) by Lm1
.= product (Carrier (M --> T)) by WAYBEL18:def_3
.= product (Carrier (M --> (Omega T))) by A1, A2, FUNCT_1:2 ;
A9: the carrier of (Omega (product (M --> T))) = the carrier of (product (M --> T)) by Lm1;
 the InternalRel of (Omega (product (M --> T))) = the InternalRel of (product (M --> (Omega T)))
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of (Omega (product (M --> T))) or [x,y] in the InternalRel of (product (M --> (Omega T))) ) & ( not [x,y] in the InternalRel of (product (M --> (Omega T))) or [x,y] in the InternalRel of (Omega (product (M --> T))) ) )
hereby  ::_thesis: ( not [x,y] in the InternalRel of (product (M --> (Omega T))) or [x,y] in the InternalRel of (Omega (product (M --> T))) )
assume A10: [x,y] in the InternalRel of (Omega (product (M --> T))) ; ::_thesis: [x,y] in the InternalRel of (product (M --> (Omega T)))
then A11: y in the carrier of (Omega (product (M --> T))) by ZFMISC_1:87;
A12: x in the carrier of (Omega (product (M --> T))) by A10, ZFMISC_1:87;
then reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by A8, A11, YELLOW_1:def_4;
reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A12, A11, Lm1;
reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A10, ZFMISC_1:87;
A13: xp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:87;
then consider f being Function such that
A14: xp = f and
 dom f = dom (Carrier (M --> (Omega T))) and
 for i being set st i in dom (Carrier (M --> (Omega T))) holds
f . i in (Carrier (M --> (Omega T))) . i by CARD_3:def_5;
 yp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:87;
then consider g being Function such that
A15: yp = g and
 dom g = dom (Carrier (M --> (Omega T))) and
 for i being set st i in dom (Carrier (M --> (Omega T))) holds
g . i in (Carrier (M --> (Omega T))) . i by CARD_3:def_5;
 xo <= yo by A10, ORDERS_2:def_5;
then A16: ex Yp being Subset of (product (M --> T)) st
( Yp = {p2} & p1 in Cl Yp ) by Def2;
 for i being set st i in M holds
ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in M implies ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) )
assume A17: i in M ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
then reconsider j = i as Element of M ;
set t1 = p1 . j;
set t2 = p2 . j;
reconsider xi = p1 . j, yi = p2 . j as Element of (Omega T) by Lm1;
take  Omega T ; ::_thesis: ex xi, yi being Element of (Omega T) st
( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of (Omega T) st
( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
take  yi ; ::_thesis: ( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
thus  Omega T = (M --> (Omega T)) . i by A17, FUNCOP_1:7; ::_thesis: ( xi = f . i & yi = g . i & xi <= yi )
thus  xi = f . i by A14; ::_thesis: ( yi = g . i & xi <= yi )
thus  yi = g . i by A15; ::_thesis: xi <= yi
 p1 . j in Cl {(p2 . j)} by A16, YELLOW14:30;
hence  xi <= yi by Def2; ::_thesis: verum
end;
then  xp <= yp by A13, A14, A15, YELLOW_1:def_4;
hence  [x,y] in the InternalRel of (product (M --> (Omega T))) by ORDERS_2:def_5; ::_thesis: verum
end;
assume A18: [x,y] in the InternalRel of (product (M --> (Omega T))) ; ::_thesis: [x,y] in the InternalRel of (Omega (product (M --> T)))
then reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by ZFMISC_1:87;
A19: xp <= yp by A18, ORDERS_2:def_5;
A20: x in the carrier of (product (M --> (Omega T))) by A18, ZFMISC_1:87;
then  xp in product (Carrier (M --> (Omega T))) by YELLOW_1:def_4;
then consider f, g being Function such that
A21: f = xp and
A22: g = yp and
A23: for i being set st i in M holds
ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) by A19, YELLOW_1:def_4;
A24: y in the carrier of (product (M --> (Omega T))) by A18, ZFMISC_1:87;
then reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A8, A20, YELLOW_1:def_4;
reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A8, A9, A20, A24, YELLOW_1:def_4;
 for i being Element of M holds p1 . i in Cl {(p2 . i)}
proof
let i be Element of M; ::_thesis: p1 . i in Cl {(p2 . i)}
consider R1 being RelStr , xi, yi being Element of R1 such that
A25: R1 = (M --> (Omega T)) . i and
A26: xi = f . i and
A27: yi = g . i and
A28: xi <= yi by A23;
reconsider xi = xi, yi = yi as Element of (Omega T) by A25, FUNCOP_1:7;
 xi <= yi by A25, A28, FUNCOP_1:7;
then  ex Y being Subset of T st
( Y = {yi} & xi in Cl Y ) by Def2;
hence  p1 . i in Cl {(p2 . i)} by A21, A22, A26, A27; ::_thesis: verum
end;
then  p1 in Cl {p2} by YELLOW14:30;
then  xo <= yo by Def2;
hence  [x,y] in the InternalRel of (Omega (product (M --> T))) by ORDERS_2:def_5; ::_thesis: verum
end;
hence  RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #) by A8, YELLOW_1:def_4; ::_thesis: verum
end;

theorem Th15: :: WAYBEL25:15
for S being complete Scott TopLattice holds Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
proof
let S be complete Scott TopLattice; ::_thesis: Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
A1: TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) = TopStruct(# the carrier of S, the topology of S #) by Def2;
 the InternalRel of (Omega S) = the InternalRel of S
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of S ) & ( not [x,y] in the InternalRel of S or [x,y] in the InternalRel of (Omega S) ) )
hereby  ::_thesis: ( not [x,y] in the InternalRel of S or [x,y] in the InternalRel of (Omega S) )
assume A2: [x,y] in the InternalRel of (Omega S) ; ::_thesis: [x,y] in the InternalRel of S
then A3: y in the carrier of (Omega S) by ZFMISC_1:87;
 x in the carrier of (Omega S) by A2, ZFMISC_1:87;
then reconsider t1 = x, t2 = y as Element of S by A3, Lm1;
reconsider o1 = x, o2 = y as Element of (Omega S) by A2, ZFMISC_1:87;
 o1 <= o2 by A2, ORDERS_2:def_5;
then  ex Y2 being Subset of S st
( Y2 = {o2} & o1 in Cl Y2 ) by Def2;
then  t1 in downarrow t2 by WAYBEL11:9;
then  ex t3 being Element of S st
( t3 >= t1 & t3 in {t2} ) by WAYBEL_0:def_15;
then  t1 <= t2 by TARSKI:def_1;
hence  [x,y] in the InternalRel of S by ORDERS_2:def_5; ::_thesis: verum
end;
assume A4: [x,y] in the InternalRel of S ; ::_thesis: [x,y] in the InternalRel of (Omega S)
then reconsider t1 = x, t2 = y as Element of S by ZFMISC_1:87;
reconsider o1 = x, o2 = y as Element of (Omega S) by A1, A4, ZFMISC_1:87;
A5: t2 in {t2} by TARSKI:def_1;
 t1 <= t2 by A4, ORDERS_2:def_5;
then  t1 in downarrow t2 by A5, WAYBEL_0:def_15;
then  t1 in Cl {t2} by WAYBEL11:9;
then  o1 <= o2 by Def2;
hence  [x,y] in the InternalRel of (Omega S) by ORDERS_2:def_5; ::_thesis: verum
end;
hence  Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by A1; ::_thesis: verum
end;

theorem Th16: :: WAYBEL25:16
for L being complete LATTICE
for S being Scott TopAugmentation of L holds RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #)
proof
let L be complete LATTICE; ::_thesis: for S being Scott TopAugmentation of L holds RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #)
let S be Scott TopAugmentation of L; ::_thesis: RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #)
 TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) = Omega S by Th15;
hence  RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4; ::_thesis: verum
end;

registration
let S be complete Scott TopLattice;
cluster Omega S ->  complete strict ;
coherence
 Omega S is complete
proof
set T = the Scott TopAugmentation of S;
A1: RelStr(# the carrier of (Omega the Scott TopAugmentation of S), the InternalRel of (Omega the Scott TopAugmentation of S) #) = RelStr(# the carrier of S, the InternalRel of S #) by Th16;
the topology of S = sigma S by WAYBEL14:23
.= the topology of the Scott TopAugmentation of S by YELLOW_9:51 ;
then  TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of the Scott TopAugmentation of S, the topology of the Scott TopAugmentation of S #) by A1, Lm1;
then  Omega S = Omega the Scott TopAugmentation of S by Th13;
hence  Omega S is complete by A1, YELLOW_0:3; ::_thesis: verum
end;
end;

theorem Th17: :: WAYBEL25:17
for T being non empty TopSpace
for S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T
proof
let T be non empty TopSpace; ::_thesis: for S being non empty SubSpace of T holds Omega S is full SubRelStr of Omega T
let S be non empty SubSpace of T; ::_thesis: Omega S is full SubRelStr of Omega T
A1: the carrier of S c= the carrier of T by BORSUK_1:1;
A2: the carrier of (Omega S) = the carrier of S by Lm1;
A3: the InternalRel of (Omega S) c= the InternalRel of (Omega T)
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) )
assume A4: [x,y] in the InternalRel of (Omega S) ; ::_thesis: [x,y] in the InternalRel of (Omega T)
then reconsider o1 = x, o2 = y as Element of (Omega S) by ZFMISC_1:87;
A5: y in the carrier of (Omega S) by A4, ZFMISC_1:87;
then reconsider s2 = y as Element of S by Lm1;
 x in the carrier of (Omega S) by A4, ZFMISC_1:87;
then reconsider o3 = x, o4 = y as Element of (Omega T) by A1, A2, A5, Lm1;
reconsider t2 = y as Element of T by A1, A2, A5;
 Cl {s2} = (Cl {t2}) /\ ([#] S) by PRE_TOPC:17;
then A6: Cl {s2} c= Cl {t2} by XBOOLE_1:17;
 o1 <= o2 by A4, ORDERS_2:def_5;
then  ex Y2 being Subset of S st
( Y2 = {o2} & o1 in Cl Y2 ) by Def2;
then  o3 <= o4 by A6, Def2;
hence  [x,y] in the InternalRel of (Omega T) by ORDERS_2:def_5; ::_thesis: verum
end;
A7: the InternalRel of (Omega S) = the InternalRel of (Omega T) |_2 the carrier of (Omega S)
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of (Omega S) or [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ) & ( not [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) or [x,y] in the InternalRel of (Omega S) ) )
thus  ( [x,y] in the InternalRel of (Omega S) implies [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ) by A3, XBOOLE_0:def_4; ::_thesis: ( not [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) or [x,y] in the InternalRel of (Omega S) )
assume A8: [x,y] in the InternalRel of (Omega T) |_2 the carrier of (Omega S) ; ::_thesis: [x,y] in the InternalRel of (Omega S)
then A9: y in the carrier of (Omega S) by ZFMISC_1:87;
A10: x in the carrier of (Omega S) by A8, ZFMISC_1:87;
then reconsider t1 = x, t2 = y as Element of T by A1, A2, A9;
reconsider o1 = x, o2 = y as Element of (Omega T) by A1, A2, A10, A9, Lm1;
 [x,y] in the InternalRel of (Omega T) by A8, XBOOLE_0:def_4;
then  o1 <= o2 by ORDERS_2:def_5;
then A11: ex Y being Subset of T st
( Y = {t2} & t1 in Cl Y ) by Def2;
reconsider s1 = x, s2 = y as Element of S by A10, A9, Lm1;
reconsider o3 = x, o4 = y as Element of (Omega S) by A8, ZFMISC_1:87;
 Cl {s2} = (Cl {t2}) /\ ([#] S) by PRE_TOPC:17;
then  s1 in Cl {s2} by A11, XBOOLE_0:def_4;
then  o3 <= o4 by Def2;
hence  [x,y] in the InternalRel of (Omega S) by ORDERS_2:def_5; ::_thesis: verum
end;
 the carrier of (Omega S) c= the carrier of (Omega T) by A1, A2, Lm1;
hence  Omega S is full SubRelStr of Omega T by A3, A7, YELLOW_0:def_13, YELLOW_0:def_14; ::_thesis: verum
end;

theorem Th18: :: WAYBEL25:18
for S, T being TopSpace
for h being Function of S,T
for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
proof
let S, T be TopSpace; ::_thesis: for h being Function of S,T
for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
let h be Function of S,T; ::_thesis: for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
let g be Function of (Omega S),(Omega T); ::_thesis: ( h = g & h is being_homeomorphism implies g is isomorphic )
assume that
A1: h = g and
A2: h is being_homeomorphism ; ::_thesis: g is isomorphic
A3: dom h = [#] S by A2, TOPS_2:def_5;
A4: rng h = [#] T by A2, TOPS_2:def_5;
A5: the carrier of T = the carrier of (Omega T) by Lm1;
A6: the carrier of S = the carrier of (Omega S) by Lm1;
A7: h is one-to-one by A2, TOPS_2:def_5;
percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
supposeA8: ( not S is empty & not T is empty ) ; ::_thesis: g is isomorphic
then reconsider s = S, t = T as non empty TopSpace ;
reconsider f = g as Function of (Omega s),(Omega t) ;
 for x, y being Element of (Omega s) holds
( x <= y iff f . x <= f . y )
proof
let x, y be Element of (Omega s); ::_thesis: ( x <= y iff f . x <= f . y )
A9: dom f = [#] S by A1, A2, TOPS_2:def_5
.= the carrier of S ;
reconsider Z = {((f ") . (f . y))} as Subset of s by Lm1;
A10: h " is being_homeomorphism by A2, A8, TOPS_2:56;
A11: f is onto by A1, A4, A5, FUNCT_2:def_3;
then A12: f " = f " by A1, A7, TOPS_2:def_4;
A13: dom h = the carrier of (Omega s) by A3, Lm1;
then A14: y = (h ") . (h . y) by A7, FUNCT_1:34
.= (f ") . (f . y) by A11, A1, A7, TOPS_2:def_4 ;
hereby  ::_thesis: ( f . x <= f . y implies x <= y )
reconsider Z = {(f . y)} as Subset of t by Lm1;
assume  x <= y ; ::_thesis: f . x <= f . y
then consider Y being Subset of s such that
A15: Y = {y} and
A16: x in Cl Y by Def2;
A17: Im (h,y) = Z by A1, A13, FUNCT_1:59;
 f . x in f .: (Cl Y) by A16, FUNCT_2:35;
then  h . x in Cl (h .: Y) by A1, A2, TOPS_2:60;
hence  f . x <= f . y by A1, A15, A17, Def2; ::_thesis: verum
end;
assume  f . x <= f . y ; ::_thesis: x <= y
then consider Y being Subset of t such that
A18: Y = {(f . y)} and
A19: f . x in Cl Y by Def2;
A20: f " = h " by A1, A5, A6;
A21: x = (f ") . (f . x) by A1, A7, A12, A13, FUNCT_1:34;
 (f ") . (f . x) in (f ") .: (Cl Y) by A19, FUNCT_2:35;
then A22: (h ") . (h . x) in Cl ((h ") .: Y) by A1, A10, A20, TOPS_2:60;
(f ") .: Y = f " Y by A1, A7, A12, FUNCT_1:85
.= Z by A1, A6, A7, A18, A14, A9, FINSEQ_5:4 ;
hence  x <= y by A1, A20, A22, A21, A14, Def2; ::_thesis: verum
end;
hence  g is isomorphic by A1, A5, A7, A4, WAYBEL_0:66; ::_thesis: verum
end;
suppose ( S is empty or T is empty ) ; ::_thesis: g is isomorphic
then reconsider s = S, t = T as empty TopSpace by A3, A4;
A23: Omega t is empty ;
 Omega s is empty ;
hence  g is isomorphic by A23, WAYBEL_0:def_38; ::_thesis: verum
end;
end;
end;

theorem Th19: :: WAYBEL25:19
for S, T being TopSpace st S,T are_homeomorphic holds
Omega S, Omega T are_isomorphic
proof
let S, T be TopSpace; ::_thesis: ( S,T are_homeomorphic implies Omega S, Omega T are_isomorphic )
assume  S,T are_homeomorphic ; ::_thesis: Omega S, Omega T are_isomorphic
then consider h being Function of S,T such that
A1: h is being_homeomorphism by T_0TOPSP:def_1;
A2: the carrier of T = the carrier of (Omega T) by Lm1;
 the carrier of S = the carrier of (Omega S) by Lm1;
then reconsider f = h as Function of (Omega S),(Omega T) by A2;
take  f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic
thus  f is isomorphic by A1, Th18; ::_thesis: verum
end;

Lm3:  for S, T being non empty RelStr
for f being Function of S,S
for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds
g is projection
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,S
for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds
g is projection
let f be Function of S,S; ::_thesis: for g being Function of T,T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection holds
g is projection
let g be Function of T,T; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & f = g & f is projection implies g is projection )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) and
A2: f = g and
A3: ( f is idempotent & f is monotone ) ; :: according to WAYBEL_1:def_13 ::_thesis: g is projection
thus  ( g is idempotent & g is monotone ) by A1, A2, A3, WAYBEL_9:1; :: according to WAYBEL_1:def_13 ::_thesis: verum
end;

theorem Th20: :: WAYBEL25:20
for T being injective T_0-TopSpace holds Omega T is complete continuous LATTICE
proof
let T be injective T_0-TopSpace; ::_thesis: Omega T is complete continuous LATTICE
set S = Sierpinski_Space ;
set B = BoolePoset 1;
consider M being non empty set  such that
A1: T is_Retract_of product (M --> Sierpinski_Space) by WAYBEL18:19;
consider f being Function of (product (M --> Sierpinski_Space)),(product (M --> Sierpinski_Space)) such that
A2: f is continuous and
A3: f * f = f and
A4: Image f,T are_homeomorphic by A1, WAYBEL18:def_8;
A5: RelStr(# the carrier of (Omega (Image f)), the InternalRel of (Omega (Image f)) #), Omega (Image f) are_isomorphic by WAYBEL13:26;
 Omega (Image f), Omega T are_isomorphic by A4, Th19;
then A6: RelStr(# the carrier of (Omega (Image f)), the InternalRel of (Omega (Image f)) #), Omega T are_isomorphic by A5, WAYBEL_1:7;
 Omega (Image f) is full SubRelStr of Omega (product (M --> Sierpinski_Space)) by Th17;
then A7: the InternalRel of (Omega (Image f)) = the InternalRel of (Omega (product (M --> Sierpinski_Space))) |_2 the carrier of (Omega (Image f)) by YELLOW_0:def_14;
set TL = the Scott TopAugmentation of product (M --> (BoolePoset 1));
A8: RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by YELLOW_9:def_4;
A9: the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the carrier of (product (M --> Sierpinski_Space)) by Th3;
then reconsider ff = f as Function of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the Scott TopAugmentation of product (M --> (BoolePoset 1)) ;
A10: the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the topology of (product (M --> Sierpinski_Space)) by WAYBEL18:15;
then A11: ff is continuous by A2, A9, YELLOW12:36;
then  ( ff is idempotent & ff is monotone ) by A3, QUANTAL1:def_9;
then  ff is projection by WAYBEL_1:def_13;
then reconsider g = ff as projection Function of (product (M --> (BoolePoset 1))),(product (M --> (BoolePoset 1))) by A8, Lm3;
A12: the InternalRel of (Image g) = the InternalRel of (product (M --> (BoolePoset 1))) |_2 the carrier of (Image g) by YELLOW_0:def_14;
 ( TopStruct(# the carrier of TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #), the topology of TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) #) = TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) implies Omega TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) = Omega the Scott TopAugmentation of product (M --> (BoolePoset 1)) ) by Th13;
then A13: RelStr(# the carrier of (Omega TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #)), the InternalRel of (Omega TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by A10, A9, Th16;
 g is directed-sups-preserving by A8, A11, WAYBEL21:6;
then A14: Image g is complete continuous LATTICE by WAYBEL15:15, YELLOW_2:35;
the carrier of (Image g) = rng g by YELLOW_0:def_15
.= the carrier of (Image f) by WAYBEL18:9
.= the carrier of (Omega (Image f)) by Lm1 ;
hence  Omega T is complete continuous LATTICE by A13, A14, A6, A12, A7, WAYBEL15:9, WAYBEL20:18, YELLOW14:11, YELLOW14:12; ::_thesis: verum
end;

registration
let T be injective T_0-TopSpace;
cluster Omega T ->  complete strict continuous ;
coherence
 ( Omega T is complete & Omega T is continuous ) by Th20;
end;

theorem Th21: :: WAYBEL25:21
for X, Y being non empty TopSpace
for f being continuous Function of (Omega X),(Omega Y) holds f is monotone
proof
let X, Y be non empty TopSpace; ::_thesis: for f being continuous Function of (Omega X),(Omega Y) holds f is monotone
let f be continuous Function of (Omega X),(Omega Y); ::_thesis: f is monotone
let x, y be Element of (Omega X); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y )
reconsider Z = {(f . y)} as Subset of Y by Lm1;
assume  x <= y ; ::_thesis: f . x <= f . y
then consider A being Subset of X such that
A1: A = {y} and
A2: x in Cl A by Def2;
A3: for G being Subset of Y st G is open & f . x in G holds
Z meets G
proof
 the carrier of X = the carrier of (Omega X) by Lm1;
then reconsider g = f as Function of X,Y by Lm1;
let G be Subset of Y; ::_thesis: ( G is open & f . x in G implies Z meets G )
assume that
A4: G is open and
A5: f . x in G ; ::_thesis: Z meets G
A6: x in g " G by A5, FUNCT_2:38;
A7: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2;
A8: f . y in Z by TARSKI:def_1;
 TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then A9: g is continuous by A7, YELLOW12:36;
 [#] Y <> {} ;
then  g " G is open by A4, A9, TOPS_2:43;
then  A meets g " G by A2, A6, PRE_TOPC:def_7;
then consider m being set  such that
A10: m in A /\ (g " G) by XBOOLE_0:4;
 m in A by A10, XBOOLE_0:def_4;
then A11: m = y by A1, TARSKI:def_1;
 m in g " G by A10, XBOOLE_0:def_4;
then  f . y in G by A11, FUNCT_2:38;
then  Z /\ G <> {} Y by A8, XBOOLE_0:def_4;
hence  Z meets G by XBOOLE_0:def_7; ::_thesis: verum
end;
 the carrier of Y = the carrier of (Omega Y) by Lm1;
then  f . x in Cl Z by A3, PRE_TOPC:def_7;
hence  f . x <= f . y by Def2; ::_thesis: verum
end;

registration
let X, Y be non empty TopSpace;
cluster Function-like quasi_total continuous  ->  monotone for Element of bool [: the carrier of (Omega X), the carrier of (Omega Y):];
coherence
 for b1 being Function of (Omega X),(Omega Y) st b1 is continuous holds
b1 is monotone by Th21;
end;

theorem Th22: :: WAYBEL25:22
for T being non empty TopSpace
for x being Element of (Omega T) holds Cl {x} = downarrow x
proof
let T be non empty TopSpace; ::_thesis: for x being Element of (Omega T) holds Cl {x} = downarrow x
let x be Element of (Omega T); ::_thesis: Cl {x} = downarrow x
A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: downarrow x c= Cl {x}
reconsider Z = {x} as Subset of T by A1;
let a be set ; ::_thesis: ( a in Cl {x} implies a in downarrow x )
assume A2: a in Cl {x} ; ::_thesis: a in downarrow x
then reconsider b = a as Element of (Omega T) ;
 a in Cl Z by A1, A2, TOPS_3:80;
then  b <= x by Def2;
hence  a in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in Cl {x} )
assume A3: a in downarrow x ; ::_thesis: a in Cl {x}
then reconsider b = a as Element of (Omega T) ;
 b <= x by A3, WAYBEL_0:17;
then  ex Z being Subset of T st
( Z = {x} & b in Cl Z ) by Def2;
hence  a in Cl {x} by A1, TOPS_3:80; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let x be Element of (Omega T);
cluster Cl {x} ->  non empty directed lower ;
coherence
 ( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed )
proof
reconsider y = x as Element of (Omega T) ;
 Cl {y} = downarrow y by Th22;
hence  ( not Cl {x} is empty & Cl {x} is lower & Cl {x} is directed ) ; ::_thesis: verum
end;
cluster downarrow x ->  closed ;
coherence
 downarrow x is closed
proof
 Cl {x} = downarrow x by Th22;
hence  downarrow x is closed ; ::_thesis: verum
end;
end;

theorem Th23: :: WAYBEL25:23
for X being TopSpace
for A being open Subset of (Omega X) holds A is upper
proof
let X be TopSpace; ::_thesis: for A being open Subset of (Omega X) holds A is upper
let A be open Subset of (Omega X); ::_thesis: A is upper
let x, y be Element of (Omega X); :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A )
assume A1: x in A ; ::_thesis: ( not x <= y or y in A )
assume  x <= y ; ::_thesis: y in A
then A2: ex Z being Subset of X st
( Z = {y} & x in Cl Z ) by Def2;
then reconsider X = X as non empty TopSpace ;
reconsider y = y as Element of (Omega X) ;
 TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then  x in Cl {y} by A2, TOPS_3:80;
then  A meets {y} by A1, PRE_TOPC:def_7;
hence  y in A by ZFMISC_1:50; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster open  ->  upper for Element of bool the carrier of (Omega T);
coherence
 for b1 being Subset of (Omega T) st b1 is open holds
b1 is upper by Th23;
end;

Lm4: now__::_thesis:_for_X,_Y_being_non_empty_TopSpace
for_N_being_net_of_ContMaps_(X,(Omega_Y))_holds_the_mapping_of_N_in_Funcs_(_the_carrier_of_N,(Funcs_(_the_carrier_of_X,_the_carrier_of_Y)))
let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) holds the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))
let N be net of ContMaps (X,(Omega Y)); ::_thesis: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))
A1: the carrier of Y = the carrier of (Omega Y) by Lm1;
 the carrier of (ContMaps (X,(Omega Y))) c= Funcs ( the carrier of X, the carrier of Y)
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in the carrier of (ContMaps (X,(Omega Y))) or f in Funcs ( the carrier of X, the carrier of Y) )
assume  f in the carrier of (ContMaps (X,(Omega Y))) ; ::_thesis: f in Funcs ( the carrier of X, the carrier of Y)
then  ex x being Function of X,(Omega Y) st
( x = f & x is continuous ) by WAYBEL24:def_3;
hence  f in Funcs ( the carrier of X, the carrier of Y) by A1, FUNCT_2:8; ::_thesis: verum
end;
then A2: Funcs ( the carrier of N, the carrier of (ContMaps (X,(Omega Y)))) c= Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_5:56;
 the mapping of N in Funcs ( the carrier of N, the carrier of (ContMaps (X,(Omega Y)))) by FUNCT_2:8;
hence  the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by A2; ::_thesis: verum
end;

definition
let I be non empty set ;
let S, T be non empty RelStr ;
let N be net of T;
let i be Element of I;
assume A1: the carrier of T c= the carrier of (S |^ I) ;
func commute (N,i,S) ->  strict net of S means :Def3: :: WAYBEL25:def 3
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = (commute the mapping of N) . i );
existence
 ex b1 being strict net of S st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = (commute the mapping of N) . i )
proof
 the carrier of T c= Funcs (I, the carrier of S) by A1, YELLOW_1:28;
then A1: Funcs ( the carrier of N, the carrier of T) c= Funcs ( the carrier of N,(Funcs (I, the carrier of S))) by FUNCT_5:56;
A2: the mapping of N in Funcs ( the carrier of N, the carrier of T) by FUNCT_2:8;
then A3: rng ((commute the mapping of N) . i) c= the carrier of S by A1, EQUATION:3;
 dom ((commute the mapping of N) . i) = the carrier of N by A2, A1, EQUATION:3;
then reconsider f = (commute the mapping of N) . i as Function of the carrier of N, the carrier of S by A3, FUNCT_2:def_1, RELSET_1:4;
set A = NetStr(# the carrier of N, the InternalRel of N,f #);
A4: RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) = RelStr(# the carrier of N, the InternalRel of N #) ;
 [#] N is directed by WAYBEL_0:def_6;
then  [#] NetStr(# the carrier of N, the InternalRel of N,f #) is directed by A4, WAYBEL_0:3;
then reconsider A = NetStr(# the carrier of N, the InternalRel of N,f #) as strict net of S by A4, WAYBEL_0:def_6, WAYBEL_8:13;
take  A ; ::_thesis: ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of A = (commute the mapping of N) . i )
thus  ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of A = (commute the mapping of N) . i ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict net of S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = (commute the mapping of N) . i & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = (commute the mapping of N) . i holds
b1 = b2 ;
end;

:: deftheorem Def3 defines commute WAYBEL25:def_3_:_
 for I being non empty set
for S, T being non empty RelStr
for N being net of T
for i being Element of I st the carrier of T c= the carrier of (S |^ I) holds
for b6 being strict net of S holds
( b6 = commute (N,i,S) iff ( RelStr(# the carrier of b6, the InternalRel of b6 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b6 = (commute the mapping of N) . i ) );

theorem Th24: :: WAYBEL25:24
for X, Y being non empty TopSpace
for N being net of ContMaps (X,(Omega Y))
for i being Element of N
for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
proof
let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y))
for i being Element of N
for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
let N be net of ContMaps (X,(Omega Y)); ::_thesis: for i being Element of N
for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
let i be Element of N; ::_thesis: for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
let x be Point of X; ::_thesis: the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
A1: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by Lm4;
 ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then  the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
hence  the mapping of (commute (N,x,(Omega Y))) . i = ((commute the mapping of N) . x) . i by Def3
.= ( the mapping of N . i) . x by A1, FUNCT_6:56 ;
::_thesis: verum
end;

theorem Th25: :: WAYBEL25:25
for X, Y being non empty TopSpace
for N being eventually-directed net of ContMaps (X,(Omega Y))
for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed
proof
let X, Y be non empty TopSpace; ::_thesis: for N being eventually-directed net of ContMaps (X,(Omega Y))
for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed
let N be eventually-directed net of ContMaps (X,(Omega Y)); ::_thesis: for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed
let x be Point of X; ::_thesis: commute (N,x,(Omega Y)) is eventually-directed
set M = commute (N,x,(Omega Y));
set L = (Omega Y) |^ the carrier of X;
 for i being Element of (commute (N,x,(Omega Y))) ex j being Element of (commute (N,x,(Omega Y))) st
for k being Element of (commute (N,x,(Omega Y))) st j <= k holds
(commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k
proof
let i be Element of (commute (N,x,(Omega Y))); ::_thesis: ex j being Element of (commute (N,x,(Omega Y))) st
for k being Element of (commute (N,x,(Omega Y))) st j <= k holds
(commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k
A1: ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then  the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
then A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (commute (N,x,(Omega Y))), the InternalRel of (commute (N,x,(Omega Y))) #) by Def3;
then reconsider a = i as Element of N ;
consider b being Element of N such that
A3: for c being Element of N st b <= c holds
N . a <= N . c by WAYBEL_0:11;
reconsider j = b as Element of (commute (N,x,(Omega Y))) by A2;
take  j ; ::_thesis: for k being Element of (commute (N,x,(Omega Y))) st j <= k holds
(commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k
let k be Element of (commute (N,x,(Omega Y))); ::_thesis: ( j <= k implies (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k )
reconsider c = k as Element of N by A2;
reconsider Na = N . a, Nc = N . c as Element of ((Omega Y) |^ the carrier of X) by A1, YELLOW_0:58;
reconsider A = Na, C = Nc as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5;
assume  j <= k ; ::_thesis: (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k
then  b <= c by A2, YELLOW_0:1;
then  N . a <= N . c by A3;
then  Na <= Nc by A1, YELLOW_0:59;
then  A <= C by YELLOW_1:def_5;
then A4: A . x <= C . x by WAYBEL_3:28;
A5: the mapping of (commute (N,x,(Omega Y))) . c = ( the mapping of N . k) . x by Th24;
 the mapping of (commute (N,x,(Omega Y))) . a = ( the mapping of N . i) . x by Th24;
hence  (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k by A4, A5, FUNCOP_1:7; ::_thesis: verum
end;
hence  commute (N,x,(Omega Y)) is eventually-directed by WAYBEL_0:11; ::_thesis: verum
end;

registration
let X, Y be non empty TopSpace;
let N be eventually-directed net of ContMaps (X,(Omega Y));
let x be Point of X;
cluster commute (N,x,(Omega Y)) ->  strict eventually-directed ;
coherence
 commute (N,x,(Omega Y)) is eventually-directed by Th25;
end;

registration
let X, Y be non empty TopSpace;
cluster non empty transitive directed  ->  Function-yielding for NetStr over ContMaps (X,(Omega Y));
coherence
 for b1 being net of ContMaps (X,(Omega Y)) holds b1 is Function-yielding ;
end;

Lm5: now__::_thesis:_for_X,_Y_being_non_empty_TopSpace
for_N_being_net_of_ContMaps_(X,(Omega_Y))
for_i_being_Element_of_N_holds_
(_the_mapping_of_N_._i_is_Function_of_X,(Omega_Y)_&_the_mapping_of_N_._i_is_Function_of_X,Y_)
let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y))
for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )
let N be net of ContMaps (X,(Omega Y)); ::_thesis: for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )
let i be Element of N; ::_thesis: ( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )
thus  the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21; ::_thesis: the mapping of N . i is Function of X,Y
 the carrier of Y = the carrier of (Omega Y) by Lm1;
hence  the mapping of N . i is Function of X,Y by WAYBEL24:21; ::_thesis: verum
end;

Lm6: now__::_thesis:_for_X,_Y_being_non_empty_TopSpace
for_N_being_net_of_ContMaps_(X,(Omega_Y))
for_x_being_Point_of_X_holds_dom_the_mapping_of_N_=_dom_the_mapping_of_(commute_(N,x,(Omega_Y)))
let X, Y be non empty TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y))
for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))
let N be net of ContMaps (X,(Omega Y)); ::_thesis: for x being Point of X holds dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))
let x be Point of X; ::_thesis: dom the mapping of N = dom the mapping of (commute (N,x,(Omega Y)))
 ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then  the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
then A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (commute (N,x,(Omega Y))), the InternalRel of (commute (N,x,(Omega Y))) #) by Def3;
thus  dom the mapping of N = the carrier of N by FUNCT_2:def_1
.= dom the mapping of (commute (N,x,(Omega Y))) by A1, FUNCT_2:def_1 ; ::_thesis: verum
end;

theorem Th26: :: WAYBEL25:26
for X being non empty TopSpace
for Y being T_0-TopSpace
for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
proof
let X be non empty TopSpace; ::_thesis: for Y being T_0-TopSpace
for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
let Y be T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
let N be net of ContMaps (X,(Omega Y)); ::_thesis: ( ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) implies ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X )
assume A1: for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ; ::_thesis: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
deffunc H1( Element of X) ->  Element of the carrier of (Omega Y) = sup (commute (N,$1,(Omega Y)));
set n = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
consider f being Function of the carrier of X, the carrier of (Omega Y) such that
A2: for u being Element of X holds f . u = H1(u) from FUNCT_2:sch_4();
reconsider a = f as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
 ex a being Element of ((Omega Y) |^ the carrier of X) st
( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b ) )
proof
take  a ; ::_thesis: ( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b ) )
A3: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
A4: (Omega Y) |^ the carrier of X = product ( the carrier of X --> (Omega Y)) by YELLOW_1:def_5;
thus  rng the mapping of N is_<=_than a ::_thesis: for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b
proof
let k be Element of ((Omega Y) |^ the carrier of X); :: according to LATTICE3:def_9 ::_thesis: ( not k in rng the mapping of N or k <= a )
reconsider k9 = k, a9 = a as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5;
assume  k in rng the mapping of N ; ::_thesis: k <= a
then consider i being set  such that
A5: i in dom the mapping of N and
A6: k = the mapping of N . i by FUNCT_1:def_3;
reconsider i = i as Point of N by A5;
 for u being Element of X holds k9 . u <= a9 . u
proof
let u be Element of X; ::_thesis: k9 . u <= a9 . u
A7: Omega Y = ( the carrier of X --> (Omega Y)) . u by FUNCOP_1:7;
 ex_sup_of commute (N,u,(Omega Y)) by A1;
then A8: ex_sup_of rng the mapping of (commute (N,u,(Omega Y))), Omega Y by WAYBEL_9:def_3;
A9: k9 . u = the mapping of (commute (N,u,(Omega Y))) . i by A6, Th24;
 dom the mapping of (commute (N,u,(Omega Y))) = the carrier of N by A3, Lm6;
then A10: k9 . u in rng the mapping of (commute (N,u,(Omega Y))) by A9, FUNCT_1:def_3;
a9 . u = sup (commute (N,u,(Omega Y))) by A2
.= Sup by WAYBEL_2:def_1
.= sup (rng the mapping of (commute (N,u,(Omega Y)))) ;
hence  k9 . u <= a9 . u by A7, A8, A10, YELLOW_4:1; ::_thesis: verum
end;
hence  k <= a by A4, WAYBEL_3:28; ::_thesis: verum
end;
let b be Element of ((Omega Y) |^ the carrier of X); ::_thesis: ( rng the mapping of N is_<=_than b implies a <= b )
assume A11: for k being Element of ((Omega Y) |^ the carrier of X) st k in rng the mapping of N holds
k <= b ; :: according to LATTICE3:def_9 ::_thesis: a <= b
reconsider a9 = a, b9 = b as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5;
 for u being Element of X holds a9 . u <= b9 . u
proof
let u be Element of X; ::_thesis: a9 . u <= b9 . u
 ex_sup_of commute (N,u,(Omega Y)) by A1;
then A12: ex_sup_of rng the mapping of (commute (N,u,(Omega Y))), Omega Y by WAYBEL_9:def_3;
A13: Omega Y = ( the carrier of X --> (Omega Y)) . u by FUNCOP_1:7;
A14: rng the mapping of (commute (N,u,(Omega Y))) is_<=_than b . u
proof
let s be Element of (Omega Y); :: according to LATTICE3:def_9 ::_thesis: ( not s in rng the mapping of (commute (N,u,(Omega Y))) or s <= b . u )
assume  s in rng the mapping of (commute (N,u,(Omega Y))) ; ::_thesis: s <= b . u
then consider i being set  such that
A15: i in dom the mapping of (commute (N,u,(Omega Y))) and
A16: the mapping of (commute (N,u,(Omega Y))) . i = s by FUNCT_1:def_3;
reconsider i = i as Point of N by A3, A15, Lm6;
 the mapping of N . i is Function of X,(Omega Y) by WAYBEL24:21;
then reconsider k = the mapping of N . i as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
reconsider k9 = k as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5;
 the mapping of N . i in rng the mapping of N by A3, FUNCT_1:def_3;
then  k <= b by A11;
then A17: k9 <= b9 by YELLOW_1:def_5;
 s = ( the mapping of N . i) . u by A16, Th24;
hence  s <= b . u by A13, A17, WAYBEL_3:28; ::_thesis: verum
end;
a9 . u = sup (commute (N,u,(Omega Y))) by A2
.= Sup by WAYBEL_2:def_1
.= sup (rng the mapping of (commute (N,u,(Omega Y)))) ;
hence  a9 . u <= b9 . u by A13, A12, A14, YELLOW_0:30; ::_thesis: verum
end;
hence  a <= b by A4, WAYBEL_3:28; ::_thesis: verum
end;
hence  ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X by YELLOW_0:15; ::_thesis: verum
end;

begin

definition
let T be non empty TopSpace;
attrT is monotone-convergence  means :Def4: :: WAYBEL25:def 4
 for D being non empty directed Subset of (Omega T) holds
( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) );
end;

:: deftheorem Def4 defines monotone-convergence WAYBEL25:def_4_:_
 for T being non empty TopSpace holds
( T is monotone-convergence iff for D being non empty directed Subset of (Omega T) holds
( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) ) );

theorem Th27: :: WAYBEL25:27
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is monotone-convergence holds
T is monotone-convergence
proof
let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is monotone-convergence implies T is monotone-convergence )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: for D being non empty directed Subset of (Omega S) holds
( ex_sup_of D, Omega S & ( for V being open Subset of S st sup D in V holds
D meets V ) ) ; :: according to WAYBEL25:def_4 ::_thesis: T is monotone-convergence
let E be non empty directed Subset of (Omega T); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of E, Omega T & ( for V being open Subset of T st sup E in V holds
E meets V ) )
A3: Omega S = Omega T by A1, Th13;
hence  ex_sup_of E, Omega T by A2; ::_thesis: for V being open Subset of T st sup E in V holds
E meets V
let V be open Subset of T; ::_thesis: ( sup E in V implies E meets V )
assume A4: sup E in V ; ::_thesis: E meets V
reconsider W = V as Subset of S by A1;
 W is open by A1, TOPS_3:76;
hence  E meets V by A2, A3, A4; ::_thesis: verum
end;

Lm7: now__::_thesis:_for_T_being_non_empty_1-sorted_
for_D_being_non_empty_Subset_of_T
for_d_being_Element_of_T_st_the_carrier_of_T_=_{d}_holds_
D_=_{d}
let T be non empty 1-sorted ; ::_thesis: for D being non empty Subset of T
for d being Element of T st the carrier of T = {d} holds
D = {d}
let D be non empty Subset of T; ::_thesis: for d being Element of T st the carrier of T = {d} holds
D = {d}
let d be Element of T; ::_thesis: ( the carrier of T = {d} implies D = {d} )
assume A1: the carrier of T = {d} ; ::_thesis: D = {d}
thus  D = {d} ::_thesis: verum
proof
thus  D c= {d} by A1; :: according to XBOOLE_0:def_10 ::_thesis: {d} c= D
set x = the Element of D;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {d} or a in D )
assume  a in {d} ; ::_thesis: a in D
then A2: a = d by TARSKI:def_1;
 the Element of D in D ;
hence  a in D by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster non empty trivial TopSpace-like T_0  ->  monotone-convergence for TopStruct ;
coherence
 for b1 being T_0-TopSpace st b1 is trivial holds
b1 is monotone-convergence
proof
let T be T_0-TopSpace; ::_thesis: ( T is trivial implies T is monotone-convergence )
assume  T is trivial ; ::_thesis: T is monotone-convergence
then consider d being Element of T such that
A1: the carrier of T = {d} by TEX_1:def_1;
reconsider d = d as Element of (Omega T) by Lm1;
let D be non empty directed Subset of (Omega T); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) )
A2: the carrier of T = the carrier of (Omega T) by Lm1;
then  D = {d} by A1, Lm7;
hence  ex_sup_of D, Omega T by YELLOW_0:38; ::_thesis: for V being open Subset of T st sup D in V holds
D meets V
let V be open Subset of T; ::_thesis: ( sup D in V implies D meets V )
A3: {d} meets {d} ;
assume  sup D in V ; ::_thesis: D meets V
then  V = {d} by A1, Lm7;
hence  D meets V by A1, A2, A3, Lm7; ::_thesis: verum
end;
end;

theorem :: WAYBEL25:28
for S being monotone-convergence T_0-TopSpace
for T being T_0-TopSpace st S,T are_homeomorphic holds
T is monotone-convergence
proof
let S be monotone-convergence T_0-TopSpace; ::_thesis: for T being T_0-TopSpace st S,T are_homeomorphic holds
T is monotone-convergence
let T be T_0-TopSpace; ::_thesis: ( S,T are_homeomorphic implies T is monotone-convergence )
given h being Function of S,T such that A1: h is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: T is monotone-convergence
 the carrier of S = the carrier of (Omega S) by Lm1;
then reconsider f = h as Function of (Omega S),(Omega T) by Lm1;
 f is isomorphic by A1, Th18;
then A2: rng f = the carrier of (Omega T) by WAYBEL_0:66;
let D be non empty directed Subset of (Omega T); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) )
A3: f " is isomorphic by A1, Th18, YELLOW14:10;
then  f " is sups-preserving by WAYBEL13:20;
then A4: f " preserves_sup_of D by WAYBEL_0:def_33;
A5: rng h = [#] T by A1, TOPS_2:def_5;
A6: h is V7() by A1, TOPS_2:def_5;
A7: h is onto by A5, FUNCT_2:def_3;
 (f ") .: D is directed by A3, YELLOW_2:15;
then A8: f " D is non empty directed Subset of (Omega S) by A2, A5, A6, TOPS_2:55;
then  ex_sup_of f " D, Omega S by Def4;
then  ex_sup_of f .: (f " D), Omega T by A1, Th18, YELLOW14:16;
hence A9: ex_sup_of D, Omega T by A2, FUNCT_1:77; ::_thesis: for V being open Subset of T st sup D in V holds
D meets V
let V be open Subset of T; ::_thesis: ( sup D in V implies D meets V )
assume  sup D in V ; ::_thesis: D meets V
then  (h ") . (sup D) in (h ") .: V by FUNCT_2:35;
then  (h ") . (sup D) in h " V by A5, A6, TOPS_2:55;
then  (h ") . (sup D) in h " V by A7, A6, TOPS_2:def_4;
then  (f ") . (sup D) in h " V by A2, A6, A7, A5, TOPS_2:def_4;
then  sup ((f ") .: D) in h " V by A9, A4, WAYBEL_0:def_31;
then A10: sup (f " D) in h " V by A2, A5, A6, TOPS_2:55;
 h " V is open by A1, TOPGRP_1:26;
then  f " D meets h " V by A8, A10, Def4;
then consider a being set  such that
A11: a in f " D and
A12: a in h " V by XBOOLE_0:3;
reconsider a = a as Element of S by A12;
now__::_thesis:_ex_b_being_Element_of_the_carrier_of_T_st_
(_b_in_D_&_b_in_V_)
take b = h . a; ::_thesis: ( b in D & b in V )
thus  ( b in D & b in V ) by A11, A12, FUNCT_2:38; ::_thesis: verum
end;
hence  D meets V by XBOOLE_0:3; ::_thesis: verum
end;

theorem Th29: :: WAYBEL25:29
for S being complete Scott TopLattice holds S is monotone-convergence
proof
let S be complete Scott TopLattice; ::_thesis: S is monotone-convergence
let D be non empty directed Subset of (Omega S); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega S & ( for V being open Subset of S st sup D in V holds
D meets V ) )
thus  ex_sup_of D, Omega S by YELLOW_0:17; ::_thesis: for V being open Subset of S st sup D in V holds
D meets V
A1: Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by Th15;
then A2: RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of S, the InternalRel of S #) ;
reconsider E = D as Subset of S by A1;
let V be open Subset of S; ::_thesis: ( sup D in V implies D meets V )
assume  sup D in V ; ::_thesis: D meets V
then A3: sup E in V by A2, YELLOW_0:17, YELLOW_0:26;
 E is non empty directed Subset of S by A2, WAYBEL_0:3;
hence  D meets V by A3, WAYBEL11:def_1; ::_thesis: verum
end;

registration
let L be complete LATTICE;
cluster Scott  ->  Scott monotone-convergence for TopAugmentation of L;
coherence
 for b1 being Scott TopAugmentation of L holds b1 is monotone-convergence by Th29;
end;

registration
let L be complete LATTICE;
let S be Scott TopAugmentation of L;
cluster TopStruct(# the carrier of S, the topology of S #) ->  monotone-convergence ;
coherence
 TopStruct(# the carrier of S, the topology of S #) is monotone-convergence by Th27;
end;

theorem Th30: :: WAYBEL25:30
for X being monotone-convergence T_0-TopSpace holds Omega X is up-complete
proof
let X be monotone-convergence T_0-TopSpace; ::_thesis: Omega X is up-complete
 for A being non empty directed Subset of (Omega X) holds ex_sup_of A, Omega X by Def4;
hence  Omega X is up-complete by WAYBEL_0:75; ::_thesis: verum
end;

registration
let X be monotone-convergence T_0-TopSpace;
cluster Omega X ->  up-complete strict ;
coherence
 Omega X is up-complete by Th30;
end;

theorem Th31: :: WAYBEL25:31
for X being non empty monotone-convergence TopSpace
for N being eventually-directed prenet of Omega X holds ex_sup_of N
proof
let X be non empty monotone-convergence TopSpace; ::_thesis: for N being eventually-directed prenet of Omega X holds ex_sup_of N
let N be eventually-directed prenet of Omega X; ::_thesis: ex_sup_of N
 rng (netmap (N,(Omega X))) is directed by WAYBEL_2:18;
hence  ex_sup_of rng the mapping of N, Omega X by Def4; :: according to WAYBEL_9:def_3 ::_thesis: verum
end;

theorem Th32: :: WAYBEL25:32
for X being non empty monotone-convergence TopSpace
for N being eventually-directed net of Omega X holds sup N in Lim N
proof
let X be non empty monotone-convergence TopSpace; ::_thesis: for N being eventually-directed net of Omega X holds sup N in Lim N
let N be eventually-directed net of Omega X; ::_thesis: sup N in Lim N
 rng (netmap (N,(Omega X))) is directed by WAYBEL_2:18;
then reconsider D = rng the mapping of N as non empty directed Subset of (Omega X) ;
 for V being a_neighborhood of sup N holds N is_eventually_in V
proof
let V be a_neighborhood of sup N; ::_thesis: N is_eventually_in V
A1: Int V c= V by TOPS_1:16;
A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then reconsider I = Int V as Subset of X ;
A3: I is open by A2, TOPS_3:76;
 sup N in I by CONNSP_2:def_1;
then  Sup in I by WAYBEL_2:def_1;
then  D meets I by A3, Def4;
then consider y being set  such that
A4: y in D and
A5: y in I by XBOOLE_0:3;
reconsider y = y as Point of X by A5;
consider x being set  such that
A6: x in dom the mapping of N and
A7: the mapping of N . x = y by A4, FUNCT_1:def_3;
reconsider x = x as Element of N by A6;
consider j being Element of N such that
A8: for k being Element of N st j <= k holds
N . x <= N . k by WAYBEL_0:11;
take  j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in V )
let k be Element of N; ::_thesis: ( not j <= k or N . k in V )
assume  j <= k ; ::_thesis: N . k in V
then  N . x <= N . k by A8;
then consider Y being Subset of X such that
A9: Y = {(N . k)} and
A10: N . x in Cl Y by Def2;
 Y meets I by A3, A5, A7, A10, PRE_TOPC:def_7;
then consider m being set  such that
A11: m in Y /\ I by XBOOLE_0:4;
 m in Y by A11, XBOOLE_0:def_4;
then A12: m = N . k by A9, TARSKI:def_1;
 m in I by A11, XBOOLE_0:def_4;
hence  N . k in V by A12, A1; ::_thesis: verum
end;
hence  sup N in Lim N by YELLOW_6:def_15; ::_thesis: verum
end;

theorem Th33: :: WAYBEL25:33
for X being non empty monotone-convergence TopSpace
for N being eventually-directed net of Omega X holds N is convergent
proof
let X be non empty monotone-convergence TopSpace; ::_thesis: for N being eventually-directed net of Omega X holds N is convergent
let N be eventually-directed net of Omega X; ::_thesis: N is convergent
thus  Lim N <> {} by Th32; :: according to YELLOW_6:def_16 ::_thesis: verum
end;

registration
let X be non empty monotone-convergence TopSpace;
cluster non empty transitive directed eventually-directed  ->  eventually-directed convergent for NetStr over Omega X;
coherence
 for b1 being eventually-directed net of Omega X holds b1 is convergent by Th33;
end;

theorem :: WAYBEL25:34
for X being non empty TopSpace st ( for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ) holds
X is monotone-convergence
proof
let X be non empty TopSpace; ::_thesis: ( ( for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ) implies X is monotone-convergence )
assume A1: for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ; ::_thesis: X is monotone-convergence
let D be non empty directed Subset of (Omega X); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega X & ( for V being open Subset of X st sup D in V holds
D meets V ) )
 Net-Str D = NetStr(# D,( the InternalRel of (Omega X) |_2 D),((id the carrier of (Omega X)) | D) #) by WAYBEL17:def_4;
then A2: rng the mapping of (Net-Str D) = D by YELLOW14:2;
 ex_sup_of Net-Str D by A1;
hence  ex_sup_of D, Omega X by A2, WAYBEL_9:def_3; ::_thesis: for V being open Subset of X st sup D in V holds
D meets V
let V be open Subset of X; ::_thesis: ( sup D in V implies D meets V )
assume A3: sup D in V ; ::_thesis: D meets V
reconsider Z = V as Subset of (Omega X) by Lm1;
A4: sup (Net-Str D) = Sup by WAYBEL_2:def_1
.= sup (rng the mapping of (Net-Str D)) ;
 TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then  Int Z = Int V by TOPS_3:77;
then  sup (Net-Str D) in Int Z by A2, A3, A4, TOPS_1:23;
then A5: Z is a_neighborhood of sup (Net-Str D) by CONNSP_2:def_1;
 sup (Net-Str D) in Lim (Net-Str D) by A1;
then  Net-Str D is_eventually_in V by A5, YELLOW_6:def_15;
then consider i being Element of (Net-Str D) such that
A6: for j being Element of (Net-Str D) st i <= j holds
(Net-Str D) . j in V by WAYBEL_0:def_11;
now__::_thesis:_ex_a_being_Element_of_the_carrier_of_(Omega_X)_st_
(_a_in_D_&_a_in_V_)
take a = (Net-Str D) . i; ::_thesis: ( a in D & a in V )
 dom the mapping of (Net-Str D) = the carrier of (Net-Str D) by FUNCT_2:def_1;
hence  a in D by A2, FUNCT_1:def_3; ::_thesis: a in V
thus  a in V by A6; ::_thesis: verum
end;
hence  D meets V by XBOOLE_0:3; ::_thesis: verum
end;

theorem Th35: :: WAYBEL25:35
for X being non empty monotone-convergence TopSpace
for Y being T_0-TopSpace
for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving
proof
let X be non empty monotone-convergence TopSpace; ::_thesis: for Y being T_0-TopSpace
for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving
let Y be T_0-TopSpace; ::_thesis: for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving
let f be continuous Function of (Omega X),(Omega Y); ::_thesis: f is directed-sups-preserving
let D be non empty directed Subset of (Omega X); :: according to YELLOW14:def_1 ::_thesis: f preserves_sup_of D
assume A1: ex_sup_of D, Omega X ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: D, Omega Y & "\/" ((f .: D),(Omega Y)) = f . ("\/" (D,(Omega X))) )
set V = (downarrow (sup (f .: D))) ` ;
A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then reconsider fV = f " ((downarrow (sup (f .: D))) `) as Subset of X ;
 [#] (Omega Y) <> {} ;
then  f " ((downarrow (sup (f .: D))) `) is open by TOPS_2:43;
then reconsider fV = fV as open Subset of X by A2, TOPS_3:76;
 sup (f .: D) <= sup (f .: D) ;
then A3: sup (f .: D) in downarrow (sup (f .: D)) by WAYBEL_0:17;
A4: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2;
 ex a being Element of (Omega Y) st
( f .: D is_<=_than a & ( for b being Element of (Omega Y) st f .: D is_<=_than b holds
a <= b ) )
proof
take a = f . (sup D); ::_thesis: ( f .: D is_<=_than a & ( for b being Element of (Omega Y) st f .: D is_<=_than b holds
a <= b ) )
 D is_<=_than sup D by A1, YELLOW_0:def_9;
hence  f .: D is_<=_than a by YELLOW_2:14; ::_thesis: for b being Element of (Omega Y) st f .: D is_<=_than b holds
a <= b
let b be Element of (Omega Y); ::_thesis: ( f .: D is_<=_than b implies a <= b )
assume A5: for c being Element of (Omega Y) st c in f .: D holds
c <= b ; :: according to LATTICE3:def_9 ::_thesis: a <= b
reconsider Z = {b} as Subset of Y by Lm1;
 for G being Subset of Y st G is open & a in G holds
Z meets G
proof
let G be Subset of Y; ::_thesis: ( G is open & a in G implies Z meets G )
assume that
A6: G is open and
A7: a in G ; ::_thesis: Z meets G
reconsider H = G as open Subset of (Omega Y) by A4, A6, TOPS_3:76;
 [#] (Omega Y) <> {} ;
then  f " H is open by TOPS_2:43;
then A8: f " H is open Subset of X by A2, TOPS_3:76;
 sup D in f " H by A7, FUNCT_2:38;
then  D meets f " H by A8, Def4;
then consider c being set  such that
A9: c in D and
A10: c in f " H by XBOOLE_0:3;
reconsider c = c as Point of (Omega X) by A9;
A11: f . c in H by A10, FUNCT_2:38;
 f . c <= b by A5, A9, FUNCT_2:35;
then A12: b in G by A11, WAYBEL_0:def_20;
 b in {b} by TARSKI:def_1;
hence  Z meets G by A12, XBOOLE_0:3; ::_thesis: verum
end;
then  a in Cl Z by A4, PRE_TOPC:def_7;
hence  a <= b by Def2; ::_thesis: verum
end;
hence A13: ex_sup_of f .: D, Omega Y by YELLOW_0:15; ::_thesis: "\/" ((f .: D),(Omega Y)) = f . ("\/" (D,(Omega X)))
assume A14: sup (f .: D) <> f . (sup D) ; ::_thesis: contradiction
 sup (f .: D) <= f . (sup D) by A1, A13, WAYBEL17:15;
then  not f . (sup D) <= sup (f .: D) by A14, ORDERS_2:2;
then  not f . (sup D) in downarrow (sup (f .: D)) by WAYBEL_0:17;
then  f . (sup D) in (downarrow (sup (f .: D))) ` by XBOOLE_0:def_5;
then  sup D in fV by FUNCT_2:38;
then  D meets fV by Def4;
then consider d being set  such that
A15: d in D and
A16: d in fV by XBOOLE_0:3;
reconsider d = d as Element of (Omega X) by A15;
A17: f . d in (downarrow (sup (f .: D))) ` by A16, FUNCT_2:38;
 f . d <= sup (f .: D) by A13, A15, FUNCT_2:35, YELLOW_4:1;
then  sup (f .: D) in (downarrow (sup (f .: D))) ` by A17, WAYBEL_0:def_20;
hence  contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

registration
let X be non empty monotone-convergence TopSpace;
let Y be T_0-TopSpace;
cluster Function-like quasi_total continuous  ->  directed-sups-preserving for Element of bool [: the carrier of (Omega X), the carrier of (Omega Y):];
coherence
 for b1 being Function of (Omega X),(Omega Y) st b1 is continuous holds
b1 is directed-sups-preserving by Th35;
end;

theorem Th36: :: WAYBEL25:36
for T being monotone-convergence T_0-TopSpace
for R being T_0-TopSpace st R is_Retract_of T holds
R is monotone-convergence
proof
let T be monotone-convergence T_0-TopSpace; ::_thesis: for R being T_0-TopSpace st R is_Retract_of T holds
R is monotone-convergence
let R be T_0-TopSpace; ::_thesis: ( R is_Retract_of T implies R is monotone-convergence )
given c being continuous Function of R,T, r being continuous Function of T,R such that A1: r * c = id R ; :: according to WAYBEL25:def_1 ::_thesis: R is monotone-convergence
let D be non empty directed Subset of (Omega R); :: according to WAYBEL25:def_4 ::_thesis: ( ex_sup_of D, Omega R & ( for V being open Subset of R st sup D in V holds
D meets V ) )
A2: TopStruct(# the carrier of R, the topology of R #) = TopStruct(# the carrier of (Omega R), the topology of (Omega R) #) by Def2;
then reconsider DR = D as non empty Subset of R ;
A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
then reconsider f = c * r as Function of (Omega T),(Omega T) ;
reconsider rr = r as Function of (Omega T),(Omega R) by A3, A2;
A4: r .: (c .: D) = (r * c) .: DR by RELAT_1:126
.= D by A1, FUNCT_1:92 ;
reconsider cc = c as Function of (Omega R),(Omega T) by A3, A2;
 cc is continuous by A3, A2, YELLOW12:36;
then A5: cc .: D is directed by YELLOW_2:15;
then A6: ex_sup_of cc .: D, Omega T by Def4;
 f is continuous by A3, YELLOW12:36;
then A7: f preserves_sup_of cc .: D by A5, WAYBEL_0:def_37;
 rr is continuous by A3, A2, YELLOW12:36;
then A8: rr preserves_sup_of cc .: D by A5, WAYBEL_0:def_37;
hence  ex_sup_of D, Omega R by A6, A4, WAYBEL_0:def_31; ::_thesis: for V being open Subset of R st sup D in V holds
D meets V
A9: c . (sup D) = c . (r . (sup (cc .: D))) by A6, A4, A8, WAYBEL_0:def_31
.= f . (sup (cc .: D)) by A3, FUNCT_2:15
.= sup (f .: (cc .: D)) by A6, A7, WAYBEL_0:def_31
.= sup (cc .: D) by A4, RELAT_1:126 ;
let V be open Subset of R; ::_thesis: ( sup D in V implies D meets V )
assume  sup D in V ; ::_thesis: D meets V
then A10: c . (sup D) in c .: V by FUNCT_2:35;
A11: c .: V c= r " V
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in c .: V or a in r " V )
assume  a in c .: V ; ::_thesis: a in r " V
then consider x being set  such that
A12: x in the carrier of R and
A13: x in V and
A14: a = c . x by FUNCT_2:64;
reconsider x = x as Point of R by A12;
A15: a = c . x by A14;
r . a = (r * c) . x by A14, FUNCT_2:15
.= x by A1, FUNCT_1:18 ;
hence  a in r " V by A13, A15, FUNCT_2:38; ::_thesis: verum
end;
 [#] R <> {} ;
then  r " V is open by TOPS_2:43;
then  c .: D meets r " V by A5, A11, A9, A10, Def4;
then consider d being set  such that
A16: d in cc .: D and
A17: d in r " V by XBOOLE_0:3;
now__::_thesis:_ex_a_being_set_st_
(_a_in_D_&_a_in_V_)
take a = r . d; ::_thesis: ( a in D & a in V )
thus  a in D by A4, A16, FUNCT_2:35; ::_thesis: a in V
thus  a in V by A17, FUNCT_2:38; ::_thesis: verum
end;
hence  D meets V by XBOOLE_0:3; ::_thesis: verum
end;

theorem Th37: :: WAYBEL25:37
for T being injective T_0-TopSpace
for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
proof
set SS = Sierpinski_Space ;
set B = BoolePoset 1;
let T be injective T_0-TopSpace; ::_thesis: for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
let S be Scott TopAugmentation of Omega T; ::_thesis: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
consider M being non empty set  such that
A1: T is_Retract_of product (M --> Sierpinski_Space) by WAYBEL18:19;
consider c being continuous Function of T,(product (M --> Sierpinski_Space)), r being continuous Function of (product (M --> Sierpinski_Space)),T such that
A2: r * c = id T by A1, Def1;
A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
A4: TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #) = TopStruct(# the carrier of (Omega (product (M --> Sierpinski_Space))), the topology of (Omega (product (M --> Sierpinski_Space))) #) by Def2;
then reconsider c1a = c as Function of (Omega T),(Omega (product (M --> Sierpinski_Space))) by A3;
set S2M = the Scott TopAugmentation of product (M --> (BoolePoset 1));
A5: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of S, the topology of S #) ;
A6: RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by YELLOW_9:def_4;
then reconsider c1 = c as Function of (Omega T),(product (M --> (BoolePoset 1))) by A3, Th3;
A7: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega T), the InternalRel of (Omega T) #) by YELLOW_9:def_4;
then reconsider c2 = c1 as Function of S, the Scott TopAugmentation of product (M --> (BoolePoset 1)) by A6;
A8: the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the carrier of (product (M --> Sierpinski_Space)) by Th3;
then reconsider rr = r as Function of the Scott TopAugmentation of product (M --> (BoolePoset 1)),T ;
A9: the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) = the topology of (product (M --> Sierpinski_Space)) by WAYBEL18:15;
then reconsider W = T as non empty monotone-convergence TopSpace by A1, A8, Th36;
 Omega (product (M --> Sierpinski_Space)) = Omega the Scott TopAugmentation of product (M --> (BoolePoset 1)) by A9, A8, Th13;
then A10: RelStr(# the carrier of (Omega (product (M --> Sierpinski_Space))), the InternalRel of (Omega (product (M --> Sierpinski_Space))) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by Th16
.= RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) by YELLOW_9:def_4 ;
reconsider r1 = r as Function of (product (M --> (BoolePoset 1))),(Omega T) by A8, A6, A3;
A11: RelStr(# the carrier of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))), the InternalRel of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))) #) = RelStr(# the carrier of (product (M --> (BoolePoset 1))), the InternalRel of (product (M --> (BoolePoset 1))) #) by Th16;
then reconsider rr1 = r1 as Function of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))),(Omega T) ;
reconsider r2 = r1 as Function of the Scott TopAugmentation of product (M --> (BoolePoset 1)),S by A6, A7;
reconsider r3 = r2 as Function of (product (M --> Sierpinski_Space)),S by Th3;
 TopStruct(# the carrier of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))), the topology of (Omega the Scott TopAugmentation of product (M --> (BoolePoset 1))) #) = TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset 1)), the topology of the Scott TopAugmentation of product (M --> (BoolePoset 1)) #) by Def2;
then  rr1 is continuous by A9, A8, A3, YELLOW12:36;
then  r2 is directed-sups-preserving by A6, A7, A11, WAYBEL21:6;
then  r3 is continuous by A9, A8, A5, YELLOW12:36;
then A12: r3 * c is continuous ;
reconsider c1a = c1a as continuous Function of (Omega W),(Omega (product (M --> Sierpinski_Space))) by A3, A4, YELLOW12:36;
 c2 = c1a ;
then A13: c2 is directed-sups-preserving by A7, A10, WAYBEL21:6;
 TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T, the topology of T #) ;
then  rr is continuous by A9, A8, YELLOW12:36;
then  rr * c2 is continuous by A13;
hence  TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) by A2, A12, YELLOW14:33; ::_thesis: verum
end;

theorem :: WAYBEL25:38
for T being injective T_0-TopSpace holds
( T is compact & T is locally-compact & T is sober )
proof
let T be injective T_0-TopSpace; ::_thesis: ( T is compact & T is locally-compact & T is sober )
set S = the Scott TopAugmentation of Omega T;
A1: ( the Scott TopAugmentation of Omega T is compact & the Scott TopAugmentation of Omega T is locally-compact & the Scott TopAugmentation of Omega T is sober ) by WAYBEL14:32;
 TopStruct(# the carrier of the Scott TopAugmentation of Omega T, the topology of the Scott TopAugmentation of Omega T #) = TopStruct(# the carrier of T, the topology of T #) by Th37;
hence  ( T is compact & T is locally-compact & T is sober ) by A1, YELLOW14:26, YELLOW14:27, YELLOW14:28; ::_thesis: verum
end;

theorem Th39: :: WAYBEL25:39
for T being injective T_0-TopSpace holds T is monotone-convergence
proof
let T be injective T_0-TopSpace; ::_thesis: T is monotone-convergence
set S = the Scott TopAugmentation of Omega T;
 TopStruct(# the carrier of the Scott TopAugmentation of Omega T, the topology of the Scott TopAugmentation of Omega T #) = TopStruct(# the carrier of T, the topology of T #) by Th37;
hence  T is monotone-convergence by Th27; ::_thesis: verum
end;

registration
cluster non empty TopSpace-like T_0 injective  ->  monotone-convergence for TopStruct ;
coherence
 for b1 being T_0-TopSpace st b1 is injective holds
b1 is monotone-convergence by Th39;
end;

theorem Th40: :: WAYBEL25:40
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y))
for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
proof
let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y))
for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
let Y be monotone-convergence T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y))
for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
let N be net of ContMaps (X,(Omega Y)); ::_thesis: for f, g being Function of X,(Omega Y) st f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N holds
g <= f
let f, g be Function of X,(Omega Y); ::_thesis: ( f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) & ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X & g in rng the mapping of N implies g <= f )
set m = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
set s = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X));
assume that
A1: f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) and
A2: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X and
A3: g in rng the mapping of N ; ::_thesis: g <= f
reconsider g1 = g as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
 rng the mapping of N is_<=_than "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) by A2, YELLOW_0:def_9;
then  g1 <= "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) by A3, LATTICE3:def_9;
hence  g <= f by A1, WAYBEL10:11; ::_thesis: verum
end;

theorem Th41: :: WAYBEL25:41
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y))
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
proof
let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y))
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let Y be monotone-convergence T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y))
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let N be net of ContMaps (X,(Omega Y)); ::_thesis: for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let x be Point of X; ::_thesis: for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let f be Function of X,(Omega Y); ::_thesis: ( ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) implies f . x = sup (commute (N,x,(Omega Y))) )
assume that
A1: for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed and
A2: f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) ; ::_thesis: f . x = sup (commute (N,x,(Omega Y)))
set n = the mapping of N;
set m = the mapping of (commute (N,x,(Omega Y)));
set L = (Omega Y) |^ the carrier of X;
A3: for x being Point of X holds ex_sup_of commute (N,x,(Omega Y))
proof
let x be Point of X; ::_thesis: ex_sup_of commute (N,x,(Omega Y))
 commute (N,x,(Omega Y)) is eventually-directed by A1;
hence  ex_sup_of commute (N,x,(Omega Y)) by Th31; ::_thesis: verum
end;
then A4: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X by Th26;
A5: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
then A6: dom the mapping of (commute (N,x,(Omega Y))) = the carrier of N by Lm6;
A7: for a being Element of (Omega Y) st rng the mapping of (commute (N,x,(Omega Y))) is_<=_than a holds
f . x <= a
proof
let a be Element of (Omega Y); ::_thesis: ( rng the mapping of (commute (N,x,(Omega Y))) is_<=_than a implies f . x <= a )
defpred S1[ set , set ] means ( ( $1 = x implies $2 = a ) & ( $1 <> x implies ex u being Element of X st
( $1 = u & $2 = sup (commute (N,u,(Omega Y))) ) ) );
A8: Omega Y = ( the carrier of X --> (Omega Y)) . x by FUNCOP_1:7;
A9: for e being Element of X ex u being Element of (Omega Y) st S1[e,u]
proof
let e be Element of X; ::_thesis: ex u being Element of (Omega Y) st S1[e,u]
percases ( e = x or e <> x ) ;
suppose e = x ; ::_thesis: ex u being Element of (Omega Y) st S1[e,u]
hence  ex u being Element of (Omega Y) st S1[e,u] ; ::_thesis: verum
end;
supposeA10: e <> x ; ::_thesis: ex u being Element of (Omega Y) st S1[e,u]
reconsider e = e as Element of X ;
take  sup (commute (N,e,(Omega Y))) ; ::_thesis: S1[e, sup (commute (N,e,(Omega Y)))]
thus  S1[e, sup (commute (N,e,(Omega Y)))] by A10; ::_thesis: verum
end;
end;
end;
consider t being Function of the carrier of X, the carrier of (Omega Y) such that
A11: for u being Element of X holds S1[u,t . u] from FUNCT_2:sch_3(A9);
reconsider t = t as Function of X,(Omega Y) ;
reconsider tt = t as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
reconsider p = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)), q = tt as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5;
assume A12: for e being Element of (Omega Y) st e in rng the mapping of (commute (N,x,(Omega Y))) holds
e <= a ; :: according to LATTICE3:def_9 ::_thesis: f . x <= a
 tt is_>=_than rng the mapping of N
proof
let s be Element of ((Omega Y) |^ the carrier of X); :: according to LATTICE3:def_9 ::_thesis: ( not s in rng the mapping of N or s <= tt )
reconsider ss = s as Function of X,(Omega Y) by WAYBEL24:19;
reconsider s9 = s, t9 = tt as Element of (product ( the carrier of X --> (Omega Y))) by YELLOW_1:def_5;
assume  s in rng the mapping of N ; ::_thesis: s <= tt
then consider i being set  such that
A13: i in dom the mapping of N and
A14: s = the mapping of N . i by FUNCT_1:def_3;
reconsider i = i as Point of N by A13;
A15: for j being Element of X holds s9 . j <= t9 . j
proof
let j be Element of X; ::_thesis: s9 . j <= t9 . j
A16: Omega Y = ( the carrier of X --> (Omega Y)) . j by FUNCOP_1:7;
A17: ss . j = the mapping of (commute (N,j,(Omega Y))) . i by A14, Th24;
percases ( j <> x or j = x ) ;
suppose j <> x ; ::_thesis: s9 . j <= t9 . j
then  ex u being Element of X st
( j = u & t . j = sup (commute (N,u,(Omega Y))) ) by A11;
then A18: t9 . j = Sup by WAYBEL_2:def_1
.= sup (rng the mapping of (commute (N,j,(Omega Y)))) ;
 commute (N,j,(Omega Y)) is eventually-directed by A1;
then  ex_sup_of commute (N,j,(Omega Y)) by Th31;
then A19: ex_sup_of rng the mapping of (commute (N,j,(Omega Y))), Omega Y by WAYBEL_9:def_3;
 i in dom the mapping of (commute (N,j,(Omega Y))) by A13, Lm6;
then  ss . j in rng the mapping of (commute (N,j,(Omega Y))) by A17, FUNCT_1:def_3;
hence  s9 . j <= t9 . j by A16, A18, A19, YELLOW_4:1; ::_thesis: verum
end;
supposeA20: j = x ; ::_thesis: s9 . j <= t9 . j
A21: the mapping of (commute (N,x,(Omega Y))) . i in rng the mapping of (commute (N,x,(Omega Y))) by A6, FUNCT_1:def_3;
 ss . x = the mapping of (commute (N,x,(Omega Y))) . i by A14, Th24;
then  ss . x <= a by A12, A21;
hence  s9 . j <= t9 . j by A11, A16, A20; ::_thesis: verum
end;
end;
end;
 (Omega Y) |^ the carrier of X = product ( the carrier of X --> (Omega Y)) by YELLOW_1:def_5;
hence  s <= tt by A15, WAYBEL_3:28; ::_thesis: verum
end;
then  "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) <= tt by A4, YELLOW_0:30;
then A22: p <= q by YELLOW_1:def_5;
 tt . x = a by A11;
hence  f . x <= a by A2, A8, A22, WAYBEL_3:28; ::_thesis: verum
end;
 rng the mapping of (commute (N,x,(Omega Y))) is_<=_than f . x
proof
let w be Element of (Omega Y); :: according to LATTICE3:def_9 ::_thesis: ( not w in rng the mapping of (commute (N,x,(Omega Y))) or w <= f . x )
assume  w in rng the mapping of (commute (N,x,(Omega Y))) ; ::_thesis: w <= f . x
then consider i being set  such that
A23: i in dom the mapping of (commute (N,x,(Omega Y))) and
A24: the mapping of (commute (N,x,(Omega Y))) . i = w by FUNCT_1:def_3;
reconsider i = i as Point of N by A5, A23, Lm6;
reconsider g = the mapping of N . i as Function of X,(Omega Y) by Lm5;
 g in rng the mapping of N by A5, FUNCT_1:def_3;
then  g <= f by A2, A3, Th26, Th40;
then  ex a, b being Element of (Omega Y) st
( a = g . x & b = f . x & a <= b ) by YELLOW_2:def_1;
hence  w <= f . x by A24, Th24; ::_thesis: verum
end;
hence f . x = Sup by A7, YELLOW_0:30
.= sup (commute (N,x,(Omega Y))) by WAYBEL_2:def_1 ;
::_thesis: verum
end;

theorem Th42: :: WAYBEL25:42
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) holds
"\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y
proof
let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) holds
"\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y
let Y be monotone-convergence T_0-TopSpace; ::_thesis: for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) holds
"\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y
let N be net of ContMaps (X,(Omega Y)); ::_thesis: ( ( for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ) implies "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y )
assume A1: for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed ; ::_thesis: "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y
set m = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
reconsider fo = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) as Function of X,(Omega Y) by WAYBEL24:19;
A2: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2;
then reconsider f = fo as Function of X,Y ;
A3: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
A4: for V being Subset of Y st V is open holds
f " V is open
proof
let V be Subset of Y; ::_thesis: ( V is open implies f " V is open )
assume A5: V is open ; ::_thesis: f " V is open
set M =  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  ;
 for x being set holds
( x in f " V iff x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  )
proof
let x be set ; ::_thesis: ( x in f " V iff x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  )
A6: dom f = the carrier of X by FUNCT_2:def_1;
thus  ( x in f " V implies x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  ) ::_thesis: ( x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  implies x in f " V )
proof
A7: the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y))) by Lm4;
assume A8: x in f " V ; ::_thesis: x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }
then A9: f . x in V by FUNCT_2:38;
reconsider x = x as Point of X by A8;
set NET = commute (N,x,(Omega Y));
 commute (N,x,(Omega Y)) is eventually-directed by A1;
then reconsider W = rng (netmap ((commute (N,x,(Omega Y))),(Omega Y))) as non empty directed Subset of (Omega Y) by WAYBEL_2:18;
f . x = sup (commute (N,x,(Omega Y))) by A1, Th41
.= Sup by WAYBEL_2:def_1
.= sup W ;
then  W meets V by A5, A9, Def4;
then consider k being set  such that
A10: k in W and
A11: k in V by XBOOLE_0:3;
consider i being set  such that
A12: i in dom (netmap ((commute (N,x,(Omega Y))),(Omega Y))) and
A13: k = (netmap ((commute (N,x,(Omega Y))),(Omega Y))) . i by A10, FUNCT_1:def_3;
 ContMaps (X,(Omega Y)) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then A14: the carrier of (ContMaps (X,(Omega Y))) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
then  RelStr(# the carrier of (commute (N,x,(Omega Y))), the InternalRel of (commute (N,x,(Omega Y))) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;
then reconsider i = i as Element of N by A12;
reconsider g = N . i as Function of X,(Omega Y) by WAYBEL24:21;
A15: dom g = the carrier of X by FUNCT_2:def_1;
A16: g " V in  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  ;
(netmap ((commute (N,x,(Omega Y))),(Omega Y))) . i = ((commute the mapping of N) . x) . i by A14, Def3
.= ( the mapping of N . i) . x by A7, FUNCT_6:56 ;
then  x in g " V by A11, A13, A15, FUNCT_1:def_7;
hence  x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  by A16, TARSKI:def_4; ::_thesis: verum
end;
assume  x in union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  ; ::_thesis: x in f " V
then consider Z being set  such that
A17: x in Z and
A18: Z in  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  by TARSKI:def_4;
consider A being Subset of X such that
A19: Z = A and
A20: ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) by A18;
consider i being Element of N, g being Function of X,(Omega Y) such that
A21: g = N . i and
A22: A = g " V by A20;
A23: g . x in V by A17, A19, A22, FUNCT_1:def_7;
A24: for x being Point of X holds ex_sup_of commute (N,x,(Omega Y))
proof
let x be Point of X; ::_thesis: ex_sup_of commute (N,x,(Omega Y))
 commute (N,x,(Omega Y)) is eventually-directed by A1;
hence  ex_sup_of commute (N,x,(Omega Y)) by Th31; ::_thesis: verum
end;
reconsider x = x as Element of X by A17, A19;
 the mapping of N . i in rng the mapping of N by A3, FUNCT_1:def_3;
then  g <= fo by A21, A24, Th26, Th40;
then  ex a, b being Element of (Omega Y) st
( a = g . x & b = fo . x & a <= b ) by YELLOW_2:def_1;
then consider O being Subset of Y such that
A25: O = {(f . x)} and
A26: g . x in Cl O by Def2;
 V meets O by A5, A23, A26, PRE_TOPC:def_7;
then consider w being set  such that
A27: w in V /\ O by XBOOLE_0:4;
 w in O by A27, XBOOLE_0:def_4;
then A28: w = f . x by A25, TARSKI:def_1;
 w in V by A27, XBOOLE_0:def_4;
hence  x in f " V by A6, A28, FUNCT_1:def_7; ::_thesis: verum
end;
then A29: f " V = union  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  by TARSKI:1;
  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  c= bool the carrier of X
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  or m in bool the carrier of X )
assume  m in  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  ; ::_thesis: m in bool the carrier of X
then  ex A being Subset of X st
( m = A & ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) ) ;
hence  m in bool the carrier of X ; ::_thesis: verum
end;
then reconsider M =  {  A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V )  }  as Subset-Family of X ;
reconsider M = M as Subset-Family of X ;
 M is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in M or P is open )
assume  P in M ; ::_thesis: P is open
then consider A being Subset of X such that
A30: P = A and
A31: ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) ;
consider i being Element of N, g being Function of X,(Omega Y) such that
A32: g = N . i and
A33: A = g " V by A31;
consider g9 being Function of X,(Omega Y) such that
A34: g = g9 and
A35: g9 is continuous by A32, WAYBEL24:def_3;
 TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ;
then reconsider g99 = g9 as continuous Function of X,Y by A2, A35, YELLOW12:36;
 [#] Y <> {} ;
then  g99 " V is open by A5, TOPS_2:43;
hence  P is open by A30, A33, A34; ::_thesis: verum
end;
hence  f " V is open by A29, TOPS_2:19; ::_thesis: verum
end;
 [#] Y <> {} ;
hence  "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y by A4, TOPS_2:43; ::_thesis: verum
end;

theorem :: WAYBEL25:43
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace holds ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
proof
let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace holds ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
let Y be monotone-convergence T_0-TopSpace; ::_thesis: ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
set L = (Omega Y) |^ the carrier of X;
reconsider C = ContMaps (X,(Omega Y)) as non empty full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
 C is directed-sups-inheriting
proof
let D be directed Subset of C; :: according to WAYBEL_0:def_4 ::_thesis: ( D = {} or not ex_sup_of D,(Omega Y) |^ the carrier of X or "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C )
assume that
A1: D <> {} and
 ex_sup_of D,(Omega Y) |^ the carrier of X ; ::_thesis: "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C
reconsider D = D as non empty directed Subset of C by A1;
set N = Net-Str D;
A2: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ;
 for x being Point of X holds commute ((Net-Str D),x,(Omega Y)) is eventually-directed ;
then A3: "\/" ((rng the mapping of (Net-Str D)),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y by Th42;
 TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by Def2;
then  "\/" ((rng the mapping of (Net-Str D)),((Omega Y) |^ the carrier of X)) is continuous Function of X,(Omega Y) by A2, A3, YELLOW12:36;
then A4: "\/" ((rng the mapping of (Net-Str D)),((Omega Y) |^ the carrier of X)) in the carrier of C by WAYBEL24:def_3;
 Net-Str D = NetStr(# D,( the InternalRel of C |_2 D),((id the carrier of C) | D) #) by WAYBEL17:def_4;
hence  "\/" (D,((Omega Y) |^ the carrier of X)) in the carrier of C by A4, YELLOW14:2; ::_thesis: verum
end;
hence  ContMaps (X,(Omega Y)) is directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X ; ::_thesis: verum
end;