:: WAYBEL11 semantic presentation

Lemma1: for b₁, b₂ being RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ & RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ <= b₄ holds
b₅ <= b₆

proof end;

scheme :: WAYBEL11:sch 1
s1{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set ], F₃( set ) -> set , F₄( set , set ) -> set } :

{ F₃(b₁) where B is Element of F₁() : P₁[b₁] } = { F₄(b₁,b₂) where B is Element of F₂(), B is Element of F₁() : P₁[b₂] }

provided

E2: for b₁ being Element of F₂()
for b₂ being Element of F₁() holds F₃(b₂) = F₄(b₁,b₂)

proof end;

theorem Th1: :: WAYBEL11:1

for b₁ being complete LATTICE
for b₂, b₃ being Subset of b₁ st b₃ is_coarser_than b₂ holds
"/\" b₂,b₁ <= "/\" b₃,b₁

proof end;

theorem Th2: :: WAYBEL11:2

for b₁ being complete LATTICE
for b₂, b₃ being Subset of b₁ st b₂ is_finer_than b₃ holds
"\/" b₂,b₁ <= "\/" b₃,b₁

proof end;

theorem Th3: :: WAYBEL11:3

for b₁ being RelStr
for b₂ being upper Subset of b₁
for b₃ being directed Subset of b₁ holds b₂ /\ b₃ is directed

proof end;

registration

let c₁ be non empty reflexive RelStr ;
cluster non empty finite directed Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th4: :: WAYBEL11:4

for b₁ being with_suprema Poset
for b₂ being non empty finite directed Subset of b₁ holds sup b₂ in b₂

proof end;

registration

cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima finite trivial RelStr ;
existence

proof end;

end;

registration

cluster strict non empty finite 1-sorted ;
existence

proof end;

end;

registration

let c₁ be finite 1-sorted ;
cluster -> finite Element of bool the carrier of a₁;
coherence

proof end;

end;

registration

let c₁ be RelStr ;
cluster {} a₁ -> lower upper ;
coherence

proof end;

end;

registration

let c₁ be non empty trivial RelStr ;
cluster -> upper Element of bool the carrier of a₁;
coherence

proof end;

end;

theorem Th5: :: WAYBEL11:5

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being upper Subset of b₁ st not b₂ in b₃ holds
b₃ misses downarrow b₂

proof end;

theorem Th6: :: WAYBEL11:6

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being lower Subset of b₁ st b₂ in b₃ holds
downarrow b₂ c= b₃

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Subset of c₁;
attr a₂ is inaccessible_by_directed_joins means :Def1: :: WAYBEL11:def 1
for b₁ being non empty directed Subset of a₁ st sup b₁ in a₂ holds
b₁ meets a₂;
attr a₂ is closed_under_directed_sups means :Def2: :: WAYBEL11:def 2
for b₁ being non empty directed Subset of a₁ st b₁ c= a₂ holds
sup b₁ in a₂;
attr a₂ is property(S) means :Def3: :: WAYBEL11:def 3
for b₁ being non empty directed Subset of a₁ st sup b₁ in a₂ holds
ex b₂ being Element of a₁ st
( b₂ in b₁ & ( for b₃ being Element of a₁ st b₃ in b₁ & b₃ >= b₂ holds
b₃ in a₂ ) );

end;

:: deftheorem Def1 defines inaccessible_by_directed_joins WAYBEL11:def 1 :

:: deftheorem Def2 defines closed_under_directed_sups WAYBEL11:def 2 :

:: deftheorem Def3 defines property(S) WAYBEL11:def 3 :

notation

let c₁ be non empty reflexive RelStr ;
let c₂ be Subset of c₁;
synonym inaccessible c₂ for inaccessible_by_directed_joins c₂;
synonym directly_closed c₂ for closed_under_directed_sups c₂;
synonym c₂ has_the_property_(S) for property(S) c₂;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster {} a₁ -> lower upper directly_closed property(S) ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster directly_closed property(S) Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be property(S) Subset of c₁;
cluster a₂ ` -> directly_closed ;
coherence

proof end;

end;

definition

let c₁ be non empty reflexive TopRelStr ;
attr a₁ is Scott means :Def4: :: WAYBEL11:def 4
for b₁ being Subset of a₁ holds
( b₁ is open iff ( b₁ is inaccessible_by_directed_joins & b₁ is upper ) );

end;

:: deftheorem Def4 defines Scott WAYBEL11:def 4 :

registration

let c₁ be non empty reflexive transitive antisymmetric with_suprema finite RelStr ;
cluster -> finite inaccessible Element of bool the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty reflexive transitive antisymmetric with_suprema finite TopRelStr ;
redefine attr a₁ is Scott means :: WAYBEL11:def 5
for b₁ being Subset of a₁ holds
( b₁ is open iff b₁ is upper );
compatibility

proof end;

end;

:: deftheorem Def5 defines Scott WAYBEL11:def 5 :

registration

cluster non empty complete strict trivial Scott TopRelStr ;
existence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster [#] a₁ -> inaccessible directly_closed ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster lower upper inaccessible directly_closed Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be inaccessible Subset of c₁;
cluster a₂ ` -> directly_closed ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be directly_closed Subset of c₁;
cluster a₂ ` -> inaccessible ;
coherence

proof end;

end;

theorem Th7: :: WAYBEL11:7

for b₁ being non empty reflexive transitive up-complete Scott TopRelStr
for b₂ being Subset of b₁ holds
( b₂ is closed iff ( b₂ is closed_under_directed_sups & b₂ is lower ) )

proof end;

theorem Th8: :: WAYBEL11:8

for b₁ being non empty reflexive transitive antisymmetric up-complete TopRelStr
for b₂ being Element of b₁ holds downarrow b₂ is closed_under_directed_sups

proof end;

theorem Th9: :: WAYBEL11:9

for b₁ being complete Scott TopLattice
for b₂ being Element of b₁ holds Cl {b₂} = downarrow b₂

proof end;

theorem Th10: :: WAYBEL11:10

for b₁ being complete Scott TopLattice holds b₁ is T_0-TopSpace

proof end;

theorem Th11: :: WAYBEL11:11

for b₁ being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for b₂ being Element of b₁ holds downarrow b₂ is closed

proof end;

theorem Th12: :: WAYBEL11:12

for b₁ being up-complete Scott TopLattice
for b₂ being Element of b₁ holds (downarrow b₂) ` is open

proof end;

theorem Th13: :: WAYBEL11:13

for b₁ being up-complete Scott TopLattice
for b₂ being Element of b₁
for b₃ being upper Subset of b₁ st not b₂ in b₃ holds
(downarrow b₂) ` is a_neighborhood of b₃

proof end;

theorem Th14: :: WAYBEL11:14

for b₁ being complete Scott TopLattice
for b₂ being upper Subset of b₁ ex b₃ being Subset-Family of b₁ st
( b₂ = meet b₃ & ( for b₄ being Subset of b₁ st b₄ in b₃ holds
b₄ is a_neighborhood of b₂ ) )

proof end;

theorem Th15: :: WAYBEL11:15

for b₁ being Scott TopLattice
for b₂ being Subset of b₁ holds
( b₂ is open iff ( b₂ is upper & b₂ is property(S) ) )

proof end;

registration

let c₁ be complete TopLattice;
cluster lower -> property(S) Element of bool the carrier of a₁;
coherence

proof end;

end;

Lemma17: for b₁ being non empty reflexive TopRelStr holds [#] b₁ has_the_property_(S)

proof end;

theorem Th16: :: WAYBEL11:16

for b₁ being non empty reflexive transitive TopRelStr st the topology of b₁ = { b₂ where B is Subset of b₁ : b₂ has_the_property_(S) } holds
b₁ is TopSpace-like

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be net of c₁;
func lim_inf c₂ -> Element of a₁ equals :: WAYBEL11:def 6
"\/" { ("/\" { (a₂ . b₂) where B is Element of a₂ : b₂ >= b₁ } ,a₁) where B is Element of a₂ : verum } ,a₁;
correctness ;

end;

:: deftheorem Def6 defines lim_inf WAYBEL11:def 6 :

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be net of c₁;
let c₃ be Element of c₁;
pred c₃ is_S-limit_of c₂ means :Def7: :: WAYBEL11:def 7
a₃ <= lim_inf a₂;

end;

:: deftheorem Def7 defines is_S-limit_of WAYBEL11:def 7 :

definition

let c₁ be non empty reflexive RelStr ;
func Scott-Convergence c₁ -> Convergence-Class of a₁ means :Def8: :: WAYBEL11:def 8
for b₁ being strict net of a₁ st b₁ in NetUniv a₁ holds
for b₂ being Element of a₁ holds
( [b₁,b₂] in a₂ iff b₂ is_S-limit_of b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Scott-Convergence WAYBEL11:def 8 :

theorem Th17: :: WAYBEL11:17

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃, b₄ being Element of b₁ st b₃ is_S-limit_of b₂ & b₂ is_eventually_in downarrow b₄ holds
b₃ <= b₄

proof end;

theorem Th18: :: WAYBEL11:18

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃, b₄ being Element of b₁ st b₂ is_eventually_in uparrow b₄ holds
lim_inf b₂ >= b₄

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty NetStr of c₁;
redefine attr a₂ is monotone means :Def9: :: WAYBEL11:def 9
for b₁, b₂ being Element of a₂ st b₁ <= b₂ holds
a₂ . b₁ <= a₂ . b₂;
compatibility

proof end;

end;

:: deftheorem Def9 defines monotone WAYBEL11:def 9 :

definition

let c₁ be non empty RelStr ;
let c₂ be non empty set ;
let c₃ be Function of c₂,the carrier of c₁;
func Net-Str c₂,c₃ -> non empty strict NetStr of a₁ means :Def10: :: WAYBEL11:def 10
( the carrier of a₄ = a₂ & the mapping of a₄ = a₃ & ( for b₁, b₂ being Element of a₄ holds
( b₁ <= b₂ iff a₄ . b₁ <= a₄ . b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Net-Str WAYBEL11:def 10 :

theorem Th19: :: WAYBEL11:19

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁ holds rng the mapping of b₂ = { (b₂ . b₃) where B is Element of b₂ : verum }

proof end;

theorem Th20: :: WAYBEL11:20

for b₁ being non empty RelStr
for b₂ being non empty set
for b₃ being Function of b₂,the carrier of b₁ st rng b₃ is directed holds
Net-Str b₂,b₃ is directed

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty set ;
let c₃ be Function of c₂,the carrier of c₁;
cluster Net-Str a₂,a₃ -> non empty strict monotone ;
coherence

proof end;

end;

registration

let c₁ be non empty transitive RelStr ;
let c₂ be non empty set ;
let c₃ be Function of c₂,the carrier of c₁;
cluster Net-Str a₂,a₃ -> non empty transitive strict monotone ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty set ;
let c₃ be Function of c₂,the carrier of c₁;
cluster Net-Str a₂,a₃ -> non empty reflexive strict monotone ;
coherence

proof end;

end;

theorem Th21: :: WAYBEL11:21

for b₁ being non empty transitive RelStr
for b₂ being non empty set
for b₃ being Function of b₂,the carrier of b₁ st b₂ c= the carrier of b₁ & Net-Str b₂,b₃ is directed holds
Net-Str b₂,b₃ in NetUniv b₁

proof end;

registration

let c₁ be LATTICE;
cluster reflexive strict monotone NetStr of a₁;
existence

proof end;

end;

theorem Th22: :: WAYBEL11:22

for b₁ being complete LATTICE
for b₂ being reflexive monotone net of b₁ holds lim_inf b₂ = sup b₂

proof end;

theorem Th23: :: WAYBEL11:23

for b₁ being complete LATTICE
for b₂ being constant net of b₁ holds the_value_of b₂ = lim_inf b₂

proof end;

theorem Th24: :: WAYBEL11:24

for b₁ being complete LATTICE
for b₂ being constant net of b₁ holds the_value_of b₂ is_S-limit_of b₂

proof end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be Element of c₁;
func Net-Str c₂ -> strict NetStr of a₁ means :Def11: :: WAYBEL11:def 11
( the carrier of a₃ = {a₂} & the InternalRel of a₃ = {[a₂,a₂]} & the mapping of a₃ = id {a₂} );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def11 defines Net-Str WAYBEL11:def 11 :

registration

let c₁ be non empty 1-sorted ;
let c₂ be Element of c₁;
cluster Net-Str a₂ -> non empty strict ;
coherence

proof end;

end;

theorem Th25: :: WAYBEL11:25

for b₁ being non empty 1-sorted
for b₂ being Element of b₁
for b₃ being Element of (Net-Str b₂) holds b₃ = b₂

proof end;

theorem Th26: :: WAYBEL11:26

for b₁ being non empty 1-sorted
for b₂ being Element of b₁
for b₃ being Element of (Net-Str b₂) holds (Net-Str b₂) . b₃ = b₂

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be Element of c₁;
cluster Net-Str a₂ -> non empty reflexive transitive antisymmetric strict directed ;
coherence

proof end;

end;

theorem Th27: :: WAYBEL11:27

for b₁ being non empty 1-sorted
for b₂ being Element of b₁
for b₃ being set holds
( Net-Str b₂ is_eventually_in b₃ iff b₂ in b₃ )

proof end;

theorem Th28: :: WAYBEL11:28

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds b₂ = lim_inf (Net-Str b₂)

proof end;

theorem Th29: :: WAYBEL11:29

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁ holds Net-Str b₂ in NetUniv b₁

proof end;

theorem Th30: :: WAYBEL11:30

for b₁ being complete LATTICE
for b₂ being net of b₁
for b₃ being Subset of b₁ st b₃ = { ("/\" { (b₂ . b₅) where B is Element of b₂ : b₅ >= b₄ } ,b₁) where B is Element of b₂ : verum } holds
( not b₃ is empty & b₃ is directed )

proof end;

theorem Th31: :: WAYBEL11:31

for b₁ being complete LATTICE
for b₂ being Subset of b₁ holds
( b₂ in the topology of (ConvergenceSpace (Scott-Convergence b₁)) iff ( b₂ is inaccessible_by_directed_joins & b₂ is upper ) )

proof end;

theorem Th32: :: WAYBEL11:32

for b₁ being complete Scott TopLattice holds TopStruct(# the carrier of b₁,the topology of b₁ #) = ConvergenceSpace (Scott-Convergence b₁)

proof end;

theorem Th33: :: WAYBEL11:33

for b₁ being complete TopLattice st TopStruct(# the carrier of b₁,the topology of b₁ #) = ConvergenceSpace (Scott-Convergence b₁) holds
for b₂ being Subset of b₁ holds
( b₂ is open iff ( b₂ is inaccessible_by_directed_joins & b₂ is upper ) )

proof end;

theorem Th34: :: WAYBEL11:34

for b₁ being complete TopLattice st TopStruct(# the carrier of b₁,the topology of b₁ #) = ConvergenceSpace (Scott-Convergence b₁) holds
b₁ is Scott

proof end;

registration

let c₁ be complete LATTICE;
cluster Scott-Convergence a₁ -> (CONSTANTS) ;
coherence

proof end;

end;

registration

let c₁ be complete LATTICE;
cluster Scott-Convergence a₁ -> (CONSTANTS) (SUBNETS) ;
coherence

proof end;

end;

theorem Th35: :: WAYBEL11:35

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being set
for b₄ being subnet of b₂ st b₄ = b₂ " b₃ holds
for b₅ being Element of b₄ holds b₄ . b₅ in b₃

proof end;

definition

let c₁ be non empty reflexive RelStr ;
func sigma c₁ -> Subset-Family of a₁ equals :: WAYBEL11:def 12
the topology of (ConvergenceSpace (Scott-Convergence a₁));
coherence by YELLOW_6:def 27;

end;

:: deftheorem Def12 defines sigma WAYBEL11:def 12 :

theorem Th36: :: WAYBEL11:36

for b₁ being continuous complete Scott TopLattice
for b₂ being Element of b₁ holds wayabove b₂ is open

proof end;

theorem Th37: :: WAYBEL11:37

for b₁ being complete TopLattice st the topology of b₁ = sigma b₁ holds
b₁ is Scott

proof end;

Lemma43: for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is TopSpace-like holds
b₂ is TopSpace-like

proof end;

Lemma44: for b₁, b₂ being non empty 1-sorted st the carrier of b₁ = the carrier of b₂ holds
for b₃ being strict net of b₁ holds b₃ is strict net of b₂
;

Lemma45: for b₁, b₂ being non empty 1-sorted st the carrier of b₁ = the carrier of b₂ holds
NetUniv b₁ = NetUniv b₂

proof end;

Lemma46: for b₁, b₂ being non empty 1-sorted
for b₃ being set st the carrier of b₁ = the carrier of b₂ holds
for b₄ being net of b₁
for b₅ being net of b₂ st b₄ = b₅ & b₄ is_eventually_in b₃ holds
b₅ is_eventually_in b₃

proof end;

Lemma47: for b₁, b₂ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
for b₃ being net of b₁
for b₄ being net of b₂ st b₃ = b₄ holds
for b₅ being Point of b₁
for b₆ being Point of b₂ st b₅ = b₆ & b₅ in Lim b₃ holds
b₆ in Lim b₄

proof end;

Lemma48: for b₁, b₂ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) holds
Convergence b₁ = Convergence b₂

proof end;

Lemma49: for b₁, b₂ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is LATTICE holds
b₂ is LATTICE

proof end;

Lemma50: for b₁, b₂ being LATTICE
for b₃ being set st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₄ being Element of b₁
for b₅ being Element of b₂ st b₄ = b₅ & b₃ is_<=_than b₄ holds
b₃ is_<=_than b₅

proof end;

Lemma51: for b₁, b₂ being LATTICE
for b₃ being set st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₄ being Element of b₁
for b₅ being Element of b₂ st b₄ = b₅ & b₃ is_>=_than b₄ holds
b₃ is_>=_than b₅

proof end;

Lemma52: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set holds "\/" b₃,b₁ = "\/" b₃,b₂

proof end;

Lemma53: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being set holds "/\" b₃,b₁ = "/\" b₃,b₂

proof end;

Lemma54: for b₁, b₂ being non empty reflexive RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & b₃ is directed holds
b₄ is directed

proof end;

Lemma55: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃, b₄ being Element of b₁ st b₃ << b₄ holds
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ holds
b₅ << b₆

proof end;

Lemma56: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being net of b₁
for b₄ being net of b₂ st b₃ = b₄ holds
lim_inf b₃ = lim_inf b₄

proof end;

Lemma57: for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty set st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₄ being net of b₁
for b₅ being net of b₂ st b₄ = b₅ holds
for b₆ being net_set of the carrier of b₄,b₁
for b₇ being net_set of the carrier of b₅,b₂ st b₆ = b₇ holds
Iterated b₆ = Iterated b₇

proof end;

Lemma58: for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty set st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₄ being net of b₁
for b₅ being net of b₂ st b₄ = b₅ holds
for b₆ being net_set of the carrier of b₄,b₁ holds b₆ is net_set of the carrier of b₅,b₂

proof end;

Lemma59: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
Scott-Convergence b₁ c= Scott-Convergence b₂

proof end;

Lemma60: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
Scott-Convergence b₁ = Scott-Convergence b₂

proof end;

Lemma61: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
sigma b₁ = sigma b₂

proof end;

Lemma62: for b₁, b₂ being LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is complete holds
b₂ is complete

proof end;

Lemma63: for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is continuous holds
b₂ is continuous

proof end;

registration

let c₁ be continuous complete LATTICE;
cluster Scott-Convergence a₁ -> (CONSTANTS) (SUBNETS) topological ;
coherence

proof end;

end;

theorem Th38: :: WAYBEL11:38

for b₁ being continuous complete Scott TopLattice
for b₂ being Element of b₁
for b₃ being net of b₁ st b₃ in NetUniv b₁ holds
( b₂ is_S-limit_of b₃ iff b₂ in Lim b₃ )

proof end;

theorem Th39: :: WAYBEL11:39

for b₁ being non empty complete Poset st Scott-Convergence b₁ is (ITERATED_LIMITS) holds
b₁ is continuous

proof end;

theorem Th40: :: WAYBEL11:40

for b₁ being complete Scott TopLattice holds
( b₁ is continuous iff Convergence b₁ = Scott-Convergence b₁ )

proof end;

theorem Th41: :: WAYBEL11:41

for b₁ being complete Scott TopLattice
for b₂ being upper Subset of b₁ st b₂ is Open holds
b₂ is open

proof end;

theorem Th42: :: WAYBEL11:42

for b₁ being non empty RelStr
for b₂ being upper Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
uparrow b₃ c= b₂

proof end;

theorem Th43: :: WAYBEL11:43

for b₁ being continuous complete Scott TopLattice
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is open & b₂ in b₃ holds
ex b₄ being Element of b₁ st
( b₄ << b₂ & b₄ in b₃ )

proof end;

theorem Th44: :: WAYBEL11:44

for b₁ being continuous complete Scott TopLattice
for b₂ being Element of b₁ holds { (wayabove b₃) where B is Element of b₁ : b₃ << b₂ } is Basis of b₂

proof end;

theorem Th45: :: WAYBEL11:45

for b₁ being continuous complete Scott TopLattice holds { (wayabove b₂) where B is Element of b₁ : verum } is Basis of b₁

proof end;

theorem Th46: :: WAYBEL11:46

for b₁ being continuous complete Scott TopLattice
for b₂ being upper Subset of b₁ holds
( b₂ is open iff b₂ is Open )

proof end;

theorem Th47: :: WAYBEL11:47

for b₁ being continuous complete Scott TopLattice
for b₂ being Element of b₁ holds Int (uparrow b₂) = wayabove b₂

proof end;

theorem Th48: :: WAYBEL11:48

for b₁ being continuous complete Scott TopLattice
for b₂ being Subset of b₁ holds Int b₂ = union { (wayabove b₃) where B is Element of b₁ : wayabove b₃ c= b₂ }

proof end;