:: WAYBEL25 semantic presentation

theorem Th1: :: WAYBEL25:1
for b1 being Point of Sierpinski_Space st b1 = 0 holds
{b1} is closed
proof end;

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

registration
cluster Sierpinski_Space -> non being_T1 ;
coherence
not Sierpinski_Space is being_T1
proof end;
end;

registration
cluster complete Scott -> discerning TopRelStr ;
coherence
for b1 being TopLattice st b1 is complete & b1 is Scott holds
b1 is discerning by WAYBEL11:10;
end;

registration
cluster strict injective TopStruct ;
existence
ex b1 being T_0-TopSpace st
( b1 is injective & b1 is strict )
proof end;
end;

registration
cluster discerning complete strict Scott TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is complete & b1 is Scott & b1 is strict )
proof end;
end;

theorem Th3: :: WAYBEL25:3
for b1 being non empty set
for b2 being Scott TopAugmentation of product (b1 --> (BoolePoset 1)) holds the carrier of b2 = the carrier of (product (b1 --> Sierpinski_Space ))
proof end;

theorem Th4: :: WAYBEL25:4
for b1, b2 being complete LATTICE
for b3 being Scott TopAugmentation of b1
for b4 being Scott TopAugmentation of b2
for b5 being Function of b1,b2
for b6 being Function of b3,b4 st b5 = b6 & b5 is isomorphic holds
b6 is_homeomorphism
proof end;

theorem Th5: :: WAYBEL25:5
for b1, b2 being complete LATTICE
for b3 being Scott TopAugmentation of b1
for b4 being Scott TopAugmentation of b2 st b1,b2 are_isomorphic holds
b3,b4 are_homeomorphic
proof end;

theorem Th6: :: WAYBEL25:6
for b1, b2 being non empty TopSpace st b1 is injective & b1,b2 are_homeomorphic holds
b2 is injective
proof end;

theorem Th7: :: WAYBEL25:7
for b1, b2 being complete LATTICE
for b3 being Scott TopAugmentation of b1
for b4 being Scott TopAugmentation of b2 st b1,b2 are_isomorphic & b3 is injective holds
b4 is injective
proof end;

definition
let c1, c2 be non empty TopSpace;
redefine pred c1 is_Retract_of c2 means :Def1: :: WAYBEL25:def 1
ex b1 being continuous Function of a1,a2ex b2 being continuous Function of a2,a1 st b2 * b1 = id a1;
compatibility
( c1 is_Retract_of c2 iff ex b1 being continuous Function of c1,c2ex b2 being continuous Function of c2,c1 st b2 * b1 = id c1 )
proof end;
end;

:: deftheorem Def1 defines is_Retract_of WAYBEL25:def 1 :
for b1, b2 being non empty TopSpace holds
( b1 is_Retract_of b2 iff ex b3 being continuous Function of b1,b2ex b4 being continuous Function of b2,b1 st b4 * b3 = id b1 );

theorem Th8: :: WAYBEL25:8
for b1, b2, b3, b4 being non empty TopSpace st TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & TopStruct(# the carrier of b3,the topology of b3 #) = TopStruct(# the carrier of b4,the topology of b4 #) & b1 is_Retract_of b3 holds
b2 is_Retract_of b4
proof end;

theorem Th9: :: WAYBEL25:9
for b1, b2, b3 being non empty TopStruct st b2,b3 are_homeomorphic & b2 is_Retract_of b1 holds
b3 is_Retract_of b1
proof end;

theorem Th10: :: WAYBEL25:10
for b1, b2 being non empty TopSpace st b2 is injective & b1 is_Retract_of b2 holds
b1 is injective
proof end;

theorem Th11: :: WAYBEL25:11
for b1 being non empty injective TopSpace
for b2 being non empty TopSpace st b1 is SubSpace of b2 holds
b1 is_Retract_of b2
proof end;

theorem Th12: :: WAYBEL25:12
for b1 being complete continuous LATTICE
for b2 being Scott TopAugmentation of b1 holds b2 is injective
proof end;

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

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

definition
let c1 be TopStruct ;
func Omega c1 -> strict TopRelStr means :Def2: :: WAYBEL25:def 2
( TopStruct(# the carrier of a2,the topology of a2 #) = TopStruct(# the carrier of a1,the topology of a1 #) & ( for b1, b2 being Element of a2 holds
( b1 <= b2 iff ex b3 being Subset of a1 st
( b3 = {b2} & b1 in Cl b3 ) ) ) );
existence
ex b1 being strict TopRelStr st
( TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of c1,the topology of c1 #) & ( for b2, b3 being Element of b1 holds
( b2 <= b3 iff ex b4 being Subset of c1 st
( b4 = {b3} & b2 in Cl b4 ) ) ) )
proof end;
uniqueness
for b1, b2 being strict TopRelStr st TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of c1,the topology of c1 #) & ( for b3, b4 being Element of b1 holds
( b3 <= b4 iff ex b5 being Subset of c1 st
( b5 = {b4} & b3 in Cl b5 ) ) ) & TopStruct(# the carrier of b2,the topology of b2 #) = TopStruct(# the carrier of c1,the topology of c1 #) & ( for b3, b4 being Element of b2 holds
( b3 <= b4 iff ex b5 being Subset of c1 st
( b5 = {b4} & b3 in Cl b5 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Omega WAYBEL25:def 2 :
for b1 being TopStruct
for b2 being strict TopRelStr holds
( b2 = Omega b1 iff ( TopStruct(# the carrier of b2,the topology of b2 #) = TopStruct(# the carrier of b1,the topology of b1 #) & ( for b3, b4 being Element of b2 holds
( b3 <= b4 iff ex b5 being Subset of b1 st
( b5 = {b4} & b3 in Cl b5 ) ) ) ) );

Lemma10: for b1 being TopStruct holds the carrier of b1 = the carrier of (Omega b1)
proof end;

then Lemma11: for b1 being TopStruct
for b2 being set holds
( b2 is Subset of b1 iff b2 is Subset of (Omega b1) )
;

registration
let c1 be empty TopStruct ;
cluster Omega a1 -> empty strict ;
coherence
Omega c1 is empty
proof end;
end;

registration
let c1 be non empty TopStruct ;
cluster Omega a1 -> non empty strict ;
coherence
not Omega c1 is empty
proof end;
end;

registration
let c1 be TopSpace;
cluster Omega a1 -> TopSpace-like strict ;
coherence
Omega c1 is TopSpace-like
proof end;
end;

registration
let c1 be TopStruct ;
cluster Omega a1 -> reflexive strict ;
coherence
Omega c1 is reflexive
proof end;
end;

Lemma12: for b1 being TopStruct
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b4 = {b2} & b5 = {b3} holds
( b2 in Cl b5 iff Cl b4 c= Cl b5 )
proof end;

registration
let c1 be TopStruct ;
cluster Omega a1 -> reflexive transitive strict ;
coherence
Omega c1 is transitive
proof end;
end;

registration
let c1 be T_0-TopSpace;
cluster Omega a1 -> non empty TopSpace-like reflexive transitive antisymmetric strict ;
coherence
Omega c1 is antisymmetric
proof end;
end;

theorem Th13: :: WAYBEL25:13
for b1, b2 being TopSpace st TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) holds
Omega b1 = Omega b2
proof end;

theorem Th14: :: WAYBEL25:14
for b1 being non empty set
for b2 being non empty TopSpace holds RelStr(# the carrier of (Omega (product (b1 --> b2))),the InternalRel of (Omega (product (b1 --> b2))) #) = RelStr(# the carrier of (product (b1 --> (Omega b2))),the InternalRel of (product (b1 --> (Omega b2))) #)
proof end;

theorem Th15: :: WAYBEL25:15
for b1 being complete Scott TopLattice holds Omega b1 = TopRelStr(# the carrier of b1,the InternalRel of b1,the topology of b1 #)
proof end;

theorem Th16: :: WAYBEL25:16
for b1 being complete LATTICE
for b2 being Scott TopAugmentation of b1 holds RelStr(# the carrier of (Omega b2),the InternalRel of (Omega b2) #) = RelStr(# the carrier of b1,the InternalRel of b1 #)
proof end;

registration
let c1 be complete Scott TopLattice;
cluster Omega a1 -> non empty TopSpace-like reflexive transitive antisymmetric complete strict ;
coherence
Omega c1 is complete
proof end;
end;

theorem Th17: :: WAYBEL25:17
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds Omega b2 is full SubRelStr of Omega b1
proof end;

theorem Th18: :: WAYBEL25:18
for b1, b2 being TopSpace
for b3 being Function of b1,b2
for b4 being Function of (Omega b1),(Omega b2) st b3 = b4 & b3 is_homeomorphism holds
b4 is isomorphic
proof end;

theorem Th19: :: WAYBEL25:19
for b1, b2 being TopSpace st b1,b2 are_homeomorphic holds
Omega b1, Omega b2 are_isomorphic
proof end;

Lemma19: for b1, b2 being non empty RelStr
for b3 being Function of b1,b1
for b4 being Function of b2,b2 st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of b2,the InternalRel of b2 #) & b3 = b4 & b3 is projection holds
b4 is projection
proof end;

theorem Th20: :: WAYBEL25:20
for b1 being injective T_0-TopSpace holds Omega b1 is complete continuous LATTICE
proof end;

registration
let c1 be injective T_0-TopSpace;
cluster Omega a1 -> non empty TopSpace-like reflexive transitive antisymmetric complete strict continuous ;
coherence
( Omega c1 is complete & Omega c1 is continuous ) by Th20;
end;

theorem Th21: :: WAYBEL25:21
for b1, b2 being non empty TopSpace
for b3 being continuous Function of (Omega b1),(Omega b2) holds b3 is monotone
proof end;

registration
let c1, c2 be non empty TopSpace;
cluster continuous -> monotone Relation of the carrier of (Omega a1),the carrier of (Omega a2);
coherence
for b1 being Function of (Omega c1),(Omega c2) st b1 is continuous holds
b1 is monotone by Th21;
end;

theorem Th22: :: WAYBEL25:22
for b1 being non empty TopSpace
for b2 being Element of (Omega b1) holds Cl {b2} = downarrow b2
proof end;

registration
let c1 be non empty TopSpace;
let c2 be Element of (Omega c1);
cluster Cl {a2} -> non empty directed lower ;
coherence
( not Cl {c2} is empty & Cl {c2} is lower & Cl {c2} is directed )
proof end;
cluster downarrow a2 -> closed ;
coherence
downarrow c2 is closed
proof end;
end;

theorem Th23: :: WAYBEL25:23
for b1 being TopSpace
for b2 being open Subset of (Omega b1) holds b2 is upper
proof end;

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

E24: now
let c1, c2 be non empty TopSpace;
let c3 be net of ContMaps c1,(Omega c2);
E25: the mapping of c3 in Funcs the carrier of c3,the carrier of (ContMaps c1,(Omega c2)) by FUNCT_2:11;
E26: the carrier of c2 = the carrier of (Omega c2) by Lemma10;
the carrier of (ContMaps c1,(Omega c2)) c= Funcs the carrier of c1,the carrier of c2
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in the carrier of (ContMaps c1,(Omega c2)) ;
then ex b1 being Function of c1,(Omega c2) st
( b1 = c4 & b1 is continuous ) by WAYBEL24:def 3;
hence c4 in Funcs the carrier of c1,the carrier of c2 by E26, FUNCT_2:11;
end;
then Funcs the carrier of c3,the carrier of (ContMaps c1,(Omega c2)) c= Funcs the carrier of c3,(Funcs the carrier of c1,the carrier of c2) by FUNCT_5:63;
hence the mapping of c3 in Funcs the carrier of c3,(Funcs the carrier of c1,the carrier of c2) by E25;
end;

definition
let c1 be non empty set ;
let c2, c3 be non empty RelStr ;
let c4 be net of c3;
let c5 be Element of c1;
assume E25: the carrier of c3 c= the carrier of (c2 |^ c1) ;
func commute c4,c5,c2 -> strict net of a2 means :Def3: :: WAYBEL25:def 3
( RelStr(# the carrier of a6,the InternalRel of a6 #) = RelStr(# the carrier of a4,the InternalRel of a4 #) & the mapping of a6 = (commute the mapping of a4) . a5 );
existence
ex b1 being strict net of c2 st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c4,the InternalRel of c4 #) & the mapping of b1 = (commute the mapping of c4) . c5 )
proof end;
uniqueness
for b1, b2 being strict net of c2 st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c4,the InternalRel of c4 #) & the mapping of b1 = (commute the mapping of c4) . c5 & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of c4,the InternalRel of c4 #) & the mapping of b2 = (commute the mapping of c4) . c5 holds
b1 = b2 ;
end;

:: deftheorem Def3 defines commute WAYBEL25:def 3 :
for b1 being non empty set
for b2, b3 being non empty RelStr
for b4 being net of b3
for b5 being Element of b1 st the carrier of b3 c= the carrier of (b2 |^ b1) holds
for b6 being strict net of b2 holds
( b6 = commute b4,b5,b2 iff ( RelStr(# the carrier of b6,the InternalRel of b6 #) = RelStr(# the carrier of b4,the InternalRel of b4 #) & the mapping of b6 = (commute the mapping of b4) . b5 ) );

theorem Th24: :: WAYBEL25:24
for b1, b2 being non empty TopSpace
for b3 being net of ContMaps b1,(Omega b2)
for b4 being Element of b3
for b5 being Point of b1 holds the mapping of (commute b3,b5,(Omega b2)) . b4 = (the mapping of b3 . b4) . b5
proof end;

theorem Th25: :: WAYBEL25:25
for b1, b2 being non empty TopSpace
for b3 being eventually-directed net of ContMaps b1,(Omega b2)
for b4 being Point of b1 holds commute b3,b4,(Omega b2) is eventually-directed
proof end;

registration
let c1, c2 be non empty TopSpace;
let c3 be eventually-directed net of ContMaps c1,(Omega c2);
let c4 be Point of c1;
cluster commute a3,a4,(Omega a2) -> strict eventually-directed ;
coherence
commute c3,c4,(Omega c2) is eventually-directed by Th25;
end;

registration
let c1, c2 be non empty TopSpace;
cluster -> Function-yielding NetStr of ContMaps a1,(Omega a2);
coherence
for b1 being net of ContMaps c1,(Omega c2) holds b1 is Function-yielding ;
end;

E28: now
let c1, c2 be non empty TopSpace;
let c3 be net of ContMaps c1,(Omega c2);
let c4 be Element of c3;
thus the mapping of c3 . c4 is Function of c1,(Omega c2) by WAYBEL24:21;
the carrier of c2 = the carrier of (Omega c2) by Lemma10;
hence the mapping of c3 . c4 is Function of c1,c2 by WAYBEL24:21;
end;

E29: now
let c1, c2 be non empty TopSpace;
let c3 be net of ContMaps c1,(Omega c2);
let c4 be Point of c1;
ContMaps c1,(Omega c2) is SubRelStr of (Omega c2) |^ the carrier of c1 by WAYBEL24:def 3;
then the carrier of (ContMaps c1,(Omega c2)) c= the carrier of ((Omega c2) |^ the carrier of c1) by YELLOW_0:def 13;
then E30: RelStr(# the carrier of c3,the InternalRel of c3 #) = RelStr(# the carrier of (commute c3,c4,(Omega c2)),the InternalRel of (commute c3,c4,(Omega c2)) #) by Def3;
thus dom the mapping of c3 = the carrier of c3 by FUNCT_2:def 1
.= dom the mapping of (commute c3,c4,(Omega c2)) by E30, FUNCT_2:def 1 ;
end;

theorem Th26: :: WAYBEL25:26
for b1 being non empty TopSpace
for b2 being T_0-TopSpace
for b3 being net of ContMaps b1,(Omega b2) st ( for b4 being Point of b1 holds ex_sup_of commute b3,b4,(Omega b2) ) holds
ex_sup_of rng the mapping of b3,(Omega b2) |^ the carrier of b1
proof end;

definition
let c1 be non empty TopSpace;
attr a1 is monotone-convergence means :Def4: :: WAYBEL25:def 4
for b1 being non empty directed Subset of (Omega a1) holds
( ex_sup_of b1, Omega a1 & ( for b2 being open Subset of a1 st sup b1 in b2 holds
b1 meets b2 ) );
end;

:: deftheorem Def4 defines monotone-convergence WAYBEL25:def 4 :
for b1 being non empty TopSpace holds
( b1 is monotone-convergence iff for b2 being non empty directed Subset of (Omega b1) holds
( ex_sup_of b2, Omega b1 & ( for b3 being open Subset of b1 st sup b2 in b3 holds
b2 meets b3 ) ) );

theorem Th27: :: WAYBEL25:27
for b1, b2 being non empty TopSpace st TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of b2,the topology of b2 #) & b1 is monotone-convergence holds
b2 is monotone-convergence
proof end;

E33: now
let c1 be non empty 1-sorted ;
let c2 be non empty Subset of c1;
let c3 be Element of c1;
assume E34: the carrier of c1 = {c3} ;
thus c2 = {c3}
proof
thus c2 c= {c3} by E34; :: according to XBOOLE_0:def 10
let c4 be set ; :: according to TARSKI:def 3
assume c4 in {c3} ;
then E35: c4 = c3 by TARSKI:def 1;
consider c5 being Element of c2;
c5 in c2 ;
hence c4 in c2 by E34, E35, TARSKI:def 1;
end;
end;

registration
cluster trivial -> monotone-convergence TopStruct ;
coherence
for b1 being T_0-TopSpace st b1 is trivial holds
b1 is monotone-convergence
proof end;
end;

registration
cluster non empty strict trivial monotone-convergence TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is trivial & not b1 is empty )
proof end;
end;

theorem Th28: :: WAYBEL25:28
for b1 being monotone-convergence T_0-TopSpace
for b2 being T_0-TopSpace st b1,b2 are_homeomorphic holds
b2 is monotone-convergence
proof end;

theorem Th29: :: WAYBEL25:29
for b1 being complete Scott TopLattice holds b1 is monotone-convergence
proof end;

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

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

theorem Th30: :: WAYBEL25:30
for b1 being monotone-convergence T_0-TopSpace holds Omega b1 is up-complete
proof end;

registration
let c1 be monotone-convergence T_0-TopSpace;
cluster Omega a1 -> non empty TopSpace-like reflexive transitive antisymmetric up-complete strict ;
coherence
Omega c1 is up-complete by Th30;
end;

theorem Th31: :: WAYBEL25:31
for b1 being non empty monotone-convergence TopSpace
for b2 being eventually-directed prenet of Omega b1 holds ex_sup_of b2
proof end;

theorem Th32: :: WAYBEL25:32
for b1 being non empty monotone-convergence TopSpace
for b2 being eventually-directed net of Omega b1 holds sup b2 in Lim b2
proof end;

theorem Th33: :: WAYBEL25:33
for b1 being non empty monotone-convergence TopSpace
for b2 being eventually-directed net of Omega b1 holds b2 is convergent
proof end;

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

theorem Th34: :: WAYBEL25:34
for b1 being non empty TopSpace st ( for b2 being eventually-directed net of Omega b1 holds
( ex_sup_of b2 & sup b2 in Lim b2 ) ) holds
b1 is monotone-convergence
proof end;

theorem Th35: :: WAYBEL25:35
for b1 being non empty monotone-convergence TopSpace
for b2 being T_0-TopSpace
for b3 being continuous Function of (Omega b1),(Omega b2) holds b3 is directed-sups-preserving
proof end;

registration
let c1 be non empty monotone-convergence TopSpace;
let c2 be T_0-TopSpace;
cluster continuous -> directed-sups-preserving Relation of the carrier of (Omega a1),the carrier of (Omega a2);
coherence
for b1 being Function of (Omega c1),(Omega c2) st b1 is continuous holds
b1 is directed-sups-preserving by Th35;
end;

theorem Th36: :: WAYBEL25:36
for b1 being monotone-convergence T_0-TopSpace
for b2 being T_0-TopSpace st b2 is_Retract_of b1 holds
b2 is monotone-convergence
proof end;

theorem Th37: :: WAYBEL25:37
for b1 being injective T_0-TopSpace
for b2 being Scott TopAugmentation of Omega b1 holds TopStruct(# the carrier of b2,the topology of b2 #) = TopStruct(# the carrier of b1,the topology of b1 #)
proof end;

theorem Th38: :: WAYBEL25:38
for b1 being injective T_0-TopSpace holds
( b1 is compact & b1 is locally-compact & b1 is sober )
proof end;

theorem Th39: :: WAYBEL25:39
for b1 being injective T_0-TopSpace holds b1 is monotone-convergence
proof end;

registration
cluster injective -> monotone-convergence 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 b1 being non empty TopSpace
for b2 being monotone-convergence T_0-TopSpace
for b3 being net of ContMaps b1,(Omega b2)
for b4, b5 being Function of b1,(Omega b2) st b4 = "\/" (rng the mapping of b3),((Omega b2) |^ the carrier of b1) & ex_sup_of rng the mapping of b3,(Omega b2) |^ the carrier of b1 & b5 in rng the mapping of b3 holds
b5 <= b4
proof end;

theorem Th41: :: WAYBEL25:41
for b1 being non empty TopSpace
for b2 being monotone-convergence T_0-TopSpace
for b3 being net of ContMaps b1,(Omega b2)
for b4 being Point of b1
for b5 being Function of b1,(Omega b2) st ( for b6 being Point of b1 holds commute b3,b6,(Omega b2) is eventually-directed ) & b5 = "\/" (rng the mapping of b3),((Omega b2) |^ the carrier of b1) holds
b5 . b4 = sup (commute b3,b4,(Omega b2))
proof end;

theorem Th42: :: WAYBEL25:42
for b1 being non empty TopSpace
for b2 being monotone-convergence T_0-TopSpace
for b3 being net of ContMaps b1,(Omega b2) st ( for b4 being Point of b1 holds commute b3,b4,(Omega b2) is eventually-directed ) holds
"\/" (rng the mapping of b3),((Omega b2) |^ the carrier of b1) is continuous Function of b1,b2
proof end;

theorem Th43: :: WAYBEL25:43
for b1 being non empty TopSpace
for b2 being monotone-convergence T_0-TopSpace holds ContMaps b1,(Omega b2) is directed-sups-inheriting SubRelStr of (Omega b2) |^ the carrier of b1
proof end;