:: Injective Spaces, Part { II }
:: by Artur Korni{\l}owicz and Jaros{\l}aw Gryko
::
:: Received July 3, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem :: WAYBEL25:1
for p being Point of Sierpinski_Space st p = 0 holds
{p} is closed
proofend;

theorem Th2: :: WAYBEL25:2
for p being Point of Sierpinski_Space st p = 1 holds
not {p} is closed
proofend;

registration
cluster Sierpinski_Space  ->  non T_1 ;
coherence
 not Sierpinski_Space is T_1
proofend;
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 )
proofend;
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 )
proofend;
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))
proofend;

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

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

theorem Th6: :: WAYBEL25:6
for S, T being non empty TopSpace st S is injective & S,T are_homeomorphic holds
T is injective
proofend;

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 )
proofend;
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
proofend;

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

theorem :: WAYBEL25:10
for S, T being non empty TopSpace st T is injective & S is_Retract_of T holds
S is injective
proofend;

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

:: p.123 proposition 3.5
:: p.124 theorem 3.8 (i, part a)
:: p.126 exercise 3.14
theorem Th12: :: WAYBEL25:12
for L being complete continuous LATTICE
for T being Scott TopAugmentation of L holds T is injective
proofend;

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

::p.124 definition 3.6
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} &amp; 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 #) &amp; ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} &amp; x in Cl Y ) ) ) )
proofend;
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 #) &amp; ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} &amp; x in Cl Y ) ) ) &amp; TopStruct(# the carrier of b2, the topology of b2 #) = TopStruct(# the carrier of T, the topology of T #) &amp; ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} &amp; x in Cl Y ) ) ) holds
b1 = b2
proofend;
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 #) &amp; ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} &amp; x in Cl Y ) ) ) ) );

Lm1:  for T being TopStruct holds the carrier of T = the carrier of (Omega T)
proofend;

registration
let T be empty TopStruct ;
cluster Omega T ->  empty strict ;
coherence
 Omega T is empty
proofend;
end;

registration
let T be non empty TopStruct ;
cluster Omega T ->  non empty strict ;
coherence
 not Omega T is empty
proofend;
end;

registration
let T be TopSpace;
cluster Omega T ->  TopSpace-like strict ;
coherence
 Omega T is TopSpace-like
proofend;
end;

registration
let T be TopStruct ;
cluster Omega T ->  reflexive strict ;
coherence
 Omega T is reflexive
proofend;
end;

Lm2:  for T being TopStruct
for x, y being Element of T
for X, Y being Subset of T st X = {x} &amp; Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
proofend;

registration
let T be TopStruct ;
cluster Omega T ->  transitive strict ;
coherence
 Omega T is transitive
proofend;
end;

registration
let T be T_0-TopSpace;
cluster Omega T ->  antisymmetric strict ;
coherence
 Omega T is antisymmetric
proofend;
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
proofend;

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))) #)
proofend;

::p.124 theorem 3.8 (i, part b)
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 #)
proofend;

::p.124 theorem 3.8 (i, part b)
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 #)
proofend;

registration
let S be complete Scott TopLattice;
cluster Omega S ->  complete strict ;
coherence
 Omega S is complete
proofend;
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
proofend;

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 &amp; h is being_homeomorphism holds
g is isomorphic
proofend;

theorem Th19: :: WAYBEL25:19
for S, T being TopSpace st S,T are_homeomorphic holds
Omega S, Omega T are_isomorphic
proofend;

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 #) &amp; f = g &amp; f is projection holds
g is projection
proofend;

::p.124 proposition 3.7
::p.124 theorem 3.8 (ii, part a)
theorem Th20: :: WAYBEL25:20
for T being injective T_0-TopSpace holds Omega T is complete continuous LATTICE
proofend;

registration
let T be injective T_0-TopSpace;
cluster Omega T ->  complete strict continuous ;
coherence
 ( Omega T is complete &amp; 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
proofend;

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

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 &amp; Cl {x} is lower &amp; Cl {x} is directed )
proofend;
cluster downarrow x ->  closed ;
coherence
 downarrow x is closed
proofend;
end;

theorem Th23: :: WAYBEL25:23
for X being TopSpace
for A being open Subset of (Omega X) holds A is upper
proofend;

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 toTARSKI: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 &amp; 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 #) &amp; 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 #) &amp; the mapping of b1 = (commute the mapping of N) . i )
proofend;
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 #) &amp; the mapping of b1 = (commute the mapping of N) . i &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; 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 #) &amp; 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
proofend;

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

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)_&amp;_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) &amp; 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) &amp; 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) &amp; 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
proofend;

begin

::p.125 definition 3.9
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 &amp; ( 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 &amp; ( 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 #) &amp; S is monotone-convergence holds
T is monotone-convergence
proofend;

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 toXBOOLE_0:def_10 ::_thesis: {d} c= D
set x = the Element of D;
let a be set ; :: according toTARSKI: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
proofend;
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
proofend;

theorem Th29: :: WAYBEL25:29
for S being complete Scott TopLattice holds S is monotone-convergence
proofend;

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

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

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

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

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 &amp; sup N in Lim N ) ) holds
X is monotone-convergence
proofend;

::p.125 lemma 3.10
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
proofend;

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

::p.124 theorem 3.8 (ii, part b)
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 #)
proofend;

theorem :: WAYBEL25:38
for T being injective T_0-TopSpace holds
( T is compact &amp; T is locally-compact &amp; T is sober )
proofend;

theorem Th39: :: WAYBEL25:39
for T being injective T_0-TopSpace holds T is monotone-convergence
proofend;

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)) &amp; ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X &amp; g in rng the mapping of N holds
g <= f
proofend;

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 ) &amp; f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
proofend;

::p.125 lemma 3.11
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
proofend;

::p.126 lemma 3.12 (i)
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
proofend;