:: WAYBEL_9 semantic presentation

registration

let c₁ be non empty RelStr ;
cluster id a₁ -> monotone ;
coherence by YELLOW_2:13;

end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
redefine attr a₃ is antitone means :Def1: :: WAYBEL_9:def 1
for b₁, b₂ being Element of a₁ st b₁ <= b₂ holds
a₃ . b₁ >= a₃ . b₂;
compatibility

proof end;

end;

:: deftheorem Def1 defines antitone WAYBEL_9:def 1 :

theorem Th1: :: WAYBEL_9:1

for b₁, b₂ being RelStr
for b₃, b₄ being non empty RelStr
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) & RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & b₅ = b₆ & b₅ is monotone holds
b₆ is monotone

proof end;

theorem Th2: :: WAYBEL_9:2

proof end;

theorem Th3: :: WAYBEL_9:3

for b₁, b₂ being 1-sorted
for b₃ being Subset-Family of b₁
for b₄ being Subset-Family of b₂ st the carrier of b₁ = the carrier of b₂ & b₃ = b₄ & b₃ is_a_cover_of b₁ holds
b₄ is_a_cover_of b₂

proof end;

Lemma5: for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Element of b₁ holds uparrow b₂ = { b₃ where B is Element of b₁ : b₃ "/\" b₂ = b₂ }

proof end;

theorem Th4: :: WAYBEL_9:4

for b₁ being reflexive antisymmetric with_suprema RelStr
for b₂ being Element of b₁ holds uparrow b₂ = {b₂} "\/" ([#] b₁)

proof end;

Lemma7: for b₁ being reflexive antisymmetric with_suprema RelStr
for b₂ being Element of b₁ holds downarrow b₂ = { b₃ where B is Element of b₁ : b₃ "\/" b₂ = b₂ }

proof end;

theorem Th5: :: WAYBEL_9:5

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Element of b₁ holds downarrow b₂ = {b₂} "/\" ([#] b₁)

proof end;

theorem Th6: :: WAYBEL_9:6

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Element of b₁ holds (b₂ "/\" ) .: (uparrow b₂) = {b₂}

proof end;

theorem Th7: :: WAYBEL_9:7

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Element of b₁ holds (b₂ "/\" ) " {b₂} = uparrow b₂

proof end;

theorem Th8: :: WAYBEL_9:8

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁ holds b₂ is_eventually_in rng the mapping of b₂

proof end;

Lemma11: for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty directed Subset of b₁
for b₃ being Function of b₂,the carrier of b₁ holds NetStr(# b₂,(the InternalRel of b₁ |_2 b₂),b₃ #) is net of b₁

proof end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty directed Subset of c₁;
let c₃ be Function of c₂,the carrier of c₁;
cluster NetStr(# a₂,(the InternalRel of a₁ |_2 a₂),a₃ #) -> directed ;
coherence by WAYBEL_2:19;

end;

registration

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be non empty directed Subset of c₁;
let c₃ be Function of c₂,the carrier of c₁;
cluster NetStr(# a₂,(the InternalRel of a₁ |_2 a₂),a₃ #) -> transitive directed ;
coherence by Lemma11;

end;

theorem Th9: :: WAYBEL_9:9

for b₁ being non empty reflexive transitive RelStr st ( for b₂ being Element of b₁
for b₃ being net of b₁ st b₃ is eventually-directed holds
b₂ "/\" (sup b₃) = sup ({b₂} "/\" (rng (netmap b₃,b₁))) ) holds
b₁ is satisfying_MC

proof end;

theorem Th10: :: WAYBEL_9:10

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being net of b₁ holds b₂ "/\" b₃ is net of b₁

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be net of c₁;
redefine func "/\" as c₂ "/\" c₃ -> strict net of a₁;
coherence by Th10;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be non empty reflexive NetStr of c₁;
cluster a₂ "/\" a₃ -> reflexive ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be non empty antisymmetric NetStr of c₁;
cluster a₂ "/\" a₃ -> antisymmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be non empty transitive NetStr of c₁;
cluster a₂ "/\" a₃ -> transitive ;
coherence

proof end;

end;

registration

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

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be NetStr of c₁;
func inf c₂ -> Element of a₁ equals :: WAYBEL_9:def 2
Inf ;
coherence ;

end;

:: deftheorem Def2 defines inf WAYBEL_9:def 2 :

definition

let c₁ be RelStr ;
let c₂ be NetStr of c₁;
pred ex_sup_of c₂ means :Def3: :: WAYBEL_9:def 3
ex_sup_of rng the mapping of a₂,a₁;
pred ex_inf_of c₂ means :Def4: :: WAYBEL_9:def 4
ex_inf_of rng the mapping of a₂,a₁;

end;

:: deftheorem Def3 defines ex_sup_of WAYBEL_9:def 3 :

:: deftheorem Def4 defines ex_inf_of WAYBEL_9:def 4 :

definition

let c₁ be RelStr ;
func c₁ +id -> strict NetStr of a₁ means :Def5: :: WAYBEL_9:def 5
( RelStr(# the carrier of a₂,the InternalRel of a₂ #) = RelStr(# the carrier of a₁,the InternalRel of a₁ #) & the mapping of a₂ = id a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines +id WAYBEL_9:def 5 :

registration

let c₁ be non empty RelStr ;
cluster a₁ +id -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be reflexive RelStr ;
cluster a₁ +id -> reflexive strict ;
coherence

proof end;

end;

registration

let c₁ be antisymmetric RelStr ;
cluster a₁ +id -> antisymmetric strict ;
coherence

proof end;

end;

registration

let c₁ be transitive RelStr ;
cluster a₁ +id -> transitive strict ;
coherence

proof end;

end;

registration

let c₁ be with_suprema RelStr ;
cluster a₁ +id -> non empty strict directed ;
coherence

proof end;

end;

registration

let c₁ be directed RelStr ;
cluster a₁ +id -> strict directed ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster a₁ +id -> non empty strict monotone eventually-directed ;
coherence

proof end;

end;

definition

let c₁ be RelStr ;
func c₁ opp+id -> strict NetStr of a₁ means :Def6: :: WAYBEL_9:def 6
( the carrier of a₂ = the carrier of a₁ & the InternalRel of a₂ = the InternalRel of a₁ ~ & the mapping of a₂ = id a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :

theorem Th11: :: WAYBEL_9:11

for b₁ being RelStr holds RelStr(# the carrier of (b₁ ~ ),the InternalRel of (b₁ ~ ) #) = RelStr(# the carrier of (b₁ opp+id ),the InternalRel of (b₁ opp+id ) #)

proof end;

registration

let c₁ be non empty RelStr ;
cluster a₁ opp+id -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be reflexive RelStr ;
cluster a₁ opp+id -> reflexive strict ;
coherence

proof end;

end;

registration

let c₁ be antisymmetric RelStr ;
cluster a₁ opp+id -> antisymmetric strict ;
coherence

proof end;

end;

registration

let c₁ be transitive RelStr ;
cluster a₁ opp+id -> transitive strict ;
coherence

proof end;

end;

registration

let c₁ be with_infima RelStr ;
cluster a₁ opp+id -> non empty strict directed ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster a₁ opp+id -> non empty strict antitone eventually-filtered ;
coherence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
let c₃ be Element of c₂;
func c₂ | c₃ -> strict NetStr of a₁ means :Def7: :: WAYBEL_9:def 7
( ( for b₁ being set holds
( b₁ in the carrier of a₄ iff ex b₂ being Element of a₂ st
( b₂ = b₁ & a₃ <= b₂ ) ) ) & the InternalRel of a₄ = the InternalRel of a₂ |_2 the carrier of a₄ & the mapping of a₄ = the mapping of a₂ | the carrier of a₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines | WAYBEL_9:def 7 :

theorem Th12: :: WAYBEL_9:12

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₂ holds the carrier of (b₂ | b₃) = { b₄ where B is Element of b₂ : b₃ <= b₄ }

proof end;

theorem Th13: :: WAYBEL_9:13

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₂ holds the carrier of (b₂ | b₃) c= the carrier of b₂

proof end;

theorem Th14: :: WAYBEL_9:14

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₂ holds b₂ | b₃ is full SubNetStr of b₂

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty reflexive NetStr of c₁;
let c₃ be Element of c₂;
cluster a₂ | a₃ -> non empty reflexive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty directed NetStr of c₁;
let c₃ be Element of c₂;
cluster a₂ | a₃ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty reflexive antisymmetric NetStr of c₁;
let c₃ be Element of c₂;
cluster a₂ | a₃ -> non empty reflexive antisymmetric strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty antisymmetric directed NetStr of c₁;
let c₃ be Element of c₂;
cluster a₂ | a₃ -> non empty antisymmetric strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty reflexive transitive NetStr of c₁;
let c₃ be Element of c₂;
cluster a₂ | a₃ -> non empty reflexive transitive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
let c₃ be Element of c₂;
cluster a₂ | a₃ -> non empty transitive strict directed ;
coherence

proof end;

end;

theorem Th15: :: WAYBEL_9:15

for b₁ being non empty 1-sorted
for b₂ being non empty reflexive NetStr of b₁
for b₃, b₄ being Element of b₂
for b₅ being Element of (b₂ | b₃) st b₄ = b₅ holds
b₂ . b₄ = (b₂ | b₃) . b₅

proof end;

theorem Th16: :: WAYBEL_9:16

for b₁ being non empty 1-sorted
for b₂ being non empty directed NetStr of b₁
for b₃, b₄ being Element of b₂
for b₅ being Element of (b₂ | b₃) st b₄ = b₅ holds
b₂ . b₄ = (b₂ | b₃) . b₅

proof end;

theorem Th17: :: WAYBEL_9:17

for b₁ being non empty 1-sorted
for b₂ being net of b₁
for b₃ being Element of b₂ holds b₂ | b₃ is subnet of b₂

proof end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
cluster strict subnet of a₂;
existence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be net of c₁;
let c₃ be Element of c₂;
redefine func | as c₂ | c₃ -> strict subnet of a₂;
coherence by Th17;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be NetStr of c₁;
func c₃ * c₄ -> strict NetStr of a₂ means :Def8: :: WAYBEL_9:def 8
( RelStr(# the carrier of a₅,the InternalRel of a₅ #) = RelStr(# the carrier of a₄,the InternalRel of a₄ #) & the mapping of a₅ = a₃ * the mapping of a₄ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines * WAYBEL_9:def 8 :

registration

let c₁ be non empty 1-sorted ;
let c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be non empty NetStr of c₁;
cluster a₃ * a₄ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be reflexive NetStr of c₁;
cluster a₃ * a₄ -> reflexive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be antisymmetric NetStr of c₁;
cluster a₃ * a₄ -> antisymmetric strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be transitive NetStr of c₁;
cluster a₃ * a₄ -> transitive strict ;
coherence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
let c₄ be directed NetStr of c₁;
cluster a₃ * a₄ -> strict directed ;
coherence

proof end;

end;

theorem Th18: :: WAYBEL_9:18

for b₁ being non empty RelStr
for b₂ being non empty NetStr of b₁
for b₃ being Element of b₁ holds (b₃ "/\" ) * b₂ = b₃ "/\" b₂

proof end;

theorem Th19: :: WAYBEL_9:19

for b₁, b₂ being TopStruct
for b₃ being Subset-Family of b₁
for b₄ being Subset-Family of b₂ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ & b₃ is open holds
b₄ is open

proof end;

theorem Th20: :: WAYBEL_9:20

proof end;

definition

attr a₁ is strict;
struct TopRelStr -> TopStruct , RelStr ;
aggr TopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;

end;

registration

let c₁ be non empty set ;
let c₂ be Relation of c₁,c₁;
let c₃ be Subset-Family of c₁;
cluster TopRelStr(# a₁,a₂,a₃ #) -> non empty ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Relation of {c₁};
let c₃ be Subset-Family of {c₁};
cluster TopRelStr(# {a₁},a₂,a₃ #) -> non empty trivial ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Order of c₁;
let c₃ be Subset-Family of c₁;
cluster TopRelStr(# a₁,a₂,a₃ #) -> reflexive transitive antisymmetric ;
coherence

proof end;

end;

Lemma27: for b₁ being Subset-Family of {0}
for b₂ being Relation of {0} st b₁ = {{} ,{0}} & b₂ = {[0,0]} holds
( TopRelStr(# {0},b₂,b₁ #) is trivial & TopRelStr(# {0},b₂,b₁ #) is reflexive & not TopRelStr(# {0},b₂,b₁ #) is empty & TopRelStr(# {0},b₂,b₁ #) is discrete & TopRelStr(# {0},b₂,b₁ #) is finite )

proof end;

registration

cluster non empty reflexive discrete finite trivial strict TopRelStr ;
existence

proof end;

end;

definition

mode TopLattice is TopSpace-like reflexive transitive antisymmetric with_suprema with_infima TopRelStr ;

end;

registration

cluster non empty compact Hausdorff discrete finite trivial strict TopRelStr ;
existence

proof end;

end;

registration

let c₁ be non empty Hausdorff TopSpace;
cluster non empty -> non empty Hausdorff SubSpace of a₁;
coherence by TOPMETR:3;

end;

theorem Th21: :: WAYBEL_9:21

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Element of (OpenNeighborhoods b₂) holds b₃ is a_neighborhood of b₂

proof end;

theorem Th22: :: WAYBEL_9:22

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃, b₄ being Element of (OpenNeighborhoods b₂) holds b₃ /\ b₄ is Element of (OpenNeighborhoods b₂)

proof end;

theorem Th23: :: WAYBEL_9:23

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃, b₄ being Element of (OpenNeighborhoods b₂) holds b₃ \/ b₄ is Element of (OpenNeighborhoods b₂)

proof end;

theorem Th24: :: WAYBEL_9:24

for b₁ being non empty TopSpace
for b₂ being Element of b₁
for b₃ being net of b₁ st b₂ in Lim b₃ holds
for b₄ being Subset of b₁ st b₄ = rng the mapping of b₃ holds
b₂ in Cl b₄

proof end;

theorem Th25: :: WAYBEL_9:25

for b₁ being Hausdorff TopLattice
for b₂ being convergent net of b₁
for b₃ being Function of b₁,b₁ st b₃ is continuous holds
b₃ . (lim b₂) in Lim (b₃ * b₂)

proof end;

theorem Th26: :: WAYBEL_9:26

for b₁ being Hausdorff TopLattice
for b₂ being convergent net of b₁
for b₃ being Element of b₁ st b₃ "/\" is continuous holds
b₃ "/\" (lim b₂) in Lim (b₃ "/\" b₂)

proof end;

theorem Th27: :: WAYBEL_9:27

for b₁ being Hausdorff TopLattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ "/\" is continuous ) holds
uparrow b₂ is closed

proof end;

theorem Th28: :: WAYBEL_9:28

for b₁ being compact Hausdorff TopLattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ "/\" is continuous ) holds
downarrow b₂ is closed

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty NetStr of c₁;
let c₃ be Point of c₁;
pred c₃ is_a_cluster_point_of c₂ means :Def9: :: WAYBEL_9:def 9
for b₁ being a_neighborhood of a₃ holds a₂ is_often_in b₁;

end;

:: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def 9 :

theorem Th29: :: WAYBEL_9:29

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ st b₃ in Lim b₂ holds
b₃ is_a_cluster_point_of b₂

proof end;

theorem Th30: :: WAYBEL_9:30

for b₁ being non empty compact Hausdorff TopSpace
for b₂ being net of b₁ ex b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂

proof end;

theorem Th31: :: WAYBEL_9:31

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being subnet of b₂
for b₄ being Point of b₁ st b₄ is_a_cluster_point_of b₃ holds
b₄ is_a_cluster_point_of b₂

proof end;

theorem Th32: :: WAYBEL_9:32

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ holds
ex b₄ being subnet of b₂ st b₃ in Lim b₄

proof end;

theorem Th33: :: WAYBEL_9:33

for b₁ being non empty compact Hausdorff TopSpace
for b₂ being net of b₁ st ( for b₃, b₄ being Point of b₁ st b₃ is_a_cluster_point_of b₂ & b₄ is_a_cluster_point_of b₂ holds
b₃ = b₄ ) holds
for b₃ being Point of b₁ st b₃ is_a_cluster_point_of b₂ holds
b₃ in Lim b₂

proof end;

theorem Th34: :: WAYBEL_9:34

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being net of b₁
for b₄ being Subset of b₁ st b₂ is_a_cluster_point_of b₃ & b₄ is closed & rng the mapping of b₃ c= b₄ holds
b₂ in b₄

proof end;

Lemma41: for b₁ being compact Hausdorff TopLattice
for b₂ being net of b₁
for b₃ being Point of b₁
for b₄ being Element of b₁ st b₃ = b₄ & ( for b₅ being Element of b₁ holds b₅ "/\" is continuous ) & b₂ is eventually-directed & b₃ is_a_cluster_point_of b₂ holds
b₄ is_>=_than rng the mapping of b₂

proof end;

Lemma42: for b₁ being compact Hausdorff TopLattice
for b₂ being net of b₁
for b₃ being Point of b₁
for b₄ being Element of b₁ st b₃ = b₄ & ( for b₅ being Element of b₁ holds b₅ "/\" is continuous ) & b₃ is_a_cluster_point_of b₂ holds
for b₅ being Element of b₁ st rng the mapping of b₂ is_<=_than b₅ holds
b₄ <= b₅

proof end;

theorem Th35: :: WAYBEL_9:35

for b₁ being compact Hausdorff TopLattice
for b₂ being Point of b₁
for b₃ being net of b₁ st ( for b₄ being Element of b₁ holds b₄ "/\" is continuous ) & b₃ is eventually-directed & b₂ is_a_cluster_point_of b₃ holds
b₂ = sup b₃

proof end;

Lemma44: for b₁ being compact Hausdorff TopLattice
for b₂ being net of b₁
for b₃ being Point of b₁
for b₄ being Element of b₁ st b₃ = b₄ & ( for b₅ being Element of b₁ holds b₅ "/\" is continuous ) & b₂ is eventually-filtered & b₃ is_a_cluster_point_of b₂ holds
b₄ is_<=_than rng the mapping of b₂

proof end;

Lemma45: for b₁ being compact Hausdorff TopLattice
for b₂ being net of b₁
for b₃ being Point of b₁
for b₄ being Element of b₁ st b₃ = b₄ & ( for b₅ being Element of b₁ holds b₅ "/\" is continuous ) & b₃ is_a_cluster_point_of b₂ holds
for b₅ being Element of b₁ st rng the mapping of b₂ is_>=_than b₅ holds
b₄ >= b₅

proof end;

theorem Th36: :: WAYBEL_9:36

for b₁ being compact Hausdorff TopLattice
for b₂ being Point of b₁
for b₃ being net of b₁ st ( for b₄ being Element of b₁ holds b₄ "/\" is continuous ) & b₃ is eventually-filtered & b₂ is_a_cluster_point_of b₃ holds
b₂ = inf b₃

proof end;

theorem Th37: :: WAYBEL_9:37

for b₁ being Hausdorff TopLattice st ( for b₂ being net of b₁ st b₂ is eventually-directed holds
( ex_sup_of b₂ & sup b₂ in Lim b₂ ) ) & ( for b₂ being Element of b₁ holds b₂ "/\" is continuous ) holds
b₁ is meet-continuous

proof end;

theorem Th38: :: WAYBEL_9:38

for b₁ being compact Hausdorff TopLattice st ( for b₂ being Element of b₁ holds b₂ "/\" is continuous ) holds
for b₂ being net of b₁ st b₂ is eventually-directed holds
( ex_sup_of b₂ & sup b₂ in Lim b₂ )

proof end;

theorem Th39: :: WAYBEL_9:39

for b₁ being compact Hausdorff TopLattice st ( for b₂ being Element of b₁ holds b₂ "/\" is continuous ) holds
for b₂ being net of b₁ st b₂ is eventually-filtered holds
( ex_inf_of b₂ & inf b₂ in Lim b₂ )

proof end;

theorem Th40: :: WAYBEL_9:40

for b₁ being compact Hausdorff TopLattice st ( for b₂ being Element of b₁ holds b₂ "/\" is continuous ) holds
b₁ is bounded

proof end;

theorem Th41: :: WAYBEL_9:41

for b₁ being compact Hausdorff TopLattice st ( for b₂ being Element of b₁ holds b₂ "/\" is continuous ) holds
b₁ is meet-continuous

proof end;