let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
A1: for X being set
for A being SetSequence of X
for n being Nat
for x being set holds
( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st
( k >= n & x in A . k ) )

let X be set ; :: thesis:
let A be SetSequence of X; :: thesis:
let n be Nat; :: thesis:
let x be set ; :: thesis:

hereby :: thesis:

given k being Nat such that A2: x in (A ^\ n) . k ; :: thesis:
A3: x in A . (k + n) by A2, NAT_1:def 3;
consider k being Nat such that
A4: x in A . (k + n) by A3;
consider k being Nat such that
A5: ( k >= n & x in A . k ) by A4, NAT_1:11;
thus ex k being Nat st
( k >= n & x in A . k ) by A5; :: thesis:

end;

given k being Nat such that A6: ( k >= n & x in A . k ) ; :: thesis:
consider knat being Nat such that
A7: k = n + knat by A6, NAT_1:10;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
( x in A . k implies x in (A ^\ n) . knat ) by A7, NAT_1:def 3;
hence ex k being Nat st x in (A ^\ n) . k by A6; :: thesis:

end;

A8: for X being set
for A being SetSequence of X
for x being object holds
( x in Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

proof

let X be set ; :: thesis:
let A be SetSequence of X; :: thesis:
let x be object ; :: thesis:

hereby :: thesis:

assume A9: x in Intersection (superior_setsequence A) ; :: thesis:
A10: for n being Nat st x in (superior_setsequence A) . n holds
ex k being Nat st
( k >= n & x in A . k )

proof

let n be Nat; :: thesis:
assume A11: x in (superior_setsequence A) . n ; :: thesis:
( x in (superior_setsequence A) . n implies x in Union (A ^\ n) ) by Def7;
then ex k being Nat st x in (A ^\ n) . k by A11, PROB_1:12;
then consider k being Nat such that
A14: ( k >= n & x in A . k ) by A1;
take k ; :: thesis:
thus ( k >= n & x in A . k ) by A14; :: thesis:

end;

for m being Nat ex n being Nat st
( n >= m & x in A . n )

proof

let m be Nat; :: thesis:
x in (superior_setsequence A) . m by A9, PROB_1:13;
hence ex n being Nat st
( n >= m & x in A . n ) by A10; :: thesis:

end;

hence for m being Nat ex n being Nat st
( n >= m & x in A . n ) ; :: thesis:

end;

assume A16: for m being Nat ex n being Nat st
( n >= m & x in A . n ) ; :: thesis:
A17: for m being Nat st ex n being Nat st
( n >= m & x in A . n ) holds
x in (superior_setsequence A) . m

proof

let m be Nat; :: thesis:
given n being Nat such that A18: ( n >= m & x in A . n ) ; :: thesis:
ex k being Nat st x in (A ^\ m) . k by A18, A1;
then x in Union (A ^\ m) by PROB_1:12;
hence x in (superior_setsequence A) . m by Def7; :: thesis:

end;

for m being Nat holds x in (superior_setsequence A) . m

proof

let m be Nat; :: thesis:
ex n being Nat st
( n >= m & x in A . n ) by A16;
hence x in (superior_setsequence A) . m by A17; :: thesis:

end;

hence x in Intersection (superior_setsequence A) by PROB_1:13; :: thesis:

end;

A19: for A being SetSequence of Sigma
for x being object holds
( x in @Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

proof

let A be SetSequence of Sigma; :: thesis:
let x be object ; :: thesis:
@Intersection (superior_setsequence A) = Intersection (superior_setsequence A) by PROB_2:def 1;
hence ( x in @Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) by A8; :: thesis:

end;

A20: for X being set
for A being SetSequence of X
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k )

proof

let X be set ; :: thesis:
let A be SetSequence of X; :: thesis:
let x be object ; :: thesis:

hereby :: thesis:

assume x in Union (inferior_setsequence A) ; :: thesis:
then consider n being Nat such that
A21: x in (inferior_setsequence A) . n by PROB_1:12;
A22: (inferior_setsequence A) . n = Intersection (A ^\ n) by Def9;
for k being Nat st k >= n holds
x in A . k

proof

let k be Nat; :: thesis:
assume n <= k ; :: thesis:
then consider knat being Nat such that
A24: k = n + knat by NAT_1:10;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
( x in A . k iff x in (A ^\ n) . knat ) by A24, NAT_1:def 3;
hence x in A . k by A22, A21, PROB_1:13; :: thesis:

end;

hence ex n being Nat st
for k being Nat st k >= n holds
x in A . k ; :: thesis:

end;

given n being Nat such that A26: for k being Nat st k >= n holds
x in A . k ; :: thesis:
set knat = the Nat;
for s being Nat holds x in (A ^\ n) . s

proof

let s be Nat; :: thesis:
( x in (A ^\ n) . s iff x in A . (n + s) ) by NAT_1:def 3;
hence x in (A ^\ n) . s by A26, NAT_1:12; :: thesis:

end;

then x in Intersection (A ^\ n) by PROB_1:13;
then x in (inferior_setsequence A) . n by Def9;
hence x in Union (inferior_setsequence A) by PROB_1:12; :: thesis:

end;

for A being SetSequence of Sigma
for x being Element of Omega holds
( x in Union (inferior_setsequence (Complement A)) iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k )

proof

let A be SetSequence of Sigma; :: thesis:
let x be Element of Omega; :: thesis:

hereby :: thesis:

assume x in Union (inferior_setsequence (Complement A)) ; :: thesis:
then consider n being Nat such that
A27: x in (inferior_setsequence (Complement A)) . n by PROB_1:12;
A28: (inferior_setsequence (Complement A)) . n = Intersection ((Complement A) ^\ n) by Def9;
set m = the Element of NAT ;
for k being Nat st k >= n holds
not x in A . k

proof

let k be Nat; :: thesis:
assume A29: n <= k ; :: thesis:
consider knat being Nat such that
A30: k = n + knat by A29, NAT_1:10;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
A31: ( x in (Complement A) . k iff x in ((Complement A) ^\ n) . knat ) by A30, NAT_1:def 3;
x in (A . k) ` by A28, A27, A31, PROB_1:13, PROB_1:def 2;
then x in Omega \ (A . k) by SUBSET_1:def 4;
hence not x in A . k by XBOOLE_0:def 5; :: thesis:

end;

hence ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ; :: thesis:

end;

given n being Nat such that A32: for k being Nat st k >= n holds
not x in A . k ; :: thesis:
set k = the Element of NAT ;
A33: for k being Nat st n <= k holds
x in (Complement A) . k

proof

let k be Nat; :: thesis:
assume A34: n <= k ; :: thesis:
A35: not x in A . k by A34, A32;
x in Omega \ (A . k) by A35, XBOOLE_0:def 5;
then x in (A . k) ` by SUBSET_1:def 4;
hence x in (Complement A) . k by PROB_1:def 2; :: thesis:

end;

for s being Nat holds x in ((Complement A) ^\ n) . s

proof

let s be Nat; :: thesis:
( x in ((Complement A) ^\ n) . s iff x in (Complement A) . (n + s) ) by NAT_1:def 3;
hence x in ((Complement A) ^\ n) . s by A33, NAT_1:12; :: thesis:

end;

then x in Intersection ((Complement A) ^\ n) by PROB_1:13;
then x in (inferior_setsequence (Complement A)) . n by Def9;
hence x in Union (inferior_setsequence (Complement A)) by PROB_1:12; :: thesis:

end;

hence ( ( for X being set
for A being SetSequence of X
for n being Nat
for x being object holds
( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st
( k >= n & x in A . k ) ) ) & ( for X being set
for A being SetSequence of X
for x being object holds
( x in Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) ) & ( for A being SetSequence of Sigma
for x being object holds
( x in @Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) ) & ( for X being set
for A being SetSequence of X
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being Element of Omega holds
( x in Union (inferior_setsequence (Complement A)) iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ) ) ) by A1, A8, A19, A20; :: thesis: