:: SETLIM_1 semantic presentation

begin

                       Lm1:  for i, j being Element of NAT holds
( not i <= j or i = j or i + 1 <= j )
proof
let i, j be Element of NAT ; ::_thesis: ( not i <= j or i = j or i + 1 <= j )
assume  i <= j ; ::_thesis: ( i = j or i + 1 <= j )
then  i + 1 <= j + 1 by XREAL_1:6;
hence  ( i = j or i + 1 <= j ) by NAT_1:8, XCMPLX_1:2; ::_thesis: verum
end;

theorem Th1: :: SETLIM_1:1
for n, m being Element of NAT
for Y being set
for f being Function of NAT,Y holds f . (n + m) in  {  (f . k) where k is Element of NAT : n <= k  }
proof
let n, m be Element of NAT ; ::_thesis: for Y being set
for f being Function of NAT,Y holds f . (n + m) in  {  (f . k) where k is Element of NAT : n <= k  }
let Y be set ; ::_thesis: for f being Function of NAT,Y holds f . (n + m) in  {  (f . k) where k is Element of NAT : n <= k  }
 n <= n + m by NAT_1:11;
hence  for f being Function of NAT,Y holds f . (n + m) in  {  (f . k) where k is Element of NAT : n <= k  }  ; ::_thesis: verum
end;

theorem Th2: :: SETLIM_1:2
for n being Element of NAT
for Y being set
for f being Function of NAT,Y holds  {  (f . k1) where k1 is Element of NAT : n <= k1  }  =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
proof
let n be Element of NAT ; ::_thesis: for Y being set
for f being Function of NAT,Y holds  {  (f . k1) where k1 is Element of NAT : n <= k1  }  =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
let Y be set ; ::_thesis: for f being Function of NAT,Y holds  {  (f . k1) where k1 is Element of NAT : n <= k1  }  =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
let f be Function of NAT,Y; ::_thesis:  {  (f . k1) where k1 is Element of NAT : n <= k1  }  =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
set Z1 =  {  (f . k1) where k1 is Element of NAT : n <= k1  }  ;
set Z2 =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  ;
A1:  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)} c=  {  (f . k1) where k1 is Element of NAT : n <= k1  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)} or x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  )
assume A2: x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)} ; ::_thesis: x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }
now__::_thesis:_(_(_x_in__{__(f_._k2)_where_k2_is_Element_of_NAT_:_n_+_1_<=_k2__}__&_x_in__{__(f_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}__)_or_(_x_in_{(f_._n)}_&_x_in__{__(f_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}__)_)
percases ( x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  or x in {(f . n)} ) by A2, XBOOLE_0:def_3;
case x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  ; ::_thesis: x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }
then consider z being set  such that
A3: x = z and
A4: z in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  ;
consider k11 being Element of NAT  such that
A5: z = f . k11 and
A6: n + 1 <= k11 by A4;
 n <= k11 by A6, NAT_1:13;
hence  x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  by A3, A5; ::_thesis: verum
end;
case x in {(f . n)} ; ::_thesis: x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }
then  x = f . n by TARSKI:def_1;
hence  x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  ; ::_thesis: verum
end;
end;
end;
hence  x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  ; ::_thesis: verum
end;
  {  (f . k1) where k1 is Element of NAT : n <= k1  }  c=  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  or x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)} )
assume  x in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  ; ::_thesis: x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)}
then consider z being set  such that
A7: x = z and
A8: z in  {  (f . k1) where k1 is Element of NAT : n <= k1  }  ;
consider k being Element of NAT  such that
A9: ( z = f . k & n <= k ) by A8;
 ( ( z = f . k & n + 1 <= k ) or ( z = f . k & n = k ) ) by A9, Lm1;
then  ( z in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  or z in {(f . n)} ) by TARSKI:def_1;
hence  x in  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)} by A7, XBOOLE_0:def_3; ::_thesis: verum
end;
hence   {  (f . k1) where k1 is Element of NAT : n <= k1  }  =  {  (f . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(f . n)} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th3: :: SETLIM_1:3
for n being Element of NAT
for Y, x being set
for f being Function of NAT,Y holds
( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z )
proof
let n be Element of NAT ; ::_thesis: for Y, x being set
for f being Function of NAT,Y holds
( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z )
let Y, x be set ; ::_thesis: for f being Function of NAT,Y holds
( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z )
let f be Function of NAT,Y; ::_thesis: ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z )
set Z =  {  (f . k2) where k2 is Element of NAT : n <= k2  }  ;
now__::_thesis:_(_(_for_k1_being_Element_of_NAT_holds_x_in_f_._(n_+_k1)_)_implies_for_Z1_being_set_st_Z1_in__{__(f_._k2)_where_k2_is_Element_of_NAT_:_n_<=_k2__}__holds_
x_in_Z1_)
assume A1: for k1 being Element of NAT holds x in f . (n + k1) ; ::_thesis: for Z1 being set st Z1 in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z1
now__::_thesis:_for_Z1_being_set_st_Z1_in__{__(f_._k2)_where_k2_is_Element_of_NAT_:_n_<=_k2__}__holds_
x_in_Z1
let Z1 be set ; ::_thesis: ( Z1 in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  implies x in Z1 )
assume  Z1 in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  ; ::_thesis: x in Z1
then consider k1 being Element of NAT  such that
A2: Z1 = f . k1 and
A3: n <= k1 ;
 ex m being Nat st k1 = n + m by A3, NAT_1:10;
then consider k2 being Nat such that
A4: Z1 = f . (n + k2) by A2;
 k2 in NAT by ORDINAL1:def_12;
hence  x in Z1 by A1, A4; ::_thesis: verum
end;
hence  for Z1 being set st Z1 in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z1 ; ::_thesis: verum
end;
hence  ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in  {  (f . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z ) by Th1; ::_thesis: verum
end;

theorem Th4: :: SETLIM_1:4
for x being set
for Y being non empty set
for f being Function of NAT,Y holds
( x in rng f iff ex n being Element of NAT st x = f . n )
proof
let x be set ; ::_thesis: for Y being non empty set
for f being Function of NAT,Y holds
( x in rng f iff ex n being Element of NAT st x = f . n )
let Y be non empty set ; ::_thesis: for f being Function of NAT,Y holds
( x in rng f iff ex n being Element of NAT st x = f . n )
let f be Function of NAT,Y; ::_thesis: ( x in rng f iff ex n being Element of NAT st x = f . n )
thus  ( x in rng f implies ex n being Element of NAT st x = f . n ) ::_thesis: ( ex n being Element of NAT st x = f . n implies x in rng f )
proof
assume  x in rng f ; ::_thesis: ex n being Element of NAT st x = f . n
then consider y being set  such that
A1: y in dom f and
A2: x = f . y by FUNCT_1:def_3;
reconsider m = y as Element of NAT by A1;
take  m ; ::_thesis: x = f . m
thus  x = f . m by A2; ::_thesis: verum
end;
given n being Element of NAT  such that A3: x = f . n ; ::_thesis: x in rng f
 dom f = NAT by FUNCT_2:def_1;
hence  x in rng f by A3, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th5: :: SETLIM_1:5
for Y being non empty set
for f being Function of NAT,Y holds rng f =  {  (f . k) where k is Element of NAT : 0 <= k  }
proof
let Y be non empty set ; ::_thesis: for f being Function of NAT,Y holds rng f =  {  (f . k) where k is Element of NAT : 0 <= k  }
let f be Function of NAT,Y; ::_thesis: rng f =  {  (f . k) where k is Element of NAT : 0 <= k  }
set Z =  {  (f . k) where k is Element of NAT : 0 <= k  }  ;
A1: dom f = NAT by FUNCT_2:def_1;
A2: rng f c=  {  (f . k) where k is Element of NAT : 0 <= k  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in  {  (f . k) where k is Element of NAT : 0 <= k  }  )
assume  y in rng f ; ::_thesis: y in  {  (f . k) where k is Element of NAT : 0 <= k  }
then consider n being set  such that
A3: n in NAT and
A4: y = f . n by A1, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A3;
 0 <= n by NAT_1:2;
hence  y in  {  (f . k) where k is Element of NAT : 0 <= k  }  by A4; ::_thesis: verum
end;
  {  (f . k) where k is Element of NAT : 0 <= k  }  c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f . k) where k is Element of NAT : 0 <= k  }  or x in rng f )
assume  x in  {  (f . k) where k is Element of NAT : 0 <= k  }  ; ::_thesis: x in rng f
then  ex n1 being Element of NAT st
( x = f . n1 & 0 <= n1 ) ;
hence  x in rng f by FUNCT_2:4; ::_thesis: verum
end;
hence  rng f =  {  (f . k) where k is Element of NAT : 0 <= k  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th6: :: SETLIM_1:6
for k being Element of NAT
for Y being non empty set
for f being Function of NAT,Y holds rng (f ^\ k) =  {  (f . n) where n is Element of NAT : k <= n  }
proof
let k be Element of NAT ; ::_thesis: for Y being non empty set
for f being Function of NAT,Y holds rng (f ^\ k) =  {  (f . n) where n is Element of NAT : k <= n  }
let Y be non empty set ; ::_thesis: for f being Function of NAT,Y holds rng (f ^\ k) =  {  (f . n) where n is Element of NAT : k <= n  }
let f be Function of NAT,Y; ::_thesis: rng (f ^\ k) =  {  (f . n) where n is Element of NAT : k <= n  }
reconsider f1 = f ^\ k as Function of NAT,Y ;
 rng f1 =  {  (f . m) where m is Element of NAT : k <= m  }
proof
set Z =  {  (f . m) where m is Element of NAT : k <= m  }  ;
A1: dom f1 = NAT by FUNCT_2:def_1;
A2: rng f1 c=  {  (f . m) where m is Element of NAT : k <= m  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f1 or y in  {  (f . m) where m is Element of NAT : k <= m  }  )
assume  y in rng f1 ; ::_thesis: y in  {  (f . m) where m is Element of NAT : k <= m  }
then consider m1 being set  such that
A3: m1 in NAT and
A4: y = f1 . m1 by A1, FUNCT_1:def_3;
reconsider m1 = m1 as Element of NAT by A3;
 y = f . (k + m1) by A4, NAT_1:def_3;
hence  y in  {  (f . m) where m is Element of NAT : k <= m  }  by Th1; ::_thesis: verum
end;
  {  (f . m) where m is Element of NAT : k <= m  }  c= rng f1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f . m) where m is Element of NAT : k <= m  }  or x in rng f1 )
assume  x in  {  (f . m) where m is Element of NAT : k <= m  }  ; ::_thesis: x in rng f1
then consider k1 being Element of NAT  such that
A5: x = f . k1 and
A6: k <= k1 ;
consider k2 being Nat such that
A7: k1 = k + k2 by A6, NAT_1:10;
 ( k2 in NAT & x = f1 . k2 ) by A5, A7, NAT_1:def_3, ORDINAL1:def_12;
hence  x in rng f1 by FUNCT_2:4; ::_thesis: verum
end;
hence  rng f1 =  {  (f . m) where m is Element of NAT : k <= m  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  rng (f ^\ k) =  {  (f . n) where n is Element of NAT : k <= n  }  ; ::_thesis: verum
end;

theorem Th7: :: SETLIM_1:7
for X, x being set
for B being SetSequence of X holds
( x in meet (rng B) iff for n being Element of NAT holds x in B . n )
proof
let X, x be set ; ::_thesis: for B being SetSequence of X holds
( x in meet (rng B) iff for n being Element of NAT holds x in B . n )
let B be SetSequence of X; ::_thesis: ( x in meet (rng B) iff for n being Element of NAT holds x in B . n )
A1: dom B = NAT by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_(_for_n_being_Element_of_NAT_holds_x_in_B_._n_)_holds_
x_in_meet_(rng_B)
let x be set ; ::_thesis: ( ( for n being Element of NAT holds x in B . n ) implies x in meet (rng B) )
assume A3: for n being Element of NAT holds x in B . n ; ::_thesis: x in meet (rng B)
now__::_thesis:_for_Y_being_set_st_Y_in_rng_B_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in rng B implies x in Y )
assume  Y in rng B ; ::_thesis: x in Y
then consider n being set  such that
A4: n in NAT and
A5: Y = B . n by A1, FUNCT_1:def_3;
thus  x in Y by A3, A4, A5; ::_thesis: verum
end;
hence  x in meet (rng B) by SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_B)_holds_
for_n_being_Element_of_NAT_holds_x_in_B_._n
let x be set ; ::_thesis: ( x in meet (rng B) implies for n being Element of NAT holds x in B . n )
assume A6: x in meet (rng B) ; ::_thesis: for n being Element of NAT holds x in B . n
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_B_._k
let k be Element of NAT ; ::_thesis: x in B . k
 B . k in rng B by FUNCT_2:4;
hence  x in B . k by A6, SETFAM_1:def_1; ::_thesis: verum
end;
hence  for n being Element of NAT holds x in B . n ; ::_thesis: verum
end;
hence  ( x in meet (rng B) iff for n being Element of NAT holds x in B . n ) by A2; ::_thesis: verum
end;

theorem Th8: :: SETLIM_1:8
for X being set
for B being SetSequence of X holds Intersection B = meet (rng B)
proof
let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B = meet (rng B)
let B be SetSequence of X; ::_thesis: Intersection B = meet (rng B)
now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_B)_holds_
x_in_Intersection_B
let x be set ; ::_thesis: ( x in meet (rng B) implies x in Intersection B )
assume  x in meet (rng B) ; ::_thesis: x in Intersection B
then  for n being Element of NAT holds x in B . n by Th7;
hence  x in Intersection B by PROB_1:13; ::_thesis: verum
end;
then A1: meet (rng B) c= Intersection B by TARSKI:def_3;
 Intersection B c= meet (rng B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection B or x in meet (rng B) )
assume  x in Intersection B ; ::_thesis: x in meet (rng B)
then  for n being Element of NAT holds x in B . n by PROB_1:13;
hence  x in meet (rng B) by Th7; ::_thesis: verum
end;
hence  Intersection B = meet (rng B) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETLIM_1:9
for X being set
for B being SetSequence of X holds Intersection B c= Union B
proof
let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B c= Union B
let B be SetSequence of X; ::_thesis: Intersection B c= Union B
 meet (rng B) c= union (rng B) by SETFAM_1:2;
then  Intersection B c= union (rng B) by Th8;
hence  Intersection B c= Union B by CARD_3:def_4; ::_thesis: verum
end;

theorem Th10: :: SETLIM_1:10
for X being set
for A being Subset of X
for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Union B = A
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Union B = A
let A be Subset of X; ::_thesis: for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Union B = A
let B be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds B . n = A ) implies Union B = A )
assume A1: for n being Element of NAT holds B . n = A ; ::_thesis: Union B = A
now__::_thesis:_for_x_being_set_st_x_in_rng_B_holds_
x_=_A
let x be set ; ::_thesis: ( x in rng B implies x = A )
assume  x in rng B ; ::_thesis: x = A
then  ex n being Element of NAT st x = B . n by Th4;
hence  x = A by A1; ::_thesis: verum
end;
then  rng B = {A} by ZFMISC_1:35;
then  union (rng B) = A by ZFMISC_1:25;
hence  Union B = A by CARD_3:def_4; ::_thesis: verum
end;

theorem Th11: :: SETLIM_1:11
for X being set
for A being Subset of X
for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Intersection B = A
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Intersection B = A
let A be Subset of X; ::_thesis: for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds
Intersection B = A
let B be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds B . n = A ) implies Intersection B = A )
assume A1: for n being Element of NAT holds B . n = A ; ::_thesis: Intersection B = A
now__::_thesis:_for_x_being_set_st_x_in_rng_B_holds_
x_=_A
let x be set ; ::_thesis: ( x in rng B implies x = A )
assume  x in rng B ; ::_thesis: x = A
then  ex n being Element of NAT st x = B . n by Th4;
hence  x = A by A1; ::_thesis: verum
end;
then  rng B = {A} by ZFMISC_1:35;
then  meet (rng B) = A by SETFAM_1:10;
hence  Intersection B = A by Th8; ::_thesis: verum
end;

theorem :: SETLIM_1:12
for X being set
for B being SetSequence of X st B is constant holds
Union B = Intersection B
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is constant holds
Union B = Intersection B
let B be SetSequence of X; ::_thesis: ( B is constant implies Union B = Intersection B )
assume  B is constant ; ::_thesis: Union B = Intersection B
then consider A being Subset of X such that
A1: for n being Nat holds B . n = A by VALUED_0:def_18;
A2: for n being Element of NAT holds B . n = A by A1;
then  Union B = A by Th10;
hence  Union B = Intersection B by A2, Th11; ::_thesis: verum
end;

Lm2:  for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A ) )
assume that
A1: B is constant and
A2: the_value_of B = A ; ::_thesis: for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A )
consider x being set  such that
A3: x in dom B and
A4: A = B . x by A1, A2, FUNCT_1:def_12;
 dom B = NAT by FUNCT_2:def_1;
then  for n being Element of NAT holds B . n = A by A1, A3, A4, FUNCT_1:def_10;
hence  for n being Element of NAT holds
( B . n = A & Union B = A & Intersection B = A ) by Th10, Th11; ::_thesis: verum
end;

theorem Th13: :: SETLIM_1:13
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds union  {  (B . k) where k is Element of NAT : n <= k  }  = A
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds union  {  (B . k) where k is Element of NAT : n <= k  }  = A
let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds union  {  (B . k) where k is Element of NAT : n <= k  }  = A
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds union  {  (B . k) where k is Element of NAT : n <= k  }  = A )
assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds union  {  (B . k) where k is Element of NAT : n <= k  }  = A
let n be Element of NAT ; ::_thesis: union  {  (B . k) where k is Element of NAT : n <= k  }  = A
set Y =  {  (B . k) where k is Element of NAT : n <= k  }  ;
A2: now__::_thesis:_for_x_being_set_st_x_in__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_=_A
let x be set ; ::_thesis: ( x in  {  (B . k) where k is Element of NAT : n <= k  }  implies x = A )
assume  x in  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: x = A
then  ex k being Element of NAT st
( x = B . k & n <= k ) ;
hence  x = A by A1, Lm2; ::_thesis: verum
end;
  {  (B . k) where k is Element of NAT : n <= k  }  <> {} by Th1;
then   {  (B . k) where k is Element of NAT : n <= k  }  = {A} by A2, ZFMISC_1:35;
hence  union  {  (B . k) where k is Element of NAT : n <= k  }  = A by ZFMISC_1:25; ::_thesis: verum
end;

theorem Th14: :: SETLIM_1:14
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds meet  {  (B . k) where k is Element of NAT : n <= k  }  = A
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds meet  {  (B . k) where k is Element of NAT : n <= k  }  = A
let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds meet  {  (B . k) where k is Element of NAT : n <= k  }  = A
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds meet  {  (B . k) where k is Element of NAT : n <= k  }  = A )
assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds meet  {  (B . k) where k is Element of NAT : n <= k  }  = A
let n be Element of NAT ; ::_thesis: meet  {  (B . k) where k is Element of NAT : n <= k  }  = A
set Y =  {  (B . k) where k is Element of NAT : n <= k  }  ;
A2: now__::_thesis:_for_x_being_set_st_x_in__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_=_A
let x be set ; ::_thesis: ( x in  {  (B . k) where k is Element of NAT : n <= k  }  implies x = A )
assume  x in  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: x = A
then  ex k being Element of NAT st
( x = B . k & n <= k ) ;
hence  x = A by A1, Lm2; ::_thesis: verum
end;
  {  (B . k) where k is Element of NAT : n <= k  }  <> {} by Th1;
then   {  (B . k) where k is Element of NAT : n <= k  }  = {A} by A2, ZFMISC_1:35;
hence  meet  {  (B . k) where k is Element of NAT : n <= k  }  = A by SETFAM_1:10; ::_thesis: verum
end;

theorem Th15: :: SETLIM_1:15
for X being set
for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is SetSequence of X
proof
let X be set ; ::_thesis: for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is SetSequence of X
let B be SetSequence of X; ::_thesis: for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is SetSequence of X
let f be Function; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) implies f is SetSequence of X )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: f is SetSequence of X
 rng f c= bool X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in bool X )
assume  z in rng f ; ::_thesis: z in bool X
then consider x being set  such that
A3: x in dom f and
A4: z = f . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A1, A3;
set Y =  {  (B . k) where k is Element of NAT : n <= k  }  ;
set y = meet  {  (B . k) where k is Element of NAT : n <= k  }  ;
A5: meet  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X
proof
A6: now__::_thesis:_(__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__<>_{}_implies_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__is_Subset_of_X_)
assume   {  (B . k) where k is Element of NAT : n <= k  }  <> {} ; ::_thesis: meet  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X
then consider Z1 being set  such that
A7: Z1 in  {  (B . k) where k is Element of NAT : n <= k  }  by XBOOLE_0:def_1;
A8: ex k1 being Element of NAT st
( Z1 = B . k1 & n <= k1 ) by A7;
now__::_thesis:_for_x_being_set_st_x_in_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in_X
let x be set ; ::_thesis: ( x in meet  {  (B . k) where k is Element of NAT : n <= k  }  implies x in X )
assume  x in meet  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: x in X
then  x in Z1 by A7, SETFAM_1:def_1;
hence  x in X by A8; ::_thesis: verum
end;
hence  meet  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X by TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_(__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__=_{}_implies_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__is_Subset_of_X_)
assume   {  (B . k) where k is Element of NAT : n <= k  }  = {} ; ::_thesis: meet  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X
then  meet  {  (B . k) where k is Element of NAT : n <= k  }  = {} by SETFAM_1:def_1;
hence  meet  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X by XBOOLE_1:2; ::_thesis: verum
end;
hence  meet  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X by A6; ::_thesis: verum
end;
 z = meet  {  (B . k) where k is Element of NAT : n <= k  }  by A2, A4;
hence  z in bool X by A5; ::_thesis: verum
end;
hence  f is SetSequence of X by A1, FUNCT_2:2; ::_thesis: verum
end;

theorem Th16: :: SETLIM_1:16
for X being set
for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is Function of NAT,(bool X)
proof
let X be set ; ::_thesis: for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is Function of NAT,(bool X)
let B be SetSequence of X; ::_thesis: for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
f is Function of NAT,(bool X)
let f be Function; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) implies f is Function of NAT,(bool X) )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: f is Function of NAT,(bool X)
 rng f c= bool X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in bool X )
assume  z in rng f ; ::_thesis: z in bool X
then consider x being set  such that
A3: x in dom f and
A4: z = f . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A1, A3;
set Y =  {  (B . k) where k is Element of NAT : n <= k  }  ;
set y = union  {  (B . k) where k is Element of NAT : n <= k  }  ;
now__::_thesis:_for_z_being_set_st_z_in_union__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
z_in_X
let z be set ; ::_thesis: ( z in union  {  (B . k) where k is Element of NAT : n <= k  }  implies z in X )
assume  z in union  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: z in X
then  ex Z being set st
( z in Z & Z in  {  (B . k) where k is Element of NAT : n <= k  }  ) by TARSKI:def_4;
then consider Z1 being set  such that
A5: Z1 in  {  (B . k) where k is Element of NAT : n <= k  }  and
A6: z in Z1 ;
 ex k1 being Element of NAT st
( Z1 = B . k1 & n <= k1 ) by A5;
hence  z in X by A6; ::_thesis: verum
end;
then A7: union  {  (B . k) where k is Element of NAT : n <= k  }  is Subset of X by TARSKI:def_3;
 z = union  {  (B . k) where k is Element of NAT : n <= k  }  by A2, A4;
hence  z in bool X by A7; ::_thesis: verum
end;
hence  f is Function of NAT,(bool X) by A1, FUNCT_2:2; ::_thesis: verum
end;

definition
let X be set ;
let B be SetSequence of X;
attrB is monotone  means :Def1: :: SETLIM_1:def 1
( not B is V50() or not B is V49() );
end;

:: deftheorem Def1 defines monotone SETLIM_1:def_1_:_
 for X being set
for B being SetSequence of X holds
( B is monotone iff ( not B is V50() or not B is V49() ) );

definition
let B be Function;
func inferior_setsequence B ->  Function means :Def2: :: SETLIM_1:def 2
( dom it = NAT & ( for n being Element of NAT holds it . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) );
existence
 ex b1 being Function st
( dom b1 = NAT & ( for n being Element of NAT holds b1 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) )
proof
deffunc H1( Nat) ->  set = meet  {  (B . k) where k is Element of NAT : $1 <= k  }  ;
thus  ex f being Function st
( dom f = NAT & ( for n being Element of NAT holds f . n = H1(n) ) ) from FUNCT_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = NAT & ( for n being Element of NAT holds b1 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) & dom b2 = NAT & ( for n being Element of NAT holds b2 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
b1 = b2
proof
let BSeq, CSeq be Function; ::_thesis: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) & dom CSeq = NAT & ( for n being Element of NAT holds CSeq . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) implies BSeq = CSeq )
assume that
A1: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) ) and
A2: ( dom CSeq = NAT & ( for m being Element of NAT holds CSeq . m = meet  {  (B . k) where k is Element of NAT : m <= k  }  ) ) ; ::_thesis: BSeq = CSeq
 for y being set st y in NAT holds
BSeq . y = CSeq . y
proof
let y be set ; ::_thesis: ( y in NAT implies BSeq . y = CSeq . y )
assume  y in NAT ; ::_thesis: BSeq . y = CSeq . y
then reconsider y = y as Element of NAT ;
set Y =  {  (B . k) where k is Element of NAT : y <= k  }  ;
 BSeq . y = meet  {  (B . k) where k is Element of NAT : y <= k  }  by A1;
hence  BSeq . y = CSeq . y by A2; ::_thesis: verum
end;
hence  BSeq = CSeq by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def_2_:_
 for B, b2 being Function holds
( b2 = inferior_setsequence B iff ( dom b2 = NAT & ( for n being Element of NAT holds b2 . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  ) ) );

definition
let X be set ;
let B be SetSequence of X;
:: original: inferior_setsequence
redefine func inferior_setsequence B ->  SetSequence of X;
coherence
 inferior_setsequence B is SetSequence of X
proof
A1: for n being Element of NAT holds (inferior_setsequence B) . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  by Def2;
 dom (inferior_setsequence B) = NAT by Def2;
hence  inferior_setsequence B is SetSequence of X by A1, Th15; ::_thesis: verum
end;
end;

definition
let B be Function;
func superior_setsequence B ->  Function means :Def3: :: SETLIM_1:def 3
( dom it = NAT & ( for n being Element of NAT holds it . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) );
existence
 ex b1 being Function st
( dom b1 = NAT & ( for n being Element of NAT holds b1 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) )
proof
deffunc H1( Nat) ->  set = union  {  (B . k) where k is Element of NAT : $1 <= k  }  ;
thus  ex f being Function st
( dom f = NAT & ( for n being Element of NAT holds f . n = H1(n) ) ) from FUNCT_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = NAT & ( for n being Element of NAT holds b1 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) & dom b2 = NAT & ( for n being Element of NAT holds b2 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) holds
b1 = b2
proof
let BSeq, CSeq be Function; ::_thesis: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) & dom CSeq = NAT & ( for n being Element of NAT holds CSeq . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) implies BSeq = CSeq )
assume that
A1: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) ) and
A2: ( dom CSeq = NAT & ( for m being Element of NAT holds CSeq . m = union  {  (B . k) where k is Element of NAT : m <= k  }  ) ) ; ::_thesis: BSeq = CSeq
 for y being set st y in NAT holds
BSeq . y = CSeq . y
proof
let y be set ; ::_thesis: ( y in NAT implies BSeq . y = CSeq . y )
assume  y in NAT ; ::_thesis: BSeq . y = CSeq . y
then reconsider y = y as Element of NAT ;
set Y =  {  (B . k) where k is Element of NAT : y <= k  }  ;
 BSeq . y = union  {  (B . k) where k is Element of NAT : y <= k  }  by A1;
hence  BSeq . y = CSeq . y by A2; ::_thesis: verum
end;
hence  BSeq = CSeq by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines superior_setsequence SETLIM_1:def_3_:_
 for B, b2 being Function holds
( b2 = superior_setsequence B iff ( dom b2 = NAT & ( for n being Element of NAT holds b2 . n = union  {  (B . k) where k is Element of NAT : n <= k  }  ) ) );

definition
let X be set ;
let B be SetSequence of X;
:: original: superior_setsequence
redefine func superior_setsequence B ->  SetSequence of X;
coherence
 superior_setsequence B is SetSequence of X
proof
A1: for n being Element of NAT holds (superior_setsequence B) . n = union  {  (B . k) where k is Element of NAT : n <= k  }  by Def3;
 dom (superior_setsequence B) = NAT by Def3;
hence  superior_setsequence B is SetSequence of X by A1, Th16; ::_thesis: verum
end;
end;

theorem Th17: :: SETLIM_1:17
for X being set
for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B
proof
let X be set ; ::_thesis: for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B
let B be SetSequence of X; ::_thesis: (inferior_setsequence B) . 0 = Intersection B
(inferior_setsequence B) . 0 = meet  {  (B . k) where k is Element of NAT : k >= 0  }  by Def2
.= meet (rng B) by Th5
.= Intersection B by Th8 ;
hence  (inferior_setsequence B) . 0 = Intersection B ; ::_thesis: verum
end;

theorem Th18: :: SETLIM_1:18
for X being set
for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B
proof
let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B
let B be SetSequence of X; ::_thesis: (superior_setsequence B) . 0 = Union B
(superior_setsequence B) . 0 = union  {  (B . k) where k is Element of NAT : 0 <= k  }  by Def3
.= union (rng B) by Th5
.= Union B by CARD_3:def_4 ;
hence  (superior_setsequence B) . 0 = Union B ; ::_thesis: verum
end;

theorem Th19: :: SETLIM_1:19
for n being Element of NAT
for X, x being set
for B being SetSequence of X holds
( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
proof
let n be Element of NAT ; ::_thesis: for X, x being set
for B being SetSequence of X holds
( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
let X, x be set ; ::_thesis: for B being SetSequence of X holds
( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
let B be SetSequence of X; ::_thesis: ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
set Y =  {  (B . k) where k is Element of NAT : n <= k  }  ;
A1: (inferior_setsequence B) . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  by Def2;
A2: now__::_thesis:_(_x_in_(inferior_setsequence_B)_._n_implies_for_k_being_Element_of_NAT_holds_x_in_B_._(n_+_k)_)
assume A3: x in (inferior_setsequence B) . n ; ::_thesis: for k being Element of NAT holds x in B . (n + k)
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_B_._(n_+_k)
let k be Element of NAT ; ::_thesis: x in B . (n + k)
 B . (n + k) in  {  (B . k) where k is Element of NAT : n <= k  }  by Th1;
hence  x in B . (n + k) by A1, A3, SETFAM_1:def_1; ::_thesis: verum
end;
hence  for k being Element of NAT holds x in B . (n + k) ; ::_thesis: verum
end;
A4:  {  (B . k) where k is Element of NAT : n <= k  }  <> {} by Th1;
now__::_thesis:_(_(_for_k_being_Element_of_NAT_holds_x_in_B_._(n_+_k)_)_implies_x_in_(inferior_setsequence_B)_._n_)
assume  for k being Element of NAT holds x in B . (n + k) ; ::_thesis: x in (inferior_setsequence B) . n
then  for Z being set st Z in  {  (B . k) where k is Element of NAT : n <= k  }  holds
x in Z by Th3;
hence  x in (inferior_setsequence B) . n by A1, A4, SETFAM_1:def_1; ::_thesis: verum
end;
hence  ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) by A2; ::_thesis: verum
end;

theorem Th20: :: SETLIM_1:20
for n being Element of NAT
for X, x being set
for B being SetSequence of X holds
( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
proof
let n be Element of NAT ; ::_thesis: for X, x being set
for B being SetSequence of X holds
( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
let X, x be set ; ::_thesis: for B being SetSequence of X holds
( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
let B be SetSequence of X; ::_thesis: ( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
set Y =  {  (B . k) where k is Element of NAT : n <= k  }  ;
A1: (superior_setsequence B) . n = union  {  (B . k) where k is Element of NAT : n <= k  }  by Def3;
thus  ( x in (superior_setsequence B) . n implies ex k being Element of NAT st x in B . (n + k) ) ::_thesis: ( ex k being Element of NAT st x in B . (n + k) implies x in (superior_setsequence B) . n )
proof
assume  x in (superior_setsequence B) . n ; ::_thesis: ex k being Element of NAT st x in B . (n + k)
then consider Y1 being set  such that
A2: x in Y1 and
A3: Y1 in  {  (B . k) where k is Element of NAT : n <= k  }  by A1, TARSKI:def_4;
consider k11 being Element of NAT  such that
A4: Y1 = B . k11 and
A5: n <= k11 by A3;
 ex k being Nat st k11 = n + k by A5, NAT_1:10;
then consider k22 being Nat such that
A6: Y1 = B . (n + k22) by A4;
 k22 in NAT by ORDINAL1:def_12;
hence  ex k being Element of NAT st x in B . (n + k) by A2, A6; ::_thesis: verum
end;
now__::_thesis:_(_ex_k_being_Element_of_NAT_st_x_in_B_._(n_+_k)_implies_x_in_(superior_setsequence_B)_._n_)
assume  ex k being Element of NAT st x in B . (n + k) ; ::_thesis: x in (superior_setsequence B) . n
then consider k1 being Element of NAT  such that
A7: x in B . (n + k1) ;
 B . (n + k1) in  {  (B . k) where k is Element of NAT : n <= k  }  by Th1;
hence  x in (superior_setsequence B) . n by A1, A7, TARSKI:def_4; ::_thesis: verum
end;
hence  ( ex k being Element of NAT st x in B . (n + k) implies x in (superior_setsequence B) . n ) ; ::_thesis: verum
end;

theorem Th21: :: SETLIM_1:21
for n being Element of NAT
for X being set
for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
let X be set ; ::_thesis: for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
let B be SetSequence of X; ::_thesis: (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_setsequence_B)_._n_=_((inferior_setsequence_B)_._(n_+_1))_/\_(B_._n)
let n be Element of NAT ; ::_thesis: (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)
A1: (inferior_setsequence B) . n = meet  {  (B . k1) where k1 is Element of NAT : n <= k1  }  by Def2;
A2:  {  (B . k1) where k1 is Element of NAT : n <= k1  }  =  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(B . n)} by Th2;
A3: (inferior_setsequence B) . (n + 1) = meet  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  by Def2;
A4:  {  (B . k1) where k1 is Element of NAT : n <= k1  }  <> {} by Th1;
A5: now__::_thesis:_for_x_being_set_st_x_in_(inferior_setsequence_B)_._(n_+_1)_&_x_in_B_._n_holds_
x_in_(inferior_setsequence_B)_._n
let x be set ; ::_thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n implies x in (inferior_setsequence B) . n )
assume that
A6: x in (inferior_setsequence B) . (n + 1) and
A7: x in B . n ; ::_thesis: x in (inferior_setsequence B) . n
 for Z being set st Z in  {  (B . k2) where k2 is Element of NAT : n <= k2  }  holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in  {  (B . k2) where k2 is Element of NAT : n <= k2  }  implies x in Z )
assume  Z in  {  (B . k1) where k1 is Element of NAT : n <= k1  }  ; ::_thesis: x in Z
then consider Z1 being set  such that
A8: ( Z = Z1 & Z1 in  {  (B . k1) where k1 is Element of NAT : n <= k1  }  ) ;
consider k11 being Element of NAT  such that
A9: ( Z1 = B . k11 & n <= k11 ) by A8;
now__::_thesis:_(_(_Z1_=_B_._k11_&_n_=_k11_&_x_in_Z1_)_or_(_Z1_=_B_._k11_&_n_+_1_<=_k11_&_x_in_Z1_)_)
percases ( ( Z1 = B . k11 & n = k11 ) or ( Z1 = B . k11 & n + 1 <= k11 ) ) by A9, Lm1;
case ( Z1 = B . k11 & n = k11 ) ; ::_thesis: x in Z1
hence  x in Z1 by A7; ::_thesis: verum
end;
case ( Z1 = B . k11 & n + 1 <= k11 ) ; ::_thesis: x in Z1
then  Z1 in  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  ;
hence  x in Z1 by A3, A6, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in Z by A8; ::_thesis: verum
end;
then  x in meet  {  (B . k2) where k2 is Element of NAT : n <= k2  }  by A4, SETFAM_1:def_1;
hence  x in (inferior_setsequence B) . n by Def2; ::_thesis: verum
end;
  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  <> {} by Th1;
then A10: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by A1, A3, A2, SETFAM_1:6, XBOOLE_1:7;
now__::_thesis:_for_x_being_set_st_x_in_(inferior_setsequence_B)_._n_holds_
(_x_in_(inferior_setsequence_B)_._(n_+_1)_&_x_in_B_._n_)
let x be set ; ::_thesis: ( x in (inferior_setsequence B) . n implies ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) )
A11: B . n in  {  (B . k1) where k1 is Element of NAT : n <= k1  }  ;
assume  x in (inferior_setsequence B) . n ; ::_thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n )
hence  ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) by A1, A10, A11, SETFAM_1:def_1; ::_thesis: verum
end;
hence  (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) ; ::_thesis: verum
end;

theorem Th22: :: SETLIM_1:22
for n being Element of NAT
for X being set
for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
let B be SetSequence of X; ::_thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_setsequence_B)_._n_=_((superior_setsequence_B)_._(n_+_1))_\/_(B_._n)
let n be Element of NAT ; ::_thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)
  {  (B . k1) where k1 is Element of NAT : n <= k1  }  =  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  \/ {(B . n)} by Th2;
then  union  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  c= union  {  (B . k1) where k1 is Element of NAT : n <= k1  }  by XBOOLE_1:7, ZFMISC_1:77;
then  (superior_setsequence B) . (n + 1) c= union  {  (B . k1) where k1 is Element of NAT : n <= k1  }  by Def3;
then A1: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by Def3;
A2: now__::_thesis:_for_x_being_set_st_(_x_in_(superior_setsequence_B)_._(n_+_1)_or_x_in_B_._n_)_holds_
x_in_(superior_setsequence_B)_._n
let x be set ; ::_thesis: ( ( x in (superior_setsequence B) . (n + 1) or x in B . n ) implies x in (superior_setsequence B) . n )
assume A3: ( x in (superior_setsequence B) . (n + 1) or x in B . n ) ; ::_thesis: x in (superior_setsequence B) . n
thus  x in (superior_setsequence B) . n ::_thesis: verum
proof
now__::_thesis:_(_(_x_in_(superior_setsequence_B)_._(n_+_1)_&_x_in_(superior_setsequence_B)_._n_)_or_(_x_in_B_._n_&_x_in_(superior_setsequence_B)_._n_)_)
percases ( x in (superior_setsequence B) . (n + 1) or x in B . n ) by A3;
case x in (superior_setsequence B) . (n + 1) ; ::_thesis: x in (superior_setsequence B) . n
hence  x in (superior_setsequence B) . n by A1; ::_thesis: verum
end;
caseA4: x in B . n ; ::_thesis: x in (superior_setsequence B) . n
 B . n in  {  (B . k1) where k1 is Element of NAT : n <= k1  }  ;
then  x in union  {  (B . k1) where k1 is Element of NAT : n <= k1  }  by A4, TARSKI:def_4;
hence  x in (superior_setsequence B) . n by Def3; ::_thesis: verum
end;
end;
end;
hence  x in (superior_setsequence B) . n ; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_holds_
(_not_x_in_(superior_setsequence_B)_._n_or_x_in_B_._n_or_x_in_(superior_setsequence_B)_._(n_+_1)_)
let x be set ; ::_thesis: ( not x in (superior_setsequence B) . n or x in B . n or x in (superior_setsequence B) . (n + 1) )
assume  x in (superior_setsequence B) . n ; ::_thesis: ( x in B . n or x in (superior_setsequence B) . (n + 1) )
then  x in union  {  (B . k1) where k1 is Element of NAT : n <= k1  }  by Def3;
then consider Y1 being set  such that
A5: ( x in Y1 & Y1 in  {  (B . k1) where k1 is Element of NAT : n <= k1  }  ) by TARSKI:def_4;
consider k11 being Element of NAT  such that
A6: ( Y1 = B . k11 & n <= k11 ) by A5;
now__::_thesis:_(_(_Y1_=_B_._k11_&_n_=_k11_&_x_in_B_._n_)_or_(_Y1_=_B_._k11_&_n_+_1_<=_k11_&_x_in_union__{__(B_._k2)_where_k2_is_Element_of_NAT_:_n_+_1_<=_k2__}__)_)
percases ( ( Y1 = B . k11 & n = k11 ) or ( Y1 = B . k11 & n + 1 <= k11 ) ) by A6, Lm1;
case ( Y1 = B . k11 & n = k11 ) ; ::_thesis: x in B . n
hence  x in B . n by A5; ::_thesis: verum
end;
case ( Y1 = B . k11 & n + 1 <= k11 ) ; ::_thesis: x in union  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }
then  Y1 in  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  ;
hence  x in union  {  (B . k2) where k2 is Element of NAT : n + 1 <= k2  }  by A5, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  ( x in B . n or x in (superior_setsequence B) . (n + 1) ) by Def3; ::_thesis: verum
end;
then  for x being set holds
( x in (superior_setsequence B) . n iff ( x in B . n or x in (superior_setsequence B) . (n + 1) ) ) by A2;
hence  (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) ; ::_thesis: verum
end;

theorem Th23: :: SETLIM_1:23
for X being set
for B being SetSequence of X holds inferior_setsequence B is V50()
proof
let X be set ; ::_thesis: for B being SetSequence of X holds inferior_setsequence B is V50()
let B be SetSequence of X; ::_thesis: inferior_setsequence B is V50()
now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_setsequence_B)_._n_c=_(inferior_setsequence_B)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1)
 (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) by Th21;
hence  (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by XBOOLE_1:17; ::_thesis: verum
end;
hence  inferior_setsequence B is V50() by PROB_2:7; ::_thesis: verum
end;

theorem Th24: :: SETLIM_1:24
for X being set
for B being SetSequence of X holds superior_setsequence B is V49()
proof
let X be set ; ::_thesis: for B being SetSequence of X holds superior_setsequence B is V49()
let B be SetSequence of X; ::_thesis: superior_setsequence B is V49()
now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_setsequence_B)_._(n_+_1)_c=_(superior_setsequence_B)_._n
let n be Element of NAT ; ::_thesis: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n
 (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by Th22;
hence  (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by XBOOLE_1:7; ::_thesis: verum
end;
hence  superior_setsequence B is V49() by PROB_2:6; ::_thesis: verum
end;

theorem :: SETLIM_1:25
for X being set
for B being SetSequence of X holds
( inferior_setsequence B is monotone & superior_setsequence B is monotone )
proof
let X be set ; ::_thesis: for B being SetSequence of X holds
( inferior_setsequence B is monotone & superior_setsequence B is monotone )
let B be SetSequence of X; ::_thesis: ( inferior_setsequence B is monotone & superior_setsequence B is monotone )
 inferior_setsequence B is V50() by Th23;
hence  inferior_setsequence B is monotone by Def1; ::_thesis: superior_setsequence B is monotone
 superior_setsequence B is V49() by Th24;
hence  superior_setsequence B is monotone by Def1; ::_thesis: verum
end;

registration
let X be set ;
let A be SetSequence of X;
cluster inferior_setsequence A -> V50() for SetSequence of X;
coherence
 for b1 being SetSequence of X st b1 = inferior_setsequence A holds
b1 is non-descending by Th23;
end;

registration
let X be set ;
let A be SetSequence of X;
cluster superior_setsequence A -> V49() for SetSequence of X;
coherence
 for b1 being SetSequence of X st b1 = superior_setsequence A holds
b1 is non-ascending by Th24;
end;

theorem :: SETLIM_1:26
for n being Element of NAT
for X being set
for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n
let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n
let B be SetSequence of X; ::_thesis: Intersection B c= (inferior_setsequence B) . n
 0 <= n by NAT_1:2;
then  (inferior_setsequence B) . 0 c= (inferior_setsequence B) . n by PROB_1:def_5;
hence  Intersection B c= (inferior_setsequence B) . n by Th17; ::_thesis: verum
end;

theorem :: SETLIM_1:27
for n being Element of NAT
for X being set
for B being SetSequence of X holds (superior_setsequence B) . n c= Union B
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X holds (superior_setsequence B) . n c= Union B
let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . n c= Union B
let B be SetSequence of X; ::_thesis: (superior_setsequence B) . n c= Union B
 0 <= n by NAT_1:2;
then  (superior_setsequence B) . n c= (superior_setsequence B) . 0 by PROB_1:def_4;
hence  (superior_setsequence B) . n c= Union B by Th18; ::_thesis: verum
end;

theorem Th28: :: SETLIM_1:28
for X being set
for B being SetSequence of X
for n being Element of NAT holds  {  (B . k) where k is Element of NAT : n <= k  }  is Subset-Family of X
proof
let X be set ; ::_thesis: for B being SetSequence of X
for n being Element of NAT holds  {  (B . k) where k is Element of NAT : n <= k  }  is Subset-Family of X
let B be SetSequence of X; ::_thesis: for n being Element of NAT holds  {  (B . k) where k is Element of NAT : n <= k  }  is Subset-Family of X
let n be Element of NAT ; ::_thesis:  {  (B . k) where k is Element of NAT : n <= k  }  is Subset-Family of X
set Y1 =  {  (B . k) where k is Element of NAT : n <= k  }  ;
  {  (B . k) where k is Element of NAT : n <= k  }  c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (B . k) where k is Element of NAT : n <= k  }  or x in bool X )
assume  x in  {  (B . k) where k is Element of NAT : n <= k  }  ; ::_thesis: x in bool X
then  ex k being Element of NAT st
( x = B . k & n <= k ) ;
hence  x in bool X ; ::_thesis: verum
end;
hence   {  (B . k) where k is Element of NAT : n <= k  }  is Subset-Family of X ; ::_thesis: verum
end;

theorem :: SETLIM_1:29
for X being set
for B being SetSequence of X holds Union B = (Intersection (Complement B)) `
proof
let X be set ; ::_thesis: for B being SetSequence of X holds Union B = (Intersection (Complement B)) `
let B be SetSequence of X; ::_thesis: Union B = (Intersection (Complement B)) `
(Intersection (Complement B)) ` = ((Union (Complement (Complement B))) `) ` by PROB_1:def_3
.= Union B ;
hence  Union B = (Intersection (Complement B)) ` ; ::_thesis: verum
end;

theorem Th30: :: SETLIM_1:30
for n being Element of NAT
for X being set
for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
let X be set ; ::_thesis: for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
let B be SetSequence of X; ::_thesis: (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
set Y1 =  {  (B . k1) where k1 is Element of NAT : n <= k1  }  ;
set Y2 =  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  ;
set Y3 =  {  ((B . k) `) where k is Element of NAT : n <= k  }  ;
A1:  {  ((B . k) `) where k is Element of NAT : n <= k  }  c=  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  ((B . k) `) where k is Element of NAT : n <= k  }  or y in  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  )
assume  y in  {  ((B . k) `) where k is Element of NAT : n <= k  }  ; ::_thesis: y in  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }
then consider k being Element of NAT  such that
A2: y = (B . k) ` and
A3: n <= k ;
 y = (Complement B) . k by A2, PROB_1:def_2;
hence  y in  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  by A3; ::_thesis: verum
end;
  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  c=  {  ((B . k) `) where k is Element of NAT : n <= k  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  or x in  {  ((B . k) `) where k is Element of NAT : n <= k  }  )
assume  x in  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  ; ::_thesis: x in  {  ((B . k) `) where k is Element of NAT : n <= k  }
then consider k being Element of NAT  such that
A4: x = (Complement B) . k and
A5: n <= k ;
 x = (B . k) ` by A4, PROB_1:def_2;
hence  x in  {  ((B . k) `) where k is Element of NAT : n <= k  }  by A5; ::_thesis: verum
end;
then A6:  {  ((Complement B) . k2) where k2 is Element of NAT : n <= k2  }  =  {  ((B . k) `) where k is Element of NAT : n <= k  }  by A1, XBOOLE_0:def_10;
A7:  {  (B . k1) where k1 is Element of NAT : n <= k1  }  <> {} by Th1;
reconsider Y1 =  {  (B . k1) where k1 is Element of NAT : n <= k1  }  as Subset-Family of X by Th28;
A8: COMPLEMENT Y1 c=  {  ((B . k) `) where k is Element of NAT : n <= k  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in COMPLEMENT Y1 or y in  {  ((B . k) `) where k is Element of NAT : n <= k  }  )
assume A9: y in COMPLEMENT Y1 ; ::_thesis: y in  {  ((B . k) `) where k is Element of NAT : n <= k  }
then reconsider y = y as Subset of X ;
 y ` in Y1 by A9, SETFAM_1:def_7;
then consider k being Element of NAT  such that
A10: y ` = B . k and
A11: n <= k ;
 y = (B . k) ` by A10;
hence  y in  {  ((B . k) `) where k is Element of NAT : n <= k  }  by A11; ::_thesis: verum
end;
  {  ((B . k) `) where k is Element of NAT : n <= k  }  c= COMPLEMENT Y1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ((B . k) `) where k is Element of NAT : n <= k  }  or x in COMPLEMENT Y1 )
assume  x in  {  ((B . k) `) where k is Element of NAT : n <= k  }  ; ::_thesis: x in COMPLEMENT Y1
then consider k being Element of NAT  such that
A12: x = (B . k) ` and
A13: n <= k ;
reconsider z = B . k as Subset of X ;
 (z `) ` in Y1 by A13;
hence  x in COMPLEMENT Y1 by A12, SETFAM_1:def_7; ::_thesis: verum
end;
then   {  ((B . k) `) where k is Element of NAT : n <= k  }  = COMPLEMENT Y1 by A8, XBOOLE_0:def_10;
then (superior_setsequence (Complement B)) . n = union (COMPLEMENT Y1) by A6, Def3
.= ([#] X) \ (meet Y1) by A7, SETFAM_1:34
.= (meet Y1) ` ;
hence  (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` by Def2; ::_thesis: verum
end;

theorem :: SETLIM_1:31
for n being Element of NAT
for X being set
for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
let B be SetSequence of X; ::_thesis: (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
reconsider Y = (inferior_setsequence (Complement B)) . n as Subset of X ;
Y = ((superior_setsequence (Complement (Complement B))) . n) ` by Th30
.= ((superior_setsequence B) . n) ` ;
hence  (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` ; ::_thesis: verum
end;

theorem Th32: :: SETLIM_1:32
for X being set
for B being SetSequence of X holds Complement (inferior_setsequence B) = superior_setsequence (Complement B)
proof
let X be set ; ::_thesis: for B being SetSequence of X holds Complement (inferior_setsequence B) = superior_setsequence (Complement B)
let B be SetSequence of X; ::_thesis: Complement (inferior_setsequence B) = superior_setsequence (Complement B)
reconsider A2 = inferior_setsequence B as SetSequence of X ;
reconsider A3 = superior_setsequence (Complement B) as SetSequence of X ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Complement_A2)_._n_=_A3_._n
let n be Element of NAT ; ::_thesis: (Complement A2) . n = A3 . n
 (A2 . n) ` = ((A3 . n) `) ` by Th30;
hence  (Complement A2) . n = A3 . n by PROB_1:def_2; ::_thesis: verum
end;
hence  Complement (inferior_setsequence B) = superior_setsequence (Complement B) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SETLIM_1:33
for X being set
for B being SetSequence of X holds Complement (superior_setsequence B) = inferior_setsequence (Complement B)
proof
let X be set ; ::_thesis: for B being SetSequence of X holds Complement (superior_setsequence B) = inferior_setsequence (Complement B)
let B be SetSequence of X; ::_thesis: Complement (superior_setsequence B) = inferior_setsequence (Complement B)
reconsider A2 = inferior_setsequence (Complement B) as SetSequence of X ;
Complement A2 = superior_setsequence (Complement (Complement B)) by Th32
.= superior_setsequence B ;
hence  Complement (superior_setsequence B) = inferior_setsequence (Complement B) ; ::_thesis: verum
end;

theorem :: SETLIM_1:34
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
proof
let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) implies for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n )
assume A1: for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ; ::_thesis: for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
let n be Element of NAT ; ::_thesis: ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
set X1 = inferior_setsequence A1;
set X2 = inferior_setsequence A2;
set X3 = inferior_setsequence A3;
now__::_thesis:_for_x_being_set_st_x_in_((inferior_setsequence_A1)_._n)_\/_((inferior_setsequence_A2)_._n)_holds_
x_in_(inferior_setsequence_A3)_._n
let x be set ; ::_thesis: ( x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) implies b1 in (inferior_setsequence A3) . n )
assume A2: x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) ; ::_thesis: b1 in (inferior_setsequence A3) . n
percases ( x in (inferior_setsequence A1) . n or x in (inferior_setsequence A2) . n ) by A2, XBOOLE_0:def_3;
supposeA3: x in (inferior_setsequence A1) . n ; ::_thesis: b1 in (inferior_setsequence A3) . n
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_A3_._(n_+_k)
let k be Element of NAT ; ::_thesis: x in A3 . (n + k)
 ( x in A1 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A3, Th19;
hence  x in A3 . (n + k) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in (inferior_setsequence A3) . n by Th19; ::_thesis: verum
end;
supposeA4: x in (inferior_setsequence A2) . n ; ::_thesis: b1 in (inferior_setsequence A3) . n
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_A3_._(n_+_k)
let k be Element of NAT ; ::_thesis: x in A3 . (n + k)
 ( x in A2 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A4, Th19;
hence  x in A3 . (n + k) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in (inferior_setsequence A3) . n by Th19; ::_thesis: verum
end;
end;
end;
hence  ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n by TARSKI:def_3; ::_thesis: verum
end;

theorem :: SETLIM_1:35
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
proof
let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) implies for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) )
assume A1: for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ; ::_thesis: for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
let n be Element of NAT ; ::_thesis: (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
reconsider X3 = inferior_setsequence A3 as SetSequence of X ;
reconsider X2 = inferior_setsequence A2 as SetSequence of X ;
set B = A1;
reconsider X1 = inferior_setsequence A1 as SetSequence of X ;
A2: (X1 . n) /\ (X2 . n) c= X3 . n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X1 . n) /\ (X2 . n) or x in X3 . n )
assume  x in (X1 . n) /\ (X2 . n) ; ::_thesis: x in X3 . n
then A3: ( x in X1 . n & x in X2 . n ) by XBOOLE_0:def_4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_A3_._(n_+_k)
let k be Element of NAT ; ::_thesis: x in A3 . (n + k)
 ( x in A1 . (n + k) & x in A2 . (n + k) ) by A3, Th19;
then  x in (A1 . (n + k)) /\ (A2 . (n + k)) by XBOOLE_0:def_4;
hence  x in A3 . (n + k) by A1; ::_thesis: verum
end;
hence  x in X3 . n by Th19; ::_thesis: verum
end;
 X3 . n c= (X1 . n) /\ (X2 . n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X3 . n or x in (X1 . n) /\ (X2 . n) )
assume A4: x in X3 . n ; ::_thesis: x in (X1 . n) /\ (X2 . n)
now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A1_._(n_+_k)_&_x_in_A2_._(n_+_k)_)
let k be Element of NAT ; ::_thesis: ( x in A1 . (n + k) & x in A2 . (n + k) )
 x in A3 . (n + k) by A4, Th19;
then  x in (A1 . (n + k)) /\ (A2 . (n + k)) by A1;
hence  ( x in A1 . (n + k) & x in A2 . (n + k) ) by XBOOLE_0:def_4; ::_thesis: verum
end;
then  ( x in X1 . n & x in X2 . n ) by Th19;
hence  x in (X1 . n) /\ (X2 . n) by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETLIM_1:36
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
proof
let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) implies for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) )
assume A1: for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ; ::_thesis: for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
let n be Element of NAT ; ::_thesis: (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
reconsider X3 = superior_setsequence A3 as SetSequence of X ;
reconsider X2 = superior_setsequence A2 as SetSequence of X ;
set B = A1;
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
A2: (X1 . n) \/ (X2 . n) c= X3 . n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X1 . n) \/ (X2 . n) or x in X3 . n )
assume A3: x in (X1 . n) \/ (X2 . n) ; ::_thesis: x in X3 . n
now__::_thesis:_(_(_x_in_X1_._n_&_x_in_X3_._n_)_or_(_x_in_X2_._n_&_x_in_X3_._n_)_)
percases ( x in X1 . n or x in X2 . n ) by A3, XBOOLE_0:def_3;
case x in X1 . n ; ::_thesis: x in X3 . n
then consider k being Element of NAT  such that
A4: x in A1 . (n + k) by Th20;
 A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) by A1;
then  x in A3 . (n + k) by A4, XBOOLE_0:def_3;
hence  x in X3 . n by Th20; ::_thesis: verum
end;
case x in X2 . n ; ::_thesis: x in X3 . n
then consider k being Element of NAT  such that
A5: x in A2 . (n + k) by Th20;
 A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) by A1;
then  x in A3 . (n + k) by A5, XBOOLE_0:def_3;
hence  x in X3 . n by Th20; ::_thesis: verum
end;
end;
end;
hence  x in X3 . n ; ::_thesis: verum
end;
 X3 . n c= (X1 . n) \/ (X2 . n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X3 . n or x in (X1 . n) \/ (X2 . n) )
assume  x in X3 . n ; ::_thesis: x in (X1 . n) \/ (X2 . n)
then consider k being Element of NAT  such that
A6: x in A3 . (n + k) by Th20;
A7: x in (A1 . (n + k)) \/ (A2 . (n + k)) by A1, A6;
now__::_thesis:_(_(_x_in_A1_._(n_+_k)_&_x_in_X1_._n_)_or_(_x_in_A2_._(n_+_k)_&_x_in_X2_._n_)_)
percases ( x in A1 . (n + k) or x in A2 . (n + k) ) by A7, XBOOLE_0:def_3;
case x in A1 . (n + k) ; ::_thesis: x in X1 . n
hence  x in X1 . n by Th20; ::_thesis: verum
end;
case x in A2 . (n + k) ; ::_thesis: x in X2 . n
hence  x in X2 . n by Th20; ::_thesis: verum
end;
end;
end;
hence  x in (X1 . n) \/ (X2 . n) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETLIM_1:37
for X being set
for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
proof
let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) implies for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) )
assume A1: for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ; ::_thesis: for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
let n be Element of NAT ; ::_thesis: (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
reconsider X3 = superior_setsequence A3 as SetSequence of X ;
reconsider X2 = superior_setsequence A2 as SetSequence of X ;
set B = A1;
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
 X3 . n c= (X1 . n) /\ (X2 . n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X3 . n or x in (X1 . n) /\ (X2 . n) )
assume  x in X3 . n ; ::_thesis: x in (X1 . n) /\ (X2 . n)
then consider k being Element of NAT  such that
A2: x in A3 . (n + k) by Th20;
A3: A3 . (n + k) = (A1 . (n + k)) /\ (A2 . (n + k)) by A1;
then  x in A2 . (n + k) by A2, XBOOLE_0:def_4;
then A4: x in X2 . n by Th20;
 x in A1 . (n + k) by A2, A3, XBOOLE_0:def_4;
then  x in X1 . n by Th20;
hence  x in (X1 . n) /\ (X2 . n) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) ; ::_thesis: verum
end;

theorem Th38: :: SETLIM_1:38
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds (inferior_setsequence B) . n = A
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds (inferior_setsequence B) . n = A
let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds (inferior_setsequence B) . n = A
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds (inferior_setsequence B) . n = A )
assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds (inferior_setsequence B) . n = A
let n be Element of NAT ; ::_thesis: (inferior_setsequence B) . n = A
 (inferior_setsequence B) . n = meet  {  (B . k) where k is Element of NAT : n <= k  }  by Def2;
hence  (inferior_setsequence B) . n = A by A1, Th14; ::_thesis: verum
end;

theorem Th39: :: SETLIM_1:39
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds (superior_setsequence B) . n = A
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds (superior_setsequence B) . n = A
let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds (superior_setsequence B) . n = A
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds (superior_setsequence B) . n = A )
assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds (superior_setsequence B) . n = A
let n be Element of NAT ; ::_thesis: (superior_setsequence B) . n = A
 (superior_setsequence B) . n = union  {  (B . k) where k is Element of NAT : n <= k  }  by Def3;
hence  (superior_setsequence B) . n = A by A1, Th13; ::_thesis: verum
end;

theorem Th40: :: SETLIM_1:40
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
B . n c= (superior_setsequence B) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V50() holds
B . n c= (superior_setsequence B) . (n + 1)
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
B . n c= (superior_setsequence B) . (n + 1)
let B be SetSequence of X; ::_thesis: ( B is V50() implies B . n c= (superior_setsequence B) . (n + 1) )
assume  B is V50() ; ::_thesis: B . n c= (superior_setsequence B) . (n + 1)
then A1: B . n c= B . (n + 1) by PROB_2:7;
 B . n c= union  {  (B . k) where k is Element of NAT : n + 1 <= k  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B . n or x in union  {  (B . k) where k is Element of NAT : n + 1 <= k  }  )
A2: B . (n + 1) in  {  (B . k) where k is Element of NAT : n + 1 <= k  }  ;
assume  x in B . n ; ::_thesis: x in union  {  (B . k) where k is Element of NAT : n + 1 <= k  }
hence  x in union  {  (B . k) where k is Element of NAT : n + 1 <= k  }  by A1, A2, TARSKI:def_4; ::_thesis: verum
end;
hence  B . n c= (superior_setsequence B) . (n + 1) by Def3; ::_thesis: verum
end;

theorem Th41: :: SETLIM_1:41
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
let B be SetSequence of X; ::_thesis: ( B is V50() implies (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) )
assume  B is V50() ; ::_thesis: (superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
then  ((superior_setsequence B) . (n + 1)) \/ (B . n) = (superior_setsequence B) . (n + 1) by Th40, XBOOLE_1:12;
hence  (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) by Th22; ::_thesis: verum
end;

theorem Th42: :: SETLIM_1:42
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = Union B
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = Union B
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
(superior_setsequence B) . n = Union B
let B be SetSequence of X; ::_thesis: ( B is V50() implies (superior_setsequence B) . n = Union B )
defpred S1[ Nat] means (superior_setsequence B) . $1 = Union B;
assume  B is V50() ; ::_thesis: (superior_setsequence B) . n = Union B
then A1: for k being Element of NAT st S1[k] holds
S1[k + 1] by Th41;
A2: S1[ 0 ] by Th18;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1);
hence  (superior_setsequence B) . n = Union B ; ::_thesis: verum
end;

theorem Th43: :: SETLIM_1:43
for X being set
for B being SetSequence of X st B is V50() holds
Intersection (superior_setsequence B) = Union B
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
Intersection (superior_setsequence B) = Union B
let B be SetSequence of X; ::_thesis: ( B is V50() implies Intersection (superior_setsequence B) = Union B )
assume A1: B is V50() ; ::_thesis: Intersection (superior_setsequence B) = Union B
now__::_thesis:_for_x_being_set_st_x_in_Intersection_(superior_setsequence_B)_holds_
x_in_Union_B
let x be set ; ::_thesis: ( x in Intersection (superior_setsequence B) implies x in Union B )
assume A2: x in Intersection (superior_setsequence B) ; ::_thesis: x in Union B
now__::_thesis:_for_n_being_Element_of_NAT_holds_x_in_Union_B
let n be Element of NAT ; ::_thesis: x in Union B
 (superior_setsequence B) . n = Union B by A1, Th42;
hence  x in Union B by A2, PROB_1:13; ::_thesis: verum
end;
hence  x in Union B ; ::_thesis: verum
end;
then A3: Intersection (superior_setsequence B) c= Union B by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_Union_B_holds_
y_in_Intersection_(superior_setsequence_B)
let y be set ; ::_thesis: ( y in Union B implies y in Intersection (superior_setsequence B) )
assume  y in Union B ; ::_thesis: y in Intersection (superior_setsequence B)
then  for n being Element of NAT holds y in (superior_setsequence B) . n by A1, Th42;
hence  y in Intersection (superior_setsequence B) by PROB_1:13; ::_thesis: verum
end;
then  Union B c= Intersection (superior_setsequence B) by TARSKI:def_3;
hence  Intersection (superior_setsequence B) = Union B by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th44: :: SETLIM_1:44
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
B . n c= (inferior_setsequence B) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V50() holds
B . n c= (inferior_setsequence B) . (n + 1)
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
B . n c= (inferior_setsequence B) . (n + 1)
let B be SetSequence of X; ::_thesis: ( B is V50() implies B . n c= (inferior_setsequence B) . (n + 1) )
set Y =  {  (B . k) where k is Element of NAT : n + 1 <= k  }  ;
assume A1: B is V50() ; ::_thesis: B . n c= (inferior_setsequence B) . (n + 1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B . n or x in (inferior_setsequence B) . (n + 1) )
assume A2: x in B . n ; ::_thesis: x in (inferior_setsequence B) . (n + 1)
A3: now__::_thesis:_for_y_being_set_st_y_in__{__(B_._k)_where_k_is_Element_of_NAT_:_n_+_1_<=_k__}__holds_
x_in_y
let y be set ; ::_thesis: ( y in  {  (B . k) where k is Element of NAT : n + 1 <= k  }  implies x in y )
assume  y in  {  (B . k) where k is Element of NAT : n + 1 <= k  }  ; ::_thesis: x in y
then consider k1 being Element of NAT  such that
A4: y = B . k1 and
A5: n + 1 <= k1 ;
 n <= k1 by A5, NAT_1:13;
then  B . n c= B . k1 by A1, PROB_1:def_5;
hence  x in y by A2, A4; ::_thesis: verum
end;
A6:  {  (B . k) where k is Element of NAT : n + 1 <= k  }  <> {} by Th1;
 (inferior_setsequence B) . (n + 1) = meet  {  (B . k) where k is Element of NAT : n + 1 <= k  }  by Def2;
hence  x in (inferior_setsequence B) . (n + 1) by A6, A3, SETFAM_1:def_1; ::_thesis: verum
end;

theorem Th45: :: SETLIM_1:45
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V50() holds
(inferior_setsequence B) . n = B . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V50() holds
(inferior_setsequence B) . n = B . n
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
(inferior_setsequence B) . n = B . n
let B be SetSequence of X; ::_thesis: ( B is V50() implies (inferior_setsequence B) . n = B . n )
assume  B is V50() ; ::_thesis: (inferior_setsequence B) . n = B . n
then  ((inferior_setsequence B) . (n + 1)) /\ (B . n) = B . n by Th44, XBOOLE_1:28;
hence  (inferior_setsequence B) . n = B . n by Th21; ::_thesis: verum
end;

theorem Th46: :: SETLIM_1:46
for X being set
for B being SetSequence of X st B is V50() holds
inferior_setsequence B = B
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
inferior_setsequence B = B
let B be SetSequence of X; ::_thesis: ( B is V50() implies inferior_setsequence B = B )
assume  B is V50() ; ::_thesis: inferior_setsequence B = B
then  for n being Element of NAT holds (inferior_setsequence B) . n = B . n by Th45;
hence  inferior_setsequence B = B by FUNCT_2:63; ::_thesis: verum
end;

theorem Th47: :: SETLIM_1:47
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . (n + 1) c= B . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . (n + 1) c= B . n
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . (n + 1) c= B . n
let B be SetSequence of X; ::_thesis: ( B is V49() implies (superior_setsequence B) . (n + 1) c= B . n )
assume A1: B is V49() ; ::_thesis: (superior_setsequence B) . (n + 1) c= B . n
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (superior_setsequence B) . (n + 1) or x in B . n )
assume  x in (superior_setsequence B) . (n + 1) ; ::_thesis: x in B . n
then consider k being Element of NAT  such that
A2: x in B . ((n + 1) + k) by Th20;
 n + 1 <= (n + 1) + k by NAT_1:11;
then  n <= (n + 1) + k by NAT_1:13;
then  B . ((n + 1) + k) c= B . n by A1, PROB_1:def_4;
hence  x in B . n by A2; ::_thesis: verum
end;

theorem Th48: :: SETLIM_1:48
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . n = B . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . n = B . n
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
(superior_setsequence B) . n = B . n
let B be SetSequence of X; ::_thesis: ( B is V49() implies (superior_setsequence B) . n = B . n )
assume  B is V49() ; ::_thesis: (superior_setsequence B) . n = B . n
then  ((superior_setsequence B) . (n + 1)) \/ (B . n) = B . n by Th47, XBOOLE_1:12;
hence  (superior_setsequence B) . n = B . n by Th22; ::_thesis: verum
end;

theorem Th49: :: SETLIM_1:49
for X being set
for B being SetSequence of X st B is V49() holds
superior_setsequence B = B
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
superior_setsequence B = B
let B be SetSequence of X; ::_thesis: ( B is V49() implies superior_setsequence B = B )
assume  B is V49() ; ::_thesis: superior_setsequence B = B
then  for n being Element of NAT holds (superior_setsequence B) . n = B . n by Th48;
hence  superior_setsequence B = B by FUNCT_2:63; ::_thesis: verum
end;

theorem Th50: :: SETLIM_1:50
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . (n + 1) c= B . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . (n + 1) c= B . n
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . (n + 1) c= B . n
let B be SetSequence of X; ::_thesis: ( B is V49() implies (inferior_setsequence B) . (n + 1) c= B . n )
set Y =  {  (B . k) where k is Element of NAT : n + 1 <= k  }  ;
assume  B is V49() ; ::_thesis: (inferior_setsequence B) . (n + 1) c= B . n
then A1: B . (n + 1) c= B . n by PROB_2:6;
A2: B . (n + 1) in  {  (B . k) where k is Element of NAT : n + 1 <= k  }  ;
A3: now__::_thesis:_for_x_being_set_st_x_in_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_+_1_<=_k__}__holds_
x_in_B_._n
let x be set ; ::_thesis: ( x in meet  {  (B . k) where k is Element of NAT : n + 1 <= k  }  implies x in B . n )
assume  x in meet  {  (B . k) where k is Element of NAT : n + 1 <= k  }  ; ::_thesis: x in B . n
then  x in B . (n + 1) by A2, SETFAM_1:def_1;
hence  x in B . n by A1; ::_thesis: verum
end;
 (inferior_setsequence B) . (n + 1) = meet  {  (B . k) where k is Element of NAT : n + 1 <= k  }  by Def2;
hence  (inferior_setsequence B) . (n + 1) c= B . n by A3, TARSKI:def_3; ::_thesis: verum
end;

theorem Th51: :: SETLIM_1:51
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1)
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1)
let B be SetSequence of X; ::_thesis: ( B is V49() implies (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) )
assume  B is V49() ; ::_thesis: (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1)
then  ((inferior_setsequence B) . (n + 1)) /\ (B . n) = (inferior_setsequence B) . (n + 1) by Th50, XBOOLE_1:28;
hence  (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) by Th21; ::_thesis: verum
end;

theorem Th52: :: SETLIM_1:52
for n being Element of NAT
for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = Intersection B
proof
let n be Element of NAT ; ::_thesis: for X being set
for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = Intersection B
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
(inferior_setsequence B) . n = Intersection B
let B be SetSequence of X; ::_thesis: ( B is V49() implies (inferior_setsequence B) . n = Intersection B )
defpred S1[ Nat] means (inferior_setsequence B) . $1 = Intersection B;
assume  B is V49() ; ::_thesis: (inferior_setsequence B) . n = Intersection B
then A1: for k being Element of NAT st S1[k] holds
S1[k + 1] by Th51;
A2: S1[ 0 ] by Th17;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1);
hence  (inferior_setsequence B) . n = Intersection B ; ::_thesis: verum
end;

theorem Th53: :: SETLIM_1:53
for X being set
for B being SetSequence of X st B is V49() holds
Union (inferior_setsequence B) = Intersection B
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
Union (inferior_setsequence B) = Intersection B
let B be SetSequence of X; ::_thesis: ( B is V49() implies Union (inferior_setsequence B) = Intersection B )
assume A1: B is V49() ; ::_thesis: Union (inferior_setsequence B) = Intersection B
now__::_thesis:_for_x_being_set_st_x_in_Union_(inferior_setsequence_B)_holds_
x_in_Intersection_B
let x be set ; ::_thesis: ( x in Union (inferior_setsequence B) implies x in Intersection B )
assume  x in Union (inferior_setsequence B) ; ::_thesis: x in Intersection B
then  ex k being Element of NAT st x in (inferior_setsequence B) . k by PROB_1:12;
hence  x in Intersection B by A1, Th52; ::_thesis: verum
end;
then A2: Union (inferior_setsequence B) c= Intersection B by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_Intersection_B_holds_
y_in_Union_(inferior_setsequence_B)
let y be set ; ::_thesis: ( y in Intersection B implies y in Union (inferior_setsequence B) )
assume  y in Intersection B ; ::_thesis: y in Union (inferior_setsequence B)
then  y in (inferior_setsequence B) . 0 by Th17;
hence  y in Union (inferior_setsequence B) by PROB_1:12; ::_thesis: verum
end;
then  Intersection B c= Union (inferior_setsequence B) by TARSKI:def_3;
hence  Union (inferior_setsequence B) = Intersection B by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let X be set ;
let B be SetSequence of X;
redefine func lim_inf B equals :: SETLIM_1:def 4
 Union (inferior_setsequence B);
compatibility
 for b1 being Element of bool X holds
( b1 = lim_inf B iff b1 = Union (inferior_setsequence B) )
proof
let F be Subset of X; ::_thesis: ( F = lim_inf B iff F = Union (inferior_setsequence B) )
hereby  ::_thesis: ( F = Union (inferior_setsequence B) implies F = lim_inf B )
assume A1: F = lim_inf B ; ::_thesis: F = Union (inferior_setsequence B)
 for x being set holds
( x in F iff x in Union (inferior_setsequence B) )
proof
let x be set ; ::_thesis: ( x in F iff x in Union (inferior_setsequence B) )
hereby  ::_thesis: ( x in Union (inferior_setsequence B) implies x in F )
assume  x in F ; ::_thesis: x in Union (inferior_setsequence B)
then consider n being Element of NAT  such that
A2: for k being Element of NAT holds x in B . (n + k) by A1, KURATO_0:4;
 x in (inferior_setsequence B) . n by A2, Th19;
hence  x in Union (inferior_setsequence B) by PROB_1:12; ::_thesis: verum
end;
assume  x in Union (inferior_setsequence B) ; ::_thesis: x in F
then consider n being Element of NAT  such that
A3: x in (inferior_setsequence B) . n by PROB_1:12;
 for k being Element of NAT holds x in B . (n + k) by A3, Th19;
hence  x in F by A1, KURATO_0:4; ::_thesis: verum
end;
hence  F = Union (inferior_setsequence B) by TARSKI:1; ::_thesis: verum
end;
assume A4: F = Union (inferior_setsequence B) ; ::_thesis: F = lim_inf B
 for x being set holds
( x in F iff x in lim_inf B )
proof
let x be set ; ::_thesis: ( x in F iff x in lim_inf B )
hereby  ::_thesis: ( x in lim_inf B implies x in F )
assume  x in F ; ::_thesis: x in lim_inf B
then consider n being Element of NAT  such that
A5: x in (inferior_setsequence B) . n by A4, PROB_1:12;
 for k being Element of NAT holds x in B . (n + k) by A5, Th19;
hence  x in lim_inf B by KURATO_0:4; ::_thesis: verum
end;
assume  x in lim_inf B ; ::_thesis: x in F
then consider n being Element of NAT  such that
A6: for k being Element of NAT holds x in B . (n + k) by KURATO_0:4;
 x in (inferior_setsequence B) . n by A6, Th19;
hence  x in F by A4, PROB_1:12; ::_thesis: verum
end;
hence  F = lim_inf B by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem  defines lim_inf SETLIM_1:def_4_:_
 for X being set
for B being SetSequence of X holds lim_inf B = Union (inferior_setsequence B);

definition
let X be set ;
let B be SetSequence of X;
redefine func lim_sup B equals :: SETLIM_1:def 5
 Intersection (superior_setsequence B);
compatibility
 for b1 being Element of bool X holds
( b1 = lim_sup B iff b1 = Intersection (superior_setsequence B) )
proof
let F be Subset of X; ::_thesis: ( F = lim_sup B iff F = Intersection (superior_setsequence B) )
hereby  ::_thesis: ( F = Intersection (superior_setsequence B) implies F = lim_sup B )
assume A1: F = lim_sup B ; ::_thesis: F = Intersection (superior_setsequence B)
 for x being set holds
( x in F iff x in Intersection (superior_setsequence B) )
proof
let x be set ; ::_thesis: ( x in F iff x in Intersection (superior_setsequence B) )
hereby  ::_thesis: ( x in Intersection (superior_setsequence B) implies x in F )
assume A2: x in F ; ::_thesis: x in Intersection (superior_setsequence B)
 for m being Element of NAT holds x in (superior_setsequence B) . m
proof
let m be Element of NAT ; ::_thesis: x in (superior_setsequence B) . m
 ex k being Element of NAT st x in B . (m + k) by A1, A2, KURATO_0:5;
hence  x in (superior_setsequence B) . m by Th20; ::_thesis: verum
end;
hence  x in Intersection (superior_setsequence B) by PROB_1:13; ::_thesis: verum
end;
assume A3: x in Intersection (superior_setsequence B) ; ::_thesis: x in F
now__::_thesis:_for_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_x_in_B_._(m_+_k)
let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k)
 x in (superior_setsequence B) . m by A3, PROB_1:13;
hence  ex k being Element of NAT st x in B . (m + k) by Th20; ::_thesis: verum
end;
hence  x in F by A1, KURATO_0:5; ::_thesis: verum
end;
hence  F = Intersection (superior_setsequence B) by TARSKI:1; ::_thesis: verum
end;
assume A4: F = Intersection (superior_setsequence B) ; ::_thesis: F = lim_sup B
 for x being set holds
( x in F iff x in lim_sup B )
proof
let x be set ; ::_thesis: ( x in F iff x in lim_sup B )
hereby  ::_thesis: ( x in lim_sup B implies x in F )
assume A5: x in F ; ::_thesis: x in lim_sup B
now__::_thesis:_for_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_x_in_B_._(m_+_k)
let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k)
 x in (superior_setsequence B) . m by A4, A5, PROB_1:13;
hence  ex k being Element of NAT st x in B . (m + k) by Th20; ::_thesis: verum
end;
hence  x in lim_sup B by KURATO_0:5; ::_thesis: verum
end;
assume A6: x in lim_sup B ; ::_thesis: x in F
 for m being Element of NAT holds x in (superior_setsequence B) . m
proof
let m be Element of NAT ; ::_thesis: x in (superior_setsequence B) . m
 ex k being Element of NAT st x in B . (m + k) by A6, KURATO_0:5;
hence  x in (superior_setsequence B) . m by Th20; ::_thesis: verum
end;
hence  x in F by A4, PROB_1:13; ::_thesis: verum
end;
hence  F = lim_sup B by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem  defines lim_sup SETLIM_1:def_5_:_
 for X being set
for B being SetSequence of X holds lim_sup B = Intersection (superior_setsequence B);

notation
let X be set ;
let B be SetSequence of X;
synonym  lim B for  lim_sup B;
end;

theorem :: SETLIM_1:54
for X being set
for B being SetSequence of X holds Intersection B c= lim_inf B
proof
let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B c= lim_inf B
let B be SetSequence of X; ::_thesis: Intersection B c= lim_inf B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection B or x in lim_inf B )
assume  x in Intersection B ; ::_thesis: x in lim_inf B
then  for k being Element of NAT holds x in B . (0 + k) by PROB_1:13;
hence  x in lim_inf B by KURATO_0:4; ::_thesis: verum
end;

theorem :: SETLIM_1:55
for X being set
for B being SetSequence of X holds lim_inf B = lim (inferior_setsequence B) by Th43;

theorem :: SETLIM_1:56
for X being set
for B being SetSequence of X holds lim_sup B = lim (superior_setsequence B) by Th49;

theorem :: SETLIM_1:57
for X being set
for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) `
proof
let X be set ; ::_thesis: for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) `
let B be SetSequence of X; ::_thesis: lim_sup B = (lim_inf (Complement B)) `
lim_inf (Complement B) = (lim_sup (Complement (Complement B))) ` by KURATO_0:9
.= (lim_sup B) ` ;
hence  lim_sup B = (lim_inf (Complement B)) ` ; ::_thesis: verum
end;

theorem Th58: :: SETLIM_1:58
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
proof
let X be set ; ::_thesis: for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) )
assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )
then  for n being Element of NAT holds (superior_setsequence B) . n = A by Th39;
then A2: lim_sup B = A by Th11;
 for n being Element of NAT holds (inferior_setsequence B) . n = A by A1, Th38;
then  lim_inf B = A by Th10;
hence  ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) by A2, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_1:59
for X being set
for B being SetSequence of X st B is V50() holds
lim_sup B = Union B by Th43;

theorem :: SETLIM_1:60
for X being set
for B being SetSequence of X st B is V50() holds
lim_inf B = Union B by Th46;

theorem :: SETLIM_1:61
for X being set
for B being SetSequence of X st B is V49() holds
lim_sup B = Intersection B by Th49;

theorem :: SETLIM_1:62
for X being set
for B being SetSequence of X st B is V49() holds
lim_inf B = Intersection B by Th53;

theorem Th63: :: SETLIM_1:63
for X being set
for B being SetSequence of X st B is V50() holds
( B is convergent & lim B = Union B )
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds
( B is convergent & lim B = Union B )
let B be SetSequence of X; ::_thesis: ( B is V50() implies ( B is convergent & lim B = Union B ) )
assume A1: B is V50() ; ::_thesis: ( B is convergent & lim B = Union B )
then  ( lim_sup B = Union B & lim_inf B = Union B ) by Th43, Th46;
hence  B is convergent by KURATO_0:def_5; ::_thesis: lim B = Union B
thus  lim B = Union B by A1, Th43; ::_thesis: verum
end;

theorem Th64: :: SETLIM_1:64
for X being set
for B being SetSequence of X st B is V49() holds
( B is convergent & lim B = Intersection B )
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds
( B is convergent & lim B = Intersection B )
let B be SetSequence of X; ::_thesis: ( B is V49() implies ( B is convergent & lim B = Intersection B ) )
assume A1: B is V49() ; ::_thesis: ( B is convergent & lim B = Intersection B )
then  ( lim_sup B = Intersection B & lim_inf B = Intersection B ) by Th49, Th53;
hence  B is convergent by KURATO_0:def_5; ::_thesis: lim B = Intersection B
thus  lim B = Intersection B by A1, Th49; ::_thesis: verum
end;

theorem :: SETLIM_1:65
for X being set
for B being SetSequence of X st B is monotone holds
B is convergent
proof
let X be set ; ::_thesis: for B being SetSequence of X st B is monotone holds
B is convergent
let B be SetSequence of X; ::_thesis: ( B is monotone implies B is convergent )
assume A1: B is monotone ; ::_thesis: B is convergent
percases ( not B is V49() or not B is V50() ) by A1, Def1;
suppose B is V49() ; ::_thesis: B is convergent
hence  B is convergent by Th64; ::_thesis: verum
end;
suppose B is V50() ; ::_thesis: B is convergent
hence  B is convergent by Th63; ::_thesis: verum
end;
end;
end;

definition
let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
:: original: inferior_setsequence
redefine func inferior_setsequence S ->  SetSequence of Si;
coherence
 inferior_setsequence S is SetSequence of Si
proof
now__::_thesis:_for_n_being_Nat_holds_(inferior_setsequence_S)_._n_in_Si
let n be Nat; ::_thesis: (inferior_setsequence S) . n in Si
reconsider DSeq = S ^\ n as SetSequence of X ;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
 for m being Nat holds DSeq . m in Si
proof
let m be Nat; ::_thesis: DSeq . m in Si
 ( DSeq . m = S . (m + n1) & S . (m + n1) in rng S ) by NAT_1:51, NAT_1:def_3;
hence  DSeq . m in Si ; ::_thesis: verum
end;
then  rng DSeq c= Si by NAT_1:52;
then A1: Intersection DSeq in Si by PROB_1:def_6;
 Intersection DSeq = meet (rng DSeq) by Th8;
then  Intersection DSeq = meet  {  (S . k) where k is Element of NAT : n1 <= k  }  by Th6;
hence  (inferior_setsequence S) . n in Si by A1, Def2; ::_thesis: verum
end;
then  rng (inferior_setsequence S) c= Si by NAT_1:52;
hence  inferior_setsequence S is SetSequence of Si by RELAT_1:def_19; ::_thesis: verum
end;
end;

definition
let X be set ;
let Si be SigmaField of X;
let S be SetSequence of Si;
:: original: superior_setsequence
redefine func superior_setsequence S ->  SetSequence of Si;
coherence
 superior_setsequence S is SetSequence of Si
proof
now__::_thesis:_for_n_being_Nat_holds_(superior_setsequence_S)_._n_in_Si
let n be Nat; ::_thesis: (superior_setsequence S) . n in Si
reconsider DSeq = S ^\ n as SetSequence of X ;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
 for m being Nat holds DSeq . m in Si
proof
let m be Nat; ::_thesis: DSeq . m in Si
 ( DSeq . m = S . (m + n1) & S . (m + n1) in rng S ) by NAT_1:51, NAT_1:def_3;
hence  DSeq . m in Si ; ::_thesis: verum
end;
then  rng DSeq c= Si by NAT_1:52;
then  DSeq is SetSequence of Si by RELAT_1:def_19;
then A1: Union DSeq in Si by PROB_1:17;
 Union DSeq = union (rng DSeq) by CARD_3:def_4;
then  Union DSeq = union  {  (S . k) where k is Element of NAT : n1 <= k  }  by Th6;
hence  (superior_setsequence S) . n in Si by A1, Def3; ::_thesis: verum
end;
then  rng (superior_setsequence S) c= Si by NAT_1:52;
hence  superior_setsequence S is SetSequence of Si by RELAT_1:def_19; ::_thesis: verum
end;
end;

theorem Th66: :: SETLIM_1:66
for X, x being set
for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) )
proof
let X, x be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) )
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds
( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) )
let S be SetSequence of Si; ::_thesis: ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) )
 for B being SetSequence of X holds
( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of NAT st x in B . (n + k) )
proof
let B be SetSequence of X; ::_thesis: ( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of NAT st x in B . (n + k) )
 lim_sup B = Intersection (superior_setsequence B) ;
hence  ( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of NAT st x in B . (n + k) ) by KURATO_0:5; ::_thesis: verum
end;
hence  ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) ) ; ::_thesis: verum
end;

theorem Th67: :: SETLIM_1:67
for X, x being set
for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
proof
let X, x be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
let S be SetSequence of Si; ::_thesis: ( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
 for B being SetSequence of X holds
( x in Union (inferior_setsequence B) iff ex n being Element of NAT st
for k being Element of NAT holds x in B . (n + k) )
proof
let B be SetSequence of X; ::_thesis: ( x in Union (inferior_setsequence B) iff ex n being Element of NAT st
for k being Element of NAT holds x in B . (n + k) )
 lim_inf B = Union (inferior_setsequence B) ;
hence  ( x in Union (inferior_setsequence B) iff ex n being Element of NAT st
for k being Element of NAT holds x in B . (n + k) ) by KURATO_0:4; ::_thesis: verum
end;
hence  ( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) ) ; ::_thesis: verum
end;

theorem :: SETLIM_1:68
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds Intersection S c= lim_inf S
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si holds Intersection S c= lim_inf S
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds Intersection S c= lim_inf S
let S be SetSequence of Si; ::_thesis: Intersection S c= lim_inf S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection S or x in lim_inf S )
assume  x in Intersection S ; ::_thesis: x in lim_inf S
then  for k being Element of NAT holds x in S . (0 + k) by PROB_1:13;
hence  x in lim_inf S by Th67; ::_thesis: verum
end;

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

theorem :: SETLIM_1:70
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S c= lim_sup S
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S c= lim_sup S
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_inf S c= lim_sup S
let S be SetSequence of Si; ::_thesis: lim_inf S c= lim_sup S
 for B being SetSequence of X holds Union (inferior_setsequence B) c= Intersection (superior_setsequence B)
proof
let B be SetSequence of X; ::_thesis: Union (inferior_setsequence B) c= Intersection (superior_setsequence B)
 ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ;
hence  Union (inferior_setsequence B) c= Intersection (superior_setsequence B) by KURATO_0:6; ::_thesis: verum
end;
hence  lim_inf S c= lim_sup S ; ::_thesis: verum
end;

theorem Th71: :: SETLIM_1:71
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `
let S be SetSequence of Si; ::_thesis: lim_inf S = (lim_sup (Complement S)) `
 for B being SetSequence of X holds Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) `
proof
let B be SetSequence of X; ::_thesis: Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) `
 ( lim_inf B = Union (inferior_setsequence B) & (lim_sup (Complement B)) ` = (Intersection (superior_setsequence (Complement B))) ` ) ;
hence  Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) ` by KURATO_0:9; ::_thesis: verum
end;
hence  lim_inf S = (lim_sup (Complement S)) ` ; ::_thesis: verum
end;

theorem :: SETLIM_1:72
for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) `
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) `
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) `
let S be SetSequence of Si; ::_thesis: lim_sup S = (lim_inf (Complement S)) `
lim_inf (Complement S) = (lim_sup (Complement (Complement S))) ` by Th71
.= (lim_sup S) ` ;
hence  lim_sup S = (lim_inf (Complement S)) ` ; ::_thesis: verum
end;

theorem :: SETLIM_1:73
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) implies (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 )
A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) holds
(Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3)
proof
let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) implies (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) )
A2: ( lim_inf B = Union (inferior_setsequence B) & lim_inf A2 = Union (inferior_setsequence A2) ) ;
A3: lim_inf A3 = Union (inferior_setsequence A3) ;
assume  for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ; ::_thesis: (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3)
hence  (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) by A2, A3, KURATO_0:12; ::_thesis: verum
end;
assume  for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ; ::_thesis: (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
hence  (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 by A1; ::_thesis: verum
end;

theorem :: SETLIM_1:74
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) implies lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) )
A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) holds
(Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3)
proof
let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) implies (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) )
A2: ( lim_inf B = Union (inferior_setsequence B) & lim_inf A2 = Union (inferior_setsequence A2) ) ;
A3: lim_inf A3 = Union (inferior_setsequence A3) ;
assume  for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ; ::_thesis: (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3)
hence  (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) by A2, A3, KURATO_0:10; ::_thesis: verum
end;
assume  for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ; ::_thesis: lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)
hence  lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) by A1; ::_thesis: verum
end;

theorem :: SETLIM_1:75
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)
let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)
let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) implies lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) )
A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) holds
(Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3)
proof
let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) implies (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) )
A2: ( lim_sup B = Intersection (superior_setsequence B) & lim_sup A2 = Intersection (superior_setsequence A2) ) ;
A3: lim_sup A3 = Intersection (superior_setsequence A3) ;
assume  for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ; ::_thesis: (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3)
hence  (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) by A2, A3, KURATO_0:11; ::_thesis: verum
end;
assume  for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ; ::_thesis: lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)
hence  lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) by A1; ::_thesis: verum
end;

theorem :: SETLIM_1:76
for X being set
for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2)
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2)
let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2)
let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) implies lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) )
A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) holds
Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2))
proof
let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) implies Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2)) )
A2: ( lim_sup B = Intersection (superior_setsequence B) & lim_sup A2 = Intersection (superior_setsequence A2) ) ;
A3: lim_sup A3 = Intersection (superior_setsequence A3) ;
assume  for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ; ::_thesis: Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2))
hence  Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2)) by A2, A3, KURATO_0:13; ::_thesis: verum
end;
assume  for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ; ::_thesis: lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2)
hence  lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) by A1; ::_thesis: verum
end;

theorem :: SETLIM_1:77
for X being set
for A being Subset of X
for Si being SigmaField of X
for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
proof
let X be set ; ::_thesis: for A being Subset of X
for Si being SigmaField of X
for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let A be Subset of X; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is constant & the_value_of S = A holds
( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let S be SetSequence of Si; ::_thesis: ( S is constant & the_value_of S = A implies ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) )
A1: for B being SetSequence of X st B is constant & the_value_of B = A holds
( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )
proof
let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) )
A2: ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ;
assume  ( B is constant & the_value_of B = A ) ; ::_thesis: ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )
hence  ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) by A2, Th58; ::_thesis: verum
end;
assume  ( S is constant & the_value_of S = A ) ; ::_thesis: ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
then  ( lim_inf S = A & lim_sup S = A ) by A1;
hence  ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) by KURATO_0:def_5; ::_thesis: verum
end;

theorem Th78: :: SETLIM_1:78
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
lim_sup S = Union S by Th43;

theorem Th79: :: SETLIM_1:79
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
lim_inf S = Union S by Th46;

theorem Th80: :: SETLIM_1:80
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
( S is convergent & lim S = Union S )
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si st S is V50() holds
( S is convergent & lim S = Union S )
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is V50() holds
( S is convergent & lim S = Union S )
let S be SetSequence of Si; ::_thesis: ( S is V50() implies ( S is convergent & lim S = Union S ) )
assume A1: S is V50() ; ::_thesis: ( S is convergent & lim S = Union S )
then  ( lim_sup S = Union S & lim_inf S = Union S ) by Th78, Th79;
hence  S is convergent by KURATO_0:def_5; ::_thesis: lim S = Union S
thus  lim S = Union S by A1, Th78; ::_thesis: verum
end;

theorem Th81: :: SETLIM_1:81
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
lim_sup S = Intersection S by Th49;

theorem Th82: :: SETLIM_1:82
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
lim_inf S = Intersection S by Th53;

theorem Th83: :: SETLIM_1:83
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
( S is convergent & lim S = Intersection S )
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si st S is V49() holds
( S is convergent & lim S = Intersection S )
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is V49() holds
( S is convergent & lim S = Intersection S )
let S be SetSequence of Si; ::_thesis: ( S is V49() implies ( S is convergent & lim S = Intersection S ) )
assume A1: S is V49() ; ::_thesis: ( S is convergent & lim S = Intersection S )
then  ( lim_sup S = Intersection S & lim_inf S = Intersection S ) by Th81, Th82;
hence  S is convergent by KURATO_0:def_5; ::_thesis: lim S = Intersection S
thus  lim S = Intersection S by A1, Th81; ::_thesis: verum
end;

theorem :: SETLIM_1:84
for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is monotone holds
S is convergent
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for S being SetSequence of Si st S is monotone holds
S is convergent
let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is monotone holds
S is convergent
let S be SetSequence of Si; ::_thesis: ( S is monotone implies S is convergent )
assume A1: S is monotone ; ::_thesis: S is convergent
percases ( not S is V49() or not S is V50() ) by A1, Def1;
suppose S is V49() ; ::_thesis: S is convergent
hence  S is convergent by Th83; ::_thesis: verum
end;
suppose S is V50() ; ::_thesis: S is convergent
hence  S is convergent by Th80; ::_thesis: verum
end;
end;
end;