:: On The Topological Properties of Meet-Continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received December 20, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users


begin

registration
let L be non empty RelStr ;
cluster id L -> monotone ;
coherence
id L is monotone by YELLOW_2:13;
end;

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
redefine attr f is antitone means :Def1: :: WAYBEL_9:def 1
 for x, y being Element of S st x <= y holds
f . x >= f . y;
compatibility
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y )
proof end;
end;

:: deftheorem Def1 defines antitone WAYBEL_9:def 1 :
for S, T being non empty RelStr
for f being Function of S,T holds
( f is antitone iff for x, y being Element of S st x <= y holds
f . x >= f . y );

theorem Th1: :: WAYBEL_9:1
for S, T being RelStr
for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is monotone holds
g is monotone
proof end;

theorem Th2: :: WAYBEL_9:2
for S, T being RelStr
for K, L being non empty RelStr
for f being Function of S,T
for g being Function of K,L st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of K, the InternalRel of K #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & f = g & f is antitone holds
g is antitone
proof end;

theorem :: WAYBEL_9:3
for A, B being 1-sorted
for F being Subset-Family of A
for G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds
G is Cover of B ;

Lm1: for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }
proof end;

theorem Th4: :: WAYBEL_9:4
for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds uparrow x = {x} "\/" ([#] L)
proof end;

Lm2: for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }
proof end;

theorem Th5: :: WAYBEL_9:5
for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds downarrow x = {x} "/\" ([#] L)
proof end;

theorem :: WAYBEL_9:6
for L being reflexive antisymmetric with_infima RelStr
for y being Element of L holds (y "/\") .: (uparrow y) = {y}
proof end;

theorem Th7: :: WAYBEL_9:7
for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds (x "/\") " {x} = uparrow x
proof end;

theorem Th8: :: WAYBEL_9:8
for T being non empty 1-sorted
for N being non empty NetStr of T holds N is_eventually_in rng the mapping of N
proof end;

Lm3: for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is net of L
proof end;

registration
let L be non empty reflexive RelStr ;
let D be non empty directed Subset of L;
let n be Function of D, the carrier of L;
cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> directed ;
coherence
NetStr(# D,( the InternalRel of L |_2 D),n #) is directed by WAYBEL_2:19;
end;

registration
let L be non empty reflexive transitive RelStr ;
let D be non empty directed Subset of L;
let n be Function of D, the carrier of L;
cluster NetStr(# D,( the InternalRel of L |_2 D),n #) -> transitive ;
coherence
NetStr(# D,( the InternalRel of L |_2 D),n #) is transitive by Lm3;
end;

theorem Th9: :: WAYBEL_9:9
for L being non empty reflexive transitive RelStr st ( for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
L is satisfying_MC
proof end;

theorem Th10: :: WAYBEL_9:10
for L being non empty RelStr
for a being Element of L
for N being net of L holds a "/\" N is net of L
proof end;

registration
let L be non empty RelStr ;
let x be Element of L;
let N be net of L;
cluster x "/\" N -> transitive ;
coherence
x "/\" N is transitive by Th10;
end;

registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty reflexive NetStr of L;
cluster x "/\" N -> reflexive ;
coherence
x "/\" N is reflexive
proof end;
end;

registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty antisymmetric NetStr of L;
cluster x "/\" N -> antisymmetric ;
coherence
x "/\" N is antisymmetric
proof end;
end;

registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty transitive NetStr of L;
cluster x "/\" N -> transitive ;
coherence
x "/\" N is transitive
proof end;
end;

registration
let L be non empty RelStr ;
let J be set ;
let f be Function of J, the carrier of L;
cluster FinSups f -> transitive ;
coherence
FinSups f is transitive
proof end;
end;

begin

definition
let L be non empty RelStr ;
let N be NetStr of L;
func inf N -> Element of L equals :: WAYBEL_9:def 2
 Inf ;
coherence
Inf is Element of L ;
end;

:: deftheorem defines inf WAYBEL_9:def 2 :
for L being non empty RelStr
for N being NetStr of L holds inf N = Inf ;

definition
let L be RelStr ;
let N be NetStr of L;
pred ex_sup_of N means :Def3: :: WAYBEL_9:def 3
 ex_sup_of rng the mapping of N,L;
pred ex_inf_of N means :Def4: :: WAYBEL_9:def 4
 ex_inf_of rng the mapping of N,L;
end;

:: deftheorem Def3 defines ex_sup_of WAYBEL_9:def 3 :
for L being RelStr
for N being NetStr of L holds
( ex_sup_of N iff ex_sup_of rng the mapping of N,L );

:: deftheorem Def4 defines ex_inf_of WAYBEL_9:def 4 :
for L being RelStr
for N being NetStr of L holds
( ex_inf_of N iff ex_inf_of rng the mapping of N,L );

definition
let L be RelStr ;
func L +id -> strict NetStr of L means :Def5: :: WAYBEL_9:def 5
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of it = id L );
existence
ex b1 being strict NetStr of L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b1 = id L )
proof end;
uniqueness
for b1, b2 being strict NetStr of L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b1 = id L & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b2 = id L holds
b1 = b2 ;
end;

:: deftheorem Def5 defines +id WAYBEL_9:def 5 :
for L being RelStr
for b2 being strict NetStr of L holds
( b2 = L +id iff ( RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) & the mapping of b2 = id L ) );

registration
let L be non empty RelStr ;
cluster L +id -> non empty strict ;
coherence
not L +id is empty
proof end;
end;

registration
let L be reflexive RelStr ;
cluster L +id -> reflexive strict ;
coherence
L +id is reflexive
proof end;
end;

registration
let L be antisymmetric RelStr ;
cluster L +id -> antisymmetric strict ;
coherence
L +id is antisymmetric
proof end;
end;

registration
let L be transitive RelStr ;
cluster L +id -> transitive strict ;
coherence
L +id is transitive
proof end;
end;

registration
let L be with_suprema RelStr ;
cluster L +id -> strict directed ;
coherence
L +id is directed
proof end;
end;

registration
let L be directed RelStr ;
cluster L +id -> strict directed ;
coherence
L +id is directed
proof end;
end;

registration
let L be non empty RelStr ;
cluster L +id -> strict monotone eventually-directed ;
coherence
( L +id is monotone & L +id is eventually-directed )
proof end;
end;

definition
let L be RelStr ;
func L opp+id -> strict NetStr of L means :Def6: :: WAYBEL_9:def 6
( the carrier of it = the carrier of L & the InternalRel of it = the InternalRel of L ~ & the mapping of it = id L );
existence
ex b1 being strict NetStr of L st
( the carrier of b1 = the carrier of L & the InternalRel of b1 = the InternalRel of L ~ & the mapping of b1 = id L )
proof end;
uniqueness
for b1, b2 being strict NetStr of L st the carrier of b1 = the carrier of L & the InternalRel of b1 = the InternalRel of L ~ & the mapping of b1 = id L & the carrier of b2 = the carrier of L & the InternalRel of b2 = the InternalRel of L ~ & the mapping of b2 = id L holds
b1 = b2 ;
end;

:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :
for L being RelStr
for b2 being strict NetStr of L holds
( b2 = L opp+id iff ( the carrier of b2 = the carrier of L & the InternalRel of b2 = the InternalRel of L ~ & the mapping of b2 = id L ) );

theorem Th11: :: WAYBEL_9:11
for L being RelStr holds RelStr(# the carrier of (L ~), the InternalRel of (L ~) #) = RelStr(# the carrier of (L opp+id), the InternalRel of (L opp+id) #)
proof end;

registration
let L be non empty RelStr ;
cluster L opp+id -> non empty strict ;
coherence
not L opp+id is empty
proof end;
end;

registration
let L be reflexive RelStr ;
cluster L opp+id -> reflexive strict ;
coherence
L opp+id is reflexive
proof end;
end;

registration
let L be antisymmetric RelStr ;
cluster L opp+id -> antisymmetric strict ;
coherence
L opp+id is antisymmetric
proof end;
end;

registration
let L be transitive RelStr ;
cluster L opp+id -> transitive strict ;
coherence
L opp+id is transitive
proof end;
end;

registration
let L be with_infima RelStr ;
cluster L opp+id -> strict directed ;
coherence
L opp+id is directed
proof end;
end;

registration
let L be non empty RelStr ;
cluster L opp+id -> strict antitone eventually-filtered ;
coherence
( L opp+id is antitone & L opp+id is eventually-filtered )
proof end;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr of L;
let i be Element of N;
func N | i -> strict NetStr of L means :Def7: :: WAYBEL_9:def 7
( ( for x being set holds
( x in the carrier of it iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of it = the InternalRel of N |_2 the carrier of it & the mapping of it = the mapping of N | the carrier of it );
existence
ex b1 being strict NetStr of L st
( ( for x being set holds
( x in the carrier of b1 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 & the mapping of b1 = the mapping of N | the carrier of b1 )
proof end;
uniqueness
for b1, b2 being strict NetStr of L st ( for x being set holds
( x in the carrier of b1 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 & the mapping of b1 = the mapping of N | the carrier of b1 & ( for x being set holds
( x in the carrier of b2 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b2 = the InternalRel of N |_2 the carrier of b2 & the mapping of b2 = the mapping of N | the carrier of b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines | WAYBEL_9:def 7 :
for L being non empty 1-sorted
for N being non empty NetStr of L
for i being Element of N
for b4 being strict NetStr of L holds
( b4 = N | i iff ( ( for x being set holds
( x in the carrier of b4 iff ex y being Element of N st
( y = x & i <= y ) ) ) & the InternalRel of b4 = the InternalRel of N |_2 the carrier of b4 & the mapping of b4 = the mapping of N | the carrier of b4 ) );

theorem :: WAYBEL_9:12
for L being non empty 1-sorted
for N being non empty NetStr of L
for i being Element of N holds the carrier of (N | i) = { y where y is Element of N : i <= y }
proof end;

theorem Th13: :: WAYBEL_9:13
for L being non empty 1-sorted
for N being non empty NetStr of L
for i being Element of N holds the carrier of (N | i) c= the carrier of N
proof end;

theorem Th14: :: WAYBEL_9:14
for L being non empty 1-sorted
for N being non empty NetStr of L
for i being Element of N holds N | i is full SubNetStr of N
proof end;

registration
let L be non empty 1-sorted ;
let N be non empty reflexive NetStr of L;
let i be Element of N;
cluster N | i -> non empty reflexive strict ;
coherence
( not N | i is empty & N | i is reflexive )
proof end;
end;

registration
let L be non empty 1-sorted ;
let N be non empty directed NetStr of L;
let i be Element of N;
cluster N | i -> non empty strict ;
coherence
not N | i is empty
proof end;
end;

registration
let L be non empty 1-sorted ;
let N be non empty reflexive antisymmetric NetStr of L;
let i be Element of N;
cluster N | i -> antisymmetric strict ;
coherence
N | i is antisymmetric
proof end;
end;

registration
let L be non empty 1-sorted ;
let N be non empty antisymmetric directed NetStr of L;
let i be Element of N;
cluster N | i -> antisymmetric strict ;
coherence
N | i is antisymmetric
proof end;
end;

registration
let L be non empty 1-sorted ;
let N be non empty reflexive transitive NetStr of L;
let i be Element of N;
cluster N | i -> transitive strict ;
coherence
N | i is transitive
proof end;
end;

registration
let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
cluster N | i -> transitive strict directed ;
coherence
( N | i is transitive & N | i is directed )
proof end;
end;

theorem :: WAYBEL_9:15
for L being non empty 1-sorted
for N being non empty reflexive NetStr of L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
proof end;

theorem Th16: :: WAYBEL_9:16
for L being non empty 1-sorted
for N being non empty directed NetStr of L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1
proof end;

theorem Th17: :: WAYBEL_9:17
for L being non empty 1-sorted
for N being net of L
for i being Element of N holds N | i is subnet of N
proof end;

registration
let T be non empty 1-sorted ;
let N be net of T;
cluster non empty transitive strict directed subnet of N;
existence
ex b1 being subnet of N st b1 is strict
proof end;
end;

definition
let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
:: original: |
redefine func N | i -> strict subnet of N;
coherence
N | i is strict subnet of N by Th17;
end;

definition
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be NetStr of S;
func f * N -> strict NetStr of T means :Def8: :: WAYBEL_9:def 8
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = f * the mapping of N );
existence
ex b1 being strict NetStr of T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = f * the mapping of N )
proof end;
uniqueness
for b1, b2 being strict NetStr of T st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = f * the mapping of N & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = f * the mapping of N holds
b1 = b2 ;
end;

:: deftheorem Def8 defines * WAYBEL_9:def 8 :
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T
for N being NetStr of S
for b5 being strict NetStr of T holds
( b5 = f * N iff ( RelStr(# the carrier of b5, the InternalRel of b5 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b5 = f * the mapping of N ) );

registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be non empty NetStr of S;
cluster f * N -> non empty strict ;
coherence
not f * N is empty
proof end;
end;

registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be reflexive NetStr of S;
cluster f * N -> reflexive strict ;
coherence
f * N is reflexive
proof end;
end;

registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be antisymmetric NetStr of S;
cluster f * N -> antisymmetric strict ;
coherence
f * N is antisymmetric
proof end;
end;

registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be transitive NetStr of S;
cluster f * N -> transitive strict ;
coherence
f * N is transitive
proof end;
end;

registration
let S be non empty 1-sorted ;
let T be 1-sorted ;
let f be Function of S,T;
let N be directed NetStr of S;
cluster f * N -> strict directed ;
coherence
f * N is directed
proof end;
end;

theorem Th18: :: WAYBEL_9:18
for L being non empty RelStr
for N being non empty NetStr of L
for x being Element of L holds (x "/\") * N = x "/\" N
proof end;

begin

theorem :: WAYBEL_9:19
for S, T being TopStruct
for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is open holds
G is open
proof end;

theorem :: WAYBEL_9:20
for S, T being TopStruct
for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed
proof end;

definition
attr c1 is strict ;
struct TopRelStr -> TopStruct , RelStr ;
aggr TopRelStr(# carrier, InternalRel, topology #) -> TopRelStr ;
end;

registration
let A be non empty set ;
let R be Relation of A,A;
let T be Subset-Family of A;
cluster TopRelStr(# A,R,T #) -> non empty ;
coherence
not TopRelStr(# A,R,T #) is empty ;
end;

registration
let x be set ;
let R be Relation of {x};
let T be Subset-Family of {x};
cluster TopRelStr(# {x},R,T #) -> trivial ;
coherence
TopRelStr(# {x},R,T #) is trivial
proof end;
end;

registration
let X be set ;
let O be Order of X;
let T be Subset-Family of X;
cluster TopRelStr(# X,O,T #) -> reflexive transitive antisymmetric ;
coherence
( TopRelStr(# X,O,T #) is reflexive & TopRelStr(# X,O,T #) is transitive & TopRelStr(# X,O,T #) is antisymmetric )
proof end;
end;

Lm4: for tau being Subset-Family of {0}
for r being Relation of {0} st tau = {{},{0}} & r = {[0,0]} holds
( TopRelStr(# {0},r,tau #) is trivial & TopRelStr(# {0},r,tau #) is reflexive & not TopRelStr(# {0},r,tau #) is empty & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite )
proof end;

registration
cluster non empty trivial finite discrete reflexive strict TopRelStr ;
existence
ex b1 being TopRelStr st
( b1 is trivial & b1 is reflexive & not b1 is empty & b1 is discrete & b1 is strict & b1 is finite )
proof end;
end;

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

registration
cluster non empty trivial finite TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is strict & not b1 is empty & b1 is trivial & b1 is discrete & b1 is finite & b1 is compact & b1 is T_2 )
proof end;
end;

registration
let T be non empty Hausdorff TopSpace;
cluster non empty -> non empty Hausdorff SubSpace of T;
coherence
for b1 being non empty SubSpace of T holds b1 is T_2 ;
end;

theorem Th21: :: WAYBEL_9:21
for T being non empty TopSpace
for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p
proof end;

theorem Th22: :: WAYBEL_9:22
for T being non empty TopSpace
for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
proof end;

theorem :: WAYBEL_9:23
for T being non empty TopSpace
for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A \/ B is Element of (OpenNeighborhoods p)
proof end;

theorem Th24: :: WAYBEL_9:24
for T being non empty TopSpace
for p being Element of T
for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S
proof end;

theorem Th25: :: WAYBEL_9:25
for T being Hausdorff TopLattice
for N being convergent net of T
for f being Function of T,T st f is continuous holds
f . (lim N) in Lim (f * N)
proof end;

theorem Th26: :: WAYBEL_9:26
for T being Hausdorff TopLattice
for N being convergent net of T
for x being Element of T st x "/\" is continuous holds
x "/\" (lim N) in Lim (x "/\" N)
proof end;

theorem Th27: :: WAYBEL_9:27
for S being Hausdorff TopLattice
for x being Element of S st ( for a being Element of S holds a "/\" is continuous ) holds
uparrow x is closed
proof end;

theorem Th28: :: WAYBEL_9:28
for S being Hausdorff compact TopLattice
for x being Element of S st ( for b being Element of S holds b "/\" is continuous ) holds
downarrow x is closed
proof end;

begin

definition
let T be non empty TopSpace;
let N be non empty NetStr of T;
let p be Point of T;
pred p is_a_cluster_point_of N means :Def9: :: WAYBEL_9:def 9
 for O being a_neighborhood of p holds N is_often_in O;
end;

:: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def 9 :
for T being non empty TopSpace
for N being non empty NetStr of T
for p being Point of T holds
( p is_a_cluster_point_of N iff for O being a_neighborhood of p holds N is_often_in O );

theorem :: WAYBEL_9:29
for L being non empty TopSpace
for N being net of L
for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N
proof end;

theorem Th30: :: WAYBEL_9:30
for T being non empty Hausdorff compact TopSpace
for N being net of T ex c being Point of T st c is_a_cluster_point_of N
proof end;

theorem Th31: :: WAYBEL_9:31
for L being non empty TopSpace
for N being net of L
for M being subnet of N
for c being Point of L st c is_a_cluster_point_of M holds
c is_a_cluster_point_of N
proof end;

theorem Th32: :: WAYBEL_9:32
for T being non empty TopSpace
for N being net of T
for x being Point of T st x is_a_cluster_point_of N holds
ex M being subnet of N st x in Lim M
proof end;

theorem Th33: :: WAYBEL_9:33
for L being non empty Hausdorff compact TopSpace
for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) holds
for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N
proof end;

theorem Th34: :: WAYBEL_9:34
for S being non empty TopSpace
for c being Point of S
for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
proof end;

Lm5: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
proof end;

Lm6: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
proof end;

theorem Th35: :: WAYBEL_9:35
for S being Hausdorff compact TopLattice
for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
c = sup N
proof end;

Lm7: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
proof end;

Lm8: for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
proof end;

theorem Th36: :: WAYBEL_9:36
for S being Hausdorff compact TopLattice
for c being Point of S
for N being net of S st ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
c = inf N
proof end;

begin

theorem Th37: :: WAYBEL_9:37
for S being Hausdorff TopLattice st ( for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N ) ) & ( for x being Element of S holds x "/\" is continuous ) holds
S is meet-continuous
proof end;

theorem Th38: :: WAYBEL_9:38
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-directed holds
( ex_sup_of N & sup N in Lim N )
proof end;

theorem Th39: :: WAYBEL_9:39
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
for N being net of S st N is eventually-filtered holds
( ex_inf_of N & inf N in Lim N )
proof end;

theorem :: WAYBEL_9:40
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
S is bounded
proof end;

theorem :: WAYBEL_9:41
for S being Hausdorff compact TopLattice st ( for x being Element of S holds x "/\" is continuous ) holds
S is meet-continuous
proof end;