:: SETLIM_2 semantic presentation

begin


theorem Th1: :: SETLIM_2:1
for n being Element of NAT
for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
let X be set ; ::_thesis: for A1 being SetSequence of X holds (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
let A1 be SetSequence of X; ::_thesis: (inferior_setsequence A1) . n = Intersection (A1 ^\ n)
reconsider Y =  {  (A1 . k) where k is Element of NAT : n <= k  }  as Subset-Family of X by SETLIM_1:28;
(inferior_setsequence A1) . n = meet Y by SETLIM_1:def_2
.= meet (rng (A1 ^\ n)) by SETLIM_1:6 ;
hence  (inferior_setsequence A1) . n = Intersection (A1 ^\ n) by SETLIM_1:8; ::_thesis: verum
end;

theorem Th2: :: SETLIM_2:2
for n being Element of NAT
for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)
let X be set ; ::_thesis: for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)
let A1 be SetSequence of X; ::_thesis: (superior_setsequence A1) . n = Union (A1 ^\ n)
reconsider Y =  {  (A1 . k) where k is Element of NAT : n <= k  }  as Subset-Family of X by SETLIM_1:28;
(superior_setsequence A1) . n = union Y by SETLIM_1:def_3
.= union (rng (A1 ^\ n)) by SETLIM_1:6 ;
hence  (superior_setsequence A1) . n = Union (A1 ^\ n) by CARD_3:def_4; ::_thesis: verum
end;

definition
let X be set ;
let A1, A2 be SetSequence of X;
funcA1 (/\) A2 ->  SetSequence of X means :Def1: :: SETLIM_2:def 1
 for n being Element of NAT holds it . n = (A1 . n) /\ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = (A1 . $1) /\ (A2 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) /\ (A2 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Element of NAT holds A4 . n = (A1 . n) /\ (A2 . n) ) implies A3 = A4 )
assume that
A1: for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) and
A2: for n being Element of NAT holds A4 . n = (A1 . n) /\ (A2 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) /\ (A2 . n) by A1
.= A4 . n by A2 ; ::_thesis: verum
end;
commutativity
 for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) /\ (A1 . n) ;
funcA1 (\/) A2 ->  SetSequence of X means :Def2: :: SETLIM_2:def 2
 for n being Element of NAT holds it . n = (A1 . n) \/ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = (A1 . $1) \/ (A2 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \/ (A2 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) & ( for n being Element of NAT holds A4 . n = (A1 . n) \/ (A2 . n) ) implies A3 = A4 )
assume that
A3: for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) and
A4: for n being Element of NAT holds A4 . n = (A1 . n) \/ (A2 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) \/ (A2 . n) by A3
.= A4 . n by A4 ; ::_thesis: verum
end;
commutativity
 for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \/ (A1 . n) ;
funcA1 (\) A2 ->  SetSequence of X means :Def3: :: SETLIM_2:def 3
 for n being Element of NAT holds it . n = (A1 . n) \ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = (A1 . $1) \ (A2 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \ (A2 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \ (A2 . n) ) & ( for n being Element of NAT holds A4 . n = (A1 . n) \ (A2 . n) ) implies A3 = A4 )
assume that
A5: for n being Element of NAT holds A3 . n = (A1 . n) \ (A2 . n) and
A6: for n being Element of NAT holds A4 . n = (A1 . n) \ (A2 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) \ (A2 . n) by A5
.= A4 . n by A6 ; ::_thesis: verum
end;
funcA1 (\+\) A2 ->  SetSequence of X means :Def4: :: SETLIM_2:def 4
 for n being Element of NAT holds it . n = (A1 . n) \+\ (A2 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = (A1 . $1) \+\ (A2 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \+\ (A2 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \+\ (A2 . n) ) & ( for n being Element of NAT holds A4 . n = (A1 . n) \+\ (A2 . n) ) implies A3 = A4 )
assume that
A7: for n being Element of NAT holds A3 . n = (A1 . n) \+\ (A2 . n) and
A8: for n being Element of NAT holds A4 . n = (A1 . n) \+\ (A2 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) \+\ (A2 . n) by A7
.= A4 . n by A8 ; ::_thesis: verum
end;
commutativity
 for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \+\ (A1 . n) ;
end;

:: deftheorem Def1 defines (/\) SETLIM_2:def_1_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (/\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) /\ (A2 . n) );

:: deftheorem Def2 defines (\/) SETLIM_2:def_2_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\/) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \/ (A2 . n) );

:: deftheorem Def3 defines (\) SETLIM_2:def_3_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \ (A2 . n) );

:: deftheorem Def4 defines (\+\) SETLIM_2:def_4_:_
 for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\+\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \+\ (A2 . n) );

theorem Th3: :: SETLIM_2:3
for X being set
for A1, A2 being SetSequence of X holds A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1)
let A1, A2 be SetSequence of X; ::_thesis: A1 (\+\) A2 = (A1 (\) A2) (\/) (A2 (\) A1)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (A1 (\+\) A2) . n = ((A1 (\) A2) (\/) (A2 (\) A1)) . n
thus (A1 (\+\) A2) . n = (A1 . n) \+\ (A2 . n) by Def4
.= ((A1 (\) A2) . n) \/ ((A2 . n) \ (A1 . n)) by Def3
.= ((A1 (\) A2) . n) \/ ((A2 (\) A1) . n) by Def3
.= ((A1 (\) A2) (\/) (A2 (\) A1)) . n by Def2 ; ::_thesis: verum
end;

theorem Th4: :: SETLIM_2:4
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)
let A1, A2 be SetSequence of X; ::_thesis: (A1 (/\) A2) ^\ k = (A1 ^\ k) (/\) (A2 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A1 (/\) A2) ^\ k) . n = ((A1 ^\ k) (/\) (A2 ^\ k)) . n
thus ((A1 (/\) A2) ^\ k) . n = (A1 (/\) A2) . (n + k) by NAT_1:def_3
.= (A1 . (n + k)) /\ (A2 . (n + k)) by Def1
.= ((A1 ^\ k) . n) /\ (A2 . (n + k)) by NAT_1:def_3
.= ((A1 ^\ k) . n) /\ ((A2 ^\ k) . n) by NAT_1:def_3
.= ((A1 ^\ k) (/\) (A2 ^\ k)) . n by Def1 ; ::_thesis: verum
end;

theorem Th5: :: SETLIM_2:5
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (\/) A2) ^\ k = (A1 ^\ k) (\/) (A2 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (A1 (\/) A2) ^\ k = (A1 ^\ k) (\/) (A2 ^\ k)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (A1 (\/) A2) ^\ k = (A1 ^\ k) (\/) (A2 ^\ k)
let A1, A2 be SetSequence of X; ::_thesis: (A1 (\/) A2) ^\ k = (A1 ^\ k) (\/) (A2 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A1 (\/) A2) ^\ k) . n = ((A1 ^\ k) (\/) (A2 ^\ k)) . n
thus ((A1 (\/) A2) ^\ k) . n = (A1 (\/) A2) . (n + k) by NAT_1:def_3
.= (A1 . (n + k)) \/ (A2 . (n + k)) by Def2
.= ((A1 ^\ k) . n) \/ (A2 . (n + k)) by NAT_1:def_3
.= ((A1 ^\ k) . n) \/ ((A2 ^\ k) . n) by NAT_1:def_3
.= ((A1 ^\ k) (\/) (A2 ^\ k)) . n by Def2 ; ::_thesis: verum
end;

theorem Th6: :: SETLIM_2:6
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (\) A2) ^\ k = (A1 ^\ k) (\) (A2 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (A1 (\) A2) ^\ k = (A1 ^\ k) (\) (A2 ^\ k)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (A1 (\) A2) ^\ k = (A1 ^\ k) (\) (A2 ^\ k)
let A1, A2 be SetSequence of X; ::_thesis: (A1 (\) A2) ^\ k = (A1 ^\ k) (\) (A2 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A1 (\) A2) ^\ k) . n = ((A1 ^\ k) (\) (A2 ^\ k)) . n
thus ((A1 (\) A2) ^\ k) . n = (A1 (\) A2) . (n + k) by NAT_1:def_3
.= (A1 . (n + k)) \ (A2 . (n + k)) by Def3
.= ((A1 ^\ k) . n) \ (A2 . (n + k)) by NAT_1:def_3
.= ((A1 ^\ k) . n) \ ((A2 ^\ k) . n) by NAT_1:def_3
.= ((A1 ^\ k) (\) (A2 ^\ k)) . n by Def3 ; ::_thesis: verum
end;

theorem Th7: :: SETLIM_2:7
for k being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (A1 (\+\) A2) ^\ k = (A1 ^\ k) (\+\) (A2 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (A1 (\+\) A2) ^\ k = (A1 ^\ k) (\+\) (A2 ^\ k)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (A1 (\+\) A2) ^\ k = (A1 ^\ k) (\+\) (A2 ^\ k)
let A1, A2 be SetSequence of X; ::_thesis: (A1 (\+\) A2) ^\ k = (A1 ^\ k) (\+\) (A2 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A1 (\+\) A2) ^\ k) . n = ((A1 ^\ k) (\+\) (A2 ^\ k)) . n
thus ((A1 (\+\) A2) ^\ k) . n = (A1 (\+\) A2) . (n + k) by NAT_1:def_3
.= (A1 . (n + k)) \+\ (A2 . (n + k)) by Def4
.= ((A1 ^\ k) . n) \+\ (A2 . (n + k)) by NAT_1:def_3
.= ((A1 ^\ k) . n) \+\ ((A2 ^\ k) . n) by NAT_1:def_3
.= ((A1 ^\ k) (\+\) (A2 ^\ k)) . n by Def4 ; ::_thesis: verum
end;

theorem Th8: :: SETLIM_2:8
for X being set
for A1, A2 being SetSequence of X holds Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)
let A1, A2 be SetSequence of X; ::_thesis: Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (A1 (/\) A2) or x in (Union A1) /\ (Union A2) )
assume  x in Union (A1 (/\) A2) ; ::_thesis: x in (Union A1) /\ (Union A2)
then consider n being Element of NAT  such that
A1: x in (A1 (/\) A2) . n by PROB_1:12;
A2: x in (A1 . n) /\ (A2 . n) by A1, Def1;
then  x in A2 . n by XBOOLE_0:def_4;
then A3: x in Union A2 by PROB_1:12;
 x in A1 . n by A2, XBOOLE_0:def_4;
then  x in Union A1 by PROB_1:12;
hence  x in (Union A1) /\ (Union A2) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th9: :: SETLIM_2:9
for X being set
for A1, A2 being SetSequence of X holds Union (A1 (\/) A2) = (Union A1) \/ (Union A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds Union (A1 (\/) A2) = (Union A1) \/ (Union A2)
let A1, A2 be SetSequence of X; ::_thesis: Union (A1 (\/) A2) = (Union A1) \/ (Union A2)
thus  Union (A1 (\/) A2) c= (Union A1) \/ (Union A2) :: according to XBOOLE_0:def_10 ::_thesis: (Union A1) \/ (Union A2) c= Union (A1 (\/) A2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (A1 (\/) A2) or x in (Union A1) \/ (Union A2) )
assume  x in Union (A1 (\/) A2) ; ::_thesis: x in (Union A1) \/ (Union A2)
then consider n1 being Element of NAT  such that
A1: x in (A1 (\/) A2) . n1 by PROB_1:12;
A2: x in (A1 . n1) \/ (A2 . n1) by A1, Def2;
percases ( x in A1 . n1 or x in A2 . n1 ) by A2, XBOOLE_0:def_3;
suppose x in A1 . n1 ; ::_thesis: x in (Union A1) \/ (Union A2)
then  x in Union A1 by PROB_1:12;
hence  x in (Union A1) \/ (Union A2) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in A2 . n1 ; ::_thesis: x in (Union A1) \/ (Union A2)
then  x in Union A2 by PROB_1:12;
hence  x in (Union A1) \/ (Union A2) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union A1) \/ (Union A2) or x in Union (A1 (\/) A2) )
assume A3: x in (Union A1) \/ (Union A2) ; ::_thesis: x in Union (A1 (\/) A2)
percases ( x in Union A1 or x in Union A2 ) by A3, XBOOLE_0:def_3;
suppose x in Union A1 ; ::_thesis: x in Union (A1 (\/) A2)
then consider n2 being Element of NAT  such that
A4: x in A1 . n2 by PROB_1:12;
 x in (A1 . n2) \/ (A2 . n2) by A4, XBOOLE_0:def_3;
then  x in (A1 (\/) A2) . n2 by Def2;
hence  x in Union (A1 (\/) A2) by PROB_1:12; ::_thesis: verum
end;
suppose x in Union A2 ; ::_thesis: x in Union (A1 (\/) A2)
then consider n3 being Element of NAT  such that
A5: x in A2 . n3 by PROB_1:12;
 x in (A1 . n3) \/ (A2 . n3) by A5, XBOOLE_0:def_3;
then  x in (A1 (\/) A2) . n3 by Def2;
hence  x in Union (A1 (\/) A2) by PROB_1:12; ::_thesis: verum
end;
end;
end;

theorem Th10: :: SETLIM_2:10
for X being set
for A1, A2 being SetSequence of X holds (Union A1) \ (Union A2) c= Union (A1 (\) A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (Union A1) \ (Union A2) c= Union (A1 (\) A2)
let A1, A2 be SetSequence of X; ::_thesis: (Union A1) \ (Union A2) c= Union (A1 (\) A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union A1) \ (Union A2) or x in Union (A1 (\) A2) )
assume A1: x in (Union A1) \ (Union A2) ; ::_thesis: x in Union (A1 (\) A2)
then  x in Union A1 by XBOOLE_0:def_5;
then consider n1 being Element of NAT  such that
A2: x in A1 . n1 by PROB_1:12;
 not x in Union A2 by A1, XBOOLE_0:def_5;
then  not x in A2 . n1 by PROB_1:12;
then  x in (A1 . n1) \ (A2 . n1) by A2, XBOOLE_0:def_5;
then  x in (A1 (\) A2) . n1 by Def3;
hence  x in Union (A1 (\) A2) by PROB_1:12; ::_thesis: verum
end;

theorem Th11: :: SETLIM_2:11
for X being set
for A1, A2 being SetSequence of X holds (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2)
let A1, A2 be SetSequence of X; ::_thesis: (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2)
A1: ( (Union A1) \ (Union A2) c= Union (A1 (\) A2) & (Union A2) \ (Union A1) c= Union (A2 (\) A1) ) by Th10;
(Union (A1 (\) A2)) \/ (Union (A2 (\) A1)) = Union ((A1 (\) A2) (\/) (A2 (\) A1)) by Th9
.= Union (A1 (\+\) A2) by Th3 ;
hence  (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2) by A1, XBOOLE_1:13; ::_thesis: verum
end;

theorem Th12: :: SETLIM_2:12
for X being set
for A1, A2 being SetSequence of X holds Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)
let A1, A2 be SetSequence of X; ::_thesis: Intersection (A1 (/\) A2) = (Intersection A1) /\ (Intersection A2)
thus  Intersection (A1 (/\) A2) c= (Intersection A1) /\ (Intersection A2) :: according to XBOOLE_0:def_10 ::_thesis: (Intersection A1) /\ (Intersection A2) c= Intersection (A1 (/\) A2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A1 (/\) A2) or x in (Intersection A1) /\ (Intersection A2) )
assume A1: x in Intersection (A1 (/\) A2) ; ::_thesis: x in (Intersection A1) /\ (Intersection A2)
now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A1_._k_&_x_in_A2_._k_)
let k be Element of NAT ; ::_thesis: ( x in A1 . k & x in A2 . k )
 x in (A1 (/\) A2) . k by A1, PROB_1:13;
then  x in (A1 . k) /\ (A2 . k) by Def1;
hence  ( x in A1 . k & x in A2 . k ) by XBOOLE_0:def_4; ::_thesis: verum
end;
then  ( x in Intersection A1 & x in Intersection A2 ) by PROB_1:13;
hence  x in (Intersection A1) /\ (Intersection A2) by XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Intersection A1) /\ (Intersection A2) or x in Intersection (A1 (/\) A2) )
assume  x in (Intersection A1) /\ (Intersection A2) ; ::_thesis: x in Intersection (A1 (/\) A2)
then A2: ( x in Intersection A1 & x in Intersection A2 ) by XBOOLE_0:def_4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(/\)_A2)_._k
let k be Element of NAT ; ::_thesis: x in (A1 (/\) A2) . k
 ( x in A1 . k & x in A2 . k ) by A2, PROB_1:13;
then  x in (A1 . k) /\ (A2 . k) by XBOOLE_0:def_4;
hence  x in (A1 (/\) A2) . k by Def1; ::_thesis: verum
end;
hence  x in Intersection (A1 (/\) A2) by PROB_1:13; ::_thesis: verum
end;

theorem Th13: :: SETLIM_2:13
for X being set
for A1, A2 being SetSequence of X holds (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)
let A1, A2 be SetSequence of X; ::_thesis: (Intersection A1) \/ (Intersection A2) c= Intersection (A1 (\/) A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Intersection A1) \/ (Intersection A2) or x in Intersection (A1 (\/) A2) )
assume A1: x in (Intersection A1) \/ (Intersection A2) ; ::_thesis: x in Intersection (A1 (\/) A2)
percases ( x in Intersection A1 or x in Intersection A2 ) by A1, XBOOLE_0:def_3;
supposeA2: x in Intersection A1 ; ::_thesis: x in Intersection (A1 (\/) A2)
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(\/)_A2)_._k
let k be Element of NAT ; ::_thesis: x in (A1 (\/) A2) . k
 x in A1 . k by A2, PROB_1:13;
then  x in (A1 . k) \/ (A2 . k) by XBOOLE_0:def_3;
hence  x in (A1 (\/) A2) . k by Def2; ::_thesis: verum
end;
hence  x in Intersection (A1 (\/) A2) by PROB_1:13; ::_thesis: verum
end;
supposeA3: x in Intersection A2 ; ::_thesis: x in Intersection (A1 (\/) A2)
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(\/)_A2)_._k
let k be Element of NAT ; ::_thesis: x in (A1 (\/) A2) . k
 x in A2 . k by A3, PROB_1:13;
then  x in (A1 . k) \/ (A2 . k) by XBOOLE_0:def_3;
hence  x in (A1 (\/) A2) . k by Def2; ::_thesis: verum
end;
hence  x in Intersection (A1 (\/) A2) by PROB_1:13; ::_thesis: verum
end;
end;
end;

theorem Th14: :: SETLIM_2:14
for X being set
for A1, A2 being SetSequence of X holds Intersection (A1 (\) A2) c= (Intersection A1) \ (Intersection A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds Intersection (A1 (\) A2) c= (Intersection A1) \ (Intersection A2)
let A1, A2 be SetSequence of X; ::_thesis: Intersection (A1 (\) A2) c= (Intersection A1) \ (Intersection A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A1 (\) A2) or x in (Intersection A1) \ (Intersection A2) )
assume A1: x in Intersection (A1 (\) A2) ; ::_thesis: x in (Intersection A1) \ (Intersection A2)
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A1_._k_&_not_x_in_A2_._k_)
let k be Element of NAT ; ::_thesis: ( x in A1 . k & not x in A2 . k )
 x in (A1 (\) A2) . k by A1, PROB_1:13;
then  x in (A1 . k) \ (A2 . k) by Def3;
hence  ( x in A1 . k & not x in A2 . k ) by XBOOLE_0:def_5; ::_thesis: verum
end;
then  not x in A2 . 0 ;
then A3: not x in Intersection A2 by PROB_1:13;
 x in Intersection A1 by A2, PROB_1:13;
hence  x in (Intersection A1) \ (Intersection A2) by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

definition
let X be set ;
let A1 be SetSequence of X;
let A be Subset of X;
funcA (/\) A1 ->  SetSequence of X means :Def5: :: SETLIM_2:def 5
 for n being Element of NAT holds it . n = A /\ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A /\ (A1 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = A /\ (A1 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A /\ (A1 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A /\ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A /\ (A1 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = A /\ (A1 . n) ) & ( for n being Element of NAT holds A4 . n = A /\ (A1 . n) ) implies A3 = A4 )
assume that
A1: for n being Element of NAT holds A3 . n = A /\ (A1 . n) and
A2: for n being Element of NAT holds A4 . n = A /\ (A1 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = A /\ (A1 . n) by A1
.= A4 . n by A2 ; ::_thesis: verum
end;
funcA (\/) A1 ->  SetSequence of X means :Def6: :: SETLIM_2:def 6
 for n being Element of NAT holds it . n = A \/ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \/ (A1 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = A \/ (A1 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \/ (A1 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A \/ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A \/ (A1 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = A \/ (A1 . n) ) & ( for n being Element of NAT holds A4 . n = A \/ (A1 . n) ) implies A3 = A4 )
assume that
A3: for n being Element of NAT holds A3 . n = A \/ (A1 . n) and
A4: for n being Element of NAT holds A4 . n = A \/ (A1 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = A \/ (A1 . n) by A3
.= A4 . n by A4 ; ::_thesis: verum
end;
funcA (\) A1 ->  SetSequence of X means :Def7: :: SETLIM_2:def 7
 for n being Element of NAT holds it . n = A \ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \ (A1 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = A \ (A1 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \ (A1 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A \ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A \ (A1 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = A \ (A1 . n) ) & ( for n being Element of NAT holds A4 . n = A \ (A1 . n) ) implies A3 = A4 )
assume that
A5: for n being Element of NAT holds A3 . n = A \ (A1 . n) and
A6: for n being Element of NAT holds A4 . n = A \ (A1 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = A \ (A1 . n) by A5
.= A4 . n by A6 ; ::_thesis: verum
end;
funcA1 (\) A ->  SetSequence of X means :Def8: :: SETLIM_2:def 8
 for n being Element of NAT holds it . n = (A1 . n) \ A;
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ A
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = (A1 . $1) \ A;
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ A ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \ A ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \ A ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \ A ) & ( for n being Element of NAT holds A4 . n = (A1 . n) \ A ) implies A3 = A4 )
assume that
A7: for n being Element of NAT holds A3 . n = (A1 . n) \ A and
A8: for n being Element of NAT holds A4 . n = (A1 . n) \ A ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = (A1 . n) \ A by A7
.= A4 . n by A8 ; ::_thesis: verum
end;
funcA (\+\) A1 ->  SetSequence of X means :Def9: :: SETLIM_2:def 9
 for n being Element of NAT holds it . n = A \+\ (A1 . n);
existence
 ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \+\ (A1 . n)
proof
deffunc H1( Element of NAT ) ->  Element of K10(X) = A \+\ (A1 . $1);
 ex f being SetSequence of X st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
hence  ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = A \+\ (A1 . n) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = A \+\ (A1 . n) ) & ( for n being Element of NAT holds b2 . n = A \+\ (A1 . n) ) holds
b1 = b2
proof
let A3, A4 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = A \+\ (A1 . n) ) & ( for n being Element of NAT holds A4 . n = A \+\ (A1 . n) ) implies A3 = A4 )
assume that
A9: for n being Element of NAT holds A3 . n = A \+\ (A1 . n) and
A10: for n being Element of NAT holds A4 . n = A \+\ (A1 . n) ; ::_thesis: A3 = A4
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: A3 . n = A4 . n
thus A3 . n = A \+\ (A1 . n) by A9
.= A4 . n by A10 ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines (/\) SETLIM_2:def_5_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (/\) A1 iff for n being Element of NAT holds b4 . n = A /\ (A1 . n) );

:: deftheorem Def6 defines (\/) SETLIM_2:def_6_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\/) A1 iff for n being Element of NAT holds b4 . n = A \/ (A1 . n) );

:: deftheorem Def7 defines (\) SETLIM_2:def_7_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\) A1 iff for n being Element of NAT holds b4 . n = A \ (A1 . n) );

:: deftheorem Def8 defines (\) SETLIM_2:def_8_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A1 (\) A iff for n being Element of NAT holds b4 . n = (A1 . n) \ A );

:: deftheorem Def9 defines (\+\) SETLIM_2:def_9_:_
 for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\+\) A1 iff for n being Element of NAT holds b4 . n = A \+\ (A1 . n) );

theorem :: SETLIM_2:15
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
let A1 be SetSequence of X; ::_thesis: A (\+\) A1 = (A (\) A1) (\/) (A1 (\) A)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (A (\+\) A1) . n = ((A (\) A1) (\/) (A1 (\) A)) . n
thus (A (\+\) A1) . n = A \+\ (A1 . n) by Def9
.= ((A (\) A1) . n) \/ ((A1 . n) \ A) by Def7
.= ((A (\) A1) . n) \/ ((A1 (\) A) . n) by Def8
.= ((A (\) A1) (\/) (A1 (\) A)) . n by Def2 ; ::_thesis: verum
end;

theorem Th16: :: SETLIM_2:16
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)
let A1 be SetSequence of X; ::_thesis: (A (/\) A1) ^\ k = A (/\) (A1 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A (/\) A1) ^\ k) . n = (A (/\) (A1 ^\ k)) . n
thus ((A (/\) A1) ^\ k) . n = (A (/\) A1) . (n + k) by NAT_1:def_3
.= A /\ (A1 . (n + k)) by Def5
.= A /\ ((A1 ^\ k) . n) by NAT_1:def_3
.= (A (/\) (A1 ^\ k)) . n by Def5 ; ::_thesis: verum
end;

theorem Th17: :: SETLIM_2:17
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)
let A1 be SetSequence of X; ::_thesis: (A (\/) A1) ^\ k = A (\/) (A1 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A (\/) A1) ^\ k) . n = (A (\/) (A1 ^\ k)) . n
thus ((A (\/) A1) ^\ k) . n = (A (\/) A1) . (n + k) by NAT_1:def_3
.= A \/ (A1 . (n + k)) by Def6
.= A \/ ((A1 ^\ k) . n) by NAT_1:def_3
.= (A (\/) (A1 ^\ k)) . n by Def6 ; ::_thesis: verum
end;

theorem Th18: :: SETLIM_2:18
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\) A1) ^\ k = A (\) (A1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\) A1) ^\ k = A (\) (A1 ^\ k)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (A (\) A1) ^\ k = A (\) (A1 ^\ k)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (A (\) A1) ^\ k = A (\) (A1 ^\ k)
let A1 be SetSequence of X; ::_thesis: (A (\) A1) ^\ k = A (\) (A1 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A (\) A1) ^\ k) . n = (A (\) (A1 ^\ k)) . n
thus ((A (\) A1) ^\ k) . n = (A (\) A1) . (n + k) by NAT_1:def_3
.= A \ (A1 . (n + k)) by Def7
.= A \ ((A1 ^\ k) . n) by NAT_1:def_3
.= (A (\) (A1 ^\ k)) . n by Def7 ; ::_thesis: verum
end;

theorem Th19: :: SETLIM_2:19
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
proof
let k be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let A1 be SetSequence of X; ::_thesis: (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A1 (\) A) ^\ k) . n = ((A1 ^\ k) (\) A) . n
thus ((A1 (\) A) ^\ k) . n = (A1 (\) A) . (n + k) by NAT_1:def_3
.= (A1 . (n + k)) \ A by Def8
.= ((A1 ^\ k) . n) \ A by NAT_1:def_3
.= ((A1 ^\ k) (\) A) . n by Def8 ; ::_thesis: verum
end;

theorem Th20: :: SETLIM_2:20
for k being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let A1 be SetSequence of X; ::_thesis: (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((A (\+\) A1) ^\ k) . n = (A (\+\) (A1 ^\ k)) . n
thus ((A (\+\) A1) ^\ k) . n = (A (\+\) A1) . (n + k) by NAT_1:def_3
.= A \+\ (A1 . (n + k)) by Def9
.= A \+\ ((A1 ^\ k) . n) by NAT_1:def_3
.= (A (\+\) (A1 ^\ k)) . n by Def9 ; ::_thesis: verum
end;

theorem Th21: :: SETLIM_2:21
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (/\) A1 is non-ascending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (/\) A1 is non-ascending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-ascending holds
A (/\) A1 is non-ascending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-ascending implies A (/\) A1 is non-ascending )
assume A1: A1 is non-ascending ; ::_thesis: A (/\) A1 is non-ascending
 for n, m being Element of NAT st n <= m holds
(A (/\) A1) . m c= (A (/\) A1) . n
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A (/\) A1) . m c= (A (/\) A1) . n )
assume  n <= m ; ::_thesis: (A (/\) A1) . m c= (A (/\) A1) . n
then  A1 . m c= A1 . n by A1, PROB_1:def_4;
then  A /\ (A1 . m) c= A /\ (A1 . n) by XBOOLE_1:27;
then  (A (/\) A1) . m c= A /\ (A1 . n) by Def5;
hence  (A (/\) A1) . m c= (A (/\) A1) . n by Def5; ::_thesis: verum
end;
hence  A (/\) A1 is non-ascending by PROB_1:def_4; ::_thesis: verum
end;

theorem Th22: :: SETLIM_2:22
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (/\) A1 is non-descending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (/\) A1 is non-descending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
A (/\) A1 is non-descending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies A (/\) A1 is non-descending )
assume A1: A1 is non-descending ; ::_thesis: A (/\) A1 is non-descending
 for n, m being Element of NAT st n <= m holds
(A (/\) A1) . n c= (A (/\) A1) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A (/\) A1) . n c= (A (/\) A1) . m )
assume  n <= m ; ::_thesis: (A (/\) A1) . n c= (A (/\) A1) . m
then  A1 . n c= A1 . m by A1, PROB_1:def_5;
then  A /\ (A1 . n) c= A /\ (A1 . m) by XBOOLE_1:27;
then  (A (/\) A1) . n c= A /\ (A1 . m) by Def5;
hence  (A (/\) A1) . n c= (A (/\) A1) . m by Def5; ::_thesis: verum
end;
hence  A (/\) A1 is non-descending by PROB_1:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:23
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (/\) A1 is monotone
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (/\) A1 is monotone
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is monotone holds
A (/\) A1 is monotone
let A1 be SetSequence of X; ::_thesis: ( A1 is monotone implies A (/\) A1 is monotone )
assume A1: A1 is monotone ; ::_thesis: A (/\) A1 is monotone
percases ( A1 is non-ascending or A1 is non-descending ) by A1, SETLIM_1:def_1;
suppose A1 is non-ascending ; ::_thesis: A (/\) A1 is monotone
then  A (/\) A1 is non-ascending by Th21;
hence  A (/\) A1 is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
suppose A1 is non-descending ; ::_thesis: A (/\) A1 is monotone
then  A (/\) A1 is non-descending by Th22;
hence  A (/\) A1 is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
end;
end;

theorem Th24: :: SETLIM_2:24
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (\/) A1 is non-ascending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (\/) A1 is non-ascending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-ascending holds
A (\/) A1 is non-ascending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-ascending implies A (\/) A1 is non-ascending )
assume A1: A1 is non-ascending ; ::_thesis: A (\/) A1 is non-ascending
 for n, m being Element of NAT st n <= m holds
(A (\/) A1) . m c= (A (\/) A1) . n
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A (\/) A1) . m c= (A (\/) A1) . n )
assume  n <= m ; ::_thesis: (A (\/) A1) . m c= (A (\/) A1) . n
then  A1 . m c= A1 . n by A1, PROB_1:def_4;
then  A \/ (A1 . m) c= A \/ (A1 . n) by XBOOLE_1:9;
then  (A (\/) A1) . m c= A \/ (A1 . n) by Def6;
hence  (A (\/) A1) . m c= (A (\/) A1) . n by Def6; ::_thesis: verum
end;
hence  A (\/) A1 is non-ascending by PROB_1:def_4; ::_thesis: verum
end;

theorem Th25: :: SETLIM_2:25
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (\/) A1 is non-descending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (\/) A1 is non-descending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
A (\/) A1 is non-descending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies A (\/) A1 is non-descending )
assume A1: A1 is non-descending ; ::_thesis: A (\/) A1 is non-descending
 for n, m being Element of NAT st n <= m holds
(A (\/) A1) . n c= (A (\/) A1) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A (\/) A1) . n c= (A (\/) A1) . m )
assume  n <= m ; ::_thesis: (A (\/) A1) . n c= (A (\/) A1) . m
then  A1 . n c= A1 . m by A1, PROB_1:def_5;
then  A \/ (A1 . n) c= A \/ (A1 . m) by XBOOLE_1:9;
then  (A (\/) A1) . n c= A \/ (A1 . m) by Def6;
hence  (A (\/) A1) . n c= (A (\/) A1) . m by Def6; ::_thesis: verum
end;
hence  A (\/) A1 is non-descending by PROB_1:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:26
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (\/) A1 is monotone
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (\/) A1 is monotone
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is monotone holds
A (\/) A1 is monotone
let A1 be SetSequence of X; ::_thesis: ( A1 is monotone implies A (\/) A1 is monotone )
assume A1: A1 is monotone ; ::_thesis: A (\/) A1 is monotone
percases ( A1 is non-ascending or A1 is non-descending ) by A1, SETLIM_1:def_1;
suppose A1 is non-ascending ; ::_thesis: A (\/) A1 is monotone
then  A (\/) A1 is non-ascending by Th24;
hence  A (\/) A1 is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
suppose A1 is non-descending ; ::_thesis: A (\/) A1 is monotone
then  A (\/) A1 is non-descending by Th25;
hence  A (\/) A1 is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
end;
end;

theorem Th27: :: SETLIM_2:27
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (\) A1 is non-descending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A (\) A1 is non-descending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-ascending holds
A (\) A1 is non-descending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-ascending implies A (\) A1 is non-descending )
assume A1: A1 is non-ascending ; ::_thesis: A (\) A1 is non-descending
 for n, m being Element of NAT st n <= m holds
(A (\) A1) . n c= (A (\) A1) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A (\) A1) . n c= (A (\) A1) . m )
assume  n <= m ; ::_thesis: (A (\) A1) . n c= (A (\) A1) . m
then  A1 . m c= A1 . n by A1, PROB_1:def_4;
then  A \ (A1 . n) c= A \ (A1 . m) by XBOOLE_1:34;
then  (A (\) A1) . n c= A \ (A1 . m) by Def7;
hence  (A (\) A1) . n c= (A (\) A1) . m by Def7; ::_thesis: verum
end;
hence  A (\) A1 is non-descending by PROB_1:def_5; ::_thesis: verum
end;

theorem Th28: :: SETLIM_2:28
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (\) A1 is non-ascending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (\) A1 is non-ascending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
A (\) A1 is non-ascending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies A (\) A1 is non-ascending )
assume A1: A1 is non-descending ; ::_thesis: A (\) A1 is non-ascending
 for n, m being Element of NAT st n <= m holds
(A (\) A1) . m c= (A (\) A1) . n
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A (\) A1) . m c= (A (\) A1) . n )
assume  n <= m ; ::_thesis: (A (\) A1) . m c= (A (\) A1) . n
then  A1 . n c= A1 . m by A1, PROB_1:def_5;
then  A \ (A1 . m) c= A \ (A1 . n) by XBOOLE_1:34;
then  (A (\) A1) . m c= A \ (A1 . n) by Def7;
hence  (A (\) A1) . m c= (A (\) A1) . n by Def7; ::_thesis: verum
end;
hence  A (\) A1 is non-ascending by PROB_1:def_4; ::_thesis: verum
end;

theorem :: SETLIM_2:29
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (\) A1 is monotone
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (\) A1 is monotone
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is monotone holds
A (\) A1 is monotone
let A1 be SetSequence of X; ::_thesis: ( A1 is monotone implies A (\) A1 is monotone )
assume A1: A1 is monotone ; ::_thesis: A (\) A1 is monotone
percases ( A1 is non-ascending or A1 is non-descending ) by A1, SETLIM_1:def_1;
suppose A1 is non-ascending ; ::_thesis: A (\) A1 is monotone
then  A (\) A1 is non-descending by Th27;
hence  A (\) A1 is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
suppose A1 is non-descending ; ::_thesis: A (\) A1 is monotone
then  A (\) A1 is non-ascending by Th28;
hence  A (\) A1 is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
end;
end;

theorem Th30: :: SETLIM_2:30
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A1 (\) A is non-ascending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-ascending holds
A1 (\) A is non-ascending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-ascending holds
A1 (\) A is non-ascending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-ascending implies A1 (\) A is non-ascending )
assume A1: A1 is non-ascending ; ::_thesis: A1 (\) A is non-ascending
 for n, m being Element of NAT st n <= m holds
(A1 (\) A) . m c= (A1 (\) A) . n
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A1 (\) A) . m c= (A1 (\) A) . n )
assume  n <= m ; ::_thesis: (A1 (\) A) . m c= (A1 (\) A) . n
then  A1 . m c= A1 . n by A1, PROB_1:def_4;
then  (A1 . m) \ A c= (A1 . n) \ A by XBOOLE_1:33;
then  (A1 (\) A) . m c= (A1 . n) \ A by Def8;
hence  (A1 (\) A) . m c= (A1 (\) A) . n by Def8; ::_thesis: verum
end;
hence  A1 (\) A is non-ascending by PROB_1:def_4; ::_thesis: verum
end;

theorem Th31: :: SETLIM_2:31
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A1 (\) A is non-descending
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A1 (\) A is non-descending
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
A1 (\) A is non-descending
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies A1 (\) A is non-descending )
assume A1: A1 is non-descending ; ::_thesis: A1 (\) A is non-descending
 for n, m being Element of NAT st n <= m holds
(A1 (\) A) . n c= (A1 (\) A) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (A1 (\) A) . n c= (A1 (\) A) . m )
assume  n <= m ; ::_thesis: (A1 (\) A) . n c= (A1 (\) A) . m
then  A1 . n c= A1 . m by A1, PROB_1:def_5;
then  (A1 . n) \ A c= (A1 . m) \ A by XBOOLE_1:33;
then  (A1 (\) A) . n c= (A1 . m) \ A by Def8;
hence  (A1 (\) A) . n c= (A1 (\) A) . m by Def8; ::_thesis: verum
end;
hence  A1 (\) A is non-descending by PROB_1:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:32
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A1 (\) A is monotone
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A1 (\) A is monotone
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is monotone holds
A1 (\) A is monotone
let A1 be SetSequence of X; ::_thesis: ( A1 is monotone implies A1 (\) A is monotone )
assume A1: A1 is monotone ; ::_thesis: A1 (\) A is monotone
percases ( A1 is non-ascending or A1 is non-descending ) by A1, SETLIM_1:def_1;
suppose A1 is non-ascending ; ::_thesis: A1 (\) A is monotone
then  A1 (\) A is non-ascending by Th30;
hence  A1 (\) A is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
suppose A1 is non-descending ; ::_thesis: A1 (\) A is monotone
then  A1 (\) A is non-descending by Th31;
hence  A1 (\) A is monotone by SETLIM_1:def_1; ::_thesis: verum
end;
end;
end;

theorem Th33: :: SETLIM_2:33
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (/\) A1) = A /\ (Intersection A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (/\) A1) = A /\ (Intersection A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Intersection (A (/\) A1) = A /\ (Intersection A1)
let A1 be SetSequence of X; ::_thesis: Intersection (A (/\) A1) = A /\ (Intersection A1)
thus  Intersection (A (/\) A1) c= A /\ (Intersection A1) :: according to XBOOLE_0:def_10 ::_thesis: A /\ (Intersection A1) c= Intersection (A (/\) A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A (/\) A1) or x in A /\ (Intersection A1) )
assume A1: x in Intersection (A (/\) A1) ; ::_thesis: x in A /\ (Intersection A1)
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A_&_x_in_A1_._k_)
let k be Element of NAT ; ::_thesis: ( x in A & x in A1 . k )
 x in (A (/\) A1) . k by A1, PROB_1:13;
then  x in A /\ (A1 . k) by Def5;
hence  ( x in A & x in A1 . k ) by XBOOLE_0:def_4; ::_thesis: verum
end;
then  x in Intersection A1 by PROB_1:13;
hence  x in A /\ (Intersection A1) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ (Intersection A1) or x in Intersection (A (/\) A1) )
assume A3: x in A /\ (Intersection A1) ; ::_thesis: x in Intersection (A (/\) A1)
then A4: x in Intersection A1 by XBOOLE_0:def_4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A_(/\)_A1)_._k
let k be Element of NAT ; ::_thesis: x in (A (/\) A1) . k
 ( x in A & x in A1 . k ) by A3, A4, PROB_1:13, XBOOLE_0:def_4;
then  x in A /\ (A1 . k) by XBOOLE_0:def_4;
hence  x in (A (/\) A1) . k by Def5; ::_thesis: verum
end;
hence  x in Intersection (A (/\) A1) by PROB_1:13; ::_thesis: verum
end;

theorem Th34: :: SETLIM_2:34
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\/) A1) = A \/ (Intersection A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\/) A1) = A \/ (Intersection A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Intersection (A (\/) A1) = A \/ (Intersection A1)
let A1 be SetSequence of X; ::_thesis: Intersection (A (\/) A1) = A \/ (Intersection A1)
thus  Intersection (A (\/) A1) c= A \/ (Intersection A1) :: according to XBOOLE_0:def_10 ::_thesis: A \/ (Intersection A1) c= Intersection (A (\/) A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A (\/) A1) or x in A \/ (Intersection A1) )
assume A1: x in Intersection (A (\/) A1) ; ::_thesis: x in A \/ (Intersection A1)
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A_or_x_in_A1_._k_)
let k be Element of NAT ; ::_thesis: ( x in A or x in A1 . k )
 x in (A (\/) A1) . k by A1, PROB_1:13;
then  x in A \/ (A1 . k) by Def6;
hence  ( x in A or x in A1 . k ) by XBOOLE_0:def_3; ::_thesis: verum
end;
percases ( x in A or for k being Element of NAT holds x in A1 . k ) by A2;
suppose x in A ; ::_thesis: x in A \/ (Intersection A1)
hence  x in A \/ (Intersection A1) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose for k being Element of NAT holds x in A1 . k ; ::_thesis: x in A \/ (Intersection A1)
then  x in Intersection A1 by PROB_1:13;
hence  x in A \/ (Intersection A1) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \/ (Intersection A1) or x in Intersection (A (\/) A1) )
assume A3: x in A \/ (Intersection A1) ; ::_thesis: x in Intersection (A (\/) A1)
percases ( x in A or x in Intersection A1 ) by A3, XBOOLE_0:def_3;
supposeA4: x in A ; ::_thesis: x in Intersection (A (\/) A1)
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A_(\/)_A1)_._k
let k be Element of NAT ; ::_thesis: x in (A (\/) A1) . k
 x in A \/ (A1 . k) by A4, XBOOLE_0:def_3;
hence  x in (A (\/) A1) . k by Def6; ::_thesis: verum
end;
hence  x in Intersection (A (\/) A1) by PROB_1:13; ::_thesis: verum
end;
supposeA5: x in Intersection A1 ; ::_thesis: x in Intersection (A (\/) A1)
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A_(\/)_A1)_._k
let k be Element of NAT ; ::_thesis: x in (A (\/) A1) . k
 x in A1 . k by A5, PROB_1:13;
then  x in A \/ (A1 . k) by XBOOLE_0:def_3;
hence  x in (A (\/) A1) . k by Def6; ::_thesis: verum
end;
hence  x in Intersection (A (\/) A1) by PROB_1:13; ::_thesis: verum
end;
end;
end;

theorem Th35: :: SETLIM_2:35
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\) A1) c= A \ (Intersection A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\) A1) c= A \ (Intersection A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Intersection (A (\) A1) c= A \ (Intersection A1)
let A1 be SetSequence of X; ::_thesis: Intersection (A (\) A1) c= A \ (Intersection A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A (\) A1) or x in A \ (Intersection A1) )
assume A1: x in Intersection (A (\) A1) ; ::_thesis: x in A \ (Intersection A1)
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A_&_not_x_in_A1_._k_)
let k be Element of NAT ; ::_thesis: ( x in A & not x in A1 . k )
 x in (A (\) A1) . k by A1, PROB_1:13;
then  x in A \ (A1 . k) by Def7;
hence  ( x in A & not x in A1 . k ) by XBOOLE_0:def_5; ::_thesis: verum
end;
then  not x in A1 . 0 ;
then  not x in Intersection A1 by PROB_1:13;
hence  x in A \ (Intersection A1) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th36: :: SETLIM_2:36
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A1 (\) A) = (Intersection A1) \ A
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A1 (\) A) = (Intersection A1) \ A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Intersection (A1 (\) A) = (Intersection A1) \ A
let A1 be SetSequence of X; ::_thesis: Intersection (A1 (\) A) = (Intersection A1) \ A
thus  Intersection (A1 (\) A) c= (Intersection A1) \ A :: according to XBOOLE_0:def_10 ::_thesis: (Intersection A1) \ A c= Intersection (A1 (\) A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A1 (\) A) or x in (Intersection A1) \ A )
assume A1: x in Intersection (A1 (\) A) ; ::_thesis: x in (Intersection A1) \ A
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A1_._k_&_not_x_in_A_)
let k be Element of NAT ; ::_thesis: ( x in A1 . k & not x in A )
 x in (A1 (\) A) . k by A1, PROB_1:13;
then  x in (A1 . k) \ A by Def8;
hence  ( x in A1 . k & not x in A ) by XBOOLE_0:def_5; ::_thesis: verum
end;
then  x in Intersection A1 by PROB_1:13;
hence  x in (Intersection A1) \ A by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Intersection A1) \ A or x in Intersection (A1 (\) A) )
assume A3: x in (Intersection A1) \ A ; ::_thesis: x in Intersection (A1 (\) A)
then A4: x in Intersection A1 by XBOOLE_0:def_5;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(\)_A)_._k
let k be Element of NAT ; ::_thesis: x in (A1 (\) A) . k
 ( x in A1 . k & not x in A ) by A3, A4, PROB_1:13, XBOOLE_0:def_5;
then  x in (A1 . k) \ A by XBOOLE_0:def_5;
hence  x in (A1 (\) A) . k by Def8; ::_thesis: verum
end;
hence  x in Intersection (A1 (\) A) by PROB_1:13; ::_thesis: verum
end;

theorem Th37: :: SETLIM_2:37
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
let A1 be SetSequence of X; ::_thesis: Intersection (A (\+\) A1) c= A \+\ (Intersection A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (A (\+\) A1) or x in A \+\ (Intersection A1) )
assume A1: x in Intersection (A (\+\) A1) ; ::_thesis: x in A \+\ (Intersection A1)
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(_x_in_A_&_not_x_in_A1_._n_)_or_(_not_x_in_A_&_x_in_A1_._n_)_)
let n be Element of NAT ; ::_thesis: ( ( x in A & not x in A1 . n ) or ( not x in A & x in A1 . n ) )
 x in (A (\+\) A1) . n by A1, PROB_1:13;
then  x in A \+\ (A1 . n) by Def9;
hence  ( ( x in A & not x in A1 . n ) or ( not x in A & x in A1 . n ) ) by XBOOLE_0:1; ::_thesis: verum
end;
assume  not x in A \+\ (Intersection A1) ; ::_thesis: contradiction
then A3: ( ( not x in A & not x in Intersection A1 ) or ( x in Intersection A1 & x in A ) ) by XBOOLE_0:1;
percases ( ( not x in A & not for n being Element of NAT holds x in A1 . n ) or ( x in A & ( for n being Element of NAT holds x in A1 . n ) ) ) by A3, PROB_1:13;
suppose ( not x in A & not for n being Element of NAT holds x in A1 . n ) ; ::_thesis: contradiction
hence  contradiction by A2; ::_thesis: verum
end;
supposeA4: ( x in A & ( for n being Element of NAT holds x in A1 . n ) ) ; ::_thesis: contradiction
then  x in A1 . 0 ;
hence  contradiction by A2, A4; ::_thesis: verum
end;
end;
end;

theorem Th38: :: SETLIM_2:38
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Union (A (/\) A1) = A /\ (Union A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Union (A (/\) A1) = A /\ (Union A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Union (A (/\) A1) = A /\ (Union A1)
let A1 be SetSequence of X; ::_thesis: Union (A (/\) A1) = A /\ (Union A1)
thus  Union (A (/\) A1) c= A /\ (Union A1) :: according to XBOOLE_0:def_10 ::_thesis: A /\ (Union A1) c= Union (A (/\) A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (A (/\) A1) or x in A /\ (Union A1) )
assume  x in Union (A (/\) A1) ; ::_thesis: x in A /\ (Union A1)
then consider n being Element of NAT  such that
A1: x in (A (/\) A1) . n by PROB_1:12;
A2: x in A /\ (A1 . n) by A1, Def5;
then  x in A1 . n by XBOOLE_0:def_4;
then A3: x in Union A1 by PROB_1:12;
 x in A by A2, XBOOLE_0:def_4;
hence  x in A /\ (Union A1) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ (Union A1) or x in Union (A (/\) A1) )
assume A4: x in A /\ (Union A1) ; ::_thesis: x in Union (A (/\) A1)
then  x in Union A1 by XBOOLE_0:def_4;
then consider n being Element of NAT  such that
A5: x in A1 . n by PROB_1:12;
 x in A by A4, XBOOLE_0:def_4;
then  x in A /\ (A1 . n) by A5, XBOOLE_0:def_4;
then  x in (A (/\) A1) . n by Def5;
hence  x in Union (A (/\) A1) by PROB_1:12; ::_thesis: verum
end;

theorem Th39: :: SETLIM_2:39
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Union (A (\/) A1) = A \/ (Union A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Union (A (\/) A1) = A \/ (Union A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Union (A (\/) A1) = A \/ (Union A1)
let A1 be SetSequence of X; ::_thesis: Union (A (\/) A1) = A \/ (Union A1)
thus  Union (A (\/) A1) c= A \/ (Union A1) :: according to XBOOLE_0:def_10 ::_thesis: A \/ (Union A1) c= Union (A (\/) A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (A (\/) A1) or x in A \/ (Union A1) )
assume A1: x in Union (A (\/) A1) ; ::_thesis: x in A \/ (Union A1)
A2: ( x in A or ex k being Element of NAT st x in A1 . k )
proof
consider k being Element of NAT  such that
A3: x in (A (\/) A1) . k by A1, PROB_1:12;
 x in A \/ (A1 . k) by A3, Def6;
then  ( x in A or x in A1 . k ) by XBOOLE_0:def_3;
hence  ( x in A or ex k being Element of NAT st x in A1 . k ) ; ::_thesis: verum
end;
percases ( x in A or ex k being Element of NAT st x in A1 . k ) by A2;
suppose x in A ; ::_thesis: x in A \/ (Union A1)
hence  x in A \/ (Union A1) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ex k being Element of NAT st x in A1 . k ; ::_thesis: x in A \/ (Union A1)
then  x in Union A1 by PROB_1:12;
hence  x in A \/ (Union A1) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \/ (Union A1) or x in Union (A (\/) A1) )
assume A4: x in A \/ (Union A1) ; ::_thesis: x in Union (A (\/) A1)
percases ( x in A or x in Union A1 ) by A4, XBOOLE_0:def_3;
suppose x in A ; ::_thesis: x in Union (A (\/) A1)
then  x in A \/ (A1 . 1) by XBOOLE_0:def_3;
then  x in (A (\/) A1) . 1 by Def6;
hence  x in Union (A (\/) A1) by PROB_1:12; ::_thesis: verum
end;
suppose x in Union A1 ; ::_thesis: x in Union (A (\/) A1)
then consider k being Element of NAT  such that
A5: x in A1 . k by PROB_1:12;
 x in A \/ (A1 . k) by A5, XBOOLE_0:def_3;
then  x in (A (\/) A1) . k by Def6;
hence  x in Union (A (\/) A1) by PROB_1:12; ::_thesis: verum
end;
end;
end;

theorem Th40: :: SETLIM_2:40
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ (Union A1) c= Union (A (\) A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A \ (Union A1) c= Union (A (\) A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A \ (Union A1) c= Union (A (\) A1)
let A1 be SetSequence of X; ::_thesis: A \ (Union A1) c= Union (A (\) A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ (Union A1) or x in Union (A (\) A1) )
assume A1: x in A \ (Union A1) ; ::_thesis: x in Union (A (\) A1)
then A2: not x in Union A1 by XBOOLE_0:def_5;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A_(\)_A1)_._k
let k be Element of NAT ; ::_thesis: x in (A (\) A1) . k
 ( x in A & not x in A1 . k ) by A1, A2, PROB_1:12, XBOOLE_0:def_5;
then  x in A \ (A1 . k) by XBOOLE_0:def_5;
hence  x in (A (\) A1) . k by Def7; ::_thesis: verum
end;
then  x in (A (\) A1) . 1 ;
hence  x in Union (A (\) A1) by PROB_1:12; ::_thesis: verum
end;

theorem Th41: :: SETLIM_2:41
for X being set
for A being Subset of X
for A1 being SetSequence of X holds Union (A1 (\) A) = (Union A1) \ A
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds Union (A1 (\) A) = (Union A1) \ A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds Union (A1 (\) A) = (Union A1) \ A
let A1 be SetSequence of X; ::_thesis: Union (A1 (\) A) = (Union A1) \ A
thus  Union (A1 (\) A) c= (Union A1) \ A :: according to XBOOLE_0:def_10 ::_thesis: (Union A1) \ A c= Union (A1 (\) A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (A1 (\) A) or x in (Union A1) \ A )
assume A1: x in Union (A1 (\) A) ; ::_thesis: x in (Union A1) \ A
A2: ex k being Element of NAT st
( x in A1 . k & not x in A )
proof
consider k being Element of NAT  such that
A3: x in (A1 (\) A) . k by A1, PROB_1:12;
 x in (A1 . k) \ A by A3, Def8;
then  ( x in A1 . k & not x in A ) by XBOOLE_0:def_5;
hence  ex k being Element of NAT st
( x in A1 . k & not x in A ) ; ::_thesis: verum
end;
then  x in Union A1 by PROB_1:12;
hence  x in (Union A1) \ A by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union A1) \ A or x in Union (A1 (\) A) )
assume A4: x in (Union A1) \ A ; ::_thesis: x in Union (A1 (\) A)
then A5: not x in A by XBOOLE_0:def_5;
A6: x in Union A1 by A4, XBOOLE_0:def_5;
 ex k being Element of NAT st x in (A1 (\) A) . k
proof
consider k being Element of NAT  such that
A7: x in A1 . k by A6, PROB_1:12;
 x in (A1 . k) \ A by A5, A7, XBOOLE_0:def_5;
then  x in (A1 (\) A) . k by Def8;
hence  ex k being Element of NAT st x in (A1 (\) A) . k ; ::_thesis: verum
end;
hence  x in Union (A1 (\) A) by PROB_1:12; ::_thesis: verum
end;

theorem Th42: :: SETLIM_2:42
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ (Union A1) c= Union (A (\+\) A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A \+\ (Union A1) c= Union (A (\+\) A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A \+\ (Union A1) c= Union (A (\+\) A1)
let A1 be SetSequence of X; ::_thesis: A \+\ (Union A1) c= Union (A (\+\) A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \+\ (Union A1) or x in Union (A (\+\) A1) )
assume A1: x in A \+\ (Union A1) ; ::_thesis: x in Union (A (\+\) A1)
percases ( ( x in A & not x in Union A1 ) or ( not x in A & x in Union A1 ) ) by A1, XBOOLE_0:1;
supposeA2: ( x in A & not x in Union A1 ) ; ::_thesis: x in Union (A (\+\) A1)
then  not x in A1 . 0 by PROB_1:12;
then  x in A \+\ (A1 . 0) by A2, XBOOLE_0:1;
then  x in (A (\+\) A1) . 0 by Def9;
hence  x in Union (A (\+\) A1) by PROB_1:12; ::_thesis: verum
end;
supposeA3: ( not x in A & x in Union A1 ) ; ::_thesis: x in Union (A (\+\) A1)
then consider n1 being Element of NAT  such that
A4: x in A1 . n1 by PROB_1:12;
 x in A \+\ (A1 . n1) by A3, A4, XBOOLE_0:1;
then  x in (A (\+\) A1) . n1 by Def9;
hence  x in Union (A (\+\) A1) by PROB_1:12; ::_thesis: verum
end;
end;
end;

theorem :: SETLIM_2:43
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (/\) A2)) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (/\) A2)) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (/\) A2)) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
let A1, A2 be SetSequence of X; ::_thesis: (inferior_setsequence (A1 (/\) A2)) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n)
(inferior_setsequence (A1 (/\) A2)) . n = Intersection ((A1 (/\) A2) ^\ n) by Th1
.= Intersection ((A1 ^\ n) (/\) (A2 ^\ n)) by Th4
.= (Intersection (A1 ^\ n)) /\ (Intersection (A2 ^\ n)) by Th12
.= ((inferior_setsequence A1) . n) /\ (Intersection (A2 ^\ n)) by Th1
.= ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) by Th1 ;
hence  (inferior_setsequence (A1 (/\) A2)) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) ; ::_thesis: verum
end;

theorem :: SETLIM_2:44
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
let A1, A2 be SetSequence of X; ::_thesis: ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
A1: Intersection ((A1 ^\ n) (\/) (A2 ^\ n)) = Intersection ((A1 (\/) A2) ^\ n) by Th5
.= (inferior_setsequence (A1 (\/) A2)) . n by Th1 ;
((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) = (Intersection (A1 ^\ n)) \/ ((inferior_setsequence A2) . n) by Th1
.= (Intersection (A1 ^\ n)) \/ (Intersection (A2 ^\ n)) by Th1 ;
hence  ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n by A1, Th13; ::_thesis: verum
end;

theorem :: SETLIM_2:45
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
let A1, A2 be SetSequence of X; ::_thesis: (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
(inferior_setsequence (A1 (\) A2)) . n = Intersection ((A1 (\) A2) ^\ n) by Th1
.= Intersection ((A1 ^\ n) (\) (A2 ^\ n)) by Th6 ;
then  (inferior_setsequence (A1 (\) A2)) . n c= (Intersection (A1 ^\ n)) \ (Intersection (A2 ^\ n)) by Th14;
then  (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ (Intersection (A2 ^\ n)) by Th1;
hence  (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n) by Th1; ::_thesis: verum
end;

theorem :: SETLIM_2:46
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
let A1, A2 be SetSequence of X; ::_thesis: (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
(superior_setsequence (A1 (/\) A2)) . n = Union ((A1 (/\) A2) ^\ n) by Th2
.= Union ((A1 ^\ n) (/\) (A2 ^\ n)) by Th4 ;
then  (superior_setsequence (A1 (/\) A2)) . n c= (Union (A1 ^\ n)) /\ (Union (A2 ^\ n)) by Th8;
then  (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ (Union (A2 ^\ n)) by Th2;
hence  (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) by Th2; ::_thesis: verum
end;

theorem :: SETLIM_2:47
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (\/) A2)) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (\/) A2)) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (\/) A2)) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
let A1, A2 be SetSequence of X; ::_thesis: (superior_setsequence (A1 (\/) A2)) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
(superior_setsequence (A1 (\/) A2)) . n = Union ((A1 (\/) A2) ^\ n) by Th2
.= Union ((A1 ^\ n) (\/) (A2 ^\ n)) by Th5
.= (Union (A1 ^\ n)) \/ (Union (A2 ^\ n)) by Th9
.= ((superior_setsequence A1) . n) \/ (Union (A2 ^\ n)) by Th2 ;
hence  (superior_setsequence (A1 (\/) A2)) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) by Th2; ::_thesis: verum
end;

theorem :: SETLIM_2:48
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
let A1, A2 be SetSequence of X; ::_thesis: ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) = (Union (A1 ^\ n)) \ ((superior_setsequence A2) . n) by Th2
.= (Union (A1 ^\ n)) \ (Union (A2 ^\ n)) by Th2 ;
then  ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= Union ((A1 ^\ n) (\) (A2 ^\ n)) by Th10;
then  ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= Union ((A1 (\) A2) ^\ n) by Th6;
hence  ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n by Th2; ::_thesis: verum
end;

theorem :: SETLIM_2:49
for n being Element of NAT
for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
let A1, A2 be SetSequence of X; ::_thesis: ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) = (Union (A1 ^\ n)) \+\ ((superior_setsequence A2) . n) by Th2
.= (Union (A1 ^\ n)) \+\ (Union (A2 ^\ n)) by Th2 ;
then  ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= Union ((A1 ^\ n) (\+\) (A2 ^\ n)) by Th11;
then  ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= Union ((A1 (\+\) A2) ^\ n) by Th7;
hence  ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n by Th2; ::_thesis: verum
end;

theorem Th50: :: SETLIM_2:50
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n)
let A1 be SetSequence of X; ::_thesis: (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n)
(inferior_setsequence (A (/\) A1)) . n = Intersection ((A (/\) A1) ^\ n) by Th1
.= Intersection (A (/\) (A1 ^\ n)) by Th16
.= A /\ (Intersection (A1 ^\ n)) by Th33
.= A /\ ((inferior_setsequence A1) . n) by Th1 ;
hence  (inferior_setsequence (A (/\) A1)) . n = A /\ ((inferior_setsequence A1) . n) ; ::_thesis: verum
end;

theorem Th51: :: SETLIM_2:51
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n)
let A1 be SetSequence of X; ::_thesis: (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n)
(inferior_setsequence (A (\/) A1)) . n = Intersection ((A (\/) A1) ^\ n) by Th1
.= Intersection (A (\/) (A1 ^\ n)) by Th17
.= A \/ (Intersection (A1 ^\ n)) by Th34
.= A \/ ((inferior_setsequence A1) . n) by Th1 ;
hence  (inferior_setsequence (A (\/) A1)) . n = A \/ ((inferior_setsequence A1) . n) ; ::_thesis: verum
end;

theorem :: SETLIM_2:52
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n)
let A1 be SetSequence of X; ::_thesis: (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n)
(inferior_setsequence (A (\) A1)) . n = Intersection ((A (\) A1) ^\ n) by Th1
.= Intersection (A (\) (A1 ^\ n)) by Th18 ;
then  (inferior_setsequence (A (\) A1)) . n c= A \ (Intersection (A1 ^\ n)) by Th35;
hence  (inferior_setsequence (A (\) A1)) . n c= A \ ((inferior_setsequence A1) . n) by Th1; ::_thesis: verum
end;

theorem Th53: :: SETLIM_2:53
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
let A1 be SetSequence of X; ::_thesis: (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A
(inferior_setsequence (A1 (\) A)) . n = Intersection ((A1 (\) A) ^\ n) by Th1
.= Intersection ((A1 ^\ n) (\) A) by Th19
.= (Intersection (A1 ^\ n)) \ A by Th36
.= ((inferior_setsequence A1) . n) \ A by Th1 ;
hence  (inferior_setsequence (A1 (\) A)) . n = ((inferior_setsequence A1) . n) \ A ; ::_thesis: verum
end;

theorem :: SETLIM_2:54
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n)
let A1 be SetSequence of X; ::_thesis: (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n)
(inferior_setsequence (A (\+\) A1)) . n = Intersection ((A (\+\) A1) ^\ n) by Th1
.= Intersection (A (\+\) (A1 ^\ n)) by Th20 ;
then  (inferior_setsequence (A (\+\) A1)) . n c= A \+\ (Intersection (A1 ^\ n)) by Th37;
hence  (inferior_setsequence (A (\+\) A1)) . n c= A \+\ ((inferior_setsequence A1) . n) by Th1; ::_thesis: verum
end;

theorem Th55: :: SETLIM_2:55
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
let A1 be SetSequence of X; ::_thesis: (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
(superior_setsequence (A (/\) A1)) . n = Union ((A (/\) A1) ^\ n) by Th2
.= Union (A (/\) (A1 ^\ n)) by Th16
.= A /\ (Union (A1 ^\ n)) by Th38
.= A /\ ((superior_setsequence A1) . n) by Th2 ;
hence  (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n) ; ::_thesis: verum
end;

theorem Th56: :: SETLIM_2:56
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n)
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n)
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n)
let A1 be SetSequence of X; ::_thesis: (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n)
(superior_setsequence (A (\/) A1)) . n = Union ((A (\/) A1) ^\ n) by Th2
.= Union (A (\/) (A1 ^\ n)) by Th17
.= A \/ (Union (A1 ^\ n)) by Th39
.= A \/ ((superior_setsequence A1) . n) by Th2 ;
hence  (superior_setsequence (A (\/) A1)) . n = A \/ ((superior_setsequence A1) . n) ; ::_thesis: verum
end;

theorem :: SETLIM_2:57
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
let A1 be SetSequence of X; ::_thesis: A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n
 A \ ((superior_setsequence A1) . n) = A \ (Union (A1 ^\ n)) by Th2;
then  A \ ((superior_setsequence A1) . n) c= Union (A (\) (A1 ^\ n)) by Th40;
then  A \ ((superior_setsequence A1) . n) c= Union ((A (\) A1) ^\ n) by Th18;
hence  A \ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\) A1)) . n by Th2; ::_thesis: verum
end;

theorem Th58: :: SETLIM_2:58
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
let A1 be SetSequence of X; ::_thesis: (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
reconsider X2 = superior_setsequence (A1 (\) A) as SetSequence of X ;
A1: (X1 . n) \ A c= X2 . n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X1 . n) \ A or x in X2 . n )
assume A2: x in (X1 . n) \ A ; ::_thesis: x in X2 . n
then A3: not x in A by XBOOLE_0:def_5;
A4: x in X1 . n by A2, XBOOLE_0:def_5;
 ex k being Element of NAT st x in (A1 (\) A) . (n + k)
proof
consider k being Element of NAT  such that
A5: x in A1 . (n + k) by A4, SETLIM_1:20;
 x in (A1 . (n + k)) \ A by A3, A5, XBOOLE_0:def_5;
then  x in (A1 (\) A) . (n + k) by Def8;
hence  ex k being Element of NAT st x in (A1 (\) A) . (n + k) ; ::_thesis: verum
end;
hence  x in X2 . n by SETLIM_1:20; ::_thesis: verum
end;
 X2 . n c= (X1 . n) \ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 . n or x in (X1 . n) \ A )
assume A6: x in X2 . n ; ::_thesis: x in (X1 . n) \ A
A7: ex k being Element of NAT st
( x in A1 . (n + k) & not x in A )
proof
consider k being Element of NAT  such that
A8: x in (A1 (\) A) . (n + k) by A6, SETLIM_1:20;
 x in (A1 . (n + k)) \ A by A8, Def8;
then  ( x in A1 . (n + k) & not x in A ) by XBOOLE_0:def_5;
hence  ex k being Element of NAT st
( x in A1 . (n + k) & not x in A ) ; ::_thesis: verum
end;
then  x in X1 . n by SETLIM_1:20;
hence  x in (X1 . n) \ A by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETLIM_2:59
for n being Element of NAT
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
proof
let n be Element of NAT ; ::_thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
let A1 be SetSequence of X; ::_thesis: A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
 A \+\ ((superior_setsequence A1) . n) = A \+\ (Union (A1 ^\ n)) by Th2;
then  A \+\ ((superior_setsequence A1) . n) c= Union (A (\+\) (A1 ^\ n)) by Th42;
then  A \+\ ((superior_setsequence A1) . n) c= Union ((A (\+\) A1) ^\ n) by Th20;
hence  A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n by Th2; ::_thesis: verum
end;

theorem Th60: :: SETLIM_2:60
for X being set
for A1, A2 being SetSequence of X holds lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2)
let A1, A2 be SetSequence of X; ::_thesis: lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2)
 for n being Element of NAT holds (A1 (/\) A2) . n = (A1 . n) /\ (A2 . n) by Def1;
hence  lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2) by KURATO_0:10; ::_thesis: verum
end;

theorem Th61: :: SETLIM_2:61
for X being set
for A1, A2 being SetSequence of X holds (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2)
let A1, A2 be SetSequence of X; ::_thesis: (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2)
 for n being Element of NAT holds (A1 (\/) A2) . n = (A1 . n) \/ (A2 . n) by Def2;
hence  (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2) by KURATO_0:12; ::_thesis: verum
end;

theorem Th62: :: SETLIM_2:62
for X being set
for A1, A2 being SetSequence of X holds lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2)
let A1, A2 be SetSequence of X; ::_thesis: lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf (A1 (\) A2) or x in (lim_inf A1) \ (lim_inf A2) )
assume  x in lim_inf (A1 (\) A2) ; ::_thesis: x in (lim_inf A1) \ (lim_inf A2)
then consider n being Element of NAT  such that
A1: for k being Element of NAT holds x in (A1 (\) A2) . (n + k) by KURATO_0:4;
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A1_._(n_+_k)_&_not_x_in_A2_._(n_+_k)_)
let k be Element of NAT ; ::_thesis: ( x in A1 . (n + k) & not x in A2 . (n + k) )
 x in (A1 (\) A2) . (n + k) by A1;
then  x in (A1 . (n + k)) \ (A2 . (n + k)) by Def3;
hence  ( x in A1 . (n + k) & not x in A2 . (n + k) ) by XBOOLE_0:def_5; ::_thesis: verum
end;
A3: not x in lim_inf A2
proof
assume  x in lim_inf A2 ; ::_thesis: contradiction
then consider n1 being Element of NAT  such that
A4: for k being Element of NAT holds x in A2 . (n1 + k) by KURATO_0:4;
 x in A2 . (n1 + n) by A4;
hence  contradiction by A2; ::_thesis: verum
end;
 x in lim_inf A1 by A2, KURATO_0:4;
hence  x in (lim_inf A1) \ (lim_inf A2) by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th63: :: SETLIM_2:63
for X being set
for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
let A1, A2 be SetSequence of X; ::_thesis: ( ( A1 is convergent or A2 is convergent ) implies lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) )
A1: for A1, A2 being SetSequence of X st A1 is convergent holds
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
proof
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) )
assume A2: A1 is convergent ; ::_thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
thus  lim_inf (A1 (\/) A2) c= (lim_inf A1) \/ (lim_inf A2) :: according to XBOOLE_0:def_10 ::_thesis: (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf (A1 (\/) A2) or x in (lim_inf A1) \/ (lim_inf A2) )
assume  x in lim_inf (A1 (\/) A2) ; ::_thesis: x in (lim_inf A1) \/ (lim_inf A2)
then consider n1 being Element of NAT  such that
A3: for k being Element of NAT holds x in (A1 (\/) A2) . (n1 + k) by KURATO_0:4;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_x_in_A1_._(n1_+_n)_or_x_in_A2_._(n1_+_n)_)
let n be Element of NAT ; ::_thesis: ( x in A1 . (n1 + n) or x in A2 . (n1 + n) )
 x in (A1 (\/) A2) . (n1 + n) by A3;
then  x in (A1 . (n1 + n)) \/ (A2 . (n1 + n)) by Def2;
hence  ( x in A1 . (n1 + n) or x in A2 . (n1 + n) ) by XBOOLE_0:def_3; ::_thesis: verum
end;
 x in (lim_inf A1) \/ (lim_inf A2)
proof
assume A5: not x in (lim_inf A1) \/ (lim_inf A2) ; ::_thesis: contradiction
then  not x in lim_inf A1 by XBOOLE_0:def_3;
then  not x in lim_sup A1 by A2, KURATO_0:def_5;
then consider n2 being Element of NAT  such that
A6: for k being Element of NAT holds not x in A1 . (n2 + k) by KURATO_0:5;
 not x in lim_inf A2 by A5, XBOOLE_0:def_3;
then consider k1 being Element of NAT  such that
A7: not x in A2 . ((n1 + n2) + k1) by KURATO_0:4;
 not x in A1 . (n2 + (n1 + k1)) by A6;
then  not x in A1 . (n1 + (n2 + k1)) ;
hence  contradiction by A4, A7; ::_thesis: verum
end;
hence  x in (lim_inf A1) \/ (lim_inf A2) ; ::_thesis: verum
end;
thus  (lim_inf A1) \/ (lim_inf A2) c= lim_inf (A1 (\/) A2) by Th61; ::_thesis: verum
end;
assume A8: ( A1 is convergent or A2 is convergent ) ; ::_thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
percases ( A1 is convergent or A2 is convergent ) by A8;
suppose A1 is convergent ; ::_thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
hence  lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) by A1; ::_thesis: verum
end;
suppose A2 is convergent ; ::_thesis: lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2)
hence  lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) by A1; ::_thesis: verum
end;
end;
end;

theorem Th64: :: SETLIM_2:64
for X being set
for A2, A1 being SetSequence of X st A2 is convergent holds
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)
proof
let X be set ; ::_thesis: for A2, A1 being SetSequence of X st A2 is convergent holds
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)
let A2, A1 be SetSequence of X; ::_thesis: ( A2 is convergent implies lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2) )
assume A1: A2 is convergent ; ::_thesis: lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2)
thus  lim_inf (A1 (\) A2) c= (lim_inf A1) \ (lim_inf A2) by Th62; :: according to XBOOLE_0:def_10 ::_thesis: (lim_inf A1) \ (lim_inf A2) c= lim_inf (A1 (\) A2)
thus  (lim_inf A1) \ (lim_inf A2) c= lim_inf (A1 (\) A2) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_inf A1) \ (lim_inf A2) or x in lim_inf (A1 (\) A2) )
assume A2: x in (lim_inf A1) \ (lim_inf A2) ; ::_thesis: x in lim_inf (A1 (\) A2)
then  x in lim_inf A1 by XBOOLE_0:def_5;
then consider n0 being Element of NAT  such that
A3: for k being Element of NAT holds x in A1 . (n0 + k) by KURATO_0:4;
 not x in lim_inf A2 by A2, XBOOLE_0:def_5;
then  not x in lim_sup A2 by A1, KURATO_0:def_5;
then consider n1 being Element of NAT  such that
A4: for k being Element of NAT holds not x in A2 . (n1 + k) by KURATO_0:5;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(\)_A2)_._((n0_+_n1)_+_k)
let k be Element of NAT ; ::_thesis: x in (A1 (\) A2) . ((n0 + n1) + k)
 ( x in A1 . (n0 + (n1 + k)) & not x in A2 . (n1 + (n0 + k)) ) by A3, A4;
then  x in (A1 . ((n0 + n1) + k)) \ (A2 . ((n0 + n1) + k)) by XBOOLE_0:def_5;
hence  x in (A1 (\) A2) . ((n0 + n1) + k) by Def3; ::_thesis: verum
end;
hence  x in lim_inf (A1 (\) A2) by KURATO_0:4; ::_thesis: verum
end;
end;

theorem Th65: :: SETLIM_2:65
for X being set
for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
let A1, A2 be SetSequence of X; ::_thesis: ( ( A1 is convergent or A2 is convergent ) implies lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) )
A1: for A1, A2 being SetSequence of X st A1 is convergent holds
lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
proof
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) )
assume A2: A1 is convergent ; ::_thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
thus  lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf (A1 (\+\) A2) or x in (lim_inf A1) \+\ (lim_inf A2) )
assume  x in lim_inf (A1 (\+\) A2) ; ::_thesis: x in (lim_inf A1) \+\ (lim_inf A2)
then consider n1 being Element of NAT  such that
A3: for k being Element of NAT holds x in (A1 (\+\) A2) . (n1 + k) by KURATO_0:4;
A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_(_x_in_A1_._(n1_+_k)_&_not_x_in_A2_._(n1_+_k)_)_or_(_not_x_in_A1_._(n1_+_k)_&_x_in_A2_._(n1_+_k)_)_)
let k be Element of NAT ; ::_thesis: ( ( x in A1 . (n1 + k) & not x in A2 . (n1 + k) ) or ( not x in A1 . (n1 + k) & x in A2 . (n1 + k) ) )
 x in (A1 (\+\) A2) . (n1 + k) by A3;
then  x in (A1 . (n1 + k)) \+\ (A2 . (n1 + k)) by Def4;
hence  ( ( x in A1 . (n1 + k) & not x in A2 . (n1 + k) ) or ( not x in A1 . (n1 + k) & x in A2 . (n1 + k) ) ) by XBOOLE_0:1; ::_thesis: verum
end;
assume A5: not x in (lim_inf A1) \+\ (lim_inf A2) ; ::_thesis: contradiction
percases ( ( not x in lim_inf A1 & not x in lim_inf A2 ) or ( x in lim_inf A1 & x in lim_inf A2 ) ) by A5, XBOOLE_0:1;
supposeA6: ( not x in lim_inf A1 & not x in lim_inf A2 ) ; ::_thesis: contradiction
then  not x in lim_sup A1 by A2, KURATO_0:def_5;
then consider n2 being Element of NAT  such that
A7: for k being Element of NAT holds not x in A1 . (n2 + k) by KURATO_0:5;
consider k1 being Element of NAT  such that
A8: not x in A2 . ((n1 + n2) + k1) by A6, KURATO_0:4;
A9: ( ( x in A1 . (n1 + (n2 + k1)) & not x in A2 . (n1 + (n2 + k1)) ) or ( not x in A1 . (n1 + (n2 + k1)) & x in A2 . (n1 + (n2 + k1)) ) ) by A4;
 not x in A1 . (n2 + (n1 + k1)) by A7;
hence  contradiction by A8, A9; ::_thesis: verum
end;
supposeA10: ( x in lim_inf A1 & x in lim_inf A2 ) ; ::_thesis: contradiction
then consider n3 being Element of NAT  such that
A11: for k being Element of NAT holds x in A2 . (n3 + k) by KURATO_0:4;
consider n2 being Element of NAT  such that
A12: for k being Element of NAT holds x in A1 . (n2 + k) by A10, KURATO_0:4;
A13: ( ( x in A1 . (n1 + (n2 + n3)) & not x in A2 . (n1 + (n2 + n3)) ) or ( not x in A1 . (n1 + (n2 + n3)) & x in A2 . (n1 + (n2 + n3)) ) ) by A4;
A14: x in A2 . (n3 + (n1 + n2)) by A11;
 x in A1 . (n2 + (n1 + n3)) by A12;
hence  contradiction by A14, A13; ::_thesis: verum
end;
end;
end;
end;
assume A15: ( A1 is convergent or A2 is convergent ) ; ::_thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
percases ( A1 is convergent or A2 is convergent ) by A15;
suppose A1 is convergent ; ::_thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
hence  lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) by A1; ::_thesis: verum
end;
suppose A2 is convergent ; ::_thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
hence  lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) by A1; ::_thesis: verum
end;
end;
end;

theorem Th66: :: SETLIM_2:66
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent & A2 is convergent implies lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; ::_thesis: lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)
thus  lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) by A1, Th65; :: according to XBOOLE_0:def_10 ::_thesis: (lim_inf A1) \+\ (lim_inf A2) c= lim_inf (A1 (\+\) A2)
thus  (lim_inf A1) \+\ (lim_inf A2) c= lim_inf (A1 (\+\) A2) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_inf A1) \+\ (lim_inf A2) or x in lim_inf (A1 (\+\) A2) )
assume A3: x in (lim_inf A1) \+\ (lim_inf A2) ; ::_thesis: x in lim_inf (A1 (\+\) A2)
percases ( ( x in lim_inf A1 & not x in lim_inf A2 ) or ( not x in lim_inf A1 & x in lim_inf A2 ) ) by A3, XBOOLE_0:1;
supposeA4: ( x in lim_inf A1 & not x in lim_inf A2 ) ; ::_thesis: x in lim_inf (A1 (\+\) A2)
then  not x in lim_sup A2 by A2, KURATO_0:def_5;
then consider n2 being Element of NAT  such that
A5: for k being Element of NAT holds not x in A2 . (n2 + k) by KURATO_0:5;
consider n1 being Element of NAT  such that
A6: for k being Element of NAT holds x in A1 . (n1 + k) by A4, KURATO_0:4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(\+\)_A2)_._((n1_+_n2)_+_k)
let k be Element of NAT ; ::_thesis: x in (A1 (\+\) A2) . ((n1 + n2) + k)
 ( x in A1 . (n1 + (n2 + k)) & not x in A2 . (n2 + (n1 + k)) ) by A6, A5;
then  x in (A1 . ((n1 + n2) + k)) \+\ (A2 . ((n1 + n2) + k)) by XBOOLE_0:1;
hence  x in (A1 (\+\) A2) . ((n1 + n2) + k) by Def4; ::_thesis: verum
end;
hence  x in lim_inf (A1 (\+\) A2) by KURATO_0:4; ::_thesis: verum
end;
supposeA7: ( not x in lim_inf A1 & x in lim_inf A2 ) ; ::_thesis: x in lim_inf (A1 (\+\) A2)
then  not x in lim_sup A1 by A1, KURATO_0:def_5;
then consider n3 being Element of NAT  such that
A8: for k being Element of NAT holds not x in A1 . (n3 + k) by KURATO_0:5;
consider n4 being Element of NAT  such that
A9: for k being Element of NAT holds x in A2 . (n4 + k) by A7, KURATO_0:4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A1_(\+\)_A2)_._((n3_+_n4)_+_k)
let k be Element of NAT ; ::_thesis: x in (A1 (\+\) A2) . ((n3 + n4) + k)
 ( not x in A1 . (n3 + (n4 + k)) & x in A2 . (n4 + (n3 + k)) ) by A8, A9;
then  x in (A1 . ((n3 + n4) + k)) \+\ (A2 . ((n3 + n4) + k)) by XBOOLE_0:1;
hence  x in (A1 (\+\) A2) . ((n3 + n4) + k) by Def4; ::_thesis: verum
end;
hence  x in lim_inf (A1 (\+\) A2) by KURATO_0:4; ::_thesis: verum
end;
end;
end;
end;

theorem Th67: :: SETLIM_2:67
for X being set
for A1, A2 being SetSequence of X holds lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2)
let A1, A2 be SetSequence of X; ::_thesis: lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2)
 for n being Element of NAT holds (A1 (/\) A2) . n = (A1 . n) /\ (A2 . n) by Def1;
hence  lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2) by KURATO_0:13; ::_thesis: verum
end;

theorem Th68: :: SETLIM_2:68
for X being set
for A1, A2 being SetSequence of X holds lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)
let A1, A2 be SetSequence of X; ::_thesis: lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)
 for n being Element of NAT holds (A1 (\/) A2) . n = (A1 . n) \/ (A2 . n) by Def2;
hence  lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2) by KURATO_0:11; ::_thesis: verum
end;

theorem Th69: :: SETLIM_2:69
for X being set
for A1, A2 being SetSequence of X holds (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2)
let A1, A2 be SetSequence of X; ::_thesis: (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_sup A1) \ (lim_sup A2) or x in lim_sup (A1 (\) A2) )
assume A1: x in (lim_sup A1) \ (lim_sup A2) ; ::_thesis: x in lim_sup (A1 (\) A2)
then  not x in lim_sup A2 by XBOOLE_0:def_5;
then consider n1 being Element of NAT  such that
A2: for k being Element of NAT holds not x in A2 . (n1 + k) by KURATO_0:5;
assume  not x in lim_sup (A1 (\) A2) ; ::_thesis: contradiction
then consider n2 being Element of NAT  such that
A3: for k being Element of NAT holds not x in (A1 (\) A2) . (n2 + k) by KURATO_0:5;
A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_not_x_in_A1_._(n2_+_k)_or_x_in_A2_._(n2_+_k)_)
let k be Element of NAT ; ::_thesis: ( not x in A1 . (n2 + k) or x in A2 . (n2 + k) )
 not x in (A1 (\) A2) . (n2 + k) by A3;
then  not x in (A1 . (n2 + k)) \ (A2 . (n2 + k)) by Def3;
hence  ( not x in A1 . (n2 + k) or x in A2 . (n2 + k) ) by XBOOLE_0:def_5; ::_thesis: verum
end;
 x in lim_sup A1 by A1, XBOOLE_0:def_5;
then consider k1 being Element of NAT  such that
A5: x in A1 . ((n1 + n2) + k1) by KURATO_0:5;
A6: x in A1 . (n2 + (k1 + n1)) by A5;
 not x in A2 . (n1 + (n2 + k1)) by A2;
hence  contradiction by A4, A6; ::_thesis: verum
end;

theorem :: SETLIM_2:70
for X being set
for A1, A2 being SetSequence of X holds (lim_sup A1) \+\ (lim_sup A2) c= lim_sup (A1 (\+\) A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X holds (lim_sup A1) \+\ (lim_sup A2) c= lim_sup (A1 (\+\) A2)
let A1, A2 be SetSequence of X; ::_thesis: (lim_sup A1) \+\ (lim_sup A2) c= lim_sup (A1 (\+\) A2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_sup A1) \+\ (lim_sup A2) or x in lim_sup (A1 (\+\) A2) )
A1: for A1, A2 being SetSequence of X st x in lim_sup A1 & not x in lim_sup A2 holds
x in lim_sup (A1 (\+\) A2)
proof
let A1, A2 be SetSequence of X; ::_thesis: ( x in lim_sup A1 & not x in lim_sup A2 implies x in lim_sup (A1 (\+\) A2) )
assume that
A2: x in lim_sup A1 and
A3: not x in lim_sup A2 ; ::_thesis: x in lim_sup (A1 (\+\) A2)
consider n1 being Element of NAT  such that
A4: for k being Element of NAT holds not x in A2 . (n1 + k) by A3, KURATO_0:5;
now__::_thesis:_for_n_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_x_in_(A1_(\+\)_A2)_._(n_+_k)
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in (A1 (\+\) A2) . (n + k)
consider k1 being Element of NAT  such that
A5: x in A1 . ((n + n1) + k1) by A2, KURATO_0:5;
 not x in A2 . (n1 + (n + k1)) by A4;
then  x in (A1 . (n + (n1 + k1))) \+\ (A2 . (n + (n1 + k1))) by A5, XBOOLE_0:1;
then  x in (A1 (\+\) A2) . (n + (n1 + k1)) by Def4;
hence  ex k being Element of NAT st x in (A1 (\+\) A2) . (n + k) ; ::_thesis: verum
end;
hence  x in lim_sup (A1 (\+\) A2) by KURATO_0:5; ::_thesis: verum
end;
assume A6: x in (lim_sup A1) \+\ (lim_sup A2) ; ::_thesis: x in lim_sup (A1 (\+\) A2)
percases ( ( x in lim_sup A1 & not x in lim_sup A2 ) or ( not x in lim_sup A1 & x in lim_sup A2 ) ) by A6, XBOOLE_0:1;
suppose ( x in lim_sup A1 & not x in lim_sup A2 ) ; ::_thesis: x in lim_sup (A1 (\+\) A2)
hence  x in lim_sup (A1 (\+\) A2) by A1; ::_thesis: verum
end;
suppose ( not x in lim_sup A1 & x in lim_sup A2 ) ; ::_thesis: x in lim_sup (A1 (\+\) A2)
hence  x in lim_sup (A1 (\+\) A2) by A1; ::_thesis: verum
end;
end;
end;

theorem Th71: :: SETLIM_2:71
for X being set
for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
let A1, A2 be SetSequence of X; ::_thesis: ( ( A1 is convergent or A2 is convergent ) implies lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) )
A1: for A1, A2 being SetSequence of X st A1 is convergent holds
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
proof
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) )
assume A2: A1 is convergent ; ::_thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
thus  lim_sup (A1 (/\) A2) c= (lim_sup A1) /\ (lim_sup A2) by Th67; :: according to XBOOLE_0:def_10 ::_thesis: (lim_sup A1) /\ (lim_sup A2) c= lim_sup (A1 (/\) A2)
thus  (lim_sup A1) /\ (lim_sup A2) c= lim_sup (A1 (/\) A2) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (lim_sup A1) /\ (lim_sup A2) or x in lim_sup (A1 (/\) A2) )
assume A3: x in (lim_sup A1) /\ (lim_sup A2) ; ::_thesis: x in lim_sup (A1 (/\) A2)
then  x in lim_sup A1 by XBOOLE_0:def_4;
then  x in lim_inf A1 by A2, KURATO_0:def_5;
then consider n1 being Element of NAT  such that
A4: for k being Element of NAT holds x in A1 . (n1 + k) by KURATO_0:4;
A5: x in lim_sup A2 by A3, XBOOLE_0:def_4;
now__::_thesis:_for_n_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_x_in_(A1_(/\)_A2)_._(n_+_k)
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in (A1 (/\) A2) . (n + k)
consider k1 being Element of NAT  such that
A6: x in A2 . ((n + n1) + k1) by A5, KURATO_0:5;
 x in A1 . (n1 + (n + k1)) by A4;
then  x in (A1 . (n + (n1 + k1))) /\ (A2 . (n + (n1 + k1))) by A6, XBOOLE_0:def_4;
then  x in (A1 (/\) A2) . (n + (n1 + k1)) by Def1;
hence  ex k being Element of NAT st x in (A1 (/\) A2) . (n + k) ; ::_thesis: verum
end;
hence  x in lim_sup (A1 (/\) A2) by KURATO_0:5; ::_thesis: verum
end;
end;
assume A7: ( A1 is convergent or A2 is convergent ) ; ::_thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
percases ( A1 is convergent or A2 is convergent ) by A7;
suppose A1 is convergent ; ::_thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
hence  lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) by A1; ::_thesis: verum
end;
suppose A2 is convergent ; ::_thesis: lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2)
hence  lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) by A1; ::_thesis: verum
end;
end;
end;

theorem Th72: :: SETLIM_2:72
for X being set
for A2, A1 being SetSequence of X st A2 is convergent holds
lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2)
proof
let X be set ; ::_thesis: for A2, A1 being SetSequence of X st A2 is convergent holds
lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2)
let A2, A1 be SetSequence of X; ::_thesis: ( A2 is convergent implies lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2) )
assume A1: A2 is convergent ; ::_thesis: lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2)
thus  lim_sup (A1 (\) A2) c= (lim_sup A1) \ (lim_sup A2) :: according to XBOOLE_0:def_10 ::_thesis: (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup (A1 (\) A2) or x in (lim_sup A1) \ (lim_sup A2) )
assume A2: x in lim_sup (A1 (\) A2) ; ::_thesis: x in (lim_sup A1) \ (lim_sup A2)
A3: now__::_thesis:_for_n_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_
(_x_in_A1_._(n_+_k)_&_not_x_in_A2_._(n_+_k)_)
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st
( x in A1 . (n + k) & not x in A2 . (n + k) )
consider k1 being Element of NAT  such that
A4: x in (A1 (\) A2) . (n + k1) by A2, KURATO_0:5;
 x in (A1 . (n + k1)) \ (A2 . (n + k1)) by A4, Def3;
then  ( x in A1 . (n + k1) & not x in A2 . (n + k1) ) by XBOOLE_0:def_5;
hence  ex k being Element of NAT st
( x in A1 . (n + k) & not x in A2 . (n + k) ) ; ::_thesis: verum
end;
assume  not x in (lim_sup A1) \ (lim_sup A2) ; ::_thesis: contradiction
then A5: ( not x in lim_sup A1 or x in lim_sup A2 ) by XBOOLE_0:def_5;
percases ( not x in lim_sup A1 or x in lim_inf A2 ) by A1, A5, KURATO_0:def_5;
suppose not x in lim_sup A1 ; ::_thesis: contradiction
then consider n1 being Element of NAT  such that
A6: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_0:5;
 ex k2 being Element of NAT st
( x in A1 . (n1 + k2) & not x in A2 . (n1 + k2) ) by A3;
hence  contradiction by A6; ::_thesis: verum
end;
suppose x in lim_inf A2 ; ::_thesis: contradiction
then consider n2 being Element of NAT  such that
A7: for k being Element of NAT holds x in A2 . (n2 + k) by KURATO_0:4;
 ex k3 being Element of NAT st
( x in A1 . (n2 + k3) & not x in A2 . (n2 + k3) ) by A3;
hence  contradiction by A7; ::_thesis: verum
end;
end;
end;
thus  (lim_sup A1) \ (lim_sup A2) c= lim_sup (A1 (\) A2) by Th69; ::_thesis: verum
end;

theorem Th73: :: SETLIM_2:73
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2)
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2)
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent & A2 is convergent implies lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; ::_thesis: lim_sup (A1 (\+\) A2) = (lim_sup A1) \+\ (lim_sup A2)
thus  lim_sup (A1 (\+\) A2) = lim_sup ((A1 (\) A2) (\/) (A2 (\) A1)) by Th3
.= (lim_sup (A1 (\) A2)) \/ (lim_sup (A2 (\) A1)) by Th68
.= ((lim_sup A1) \ (lim_sup A2)) \/ (lim_sup (A2 (\) A1)) by A2, Th72
.= (lim_sup A1) \+\ (lim_sup A2) by A1, Th72 ; ::_thesis: verum
end;

theorem Th74: :: SETLIM_2:74
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (/\) A1) = A /\ (lim_inf A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (/\) A1) = A /\ (lim_inf A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_inf (A (/\) A1) = A /\ (lim_inf A1)
let A1 be SetSequence of X; ::_thesis: lim_inf (A (/\) A1) = A /\ (lim_inf A1)
reconsider X1 = inferior_setsequence A1 as SetSequence of X ;
reconsider X2 = inferior_setsequence (A (/\) A1) as SetSequence of X ;
 X2 = A (/\) X1
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: X2 . n = (A (/\) X1) . n
thus X2 . n = A /\ (X1 . n) by Th50
.= (A (/\) X1) . n by Def5 ; ::_thesis: verum
end;
then  Union X2 = A /\ (Union X1) by Th38;
then  lim_inf (A (/\) A1) = A /\ (Union X1) by SETLIM_1:def_4;
hence  lim_inf (A (/\) A1) = A /\ (lim_inf A1) by SETLIM_1:def_4; ::_thesis: verum
end;

theorem Th75: :: SETLIM_2:75
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\/) A1) = A \/ (lim_inf A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\/) A1) = A \/ (lim_inf A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_inf (A (\/) A1) = A \/ (lim_inf A1)
let A1 be SetSequence of X; ::_thesis: lim_inf (A (\/) A1) = A \/ (lim_inf A1)
reconsider X1 = inferior_setsequence A1 as SetSequence of X ;
reconsider X2 = inferior_setsequence (A (\/) A1) as SetSequence of X ;
 X2 = A (\/) X1
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: X2 . n = (A (\/) X1) . n
thus X2 . n = A \/ (X1 . n) by Th51
.= (A (\/) X1) . n by Def6 ; ::_thesis: verum
end;
then  Union X2 = A \/ (Union X1) by Th39;
then  lim_inf (A (\/) A1) = A \/ (Union X1) by SETLIM_1:def_4;
hence  lim_inf (A (\/) A1) = A \/ (lim_inf A1) by SETLIM_1:def_4; ::_thesis: verum
end;

theorem Th76: :: SETLIM_2:76
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\) A1) c= A \ (lim_inf A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\) A1) c= A \ (lim_inf A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_inf (A (\) A1) c= A \ (lim_inf A1)
let A1 be SetSequence of X; ::_thesis: lim_inf (A (\) A1) c= A \ (lim_inf A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf (A (\) A1) or x in A \ (lim_inf A1) )
assume  x in lim_inf (A (\) A1) ; ::_thesis: x in A \ (lim_inf A1)
then consider n being Element of NAT  such that
A1: for k being Element of NAT holds x in (A (\) A1) . (n + k) by KURATO_0:4;
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_x_in_A_&_not_x_in_A1_._(n_+_k)_)
let k be Element of NAT ; ::_thesis: ( x in A & not x in A1 . (n + k) )
 x in (A (\) A1) . (n + k) by A1;
then  x in A \ (A1 . (n + k)) by Def7;
hence  ( x in A & not x in A1 . (n + k) ) by XBOOLE_0:def_5; ::_thesis: verum
end;
 not x in lim_inf A1
proof
assume  x in lim_inf A1 ; ::_thesis: contradiction
then consider n1 being Element of NAT  such that
A3: for k being Element of NAT holds x in A1 . (n1 + k) by KURATO_0:4;
 x in A1 . (n1 + n) by A3;
hence  contradiction by A2; ::_thesis: verum
end;
hence  x in A \ (lim_inf A1) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th77: :: SETLIM_2:77
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A1 (\) A) = (lim_inf A1) \ A
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A1 (\) A) = (lim_inf A1) \ A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_inf (A1 (\) A) = (lim_inf A1) \ A
let A1 be SetSequence of X; ::_thesis: lim_inf (A1 (\) A) = (lim_inf A1) \ A
reconsider X1 = inferior_setsequence A1 as SetSequence of X ;
reconsider X2 = inferior_setsequence (A1 (\) A) as SetSequence of X ;
 X2 = X1 (\) A
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: X2 . n = (X1 (\) A) . n
thus X2 . n = (X1 . n) \ A by Th53
.= (X1 (\) A) . n by Def8 ; ::_thesis: verum
end;
then  Union X2 = (Union X1) \ A by Th41;
then  lim_inf (A1 (\) A) = (Union X1) \ A by SETLIM_1:def_4;
hence  lim_inf (A1 (\) A) = (lim_inf A1) \ A by SETLIM_1:def_4; ::_thesis: verum
end;

theorem Th78: :: SETLIM_2:78
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
let A1 be SetSequence of X; ::_thesis: lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_inf (A (\+\) A1) or x in A \+\ (lim_inf A1) )
assume  x in lim_inf (A (\+\) A1) ; ::_thesis: x in A \+\ (lim_inf A1)
then consider n1 being Element of NAT  such that
A1: for k being Element of NAT holds x in (A (\+\) A1) . (n1 + k) by KURATO_0:4;
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_(_x_in_A_&_not_x_in_A1_._(n1_+_k)_)_or_(_not_x_in_A_&_x_in_A1_._(n1_+_k)_)_)
let k be Element of NAT ; ::_thesis: ( ( x in A & not x in A1 . (n1 + k) ) or ( not x in A & x in A1 . (n1 + k) ) )
 x in (A (\+\) A1) . (n1 + k) by A1;
then  x in A \+\ (A1 . (n1 + k)) by Def9;
hence  ( ( x in A & not x in A1 . (n1 + k) ) or ( not x in A & x in A1 . (n1 + k) ) ) by XBOOLE_0:1; ::_thesis: verum
end;
assume  not x in A \+\ (lim_inf A1) ; ::_thesis: contradiction
then A3: ( ( not x in A & not x in lim_inf A1 ) or ( x in lim_inf A1 & x in A ) ) by XBOOLE_0:1;
percases ( ( not x in A & ( for n being Element of NAT holds
not for k being Element of NAT holds x in A1 . (n + k) ) ) or ( x in A & ex n being Element of NAT st
for k being Element of NAT holds x in A1 . (n + k) ) ) by A3, KURATO_0:4;
supposeA4: ( not x in A & ( for n being Element of NAT holds
not for k being Element of NAT holds x in A1 . (n + k) ) ) ; ::_thesis: contradiction
then  not for k1 being Element of NAT holds x in A1 . (n1 + k1) ;
hence  contradiction by A2, A4; ::_thesis: verum
end;
supposeA5: ( x in A & ex n being Element of NAT st
for k being Element of NAT holds x in A1 . (n + k) ) ; ::_thesis: contradiction
then consider n2 being Element of NAT  such that
A6: for k being Element of NAT holds x in A1 . (n2 + k) ;
 x in A1 . (n2 + n1) by A6;
hence  contradiction by A2, A5; ::_thesis: verum
end;
end;
end;

theorem Th79: :: SETLIM_2:79
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\) A1) = A \ (lim_inf A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\) A1) = A \ (lim_inf A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\) A1) = A \ (lim_inf A1)
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_inf (A (\) A1) = A \ (lim_inf A1) )
assume A1: A1 is convergent ; ::_thesis: lim_inf (A (\) A1) = A \ (lim_inf A1)
thus  lim_inf (A (\) A1) c= A \ (lim_inf A1) by Th76; :: according to XBOOLE_0:def_10 ::_thesis: A \ (lim_inf A1) c= lim_inf (A (\) A1)
thus  A \ (lim_inf A1) c= lim_inf (A (\) A1) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ (lim_inf A1) or x in lim_inf (A (\) A1) )
assume A2: x in A \ (lim_inf A1) ; ::_thesis: x in lim_inf (A (\) A1)
then  x in A \ (lim_sup A1) by A1, KURATO_0:def_5;
then  not x in lim_sup A1 by XBOOLE_0:def_5;
then consider n1 being Element of NAT  such that
A3: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_0:5;
assume A4: not x in lim_inf (A (\) A1) ; ::_thesis: contradiction
A5: for n being Element of NAT holds
( not x in A or ex k being Element of NAT st x in A1 . (n + k) )
proof
let n be Element of NAT ; ::_thesis: ( not x in A or ex k being Element of NAT st x in A1 . (n + k) )
consider k being Element of NAT  such that
A6: not x in (A (\) A1) . (n + k) by A4, KURATO_0:4;
 not x in A \ (A1 . (n + k)) by A6, Def7;
then  ( not x in A or x in A1 . (n + k) ) by XBOOLE_0:def_5;
hence  ( not x in A or ex k being Element of NAT st x in A1 . (n + k) ) ; ::_thesis: verum
end;
percases ( not x in A or ex k being Element of NAT st x in A1 . (n1 + k) ) by A5;
suppose not x in A ; ::_thesis: contradiction
hence  contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose ex k being Element of NAT st x in A1 . (n1 + k) ; ::_thesis: contradiction
hence  contradiction by A3; ::_thesis: verum
end;
end;
end;
end;

theorem Th80: :: SETLIM_2:80
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_inf (A (\+\) A1) = A \+\ (lim_inf A1) )
assume A1: A1 is convergent ; ::_thesis: lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
thus  lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1) by Th78; :: according to XBOOLE_0:def_10 ::_thesis: A \+\ (lim_inf A1) c= lim_inf (A (\+\) A1)
thus  A \+\ (lim_inf A1) c= lim_inf (A (\+\) A1) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \+\ (lim_inf A1) or x in lim_inf (A (\+\) A1) )
assume A2: x in A \+\ (lim_inf A1) ; ::_thesis: x in lim_inf (A (\+\) A1)
percases ( ( x in A & not x in lim_inf A1 ) or ( not x in A & x in lim_inf A1 ) ) by A2, XBOOLE_0:1;
supposeA3: ( x in A & not x in lim_inf A1 ) ; ::_thesis: x in lim_inf (A (\+\) A1)
then  not x in lim_sup A1 by A1, KURATO_0:def_5;
then consider n1 being Element of NAT  such that
A4: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_0:5;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A_(\+\)_A1)_._(n1_+_k)
let k be Element of NAT ; ::_thesis: x in (A (\+\) A1) . (n1 + k)
 not x in A1 . (n1 + k) by A4;
then  x in A \+\ (A1 . (n1 + k)) by A3, XBOOLE_0:1;
hence  x in (A (\+\) A1) . (n1 + k) by Def9; ::_thesis: verum
end;
hence  x in lim_inf (A (\+\) A1) by KURATO_0:4; ::_thesis: verum
end;
supposeA5: ( not x in A & x in lim_inf A1 ) ; ::_thesis: x in lim_inf (A (\+\) A1)
then consider n2 being Element of NAT  such that
A6: for k being Element of NAT holds x in A1 . (n2 + k) by KURATO_0:4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_(A_(\+\)_A1)_._(n2_+_k)
let k be Element of NAT ; ::_thesis: x in (A (\+\) A1) . (n2 + k)
 x in A1 . (n2 + k) by A6;
then  x in A \+\ (A1 . (n2 + k)) by A5, XBOOLE_0:1;
hence  x in (A (\+\) A1) . (n2 + k) by Def9; ::_thesis: verum
end;
hence  x in lim_inf (A (\+\) A1) by KURATO_0:4; ::_thesis: verum
end;
end;
end;
end;

theorem Th81: :: SETLIM_2:81
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (/\) A1) = A /\ (lim_sup A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (/\) A1) = A /\ (lim_sup A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_sup (A (/\) A1) = A /\ (lim_sup A1)
let A1 be SetSequence of X; ::_thesis: lim_sup (A (/\) A1) = A /\ (lim_sup A1)
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
reconsider X2 = superior_setsequence (A (/\) A1) as SetSequence of X ;
 X2 = A (/\) X1
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: X2 . n = (A (/\) X1) . n
thus X2 . n = A /\ (X1 . n) by Th55
.= (A (/\) X1) . n by Def5 ; ::_thesis: verum
end;
then  Intersection X2 = A /\ (Intersection X1) by Th33;
then  lim_sup (A (/\) A1) = A /\ (Intersection X1) by SETLIM_1:def_5;
hence  lim_sup (A (/\) A1) = A /\ (lim_sup A1) by SETLIM_1:def_5; ::_thesis: verum
end;

theorem Th82: :: SETLIM_2:82
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (\/) A1) = A \/ (lim_sup A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A (\/) A1) = A \/ (lim_sup A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_sup (A (\/) A1) = A \/ (lim_sup A1)
let A1 be SetSequence of X; ::_thesis: lim_sup (A (\/) A1) = A \/ (lim_sup A1)
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
reconsider X2 = superior_setsequence (A (\/) A1) as SetSequence of X ;
 X2 = A (\/) X1
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: X2 . n = (A (\/) X1) . n
thus X2 . n = A \/ (X1 . n) by Th56
.= (A (\/) X1) . n by Def6 ; ::_thesis: verum
end;
then  Intersection X2 = A \/ (Intersection X1) by Th34;
then  lim_sup (A (\/) A1) = A \/ (Intersection X1) by SETLIM_1:def_5;
hence  lim_sup (A (\/) A1) = A \/ (lim_sup A1) by SETLIM_1:def_5; ::_thesis: verum
end;

theorem Th83: :: SETLIM_2:83
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)
let A1 be SetSequence of X; ::_thesis: A \ (lim_sup A1) c= lim_sup (A (\) A1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ (lim_sup A1) or x in lim_sup (A (\) A1) )
assume A1: x in A \ (lim_sup A1) ; ::_thesis: x in lim_sup (A (\) A1)
then  not x in lim_sup A1 by XBOOLE_0:def_5;
then consider n1 being Element of NAT  such that
A2: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_0:5;
assume  not x in lim_sup (A (\) A1) ; ::_thesis: contradiction
then consider n being Element of NAT  such that
A3: for k being Element of NAT holds not x in (A (\) A1) . (n + k) by KURATO_0:5;
A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_
(_not_x_in_A_or_x_in_A1_._(n_+_k)_)
let k be Element of NAT ; ::_thesis: ( not x in A or x in A1 . (n + k) )
 not x in (A (\) A1) . (n + k) by A3;
then  not x in A \ (A1 . (n + k)) by Def7;
hence  ( not x in A or x in A1 . (n + k) ) by XBOOLE_0:def_5; ::_thesis: verum
end;
percases ( not x in A or for k being Element of NAT holds x in A1 . (n + k) ) by A4;
suppose not x in A ; ::_thesis: contradiction
hence  contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA5: for k being Element of NAT holds x in A1 . (n + k) ; ::_thesis: contradiction
 not x in A1 . (n1 + n) by A2;
hence  contradiction by A5; ::_thesis: verum
end;
end;
end;

theorem Th84: :: SETLIM_2:84
for X being set
for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A1 (\) A) = (lim_sup A1) \ A
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_sup (A1 (\) A) = (lim_sup A1) \ A
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds lim_sup (A1 (\) A) = (lim_sup A1) \ A
let A1 be SetSequence of X; ::_thesis: lim_sup (A1 (\) A) = (lim_sup A1) \ A
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
reconsider X2 = superior_setsequence (A1 (\) A) as SetSequence of X ;
 X2 = X1 (\) A
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: X2 . n = (X1 (\) A) . n
thus X2 . n = (X1 . n) \ A by Th58
.= (X1 (\) A) . n by Def8 ; ::_thesis: verum
end;
then  Intersection X2 = (Intersection X1) \ A by Th36;
then  lim_sup (A1 (\) A) = (Intersection X1) \ A by SETLIM_1:def_5;
hence  lim_sup (A1 (\) A) = (lim_sup A1) \ A by SETLIM_1:def_5; ::_thesis: verum
end;

theorem Th85: :: SETLIM_2:85
for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X holds A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X holds A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
let A1 be SetSequence of X; ::_thesis: A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
 for n being Element of NAT holds (A (\+\) A1) . n = A \+\ (A1 . n) by Def9;
hence  A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1) by KURATO_0:17; ::_thesis: verum
end;

theorem Th86: :: SETLIM_2:86
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\) A1) = A \ (lim_sup A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\) A1) = A \ (lim_sup A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\) A1) = A \ (lim_sup A1)
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_sup (A (\) A1) = A \ (lim_sup A1) )
assume A1: A1 is convergent ; ::_thesis: lim_sup (A (\) A1) = A \ (lim_sup A1)
thus  lim_sup (A (\) A1) c= A \ (lim_sup A1) :: according to XBOOLE_0:def_10 ::_thesis: A \ (lim_sup A1) c= lim_sup (A (\) A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup (A (\) A1) or x in A \ (lim_sup A1) )
assume A2: x in lim_sup (A (\) A1) ; ::_thesis: x in A \ (lim_sup A1)
A3: for n being Element of NAT ex k being Element of NAT st
( x in A & not x in A1 . (n + k) )
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st
( x in A & not x in A1 . (n + k) )
consider k being Element of NAT  such that
A4: x in (A (\) A1) . (n + k) by A2, KURATO_0:5;
 x in A \ (A1 . (n + k)) by A4, Def7;
then  ( x in A & not x in A1 . (n + k) ) by XBOOLE_0:def_5;
hence  ex k being Element of NAT st
( x in A & not x in A1 . (n + k) ) ; ::_thesis: verum
end;
A5: x in A
proof
A6: for n being Element of NAT ex k being Element of NAT st x in A
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st x in A
 ex k being Element of NAT st
( x in A & not x in A1 . (n + k) ) by A3;
hence  ex k being Element of NAT st x in A ; ::_thesis: verum
end;
assume  not x in A ; ::_thesis: contradiction
then  for n being Element of NAT holds not x in A ;
hence  contradiction by A6; ::_thesis: verum
end;
 for n being Element of NAT holds
not for k being Element of NAT holds x in A1 . (n + k)
proof
let n be Element of NAT ; ::_thesis: not for k being Element of NAT holds x in A1 . (n + k)
 ex k being Element of NAT st
( x in A & not x in A1 . (n + k) ) by A3;
hence  not for k being Element of NAT holds x in A1 . (n + k) ; ::_thesis: verum
end;
then  not x in lim_inf A1 by KURATO_0:4;
then  not x in lim_sup A1 by A1, KURATO_0:def_5;
hence  x in A \ (lim_sup A1) by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  A \ (lim_sup A1) c= lim_sup (A (\) A1) by Th83; ::_thesis: verum
end;

theorem Th87: :: SETLIM_2:87
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\+\) A1) = A \+\ (lim_sup A1)
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\+\) A1) = A \+\ (lim_sup A1)
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
lim_sup (A (\+\) A1) = A \+\ (lim_sup A1)
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies lim_sup (A (\+\) A1) = A \+\ (lim_sup A1) )
assume A1: A1 is convergent ; ::_thesis: lim_sup (A (\+\) A1) = A \+\ (lim_sup A1)
thus  lim_sup (A (\+\) A1) c= A \+\ (lim_sup A1) :: according to XBOOLE_0:def_10 ::_thesis: A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup (A (\+\) A1) or x in A \+\ (lim_sup A1) )
assume A2: x in lim_sup (A (\+\) A1) ; ::_thesis: x in A \+\ (lim_sup A1)
A3: now__::_thesis:_for_n_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_
(_(_x_in_A_&_not_x_in_A1_._(n_+_k)_)_or_(_not_x_in_A_&_x_in_A1_._(n_+_k)_)_)
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st
( ( x in A & not x in A1 . (n + k) ) or ( not x in A & x in A1 . (n + k) ) )
consider k1 being Element of NAT  such that
A4: x in (A (\+\) A1) . (n + k1) by A2, KURATO_0:5;
 x in A \+\ (A1 . (n + k1)) by A4, Def9;
then  ( ( x in A & not x in A1 . (n + k1) ) or ( not x in A & x in A1 . (n + k1) ) ) by XBOOLE_0:1;
hence  ex k being Element of NAT st
( ( x in A & not x in A1 . (n + k) ) or ( not x in A & x in A1 . (n + k) ) ) ; ::_thesis: verum
end;
assume A5: not x in A \+\ (lim_sup A1) ; ::_thesis: contradiction
percases ( ( not x in A & not x in lim_sup A1 ) or ( x in A & x in lim_sup A1 ) ) by A5, XBOOLE_0:1;
supposeA6: ( not x in A & not x in lim_sup A1 ) ; ::_thesis: contradiction
then consider n1 being Element of NAT  such that
A7: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_0:5;
 ex k1 being Element of NAT st
( ( x in A & not x in A1 . (n1 + k1) ) or ( not x in A & x in A1 . (n1 + k1) ) ) by A3;
hence  contradiction by A6, A7; ::_thesis: verum
end;
supposeA8: ( x in A & x in lim_sup A1 ) ; ::_thesis: contradiction
then  x in lim_inf A1 by A1, KURATO_0:def_5;
then consider n2 being Element of NAT  such that
A9: for k being Element of NAT holds x in A1 . (n2 + k) by KURATO_0:4;
 ex k2 being Element of NAT st
( ( x in A & not x in A1 . (n2 + k2) ) or ( not x in A & x in A1 . (n2 + k2) ) ) by A3;
hence  contradiction by A8, A9; ::_thesis: verum
end;
end;
end;
thus  A \+\ (lim_sup A1) c= lim_sup (A (\+\) A1) by Th85; ::_thesis: verum
end;

theorem :: SETLIM_2:88
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) )
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) )
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent & A2 is convergent implies ( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) ) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; ::_thesis: ( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) )
A3: lim_sup (A1 (/\) A2) = (lim A1) /\ (lim A2) by A1, Th71;
lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2) by Th60
.= (lim A1) /\ (lim_inf A2) by A1, KURATO_0:def_5
.= (lim A1) /\ (lim A2) by A2, KURATO_0:def_5 ;
hence  ( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) ) by A3, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:89
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\/) A2 is convergent & lim (A1 (\/) A2) = (lim A1) \/ (lim A2) )
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\/) A2 is convergent & lim (A1 (\/) A2) = (lim A1) \/ (lim A2) )
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent & A2 is convergent implies ( A1 (\/) A2 is convergent & lim (A1 (\/) A2) = (lim A1) \/ (lim A2) ) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; ::_thesis: ( A1 (\/) A2 is convergent & lim (A1 (\/) A2) = (lim A1) \/ (lim A2) )
A3: lim_sup (A1 (\/) A2) = (lim A1) \/ (lim A2) by Th68;
lim_inf (A1 (\/) A2) = (lim_inf A1) \/ (lim_inf A2) by A1, Th63
.= (lim A1) \/ (lim_inf A2) by A1, KURATO_0:def_5
.= (lim A1) \/ (lim A2) by A2, KURATO_0:def_5 ;
hence  ( A1 (\/) A2 is convergent & lim (A1 (\/) A2) = (lim A1) \/ (lim A2) ) by A3, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:90
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) )
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) )
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent & A2 is convergent implies ( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) ) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; ::_thesis: ( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) )
A3: lim_sup (A1 (\) A2) = (lim A1) \ (lim A2) by A2, Th72;
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2) by A2, Th64
.= (lim A1) \ (lim_inf A2) by A1, KURATO_0:def_5
.= (lim A1) \ (lim A2) by A2, KURATO_0:def_5 ;
hence  ( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) ) by A3, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:91
for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\+\) A2 is convergent & lim (A1 (\+\) A2) = (lim A1) \+\ (lim A2) )
proof
let X be set ; ::_thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (\+\) A2 is convergent & lim (A1 (\+\) A2) = (lim A1) \+\ (lim A2) )
let A1, A2 be SetSequence of X; ::_thesis: ( A1 is convergent & A2 is convergent implies ( A1 (\+\) A2 is convergent & lim (A1 (\+\) A2) = (lim A1) \+\ (lim A2) ) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; ::_thesis: ( A1 (\+\) A2 is convergent & lim (A1 (\+\) A2) = (lim A1) \+\ (lim A2) )
A3: lim_sup (A1 (\+\) A2) = (lim A1) \+\ (lim A2) by A1, A2, Th73;
lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2) by A1, A2, Th66
.= (lim A1) \+\ (lim_inf A2) by A1, KURATO_0:def_5
.= (lim A1) \+\ (lim A2) by A2, KURATO_0:def_5 ;
hence  ( A1 (\+\) A2 is convergent & lim (A1 (\+\) A2) = (lim A1) \+\ (lim A2) ) by A3, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:92
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) )
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) )
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) )
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies ( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) ) )
assume A1: A1 is convergent ; ::_thesis: ( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) )
A2: lim_inf (A (/\) A1) = A /\ (lim_inf A1) by Th74
.= A /\ (lim A1) by A1, KURATO_0:def_5 ;
then  lim_sup (A (/\) A1) = lim_inf (A (/\) A1) by Th81;
hence  ( A (/\) A1 is convergent & lim (A (/\) A1) = A /\ (lim A1) ) by A2, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:93
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) )
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) )
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) )
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies ( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) ) )
assume A1: A1 is convergent ; ::_thesis: ( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) )
A2: lim_inf (A (\/) A1) = A \/ (lim_inf A1) by Th75
.= A \/ (lim A1) by A1, KURATO_0:def_5 ;
then  lim_sup (A (\/) A1) = lim_inf (A (\/) A1) by Th82;
hence  ( A (\/) A1 is convergent & lim (A (\/) A1) = A \/ (lim A1) ) by A2, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:94
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) )
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) )
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) )
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies ( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) ) )
assume A1: A1 is convergent ; ::_thesis: ( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) )
then A2: lim_inf (A (\) A1) = A \ (lim_inf A1) by Th79
.= A \ (lim A1) by A1, KURATO_0:def_5 ;
then  lim_sup (A (\) A1) = lim_inf (A (\) A1) by A1, Th86;
hence  ( A (\) A1 is convergent & lim (A (\) A1) = A \ (lim A1) ) by A2, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:95
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A )
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A )
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A )
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies ( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A ) )
assume A1: A1 is convergent ; ::_thesis: ( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A )
A2: lim_inf (A1 (\) A) = (lim_inf A1) \ A by Th77
.= (lim A1) \ A by A1, KURATO_0:def_5 ;
then  lim_sup (A1 (\) A) = lim_inf (A1 (\) A) by Th84;
hence  ( A1 (\) A is convergent & lim (A1 (\) A) = (lim A1) \ A ) by A2, KURATO_0:def_5; ::_thesis: verum
end;

theorem :: SETLIM_2:96
for X being set
for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
proof
let X be set ; ::_thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
let A be Subset of X; ::_thesis: for A1 being SetSequence of X st A1 is convergent holds
( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
let A1 be SetSequence of X; ::_thesis: ( A1 is convergent implies ( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) ) )
assume A1: A1 is convergent ; ::_thesis: ( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
then A2: lim_inf (A (\+\) A1) = A \+\ (lim_inf A1) by Th80
.= A \+\ (lim A1) by A1, KURATO_0:def_5 ;
then  lim_sup (A (\+\) A1) = lim_inf (A (\+\) A1) by A1, Th87;
hence  ( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) ) by A2, KURATO_0:def_5; ::_thesis: verum
end;