:: KURATO_0 semantic presentation

begin

theorem :: KURATO_0:1
for F being Function
for i being set st i in dom F holds
meet F c= F . i
proof
let F be Function; ::_thesis: for i being set st i in dom F holds
meet F c= F . i
let i be set ; ::_thesis: ( i in dom F implies meet F c= F . i )
assume A1: i in dom F ; ::_thesis: meet F c= F . i
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F or x in F . i )
assume  x in meet F ; ::_thesis: x in F . i
hence  x in F . i by A1, FUNCT_6:25, RELAT_1:38; ::_thesis: verum
end;

theorem :: KURATO_0:2
for A, B, C, D being set st A meets B & C meets D holds
[:A,C:] meets [:B,D:]
proof
let A, B, C, D be set ; ::_thesis: ( A meets B & C meets D implies [:A,C:] meets [:B,D:] )
assume that
A1: A meets B and
A2: C meets D ; ::_thesis: [:A,C:] meets [:B,D:]
consider x being set  such that
A3: ( x in A & x in B ) by A1, XBOOLE_0:3;
consider y being set  such that
A4: ( y in C & y in D ) by A2, XBOOLE_0:3;
 ( [x,y] in [:A,C:] & [x,y] in [:B,D:] ) by A3, A4, ZFMISC_1:87;
hence  [:A,C:] meets [:B,D:] by XBOOLE_0:3; ::_thesis: verum
end;

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

registration
let T be non empty set ;
cluster non empty Relation-like non-empty NAT -defined bool T -valued Function-like V29( NAT ) V33( NAT , bool T) for Element of bool [:NAT,(bool T):];
existence
 ex b1 being SetSequence of T st b1 is non-empty
proof
set a = the Element of T;
reconsider A = { the Element of T} as Subset of T ;
set X = NAT --> A;
reconsider X = NAT --> A as SetSequence of T ;
take  X ; ::_thesis: X is non-empty
thus  X is non-empty ; ::_thesis: verum
end;
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
 Union F c= X ;
hence  Union F is Subset of X ; ::_thesis: verum
end;
:: original: meet
redefine func meet F ->  Subset of X;
coherence
 meet F is Subset of X
proof
reconsider G = rng F as Subset-Family of X ;
 meet G c= X ;
hence  meet F is Subset of X by FUNCT_6:def_4; ::_thesis: verum
end;
end;

begin

definition
let X be set ;
let F be SetSequence of X;
func lim_inf F ->  Subset of X means :Def1: :: KURATO_0:def 1
 ex f being SetSequence of X st
( it = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) );
existence
 ex b1 being Subset of X ex f being SetSequence of X st
( b1 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) )
proof
deffunc H1( Element of NAT ) ->  Subset of X = meet (F ^\ $1);
consider f being SetSequence of X such that
A1: for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
take  Union f ; ::_thesis: ex f being SetSequence of X st
( Union f = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) )
thus  ex f being SetSequence of X st
( Union f = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of X st ex f being SetSequence of X st
( b1 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( b2 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) holds
b1 = b2
proof
let A1, A2 be Subset of X; ::_thesis: ( ex f being SetSequence of X st
( A1 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) & ex f being SetSequence of X st
( A2 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) implies A1 = A2 )
given f1 being SetSequence of X such that A2: A1 = Union f1 and
A3: for n being Element of NAT holds f1 . n = meet (F ^\ n) ; ::_thesis: ( for f being SetSequence of X holds
( not A2 = Union f or ex n being Element of NAT st not f . n = meet (F ^\ n) ) or A1 = A2 )
given f2 being SetSequence of X such that A4: A2 = Union f2 and
A5: for n being Element of NAT holds f2 . n = meet (F ^\ n) ; ::_thesis: A1 = A2
 for n being Element of NAT holds f1 . n = f2 . n
proof
let n be Element of NAT ; ::_thesis: f1 . n = f2 . n
f1 . n = meet (F ^\ n) by A3
.= f2 . n by A5 ;
hence  f1 . n = f2 . n ; ::_thesis: verum
end;
hence  A1 = A2 by A2, A4, FUNCT_2:63; ::_thesis: verum
end;
func lim_sup F ->  Subset of X means :Def2: :: KURATO_0:def 2
 ex f being SetSequence of X st
( it = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) );
existence
 ex b1 being Subset of X ex f being SetSequence of X st
( b1 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) )
proof
deffunc H1( Element of NAT ) ->  Subset of X = Union (F ^\ $1);
consider f being SetSequence of X such that
A6: for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
take  meet f ; ::_thesis: ex f being SetSequence of X st
( meet f = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) )
thus  ex f being SetSequence of X st
( meet f = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) by A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of X st ex f being SetSequence of X st
( b1 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( b2 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) holds
b1 = b2
proof
let A1, A2 be Subset of X; ::_thesis: ( ex f being SetSequence of X st
( A1 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) & ex f being SetSequence of X st
( A2 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) implies A1 = A2 )
given f1 being SetSequence of X such that A7: A1 = meet f1 and
A8: for n being Element of NAT holds f1 . n = Union (F ^\ n) ; ::_thesis: ( for f being SetSequence of X holds
( not A2 = meet f or ex n being Element of NAT st not f . n = Union (F ^\ n) ) or A1 = A2 )
given f2 being SetSequence of X such that A9: A2 = meet f2 and
A10: for n being Element of NAT holds f2 . n = Union (F ^\ n) ; ::_thesis: A1 = A2
 for n being Element of NAT holds f1 . n = f2 . n
proof
let n be Element of NAT ; ::_thesis: f1 . n = f2 . n
f1 . n = Union (F ^\ n) by A8
.= f2 . n by A10 ;
hence  f1 . n = f2 . n ; ::_thesis: verum
end;
hence  A1 = A2 by A7, A9, FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines lim_inf KURATO_0:def_1_:_
 for X being set
for F being SetSequence of X
for b3 being Subset of X holds
( b3 = lim_inf F iff ex f being SetSequence of X st
( b3 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) );

:: deftheorem Def2 defines lim_sup KURATO_0:def_2_:_
 for X being set
for F being SetSequence of X
for b3 being Subset of X holds
( b3 = lim_sup F iff ex f being SetSequence of X st
( b3 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) );

theorem Th3: :: KURATO_0:3
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
let X be set ; ::_thesis: 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 )
let F be SetSequence of X; ::_thesis: for x being set holds
( x in meet F iff for z being Element of NAT holds x in F . z )
let x be set ; ::_thesis: ( x in meet F iff for z being Element of NAT holds x in F . z )
hereby  ::_thesis: ( ( for z being Element of NAT holds x in F . z ) implies x in meet F )
assume A1: x in meet F ; ::_thesis: for z being Element of NAT holds x in F . z
let z be Element of NAT ; ::_thesis: x in F . z
 z in NAT ;
then  z in dom F by FUNCT_2:def_1;
hence  x in F . z by A1, FUNCT_6:25; ::_thesis: verum
end;
assume  for z being Element of NAT holds x in F . z ; ::_thesis: x in meet F
then  for y being set st y in dom F holds
x in F . y ;
hence  x in meet F by FUNCT_6:25; ::_thesis: verum
end;

theorem Th4: :: KURATO_0:4
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
let X be set ; ::_thesis: 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) )
let F be SetSequence of X; ::_thesis: 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) )
let x be set ; ::_thesis: ( 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) )
consider f being SetSequence of X such that
A1: lim_inf F = Union f and
A2: for n being Element of NAT holds f . n = meet (F ^\ n) by Def1;
hereby  ::_thesis: ( ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k) implies x in lim_inf F )
consider f being SetSequence of X such that
A3: lim_inf F = Union f and
A4: for n being Element of NAT holds f . n = meet (F ^\ n) by Def1;
assume  x in lim_inf F ; ::_thesis: ex n being Element of NAT st
for k being Element of NAT holds x in F . (n + k)
then consider n being Element of NAT  such that
A5: x in f . n by A3, PROB_1:12;
set G = F ^\ n;
take n = n; ::_thesis: for k being Element of NAT holds x in F . (n + k)
let k be Element of NAT ; ::_thesis: x in F . (n + k)
A6: (F ^\ n) . k = F . (n + k) by NAT_1:def_3;
 x in meet (F ^\ n) by A4, A5;
hence  x in F . (n + k) by A6, Th3; ::_thesis: verum
end;
given n being Element of NAT  such that A7: for k being Element of NAT holds x in F . (n + k) ; ::_thesis: x in lim_inf F
set G = F ^\ n;
 for z being Element of NAT holds x in (F ^\ n) . z
proof
let z be Element of NAT ; ::_thesis: x in (F ^\ n) . z
 (F ^\ n) . z = F . (n + z) by NAT_1:def_3;
hence  x in (F ^\ n) . z by A7; ::_thesis: verum
end;
then  x in meet (F ^\ n) by Th3;
then  x in f . n by A2;
hence  x in lim_inf F by A1, PROB_1:12; ::_thesis: verum
end;

theorem Th5: :: KURATO_0:5
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
let X be set ; ::_thesis: 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) )
let F be SetSequence of X; ::_thesis: 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) )
let x be set ; ::_thesis: ( x in lim_sup F iff for n being Element of NAT ex k being Element of NAT st x in F . (n + k) )
consider f being SetSequence of X such that
A1: lim_sup F = meet f and
A2: for n being Element of NAT holds f . n = Union (F ^\ n) by Def2;
hereby  ::_thesis: ( ( for n being Element of NAT ex k being Element of NAT st x in F . (n + k) ) implies x in lim_sup F )
assume A3: x in lim_sup F ; ::_thesis: for n being Element of NAT ex k being Element of NAT st x in F . (n + k)
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in F . (n + k)
set G = F ^\ n;
consider f being SetSequence of X such that
A4: lim_sup F = meet f and
A5: for n being Element of NAT holds f . n = Union (F ^\ n) by Def2;
 f . n = Union (F ^\ n) by A5;
then  x in Union (F ^\ n) by A3, A4, Th3;
then consider k being Element of NAT  such that
A6: x in (F ^\ n) . k by PROB_1:12;
take k = k; ::_thesis: x in F . (n + k)
thus  x in F . (n + k) by A6, NAT_1:def_3; ::_thesis: verum
end;
assume A7: for n being Element of NAT ex k being Element of NAT st x in F . (n + k) ; ::_thesis: x in lim_sup F
 for z being Element of NAT holds x in f . z
proof
let z be Element of NAT ; ::_thesis: x in f . z
set G = F ^\ z;
consider k being Element of NAT  such that
A8: x in F . (z + k) by A7;
 ( f . z = Union (F ^\ z) & (F ^\ z) . k = F . (z + k) ) by A2, NAT_1:def_3;
hence  x in f . z by A8, PROB_1:12; ::_thesis: verum
end;
hence  x in lim_sup F by A1, Th3; ::_thesis: verum
end;

theorem :: KURATO_0:6
for X being set
for F being SetSequence of X holds lim_inf F c= lim_sup F
proof
let X be set ; ::_thesis: for F being SetSequence of X holds lim_inf F c= lim_sup F
let F be SetSequence of X; ::_thesis: lim_inf F c= lim_sup F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf F or x in lim_sup F )
assume  x in lim_inf F ; ::_thesis: x in lim_sup F
then consider n being Element of NAT  such that
A1: for k being Element of NAT holds x in F . (n + k) by Th4;
now__::_thesis:_for_k_being_Element_of_NAT_ex_n_being_Element_of_NAT_st_x_in_F_._(k_+_n)
let k be Element of NAT ; ::_thesis: ex n being Element of NAT st x in F . (k + n)
 x in F . (n + k) by A1;
hence  ex n being Element of NAT st x in F . (k + n) ; ::_thesis: verum
end;
hence  x in lim_sup F by Th5; ::_thesis: verum
end;

theorem Th7: :: KURATO_0:7
for X being set
for F being SetSequence of X holds meet F c= lim_inf F
proof
let X be set ; ::_thesis: for F being SetSequence of X holds meet F c= lim_inf F
let F be SetSequence of X; ::_thesis: meet F c= lim_inf F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F or x in lim_inf F )
assume  x in meet F ; ::_thesis: x in lim_inf F
then  for k being Element of NAT holds x in F . (0 + k) by Th3;
hence  x in lim_inf F by Th4; ::_thesis: verum
end;

theorem Th8: :: KURATO_0:8
for X being set
for F being SetSequence of X holds lim_sup F c= Union F
proof
let X be set ; ::_thesis: for F being SetSequence of X holds lim_sup F c= Union F
let F be SetSequence of X; ::_thesis: lim_sup F c= Union F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup F or x in Union F )
assume  x in lim_sup F ; ::_thesis: x in Union F
then  ex k being Element of NAT st x in F . (0 + k) by Th5;
hence  x in Union F by PROB_1:12; ::_thesis: verum
end;

theorem :: KURATO_0:9
for X being set
for F being SetSequence of X holds lim_inf F = (lim_sup (Complement F)) `
proof
let X be set ; ::_thesis: for F being SetSequence of X holds lim_inf F = (lim_sup (Complement F)) `
let F be SetSequence of X; ::_thesis: lim_inf F = (lim_sup (Complement F)) `
set G = Complement F;
thus  lim_inf F c= (lim_sup (Complement F)) ` :: according to XBOOLE_0:def_10 ::_thesis: (lim_sup (Complement F)) ` c= lim_inf F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf F or x in (lim_sup (Complement F)) ` )
assume A1: x in lim_inf F ; ::_thesis: x in (lim_sup (Complement F)) `
then consider n being Element of NAT  such that
A2: for k being Element of NAT holds x in F . (n + k) by Th4;
 for k being Element of NAT holds not x in (Complement F) . (n + k)
proof
let k be Element of NAT ; ::_thesis: not x in (Complement F) . (n + k)
A3: (Complement F) . (n + k) = (F . (n + k)) ` by PROB_1:def_2;
assume  x in (Complement F) . (n + k) ; ::_thesis: contradiction
then  not x in F . (n + k) by A3, XBOOLE_0:def_5;
hence  contradiction by A2; ::_thesis: verum
end;
then  not x in lim_sup (Complement F) by Th5;
hence  x in (lim_sup (Complement F)) ` by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  (lim_sup (Complement F)) ` c= lim_inf F ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_sup (Complement F)) ` or x in lim_inf F )
assume A4: x in (lim_sup (Complement F)) ` ; ::_thesis: x in lim_inf F
then  not x in lim_sup (Complement F) by XBOOLE_0:def_5;
then consider n being Element of NAT  such that
A5: for k being Element of NAT holds not x in (Complement F) . (n + k) by Th5;
 for k being Element of NAT holds x in F . (n + k)
proof
let k be Element of NAT ; ::_thesis: x in F . (n + k)
assume  not x in F . (n + k) ; ::_thesis: contradiction
then  x in (F . (n + k)) ` by A4, XBOOLE_0:def_5;
then  x in (Complement F) . (n + k) by PROB_1:def_2;
hence  contradiction by A5; ::_thesis: verum
end;
hence  x in lim_inf F by Th4; ::_thesis: verum
end;
end;

theorem :: KURATO_0:10
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
let X be set ; ::_thesis: 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)
let A, B, C be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds C . n = (A . n) /\ (B . n) ) implies lim_inf C = (lim_inf A) /\ (lim_inf B) )
assume A1: for n being Element of NAT holds C . n = (A . n) /\ (B . n) ; ::_thesis: lim_inf C = (lim_inf A) /\ (lim_inf B)
thus  lim_inf C c= (lim_inf A) /\ (lim_inf B) :: according to XBOOLE_0:def_10 ::_thesis: (lim_inf A) /\ (lim_inf B) c= lim_inf C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf C or x in (lim_inf A) /\ (lim_inf B) )
assume  x in lim_inf C ; ::_thesis: x in (lim_inf A) /\ (lim_inf B)
then consider n being Element of NAT  such that
A2: for k being Element of NAT holds x in C . (n + k) by Th4;
 for k being Element of NAT holds x in B . (n + k)
proof
let k be Element of NAT ; ::_thesis: x in B . (n + k)
 ( C . (n + k) = (A . (n + k)) /\ (B . (n + k)) & x in C . (n + k) ) by A1, A2;
hence  x in B . (n + k) by XBOOLE_0:def_4; ::_thesis: verum
end;
then A3: x in lim_inf B by Th4;
 for k being Element of NAT holds x in A . (n + k)
proof
let k be Element of NAT ; ::_thesis: x in A . (n + k)
 ( C . (n + k) = (A . (n + k)) /\ (B . (n + k)) & x in C . (n + k) ) by A1, A2;
hence  x in A . (n + k) by XBOOLE_0:def_4; ::_thesis: verum
end;
then  x in lim_inf A by Th4;
hence  x in (lim_inf A) /\ (lim_inf B) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  (lim_inf A) /\ (lim_inf B) c= lim_inf C ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_inf A) /\ (lim_inf B) or x in lim_inf C )
assume A4: x in (lim_inf A) /\ (lim_inf B) ; ::_thesis: x in lim_inf C
then  x in lim_inf A by XBOOLE_0:def_4;
then consider n1 being Element of NAT  such that
A5: for k being Element of NAT holds x in A . (n1 + k) by Th4;
 x in lim_inf B by A4, XBOOLE_0:def_4;
then consider n2 being Element of NAT  such that
A6: for k being Element of NAT holds x in B . (n2 + k) by Th4;
set n = max (n1,n2);
A7: for k being Element of NAT holds x in B . ((max (n1,n2)) + k)
proof
let k be Element of NAT ; ::_thesis: x in B . ((max (n1,n2)) + k)
consider g being Nat such that
A8: max (n1,n2) = n2 + g by NAT_1:10, XXREAL_0:25;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
 x in B . (n2 + (g + k)) by A6;
hence  x in B . ((max (n1,n2)) + k) by A8; ::_thesis: verum
end;
A9: for k being Element of NAT holds x in A . ((max (n1,n2)) + k)
proof
let k be Element of NAT ; ::_thesis: x in A . ((max (n1,n2)) + k)
consider g being Nat such that
A10: max (n1,n2) = n1 + g by NAT_1:10, XXREAL_0:25;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
 x in A . (n1 + (g + k)) by A5;
hence  x in A . ((max (n1,n2)) + k) by A10; ::_thesis: verum
end;
 for k being Element of NAT holds x in C . ((max (n1,n2)) + k)
proof
let k be Element of NAT ; ::_thesis: x in C . ((max (n1,n2)) + k)
 ( x in A . ((max (n1,n2)) + k) & x in B . ((max (n1,n2)) + k) ) by A9, A7;
then  x in (A . ((max (n1,n2)) + k)) /\ (B . ((max (n1,n2)) + k)) by XBOOLE_0:def_4;
hence  x in C . ((max (n1,n2)) + k) by A1; ::_thesis: verum
end;
hence  x in lim_inf C by Th4; ::_thesis: verum
end;
end;

theorem :: KURATO_0:11
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
let X be set ; ::_thesis: 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)
let A, B, C be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds C . n = (A . n) \/ (B . n) ) implies lim_sup C = (lim_sup A) \/ (lim_sup B) )
assume A1: for n being Element of NAT holds C . n = (A . n) \/ (B . n) ; ::_thesis: lim_sup C = (lim_sup A) \/ (lim_sup B)
thus  lim_sup C c= (lim_sup A) \/ (lim_sup B) :: according to XBOOLE_0:def_10 ::_thesis: (lim_sup A) \/ (lim_sup B) c= lim_sup C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup C or x in (lim_sup A) \/ (lim_sup B) )
assume A2: x in lim_sup C ; ::_thesis: x in (lim_sup A) \/ (lim_sup B)
 ( for n being Element of NAT ex k being Element of NAT st x in A . (n + k) or for n being Element of NAT ex k being Element of NAT st x in B . (n + k) )
proof
given n1 being Element of NAT  such that A3: for k being Element of NAT holds not x in A . (n1 + k) ; ::_thesis: for n being Element of NAT ex k being Element of NAT st x in B . (n + k)
given n2 being Element of NAT  such that A4: for k being Element of NAT holds not x in B . (n2 + k) ; ::_thesis: contradiction
set n = max (n1,n2);
consider g being Nat such that
A5: max (n1,n2) = n1 + g by NAT_1:10, XXREAL_0:25;
consider h being Nat such that
A6: max (n1,n2) = n2 + h by NAT_1:10, XXREAL_0:25;
reconsider g = g, h = h as Element of NAT by ORDINAL1:def_12;
consider k being Element of NAT  such that
A7: x in C . ((max (n1,n2)) + k) by A2, Th5;
A8: x in (A . ((max (n1,n2)) + k)) \/ (B . ((max (n1,n2)) + k)) by A1, A7;
percases ( x in A . ((max (n1,n2)) + k) or x in B . ((max (n1,n2)) + k) ) by A8, XBOOLE_0:def_3;
suppose x in A . ((max (n1,n2)) + k) ; ::_thesis: contradiction
then  x in A . (n1 + (g + k)) by A5;
hence  contradiction by A3; ::_thesis: verum
end;
suppose x in B . ((max (n1,n2)) + k) ; ::_thesis: contradiction
then  x in B . (n2 + (h + k)) by A6;
hence  contradiction by A4; ::_thesis: verum
end;
end;
end;
then  ( x in lim_sup A or x in lim_sup B ) by Th5;
hence  x in (lim_sup A) \/ (lim_sup B) by XBOOLE_0:def_3; ::_thesis: verum
end;
thus  (lim_sup A) \/ (lim_sup B) c= lim_sup C ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_sup A) \/ (lim_sup B) or x in lim_sup C )
assume A9: x in (lim_sup A) \/ (lim_sup B) ; ::_thesis: x in lim_sup C
percases ( x in lim_sup A or x in lim_sup B ) by A9, XBOOLE_0:def_3;
supposeA10: x in lim_sup A ; ::_thesis: x in lim_sup C
 for n being Element of NAT ex k being Element of NAT st x in C . (n + k)
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in C . (n + k)
consider k being Element of NAT  such that
A11: x in A . (n + k) by A10, Th5;
take  k ; ::_thesis: x in C . (n + k)
 x in (A . (n + k)) \/ (B . (n + k)) by A11, XBOOLE_0:def_3;
hence  x in C . (n + k) by A1; ::_thesis: verum
end;
hence  x in lim_sup C by Th5; ::_thesis: verum
end;
supposeA12: x in lim_sup B ; ::_thesis: x in lim_sup C
 for n being Element of NAT ex k being Element of NAT st x in C . (n + k)
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in C . (n + k)
consider k being Element of NAT  such that
A13: x in B . (n + k) by A12, Th5;
take  k ; ::_thesis: x in C . (n + k)
 x in (A . (n + k)) \/ (B . (n + k)) by A13, XBOOLE_0:def_3;
hence  x in C . (n + k) by A1; ::_thesis: verum
end;
hence  x in lim_sup C by Th5; ::_thesis: verum
end;
end;
end;
end;

theorem :: KURATO_0:12
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
let X be set ; ::_thesis: 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
let A, B, C be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds C . n = (A . n) \/ (B . n) ) implies (lim_inf A) \/ (lim_inf B) c= lim_inf C )
assume A1: for n being Element of NAT holds C . n = (A . n) \/ (B . n) ; ::_thesis: (lim_inf A) \/ (lim_inf B) c= lim_inf C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_inf A) \/ (lim_inf B) or x in lim_inf C )
assume A2: x in (lim_inf A) \/ (lim_inf B) ; ::_thesis: x in lim_inf C
percases ( x in lim_inf A or x in lim_inf B ) by A2, XBOOLE_0:def_3;
suppose x in lim_inf A ; ::_thesis: x in lim_inf C
then consider n being Element of NAT  such that
A3: for k being Element of NAT holds x in A . (n + k) by Th4;
 for k being Element of NAT holds x in C . (n + k)
proof
let k be Element of NAT ; ::_thesis: x in C . (n + k)
 x in A . (n + k) by A3;
then  x in (A . (n + k)) \/ (B . (n + k)) by XBOOLE_0:def_3;
hence  x in C . (n + k) by A1; ::_thesis: verum
end;
hence  x in lim_inf C by Th4; ::_thesis: verum
end;
suppose x in lim_inf B ; ::_thesis: x in lim_inf C
then consider n being Element of NAT  such that
A4: for k being Element of NAT holds x in B . (n + k) by Th4;
 for k being Element of NAT holds x in C . (n + k)
proof
let k be Element of NAT ; ::_thesis: x in C . (n + k)
 x in B . (n + k) by A4;
then  x in (A . (n + k)) \/ (B . (n + k)) by XBOOLE_0:def_3;
hence  x in C . (n + k) by A1; ::_thesis: verum
end;
hence  x in lim_inf C by Th4; ::_thesis: verum
end;
end;
end;

theorem :: KURATO_0: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_sup C c= (lim_sup A) /\ (lim_sup B)
proof
let X be set ; ::_thesis: 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)
let A, B, C be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds C . n = (A . n) /\ (B . n) ) implies lim_sup C c= (lim_sup A) /\ (lim_sup B) )
assume A1: for n being Element of NAT holds C . n = (A . n) /\ (B . n) ; ::_thesis: lim_sup C c= (lim_sup A) /\ (lim_sup B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup C or x in (lim_sup A) /\ (lim_sup B) )
assume A2: x in lim_sup C ; ::_thesis: x in (lim_sup A) /\ (lim_sup B)
 for n being Element of NAT ex k being Element of NAT st x in B . (n + k)
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (n + k)
consider k being Element of NAT  such that
A3: x in C . (n + k) by A2, Th5;
take  k ; ::_thesis: x in B . (n + k)
 x in (A . (n + k)) /\ (B . (n + k)) by A1, A3;
hence  x in B . (n + k) by XBOOLE_0:def_4; ::_thesis: verum
end;
then A4: x in lim_sup B by Th5;
 for n being Element of NAT ex k being Element of NAT st x in A . (n + k)
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in A . (n + k)
consider k being Element of NAT  such that
A5: x in C . (n + k) by A2, Th5;
take  k ; ::_thesis: x in A . (n + k)
 x in (A . (n + k)) /\ (B . (n + k)) by A1, A5;
hence  x in A . (n + k) by XBOOLE_0:def_4; ::_thesis: verum
end;
then  x in lim_sup A by Th5;
hence  x in (lim_sup A) /\ (lim_sup B) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th14: :: KURATO_0:14
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
let X be set ; ::_thesis: 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
let A be SetSequence of X; ::_thesis: for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B
let B be Subset of X; ::_thesis: ( ( for n being Nat holds A . n = B ) implies lim_sup A = B )
assume A1: for n being Nat holds A . n = B ; ::_thesis: lim_sup A = B
thus  lim_sup A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= lim_sup A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup A or x in B )
assume  x in lim_sup A ; ::_thesis: x in B
then  ex k being Element of NAT st x in A . (0 + k) by Th5;
hence  x in B by A1; ::_thesis: verum
end;
thus  B c= lim_sup A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in lim_sup A )
assume A2: x in B ; ::_thesis: x in lim_sup A
 for m being Element of NAT ex k being Element of NAT st x in A . (m + k)
proof
let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in A . (m + k)
take  0 ; ::_thesis: x in A . (m + 0)
thus  x in A . (m + 0) by A1, A2; ::_thesis: verum
end;
hence  x in lim_sup A by Th5; ::_thesis: verum
end;
end;

theorem Th15: :: KURATO_0:15
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
let X be set ; ::_thesis: 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
let A be SetSequence of X; ::_thesis: for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_inf A = B
let B be Subset of X; ::_thesis: ( ( for n being Nat holds A . n = B ) implies lim_inf A = B )
assume A1: for n being Nat holds A . n = B ; ::_thesis: lim_inf A = B
thus  lim_inf A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= lim_inf A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf A or x in B )
assume  x in lim_inf A ; ::_thesis: x in B
then consider m being Element of NAT  such that
A2: for k being Element of NAT holds x in A . (m + k) by Th4;
 x in A . (m + 0) by A2;
hence  x in B by A1; ::_thesis: verum
end;
thus  B c= lim_inf A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in lim_inf A )
assume A3: x in B ; ::_thesis: x in lim_inf A
 ex m being Element of NAT st
for k being Element of NAT holds x in A . (m + k)
proof
take  0 ; ::_thesis: for k being Element of NAT holds x in A . (0 + k)
let k be Element of NAT ; ::_thesis: x in A . (0 + k)
thus  x in A . (0 + k) by A1, A3; ::_thesis: verum
end;
hence  x in lim_inf A by Th4; ::_thesis: verum
end;
end;

theorem :: KURATO_0:16
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
let X be set ; ::_thesis: 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
let A, B be SetSequence of X; ::_thesis: 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
let C be Subset of X; ::_thesis: ( ( for n being Element of NAT holds B . n = C \+\ (A . n) ) implies C \+\ (lim_inf A) c= lim_sup B )
assume A1: for n being Element of NAT holds B . n = C \+\ (A . n) ; ::_thesis: C \+\ (lim_inf A) c= lim_sup B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C \+\ (lim_inf A) or x in lim_sup B )
assume A2: x in C \+\ (lim_inf A) ; ::_thesis: x in lim_sup B
percases ( ( x in C & not x in lim_inf A ) or ( not x in C & x in lim_inf A ) ) by A2, XBOOLE_0:1;
supposeA3: ( x in C & not x in lim_inf A ) ; ::_thesis: x in lim_sup B
 for n being Element of NAT ex k being Element of NAT st x in B . (n + k)
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (n + k)
consider k being Element of NAT  such that
A4: not x in A . (n + k) by A3, Th4;
take  k ; ::_thesis: x in B . (n + k)
 x in C \+\ (A . (n + k)) by A3, A4, XBOOLE_0:1;
hence  x in B . (n + k) by A1; ::_thesis: verum
end;
hence  x in lim_sup B by Th5; ::_thesis: verum
end;
supposeA5: ( not x in C & x in lim_inf A ) ; ::_thesis: x in lim_sup B
then consider n being Element of NAT  such that
A6: for k being Element of NAT holds x in A . (n + k) by Th4;
 for m being Element of NAT ex k being Element of NAT st x in B . (m + k)
proof
let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k)
take k = n; ::_thesis: x in B . (m + k)
 x in A . (m + k) by A6;
then  x in C \+\ (A . (m + k)) by A5, XBOOLE_0:1;
hence  x in B . (m + k) by A1; ::_thesis: verum
end;
hence  x in lim_sup B by Th5; ::_thesis: verum
end;
end;
end;

theorem :: KURATO_0:17
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
let X be set ; ::_thesis: 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
let A, B be SetSequence of X; ::_thesis: 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
let C be Subset of X; ::_thesis: ( ( for n being Element of NAT holds B . n = C \+\ (A . n) ) implies C \+\ (lim_sup A) c= lim_sup B )
assume A1: for n being Element of NAT holds B . n = C \+\ (A . n) ; ::_thesis: C \+\ (lim_sup A) c= lim_sup B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C \+\ (lim_sup A) or x in lim_sup B )
assume A2: x in C \+\ (lim_sup A) ; ::_thesis: x in lim_sup B
percases ( ( x in C & not x in lim_sup A ) or ( not x in C & x in lim_sup A ) ) by A2, XBOOLE_0:1;
supposeA3: ( x in C & not x in lim_sup A ) ; ::_thesis: x in lim_sup B
then consider n being Element of NAT  such that
A4: for k being Element of NAT holds not x in A . (n + k) by Th5;
 for m being Element of NAT ex k being Element of NAT st x in B . (m + k)
proof
let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k)
take k = n; ::_thesis: x in B . (m + k)
 not x in A . (m + k) by A4;
then  x in C \+\ (A . (m + k)) by A3, XBOOLE_0:1;
hence  x in B . (m + k) by A1; ::_thesis: verum
end;
hence  x in lim_sup B by Th5; ::_thesis: verum
end;
supposeA5: ( not x in C & x in lim_sup A ) ; ::_thesis: x in lim_sup B
 for m being Element of NAT ex k being Element of NAT st x in B . (m + k)
proof
let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k)
consider k being Element of NAT  such that
A6: x in A . (m + k) by A5, Th5;
take  k ; ::_thesis: x in B . (m + k)
 x in C \+\ (A . (m + k)) by A5, A6, XBOOLE_0:1;
hence  x in B . (m + k) by A1; ::_thesis: verum
end;
hence  x in lim_sup B by Th5; ::_thesis: verum
end;
end;
end;

begin

theorem Th18: :: KURATO_0:18
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
let f be Function; ::_thesis: ( ( for i being Element of NAT holds f . (i + 1) c= f . i ) implies for i, j being Element of NAT st i <= j holds
f . j c= f . i )
assume A1: for i being Element of NAT holds f . (i + 1) c= f . i ; ::_thesis: for i, j being Element of NAT st i <= j holds
f . j c= f . i
let i, j be Element of NAT ; ::_thesis: ( i <= j implies f . j c= f . i )
defpred S1[ Element of NAT ] means ( i + $1 <= j implies f . (i + $1) c= f . i );
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
A4: (i + k) + 1 = i + (k + 1) ;
then  f . (i + (k + 1)) c= f . (i + k) by A1;
hence  S1[k + 1] by A4, A3, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
A5: S1[ 0 ] ;
A6: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2);
assume  i <= j ; ::_thesis: f . j c= f . i
then consider k being Nat such that
A7: i + k = j by NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  f . j c= f . i by A6, A7; ::_thesis: verum
end;

definition
let T be set ;
let S be SetSequence of T;
:: original: non-ascending
redefine attrS is non-ascending  means :Def3: :: KURATO_0:def 3
 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
thus  ( S is non-ascending implies for i being Element of NAT holds S . (i + 1) c= S . i ) ::_thesis: ( ( for i being Element of NAT holds S . (i + 1) c= S . i ) implies S is non-ascending )
proof
assume A1: S is non-ascending ; ::_thesis: for i being Element of NAT holds S . (i + 1) c= S . i
let i be Element of NAT ; ::_thesis: S . (i + 1) c= S . i
 i <= i + 1 by NAT_1:13;
hence  S . (i + 1) c= S . i by A1, PROB_1:def_4; ::_thesis: verum
end;
assume  for i being Element of NAT holds S . (i + 1) c= S . i ; ::_thesis: S is non-ascending
then  for i, j being Element of NAT st i <= j holds
S . j c= S . i by Th18;
hence  S is non-ascending by PROB_1:def_4; ::_thesis: verum
end;
:: original: non-descending
redefine attrS is non-descending  means :Def4: :: KURATO_0:def 4
 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
thus  ( S is non-descending implies for i being Element of NAT holds S . i c= S . (i + 1) ) ::_thesis: ( ( for i being Element of NAT holds S . i c= S . (i + 1) ) implies S is non-descending )
proof
assume A2: S is non-descending ; ::_thesis: for i being Element of NAT holds S . i c= S . (i + 1)
let i be Element of NAT ; ::_thesis: S . i c= S . (i + 1)
 i <= i + 1 by NAT_1:13;
hence  S . i c= S . (i + 1) by A2, PROB_1:def_5; ::_thesis: verum
end;
assume  for i being Element of NAT holds S . i c= S . (i + 1) ; ::_thesis: S is non-descending
then  for i, j being Element of NAT st i <= j holds
S . i c= S . j by MEASURE2:18;
hence  S is non-descending by PROB_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines non-ascending KURATO_0:def_3_:_
 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 Def4 defines non-descending KURATO_0:def_4_:_
 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 Th19: :: KURATO_0:19
for T being set
for F being SetSequence of T
for x being set st F is V50() & 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
let T be set ; ::_thesis: for F being SetSequence of T
for x being set st F is V50() & 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
let F be SetSequence of T; ::_thesis: for x being set st F is V50() & 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
let x be set ; ::_thesis: ( F is V50() & ex k being Element of NAT st
for n being Element of NAT st n > k holds
x in F . n implies x in meet F )
assume A1: F is V50() ; ::_thesis: ( for k being Element of NAT ex n being Element of NAT st
( n > k & not x in F . n ) or x in meet F )
given k being Element of NAT  such that A2: for n being Element of NAT st n > k holds
x in F . n ; ::_thesis: x in meet F
 k + 1 > k by NAT_1:13;
then A3: x in F . (k + 1) by A2;
assume  not x in meet F ; ::_thesis: contradiction
then  not x in meet (rng F) by FUNCT_6:def_4;
then consider Y being set  such that
A4: Y in rng F and
A5: not x in Y by SETFAM_1:def_1;
consider y being set  such that
A6: y in dom F and
A7: Y = F . y by A4, FUNCT_1:def_3;
reconsider y = y as Element of NAT by A6;
percases ( y > k or y <= k ) ;
suppose y > k ; ::_thesis: contradiction
hence  contradiction by A2, A5, A7; ::_thesis: verum
end;
suppose y <= k ; ::_thesis: contradiction
then  F . k c= F . y by A1, PROB_1:def_4;
then A8: not x in F . k by A5, A7;
 F . (k + 1) c= F . k by A1, Def3;
hence  contradiction by A3, A8; ::_thesis: verum
end;
end;
end;

theorem :: KURATO_0:20
for T being set
for F being SetSequence of T st F is V50() holds
lim_inf F = meet F
proof
let T be set ; ::_thesis: for F being SetSequence of T st F is V50() holds
lim_inf F = meet F
let F be SetSequence of T; ::_thesis: ( F is V50() implies lim_inf F = meet F )
assume A1: F is V50() ; ::_thesis: lim_inf F = meet F
thus  lim_inf F c= meet F :: according to XBOOLE_0:def_10 ::_thesis: meet F c= lim_inf F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf F or x in meet F )
assume  x in lim_inf F ; ::_thesis: x in meet F
then consider n being Element of NAT  such that
A2: for k being Element of NAT holds x in F . (n + k) by Th4;
 for k being Element of NAT st k > n holds
x in F . k
proof
let k be Element of NAT ; ::_thesis: ( k > n implies x in F . k )
assume  k > n ; ::_thesis: x in F . k
then consider h being Nat such that
A3: k = n + h by NAT_1:10;
 h in NAT by ORDINAL1:def_12;
hence  x in F . k by A2, A3; ::_thesis: verum
end;
hence  x in meet F by A1, Th19; ::_thesis: verum
end;
thus  meet F c= lim_inf F by Th7; ::_thesis: verum
end;

theorem :: KURATO_0:21
for T being set
for F being SetSequence of T st F is V51() holds
lim_sup F = Union F
proof
let T be set ; ::_thesis: for F being SetSequence of T st F is V51() holds
lim_sup F = Union F
let F be SetSequence of T; ::_thesis: ( F is V51() implies lim_sup F = Union F )
assume A1: F is V51() ; ::_thesis: lim_sup F = Union F
thus  lim_sup F c= Union F by Th8; :: according to XBOOLE_0:def_10 ::_thesis: Union F c= lim_sup F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union F or x in lim_sup F )
assume  x in Union F ; ::_thesis: x in lim_sup F
then consider n being Element of NAT  such that
A2: x in F . n by PROB_1:12;
assume  not x in lim_sup F ; ::_thesis: contradiction
then consider m being Element of NAT  such that
A3: for k being Element of NAT holds not x in F . (m + k) by Th5;
A4: not x in F . (m + 0) by A3;
percases ( n <= m or n > m ) ;
suppose n <= m ; ::_thesis: contradiction
then  F . n c= F . m by A1, PROB_1:def_5;
hence  contradiction by A2, A4; ::_thesis: verum
end;
suppose n > m ; ::_thesis: contradiction
then consider h being Nat such that
A5: n = m + h by NAT_1:10;
 h in NAT by ORDINAL1:def_12;
hence  contradiction by A2, A3, A5; ::_thesis: verum
end;
end;
end;

begin

definition
let T be set ;
let S be SetSequence of T;
attrS is convergent  means :Def5: :: KURATO_0:def 5
 lim_sup S = lim_inf S;
end;

:: deftheorem Def5 defines convergent KURATO_0:def_5_:_
 for T being set
for S being SetSequence of T holds
( S is convergent iff lim_sup S = lim_inf S );

theorem :: KURATO_0:22
for T being set
for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T
proof
let T be set ; ::_thesis: for S being SetSequence of T st S is constant holds
the_value_of S is Subset of T
let S be SetSequence of T; ::_thesis: ( S is constant implies the_value_of S is Subset of T )
assume  S is constant ; ::_thesis: the_value_of S is Subset of T
then consider x being set  such that
A1: x in dom S and
A2: the_value_of S = S . x by FUNCT_1:def_12;
reconsider n = x as Element of NAT by A1;
 S . n in bool T ;
hence  the_value_of S is Subset of T by A2; ::_thesis: verum
end;

registration
let T be set ;
cluster Function-like constant V33( NAT , bool T)  -> V50() V51() convergent for Element of bool [:NAT,(bool T):];
coherence
 for b1 being SetSequence of T st b1 is constant holds
( b1 is convergent & b1 is V51() & b1 is V50() )
proof
let S be SetSequence of T; ::_thesis: ( S is constant implies ( S is convergent & S is V51() & S is V50() ) )
assume  S is constant ; ::_thesis: ( S is convergent & S is V51() & S is V50() )
then consider A being Subset of T such that
A1: for n being Nat holds S . n = A by VALUED_0:def_18;
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_S_._(n_+_1)_c=_S_._n
let n be Element of NAT ; ::_thesis: S . (n + 1) c= S . n
 S . n = A by A1;
hence  S . (n + 1) c= S . n by A1; ::_thesis: verum
end;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_S_._n_c=_S_._(n_+_1)
let n be Element of NAT ; ::_thesis: S . n c= S . (n + 1)
 S . n = A by A1;
hence  S . n c= S . (n + 1) by A1; ::_thesis: verum
end;
 ( lim_sup S = A & lim_inf S = A ) by A1, Th14, Th15;
hence  ( S is convergent & S is V51() & S is V50() ) by A3, A2, Def3, Def4, Def5; ::_thesis: verum
end;
end;

registration
let T be set ;
cluster non empty Relation-like NAT -defined bool T -valued Function-like constant V29( NAT ) V33( NAT , bool T) for Element of bool [:NAT,(bool T):];
existence
 ex b1 being SetSequence of T st
( b1 is constant & not b1 is empty )
proof
reconsider E = NAT --> ({} T) as SetSequence of T ;
 E is constant ;
hence  ex b1 being SetSequence of T st
( b1 is constant & not b1 is empty ) ; ::_thesis: verum
end;
end;

notation
let T be set ;
let S be convergent SetSequence of T;
synonym  Lim_K S for  lim_sup S;
end;

theorem :: KURATO_0:23
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
let X be set ; ::_thesis: 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) )
let F be convergent SetSequence of X; ::_thesis: 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) )
let x be set ; ::_thesis: ( 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) )
 Lim_K F = lim_inf F by Def5;
hence  ( 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) ) by Th4; ::_thesis: verum
end;