let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega holds
( ( 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 () 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 () 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 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 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 iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ) ) )

let Sigma be SigmaField of Omega; :: thesis: ( ( 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 () 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 () 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 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 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 iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ) ) )

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 ) )
proof
let X be set ; :: thesis: 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 A be SetSequence of X; :: thesis: 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 n be Nat; :: thesis: 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: ( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st
( k >= n & x in A . k ) )

hereby :: thesis: ( ex k being Nat st
( k >= n & x in A . k ) implies ex k being Nat st x in (A ^\ n) . k )
assume ex k being Nat st x in (A ^\ n) . k ; :: thesis: ex k being Nat st
( k >= n & x in A . k )

then consider k being Nat such that
A2: x in (A ^\ n) . k ;
A3: x in A . (k + n) by ;
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 ;
thus ex k being Nat st
( k >= n & x in A . k ) by A5; :: thesis: verum
end;
assume ex k being Nat st
( k >= n & x in A . k ) ; :: thesis: ex k being Nat st x in (A ^\ n) . k
then consider k being Nat such that
A6: ( k >= n & x in A . k ) ;
consider knat being Nat such that
A7: k = n + knat by ;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
( x in A . k implies x in (A ^\ n) . knat ) by ;
hence ex k being Nat st x in (A ^\ n) . k by A6; :: thesis: verum
end;
A8: for X being set
for A being SetSequence of X
for x being object holds
( x in Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )
proof
let X be set ; :: thesis: for A being SetSequence of X
for x being object holds
( x in Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

let A be SetSequence of X; :: thesis: for x being object holds
( x in Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

let x be object ; :: thesis: ( x in Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

hereby :: thesis: ( ( for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) implies x in Intersection () )
assume A9: x in Intersection () ; :: thesis: for m being Nat ex n being Nat st
( n >= m & x in A . n )

A10: for n being Nat st x in () . n holds
ex k being Nat st
( k >= n & x in A . k )
proof
let n be Nat; :: thesis: ( x in () . n implies ex k being Nat st
( k >= n & x in A . k ) )

assume A11: x in () . n ; :: thesis: ex k being Nat st
( k >= n & x in A . k )

A12: ( x in () . n implies x in Union (A ^\ n) ) by Def7;
A13: ex k being Nat st x in (A ^\ n) . k by ;
consider k being Nat such that
A14: ( k >= n & x in A . k ) by ;
take k ; :: thesis: ( k >= n & x in A . k )
thus ( k >= n & x in A . k ) by A14; :: thesis: verum
end;
A15: for m being Nat ex n being Nat st
( n >= m & x in A . n )
proof
let m be Nat; :: thesis: ex n being Nat st
( n >= m & x in A . n )

x in () . m by ;
hence ex n being Nat st
( n >= m & x in A . n ) by A10; :: thesis: verum
end;
thus for m being Nat ex n being Nat st
( n >= m & x in A . n ) by A15; :: thesis: verum
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 () . m
proof
let m be Nat; :: thesis: ( ex n being Nat st
( n >= m & x in A . n ) implies x in () . m )

assume ex n being Nat st
( n >= m & x in A . n ) ; :: thesis: x in () . m
then consider n being Nat such that
A18: ( n >= m & x in A . n ) ;
ex k being Nat st x in (A ^\ m) . k by ;
then x in Union (A ^\ m) by PROB_1:12;
hence x in () . m by Def7; :: thesis: verum
end;
for m being Nat holds x in () . m
proof
let m be Nat; :: thesis: x in () . m
ex n being Nat st
( n >= m & x in A . n ) by A16;
hence x in () . m by A17; :: thesis: verum
end;
hence x in Intersection () by PROB_1:13; :: thesis: verum
end;
A19: for A being SetSequence of Sigma
for x being object holds
( x in @Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )
proof
let A be SetSequence of Sigma; :: thesis: for x being object holds
( x in @Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

let x be object ; :: thesis: ( x in @Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) )

@Intersection () = Intersection () by PROB_2:def 1;
hence ( x in @Intersection () iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) by A8; :: thesis: verum
end;
A20: for X being set
for A being SetSequence of X
for x being object holds
( x in Union iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k )
proof
let X be set ; :: thesis: for A being SetSequence of X
for x being object holds
( x in Union iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k )

let A be SetSequence of X; :: thesis: for x being object holds
( x in Union iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k )

let x be object ; :: thesis: ( x in Union iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k )

hereby :: thesis: ( ex n being Nat st
for k being Nat st k >= n holds
x in A . k implies x in Union )
assume x in Union ; :: thesis: ex n being Nat st
for k being Nat st k >= n holds
x in A . k

then consider n being Nat such that
A21: x in . n by PROB_1:12;
A22: (Intersect_Shift_Seq 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: ( k >= n implies x in A . k )
assume A23: n <= k ; :: thesis: x in A . k
consider knat being Nat such that
A24: k = n + knat by ;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
A25: ( x in A . k iff x in (A ^\ n) . knat ) by ;
thus x in A . k by ; :: thesis: verum
end;
hence ex n being Nat st
for k being Nat st k >= n holds
x in A . k ; :: thesis: verum
end;
assume ex n being Nat st
for k being Nat st k >= n holds
x in A . k ; :: thesis:
then consider n being Nat such that
A26: for k being Nat st k >= n holds
x in A . k ;
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
( x in (A ^\ n) . s iff x in A . (n + s) ) by NAT_1:def 3;
hence x in (A ^\ n) . s by ; :: thesis: verum
end;
then x in Intersection (A ^\ n) by PROB_1:13;
then x in . n by Def9;
hence x in Union by PROB_1:12; :: thesis: verum
end;
for A being SetSequence of Sigma
for x being Element of Omega holds
( x in Union 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: for x being Element of Omega holds
( x in Union iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k )

let x be Element of Omega; :: thesis: ( x in Union iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k )

hereby :: thesis: ( ex n being Nat st
for k being Nat st k >= n holds
not x in A . k implies x in Union )
assume x in Union ; :: thesis: ex n being Nat st
for k being Nat st k >= n holds
not x in A . k

then consider n being Nat such that
A27: x in . n by PROB_1:12;
A28: (Intersect_Shift_Seq ()) . n = Intersection (() ^\ 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: ( k >= n implies not x in A . k )
assume A29: n <= k ; :: thesis: not x in A . k
consider knat being Nat such that
A30: k = n + knat by ;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
A31: ( x in () . k iff x in (() ^\ n) . knat ) by ;
x in (A . k) ` by ;
then x in Omega \ (A . k) by SUBSET_1:def 4;
hence not x in A . k by XBOOLE_0:def 5; :: thesis: verum
end;
hence ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ; :: thesis: verum
end;
assume ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ; :: thesis:
then consider n being Nat such that
A32: for k being Nat st k >= n holds
not x in A . k ;
set k = the Element of NAT ;
A33: for k being Nat st n <= k holds
x in () . k
proof
let k be Nat; :: thesis: ( n <= k implies x in () . k )
assume A34: n <= k ; :: thesis: x in () . k
A35: not x in A . k by ;
x in Omega \ (A . k) by ;
then x in (A . k) ` by SUBSET_1:def 4;
hence x in () . k by PROB_1:def 2; :: thesis: verum
end;
for s being Nat holds x in (() ^\ n) . s
proof
let s be Nat; :: thesis: x in (() ^\ n) . s
( x in (() ^\ n) . s iff x in () . (n + s) ) by NAT_1:def 3;
hence x in (() ^\ n) . s by ; :: thesis: verum
end;
then x in Intersection (() ^\ n) by PROB_1:13;
then x in . n by Def9;
hence x in Union by PROB_1:12; :: thesis: verum
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 () 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 () 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 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 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 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: verum