:: On the {K}uratowski Limit Operators
:: by Adam Grabowski
::
:: Received August 12, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users

begin

theorem :: KURATO_2:1

canceled;

theorem :: KURATO_2:2

for F being Function
for i being set st i in dom F holds
meet F c= F . i

proof end;

theorem :: KURATO_2:3

canceled;

theorem Th4: :: KURATO_2:4

for A, B, C, D being set st A meets B & C meets D holds
[:A,C:] meets [:B,D:]

proof end;

registration

let X be set ;
cluster Function-like V30( NAT , bool X) -> non empty Element of bool [:NAT,(bool X):];
coherence
for b₁ being SetSequence of X holds not b₁ is empty ;

end;

registration

let T be non empty set ;
cluster non empty Relation-like non-empty Function-like V29( NAT ) V30( NAT , bool T) Element of bool [:NAT,(bool T):];
existence
ex b₁ being SetSequence of T st b₁ is non-empty

proof end;

end;

definition

let T be 1-sorted ;
mode SetSequence of T is SetSequence of the carrier of T;

end;

definition

let X be set ;
let F be SetSequence of X;
:: original: Union
redefine func Union F -> Subset of X;
coherence
Union F is Subset of X

proof end;

:: original: meet
redefine func meet F -> Subset of X;
coherence
meet F is Subset of X

proof end;

end;

begin

definition

let X be set ;
let F be SetSequence of X;
canceled;
canceled;
func lim_inf F -> Subset of X means :Def3: :: KURATO_2:def 3
ex f being SetSequence of X st
( it = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) );
existence
ex b₁ being Subset of X ex f being SetSequence of X st
( b₁ = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ex f being SetSequence of X st
( b₁ = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( b₂ = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) holds
b₁ = b₂

proof end;

func lim_sup F -> Subset of X means :Def4: :: KURATO_2:def 4
ex f being SetSequence of X st
( it = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) );
existence
ex b₁ being Subset of X ex f being SetSequence of X st
( b₁ = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ex f being SetSequence of X st
( b₁ = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( b₂ = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem KURATO_2:def 1 :
canceled;

:: deftheorem KURATO_2:def 2 :
canceled;

:: deftheorem Def3 defines lim_inf KURATO_2:def 3 :
for X being set
for F being SetSequence of X
for b₃ being Subset of X holds
( b₃ = lim_inf F iff ex f being SetSequence of X st
( b₃ = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) );

:: deftheorem Def4 defines lim_sup KURATO_2:def 4 :
for X being set
for F being SetSequence of X
for b₃ being Subset of X holds
( b₃ = lim_sup F iff ex f being SetSequence of X st
( b₃ = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) );

theorem :: KURATO_2:5

canceled;

theorem Th6: :: KURATO_2:6

for X being set
for F being SetSequence of X
for x being set holds
( x in meet F iff for z being Element of NAT holds x in F . z )

proof end;

theorem Th7: :: KURATO_2:7

for X being set
for F being SetSequence of X
for x being set holds
( x in lim_inf F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) )

proof end;

theorem Th8: :: KURATO_2:8

for X being set
for F being SetSequence of X
for x being set holds
( x in lim_sup F iff for n being Element of NAT ex k being Element of NAT st x in F . (n + k) )

proof end;

theorem :: KURATO_2:9

for X being set
for F being SetSequence of X holds lim_inf F c= lim_sup F

proof end;

theorem Th10: :: KURATO_2:10

for X being set
for F being SetSequence of X holds meet F c= lim_inf F

proof end;

theorem Th11: :: KURATO_2:11

for X being set
for F being SetSequence of X holds lim_sup F c= Union F

proof end;

theorem :: KURATO_2:12

for X being set
for F being SetSequence of X holds lim_inf F = (lim_sup (Complement F)) `

proof end;

theorem :: KURATO_2:13

for X being set
for A, B, C being SetSequence of X st ( for n being Element of NAT holds C . n = (A . n) /\ (B . n) ) holds
lim_inf C = (lim_inf A) /\ (lim_inf B)

proof end;

theorem :: KURATO_2:14

for X being set
for A, B, C being SetSequence of X st ( for n being Element of NAT holds C . n = (A . n) \/ (B . n) ) holds
lim_sup C = (lim_sup A) \/ (lim_sup B)

proof end;

theorem :: KURATO_2:15

for X being set
for A, B, C being SetSequence of X st ( for n being Element of NAT holds C . n = (A . n) \/ (B . n) ) holds
(lim_inf A) \/ (lim_inf B) c= lim_inf C

proof end;

theorem :: KURATO_2:16

for X being set
for A, B, C being SetSequence of X st ( for n being Element of NAT holds C . n = (A . n) /\ (B . n) ) holds
lim_sup C c= (lim_sup A) /\ (lim_sup B)

proof end;

theorem Th17: :: KURATO_2:17

for X being set
for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B

proof end;

theorem Th18: :: KURATO_2:18

for X being set
for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_inf A = B

proof end;

theorem :: KURATO_2:19

for X being set
for A, B being SetSequence of X
for C being Subset of X st ( for n being Element of NAT holds B . n = C \+\ (A . n) ) holds
C \+\ (lim_inf A) c= lim_sup B

proof end;

theorem :: KURATO_2:20

for X being set
for A, B being SetSequence of X
for C being Subset of X st ( for n being Element of NAT holds B . n = C \+\ (A . n) ) holds
C \+\ (lim_sup A) c= lim_sup B

proof end;

begin

theorem Th21: :: KURATO_2:21

for f being Function st ( for i being Element of NAT holds f . (i + 1) c= f . i ) holds
for i, j being Element of NAT st i <= j holds
f . j c= f . i

proof end;

definition

let T be set ;
let S be SetSequence of T;
:: original: non-ascending
redefine attr S is non-ascending means :Def5: :: KURATO_2:def 5
for i being Element of NAT holds S . (i + 1) c= S . i;
compatibility
( S is non-ascending iff for i being Element of NAT holds S . (i + 1) c= S . i )

proof end;

:: original: non-descending
redefine attr S is non-descending means :Def6: :: KURATO_2:def 6
for i being Element of NAT holds S . i c= S . (i + 1);
compatibility
( S is non-descending iff for i being Element of NAT holds S . i c= S . (i + 1) )

proof end;

end;

:: deftheorem Def5 defines non-ascending KURATO_2:def 5 :
for T being set
for S being SetSequence of T holds
( S is non-ascending iff for i being Element of NAT holds S . (i + 1) c= S . i );

:: deftheorem Def6 defines non-descending KURATO_2:def 6 :
for T being set
for S being SetSequence of T holds
( S is non-descending iff for i being Element of NAT holds S . i c= S . (i + 1) );

theorem :: KURATO_2:22

canceled;

theorem :: KURATO_2:23

canceled;

theorem Th24: :: KURATO_2:24

for T being set
for F being SetSequence of T
for x being set st F is non-ascending & ex k being Element of NAT st
for n being Element of NAT st n > k holds
x in F . n holds
x in meet F

proof end;

theorem :: KURATO_2:25

for T being set
for F being SetSequence of T st F is non-ascending holds
lim_inf F = meet F

proof end;

theorem :: KURATO_2:26

for T being set
for F being SetSequence of T st F is non-descending holds
lim_sup F = Union F

proof end;

begin

definition

let T be set ;
let S be SetSequence of T;
attr S is convergent means :Def7: :: KURATO_2:def 7
lim_sup S = lim_inf S;

end;

:: deftheorem Def7 defines convergent KURATO_2:def 7 :
for T being set
for S being SetSequence of T holds
( S is convergent iff lim_sup S = lim_inf S );

theorem :: KURATO_2:27

for T being set
for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T

proof end;

registration

let T be set ;
cluster Function-like V26() V30( NAT , bool T) -> V46() V47() convergent Element of bool [:NAT,(bool T):];
coherence
for b₁ being SetSequence of T st b₁ is constant holds
( b₁ is convergent & b₁ is non-descending & b₁ is non-ascending )

proof end;

end;

registration

let T be set ;
cluster non empty Relation-like Function-like V26() V29( NAT ) V30( NAT , bool T) Element of bool [:NAT,(bool T):];
existence
ex b₁ being SetSequence of T st
( b₁ is constant & not b₁ is empty )

proof end;

end;

definition

canceled;
let T be set ;
let S be convergent SetSequence of T;
func Lim_K S -> Subset of T means :Def9: :: KURATO_2:def 9
( it = lim_sup S & it = lim_inf S );
existence
ex b₁ being Subset of T st
( b₁ = lim_sup S & b₁ = lim_inf S )

proof end;

uniqueness
for b₁, b₂ being Subset of T st b₁ = lim_sup S & b₁ = lim_inf S & b₂ = lim_sup S & b₂ = lim_inf S holds
b₁ = b₂ ;

end;

:: deftheorem KURATO_2:def 8 :
canceled;

:: deftheorem Def9 defines Lim_K KURATO_2:def 9 :
for T being set
for S being convergent SetSequence of T
for b₃ being Subset of T holds
( b₃ = Lim_K S iff ( b₃ = lim_sup S & b₃ = lim_inf S ) );

theorem :: KURATO_2:28

for X being set
for F being convergent SetSequence of X
for x being set holds
( x in Lim_K F iff ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) )

proof end;

begin

registration

let f be FinSequence of the carrier of (TOP-REAL 2);
cluster L~ f -> closed ;
coherence
L~ f is closed ;

end;

theorem :: KURATO_2:29

canceled;

theorem Th30: :: KURATO_2:30

for n being Element of NAT
for x being Point of (Euclid n)
for r being real number holds Ball (x,r) is open Subset of (TOP-REAL n)

proof end;

theorem :: KURATO_2:31

canceled;

theorem Th32: :: KURATO_2:32

for n being Element of NAT
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & x in Ball (p,r) holds
|.(x - p9).| < r

proof end;

theorem Th33: :: KURATO_2:33

for n being Element of NAT
for p being Point of (Euclid n)
for x, p9 being Point of (TOP-REAL n)
for r being real number st p = p9 & |.(x - p9).| < r holds
x in Ball (p,r)

proof end;

theorem :: KURATO_2:34

for n being Element of NAT
for r being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) st r in Cl X holds
ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )

proof end;

registration

let M be non empty MetrSpace;
cluster TopSpaceMetr M -> first-countable ;
coherence
TopSpaceMetr M is first-countable by FRECHET:21;

end;

Lm1: for T being non empty TopSpace
for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )

proof end;

theorem Th35: :: KURATO_2:35

for T being non empty TopSpace holds
( T is first-countable iff TopStruct(# the carrier of T, the topology of T #) is first-countable )

proof end;

registration

let n be Element of NAT ;
cluster TOP-REAL n -> first-countable ;
coherence
TOP-REAL n is first-countable

proof end;

end;

theorem :: KURATO_2:36

for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being real number st r > 0 holds
Ball (p9,r) meets A )

proof end;

theorem :: KURATO_2:37

for n being Element of NAT
for x, y being Point of (TOP-REAL n)
for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)

proof end;

theorem Th38: :: KURATO_2:38

for n being Element of NAT
for S being Subset of (TOP-REAL n) holds
( not S is Bounded iff for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) )

proof end;

theorem Th39: :: KURATO_2:39

for n being Element of NAT
for a, b being real number
for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b

proof end;

theorem Th40: :: KURATO_2:40

for n being Element of NAT
for a, b, c being real number
for x, y, z being Point of (Euclid n) st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)

proof end;

theorem Th41: :: KURATO_2:41

for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )

proof end;

begin

theorem :: KURATO_2:42

canceled;

theorem :: KURATO_2:43

canceled;

theorem :: KURATO_2:44

canceled;

theorem Th45: :: KURATO_2:45

for T being non empty 1-sorted
for F, G being SetSequence of the carrier of T
for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F

proof end;

theorem :: KURATO_2:46

canceled;

theorem :: KURATO_2:47

for T being non empty 1-sorted
for S being SetSequence of the carrier of T
for R being subsequence of S
for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )

proof end;

begin

definition

let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
canceled;
func Lim_inf S -> Subset of T means :Def11: :: KURATO_2:def 11
for p being Point of T holds
( p in it iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G );
existence
ex b₁ being Subset of T st
for p being Point of T holds
( p in b₁ iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for p being Point of T holds
( p in b₁ iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) ) & ( for p being Point of T holds
( p in b₂ iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem KURATO_2:def 10 :
canceled;

:: deftheorem Def11 defines Lim_inf KURATO_2:def 11 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b₃ being Subset of T holds
( b₃ = Lim_inf S iff for p being Point of T holds
( p in b₃ iff for G being a_neighborhood of p ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G ) );

theorem Th48: :: KURATO_2:48

for n being Element of NAT
for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball (p9,r) )

proof end;

theorem Th49: :: KURATO_2:49

for T being non empty TopSpace
for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S

proof end;

theorem :: KURATO_2:50

canceled;

registration

let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
cluster Lim_inf S -> closed ;
coherence
Lim_inf S is closed

proof end;

end;

theorem :: KURATO_2:51

for T being non empty TopSpace
for R, S being SetSequence of the carrier of T st R is subsequence of S holds
Lim_inf S c= Lim_inf R

proof end;

theorem Th52: :: KURATO_2:52

for T being non empty TopSpace
for A, B being SetSequence of the carrier of T st ( for i being Element of NAT holds A . i c= B . i ) holds
Lim_inf A c= Lim_inf B

proof end;

theorem :: KURATO_2:53

for T being non empty TopSpace
for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) holds
(Lim_inf A) \/ (Lim_inf B) c= Lim_inf C

proof end;

theorem :: KURATO_2:54

for T being non empty TopSpace
for A, B, C being SetSequence of the carrier of T st ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) holds
Lim_inf C c= (Lim_inf A) /\ (Lim_inf B)

proof end;

theorem Th55: :: KURATO_2:55

for T being non empty TopSpace
for F, G being SetSequence of the carrier of T st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds
Lim_inf G = Lim_inf F

proof end;

theorem :: KURATO_2:56

for n being Element of NAT
for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of (TOP-REAL n) st ex s being Real_Sequence of n st
( s is convergent & ( for x being Element of NAT holds s . x in S . x ) & p = lim s ) holds
p in Lim_inf S

proof end;

theorem Th57: :: KURATO_2:57

for T being non empty TopSpace
for P being Subset of T
for s being SetSequence of the carrier of T st ( for i being Nat holds s . i c= P ) holds
Lim_inf s c= Cl P

proof end;

theorem Th58: :: KURATO_2:58

for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Cl A

proof end;

theorem :: KURATO_2:59

for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being closed Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = A

proof end;

theorem Th60: :: KURATO_2:60

for n being Element of NAT
for S being SetSequence of the carrier of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is Bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is Bounded

proof end;

theorem :: KURATO_2:61

for S being SetSequence of the carrier of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P is Bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is compact

proof end;

theorem Th62: :: KURATO_2:62

for n being Element of NAT
for A, B being SetSequence of the carrier of (TOP-REAL n)
for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C

proof end;

theorem :: KURATO_2:63

for S being SetSequence of (TOP-REAL 2) holds lim_inf S c= Lim_inf S

proof end;

theorem :: KURATO_2:64

for C being Simple_closed_curve
for i being Element of NAT holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))

proof end;

begin

definition

let T be non empty TopSpace;
let S be SetSequence of the carrier of T;
func Lim_sup S -> Subset of T means :Def12: :: KURATO_2:def 12
for x being set holds
( x in it iff ex A being subsequence of S st x in Lim_inf A );
existence
ex b₁ being Subset of T st
for x being set holds
( x in b₁ iff ex A being subsequence of S st x in Lim_inf A )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for x being set holds
( x in b₁ iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being set holds
( x in b₂ iff ex A being subsequence of S st x in Lim_inf A ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines Lim_sup KURATO_2:def 12 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b₃ being Subset of T holds
( b₃ = Lim_sup S iff for x being set holds
( x in b₃ iff ex A being subsequence of S st x in Lim_inf A ) );

theorem :: KURATO_2:65

for N being Element of NAT
for F being sequence of (TOP-REAL N)
for x being Point of (TOP-REAL N)
for x9 being Point of (Euclid N) st x = x9 holds
( x is_a_cluster_point_of F iff for r being real number
for n being Element of NAT st r > 0 holds
ex m being Element of NAT st
( n <= m & F . m in Ball (x9,r) ) )

proof end;

theorem Th66: :: KURATO_2:66

for T being non empty TopSpace
for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A

proof end;

theorem Th67: :: KURATO_2:67

for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of A holds
ex D being subsequence of B st
for i being Element of NAT holds C . i c= D . i

proof end;

theorem :: KURATO_2:68

for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of B holds
ex D being subsequence of A st
for i being Element of NAT holds D . i c= C . i

proof end;

theorem Th69: :: KURATO_2:69

for A, B being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds A . i c= B . i ) holds
Lim_sup A c= Lim_sup B

proof end;

theorem :: KURATO_2:70

for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds C . i = (A . i) \/ (B . i) ) holds
(Lim_sup A) \/ (Lim_sup B) c= Lim_sup C

proof end;

theorem :: KURATO_2:71

for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds C . i = (A . i) /\ (B . i) ) holds
Lim_sup C c= (Lim_sup A) /\ (Lim_sup B)

proof end;

theorem Th72: :: KURATO_2:72

for A, B being SetSequence of the carrier of (TOP-REAL 2)
for C, C1 being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) & C1 is subsequence of C holds
ex A1, B1 being SetSequence of the carrier of (TOP-REAL 2) st
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Element of NAT holds C1 . i = [:(A1 . i),(B1 . i):] ) )

proof end;

theorem :: KURATO_2:73

for A, B being SetSequence of the carrier of (TOP-REAL 2)
for C being SetSequence of the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) holds
Lim_sup C c= [:(Lim_sup A),(Lim_sup B):]

proof end;

theorem Th74: :: KURATO_2:74

for T being non empty TopSpace
for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F

proof end;

theorem :: KURATO_2:75

for F being SetSequence of the carrier of (TOP-REAL 2)
for A being Subset of (TOP-REAL 2) st ( for i being Nat holds F . i = A ) holds
Lim_sup F = Cl A

proof end;

theorem :: KURATO_2:76

for F, G being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds G . i = Cl (F . i) ) holds
Lim_sup G = Lim_sup F

proof end;