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


begin

::-------------------------------------------------------------------
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor A. Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------
registration
let L be non empty RelStr ;
cluster id L ->  monotone ;
coherence
 id L is monotone by YELLOW_2:11;
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 )
proofend;
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 #) &amp; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) &amp; f = g &amp; f is monotone holds
g is monotone
proofend;

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 #) &amp; RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) &amp; f = g &amp; f is antitone holds
g is antitone
proofend;

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 &amp; F = G &amp; 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  }
proofend;

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

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

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

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

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

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

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

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;

:: cf WAYBEL_2:42
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
proofend;

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

registration
let L be non empty RelStr ;
let x be Element of L;
let N be net of L;
clusterx "/\" 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 over L;
clusterx "/\" N ->  reflexive ;
coherence
 x "/\" N is reflexive
proofend;
end;

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

registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty transitive NetStr over L;
clusterx "/\" N ->  transitive ;
coherence
 x "/\" N is transitive
proofend;
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
proofend;
end;

begin

definition
let L be non empty RelStr ;
let N be NetStr over 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 over L holds inf N = Inf ;

definition
let L be RelStr ;
let N be NetStr over 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 over 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 over L holds
( ex_inf_of N iff ex_inf_of rng the mapping of N,L );

definition
let L be RelStr ;
funcL +id  ->  strict NetStr over 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 #) &amp; the mapping of it = id L );
existence
 ex b1 being strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) &amp; the mapping of b1 = id L )
proofend;
uniqueness
 for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of L, the InternalRel of L #) &amp; the mapping of b1 = id L &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) &amp; 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 over L holds
( b2 = L +id iff ( RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of L, the InternalRel of L #) &amp; the mapping of b2 = id L ) );

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

registration
let L be reflexive RelStr ;
clusterL +id  ->  reflexive strict ;
coherence
 L +id is reflexive
proofend;
end;

registration
let L be antisymmetric RelStr ;
clusterL +id  ->  antisymmetric strict ;
coherence
 L +id is antisymmetric
proofend;
end;

registration
let L be transitive RelStr ;
clusterL +id  ->  transitive strict ;
coherence
 L +id is transitive
proofend;
end;

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

registration
let L be directed RelStr ;
clusterL +id  ->  strict directed ;
coherence
 L +id is directed
proofend;
end;

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

definition
let L be RelStr ;
funcL opp+id  ->  strict NetStr over L means :Def6: :: WAYBEL_9:def 6
( the carrier of it = the carrier of L &amp; the InternalRel of it = the InternalRel of L ~ &amp; the mapping of it = id L );
existence
 ex b1 being strict NetStr over L st
( the carrier of b1 = the carrier of L &amp; the InternalRel of b1 = the InternalRel of L ~ &amp; the mapping of b1 = id L )
proofend;
uniqueness
 for b1, b2 being strict NetStr over L st the carrier of b1 = the carrier of L &amp; the InternalRel of b1 = the InternalRel of L ~ &amp; the mapping of b1 = id L &amp; the carrier of b2 = the carrier of L &amp; the InternalRel of b2 = the InternalRel of L ~ &amp; 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 over L holds
( b2 = L opp+id iff ( the carrier of b2 = the carrier of L &amp; the InternalRel of b2 = the InternalRel of L ~ &amp; 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) #)
proofend;

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

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

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

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

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

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

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let i be Element of N;
funcN | i ->  strict NetStr over 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 &amp; i <= y ) ) ) &amp; the InternalRel of it = the InternalRel of N |_2 the carrier of it &amp; the mapping of it = the mapping of N | the carrier of it );
existence
 ex b1 being strict NetStr over L st
( ( for x being set holds
( x in the carrier of b1 iff ex y being Element of N st
( y = x &amp; i <= y ) ) ) &amp; the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 &amp; the mapping of b1 = the mapping of N | the carrier of b1 )
proofend;
uniqueness
 for b1, b2 being strict NetStr over L st ( for x being set holds
( x in the carrier of b1 iff ex y being Element of N st
( y = x &amp; i <= y ) ) ) &amp; the InternalRel of b1 = the InternalRel of N |_2 the carrier of b1 &amp; the mapping of b1 = the mapping of N | the carrier of b1 &amp; ( for x being set holds
( x in the carrier of b2 iff ex y being Element of N st
( y = x &amp; i <= y ) ) ) &amp; the InternalRel of b2 = the InternalRel of N |_2 the carrier of b2 &amp; the mapping of b2 = the mapping of N | the carrier of b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines | WAYBEL_9:def_7_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N
for b4 being strict NetStr over 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 &amp; i <= y ) ) ) &amp; the InternalRel of b4 = the InternalRel of N |_2 the carrier of b4 &amp; 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 over L
for i being Element of N holds the carrier of (N | i) =  {  y where y is Element of N : i <= y  }
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

definition
let L be non empty 1-sorted ;
let N be net of L;
let i be Element of N;
:: original:|
redefine funcN | 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 over S;
funcf * N ->  strict NetStr over 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 #) &amp; the mapping of it = f * the mapping of N );
existence
 ex b1 being strict NetStr over T st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of b1 = f * the mapping of N )
proofend;
uniqueness
 for b1, b2 being strict NetStr over T st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of b1 = f * the mapping of N &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; 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 over S
for b5 being strict NetStr over T holds
( b5 = f * N iff ( RelStr(# the carrier of b5, the InternalRel of b5 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; 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 over S;
clusterf * N ->  non empty strict ;
coherence
 not f * N is empty
proofend;
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 over S;
clusterf * N ->  reflexive strict ;
coherence
 f * N is reflexive
proofend;
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 over S;
clusterf * N ->  antisymmetric strict ;
coherence
 f * N is antisymmetric
proofend;
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 over S;
clusterf * N ->  transitive strict ;
coherence
 f * N is transitive
proofend;
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 over S;
clusterf * N ->  strict directed ;
coherence
 f * N is directed
proofend;
end;

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

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 #) &amp; F = G &amp; F is open holds
G is open
proofend;

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 #) &amp; F = G &amp; F is closed holds
G is closed
proofend;

definition
attrc1 is strict ;
struct TopRelStr  ->  TopStruct , RelStr ;
aggrTopRelStr(# 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 #) -> 1 -element ;
coherence
 TopRelStr(# {x},R,T #) is 1 -element
proofend;
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 &amp; TopRelStr(# X,O,T #) is transitive &amp; TopRelStr(# X,O,T #) is antisymmetric )
proofend;
end;

Lm4:  for tau being Subset-Family of {0}
for r being Relation of {0} st tau = {{},{0}} &amp; r = {[0,0]} holds
( TopRelStr(# {0},r,tau #) is reflexive &amp; TopRelStr(# {0},r,tau #) is discrete &amp; TopRelStr(# {0},r,tau #) is finite &amp; TopRelStr(# {0},r,tau #) is 1 -element )
proofend;

registration
cluster finite 1 -element discrete reflexive strict for TopRelStr ;
existence
 ex b1 being TopRelStr st
( b1 is reflexive &amp; b1 is discrete &amp; b1 is strict &amp; b1 is finite &amp; b1 is 1 -element )
proofend;
end;

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

registration
cluster non empty finite 1 -element TopSpace-like Hausdorff discrete reflexive transitive antisymmetric with_suprema with_infima compact strict for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is strict &amp; b1 is discrete &amp; b1 is finite &amp; b1 is compact &amp; b1 is Hausdorff &amp; b1 is 1 -element )
proofend;
end;

registration
let T be non empty Hausdorff TopSpace;
cluster non empty  ->  non empty Hausdorff for SubSpace of T;
coherence
 for b1 being non empty SubSpace of T holds b1 is Hausdorff ;
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
proofend;

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

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

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

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

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

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

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

begin

definition
let T be non empty TopSpace;
let N be non empty NetStr over T;
let p be Point of T;
predp 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 over 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
proofend;

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

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

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

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

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 &amp; A is closed &amp; rng the mapping of N c= A holds
c in A
proofend;

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 &amp; ( for x being Element of S holds x "/\" is continuous ) &amp; N is eventually-directed &amp; c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
proofend;

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 &amp; ( for x being Element of S holds x "/\" is continuous ) &amp; 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
proofend;

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 ) &amp; N is eventually-directed &amp; c is_a_cluster_point_of N holds
c = sup N
proofend;

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 &amp; ( for x being Element of S holds x "/\" is continuous ) &amp; N is eventually-filtered &amp; c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
proofend;

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 &amp; ( for x being Element of S holds x "/\" is continuous ) &amp; 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
proofend;

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 ) &amp; N is eventually-filtered &amp; c is_a_cluster_point_of N holds
c = inf N
proofend;

begin

:: Proposition 4.4 s. 32 (i) &amp; (ii) => MC
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 &amp; sup N in Lim N ) ) &amp; ( for x being Element of S holds x "/\" is continuous ) holds
S is meet-continuous
proofend;

:: Proposition 4.4 s. 32 (ii) => (i)
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 &amp; sup N in Lim N )
proofend;

:: Proposition 4.4 s. 32 (ii) => (i) dual
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 &amp; inf N in Lim N )
proofend;

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

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