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 (Union_Shift_Seq 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 (Union_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq (Complement A)) 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 (Union_Shift_Seq 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 (Union_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq (Complement A)) 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 ) )

for A being SetSequence of X

for x being object holds

( x in Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

for x being object holds

( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

for A being SetSequence of X

for x being object holds

( x in Union (Intersect_Shift_Seq A) iff ex n being Nat st

for k being Nat st k >= n holds

x in A . k )

for x being Element of Omega holds

( x in Union (Intersect_Shift_Seq (Complement A)) iff ex n being Nat st

for k being Nat st k >= n holds

not x in A . k )

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 (Union_Shift_Seq 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 (Union_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq (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: verum

( ( 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 (Union_Shift_Seq 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 (Union_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq (Complement A)) 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 (Union_Shift_Seq 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 (Union_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq (Complement A)) 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

A8:
for X being set
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 ) )

( 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 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: verum

end;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 ( 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 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: verum

end;( 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 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: verum

( 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 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: verum

for A being SetSequence of X

for x being object holds

( x in Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

proof

A19:
for A being SetSequence of Sigma
let X be set ; :: thesis: for A being SetSequence of X

for x being object holds

( x in Intersection (Union_Shift_Seq A) 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 (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

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

( n >= m & x in A . n ) )

( n >= m & x in A . n ) ; :: thesis: x in Intersection (Union_Shift_Seq A)

A17: for m being Nat st ex n being Nat st

( n >= m & x in A . n ) holds

x in (Union_Shift_Seq A) . m

end;for x being object holds

( x in Intersection (Union_Shift_Seq A) 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 (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

let x be object ; :: thesis: ( x in Intersection (Union_Shift_Seq A) 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 (Union_Shift_Seq A) )

assume A16:
for m being Nat ex n being Nat st ( n >= m & x in A . n ) ) implies x in Intersection (Union_Shift_Seq A) )

assume A9:
x in Intersection (Union_Shift_Seq A)
; :: thesis: for m being Nat ex n being Nat st

( n >= m & x in A . n )

A10: for n being Nat st x in (Union_Shift_Seq A) . n holds

ex k being Nat st

( k >= n & x in A . k )

( n >= m & x in A . n )

( n >= m & x in A . n ) by A15; :: thesis: verum

end;( n >= m & x in A . n )

A10: for n being Nat st x in (Union_Shift_Seq A) . n holds

ex k being Nat st

( k >= n & x in A . k )

proof

A15:
for m being Nat ex n being Nat st
let n be Nat; :: thesis: ( x in (Union_Shift_Seq A) . n implies ex k being Nat st

( k >= n & x in A . k ) )

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

( k >= n & x in A . k )

A12: ( x in (Union_Shift_Seq A) . n implies x in Union (A ^\ n) ) by Def7;

A13: ex k being Nat st x in (A ^\ n) . k by A11, A12, PROB_1:12;

consider k being Nat such that

A14: ( k >= n & x in A . k ) by A13, A1;

take k ; :: thesis: ( k >= n & x in A . k )

thus ( k >= n & x in A . k ) by A14; :: thesis: verum

end;( k >= n & x in A . k ) )

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

( k >= n & x in A . k )

A12: ( x in (Union_Shift_Seq A) . n implies x in Union (A ^\ n) ) by Def7;

A13: ex k being Nat st x in (A ^\ n) . k by A11, A12, PROB_1:12;

consider k being Nat such that

A14: ( k >= n & x in A . k ) by A13, A1;

take k ; :: thesis: ( k >= n & x in A . k )

thus ( k >= n & x in A . k ) by A14; :: thesis: verum

( n >= m & x in A . n )

proof

thus
for m being Nat ex n being Nat st
let m be Nat; :: thesis: ex n being Nat st

( n >= m & x in A . n )

x in (Union_Shift_Seq A) . m by A9, PROB_1:13;

hence ex n being Nat st

( n >= m & x in A . n ) by A10; :: thesis: verum

end;( n >= m & x in A . n )

x in (Union_Shift_Seq A) . m by A9, PROB_1:13;

hence ex n being Nat st

( n >= m & x in A . n ) by A10; :: thesis: verum

( n >= m & x in A . n ) by A15; :: thesis: verum

( n >= m & x in A . n ) ; :: thesis: x in Intersection (Union_Shift_Seq A)

A17: for m being Nat st ex n being Nat st

( n >= m & x in A . n ) holds

x in (Union_Shift_Seq A) . m

proof

for m being Nat holds x in (Union_Shift_Seq A) . m
let m be Nat; :: thesis: ( ex n being Nat st

( n >= m & x in A . n ) implies x in (Union_Shift_Seq A) . m )

assume ex n being Nat st

( n >= m & x in A . n ) ; :: thesis: x in (Union_Shift_Seq A) . 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 A18, A1;

then x in Union (A ^\ m) by PROB_1:12;

hence x in (Union_Shift_Seq A) . m by Def7; :: thesis: verum

end;( n >= m & x in A . n ) implies x in (Union_Shift_Seq A) . m )

assume ex n being Nat st

( n >= m & x in A . n ) ; :: thesis: x in (Union_Shift_Seq A) . 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 A18, A1;

then x in Union (A ^\ m) by PROB_1:12;

hence x in (Union_Shift_Seq A) . m by Def7; :: thesis: verum

proof

hence
x in Intersection (Union_Shift_Seq A)
by PROB_1:13; :: thesis: verum
let m be Nat; :: thesis: x in (Union_Shift_Seq A) . m

ex n being Nat st

( n >= m & x in A . n ) by A16;

hence x in (Union_Shift_Seq A) . m by A17; :: thesis: verum

end;ex n being Nat st

( n >= m & x in A . n ) by A16;

hence x in (Union_Shift_Seq A) . m by A17; :: thesis: verum

for x being object holds

( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

proof

A20:
for X being set
let A be SetSequence of Sigma; :: thesis: for x being object holds

( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

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

( n >= m & x in A . n ) )

@Intersection (Union_Shift_Seq A) = Intersection (Union_Shift_Seq A) by PROB_2:def 1;

hence ( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) ) by A8; :: thesis: verum

end;( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) )

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

( n >= m & x in A . n ) )

@Intersection (Union_Shift_Seq A) = Intersection (Union_Shift_Seq A) by PROB_2:def 1;

hence ( x in @Intersection (Union_Shift_Seq A) iff for m being Nat ex n being Nat st

( n >= m & x in A . n ) ) by A8; :: thesis: verum

for A being SetSequence of X

for x being object holds

( x in Union (Intersect_Shift_Seq A) iff ex n being Nat st

for k being Nat st k >= n holds

x in A . k )

proof

for A being SetSequence of Sigma
let X be set ; :: thesis: for A being SetSequence of X

for x being object holds

( x in Union (Intersect_Shift_Seq A) 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 (Intersect_Shift_Seq A) 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 (Intersect_Shift_Seq A) iff ex n being Nat st

for k being Nat st k >= n holds

x in A . k )

for k being Nat st k >= n holds

x in A . k ; :: thesis: x in Union (Intersect_Shift_Seq A)

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

then x in (Intersect_Shift_Seq A) . n by Def9;

hence x in Union (Intersect_Shift_Seq A) by PROB_1:12; :: thesis: verum

end;for x being object holds

( x in Union (Intersect_Shift_Seq A) 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 (Intersect_Shift_Seq A) 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 (Intersect_Shift_Seq A) 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 (Intersect_Shift_Seq A) )

assume
ex n being Nat st for k being Nat st k >= n holds

x in A . k implies x in Union (Intersect_Shift_Seq A) )

assume
x in Union (Intersect_Shift_Seq A)
; :: 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 (Intersect_Shift_Seq A) . 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

for k being Nat st k >= n holds

x in A . k ; :: thesis: verum

end;for k being Nat st k >= n holds

x in A . k

then consider n being Nat such that

A21: x in (Intersect_Shift_Seq A) . 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

hence
ex n being Nat st
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 A23, NAT_1:10;

reconsider knat = knat as Element of NAT by ORDINAL1:def 12;

A25: ( x in A . k iff x in (A ^\ n) . knat ) by A24, NAT_1:def 3;

thus x in A . k by A22, A21, A25, PROB_1:13; :: thesis: verum

end;assume A23: n <= k ; :: thesis: x in A . k

consider knat being Nat such that

A24: k = n + knat by A23, NAT_1:10;

reconsider knat = knat as Element of NAT by ORDINAL1:def 12;

A25: ( x in A . k iff x in (A ^\ n) . knat ) by A24, NAT_1:def 3;

thus x in A . k by A22, A21, A25, PROB_1:13; :: thesis: verum

for k being Nat st k >= n holds

x in A . k ; :: thesis: verum

for k being Nat st k >= n holds

x in A . k ; :: thesis: x in Union (Intersect_Shift_Seq A)

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

then
x in Intersection (A ^\ n)
by PROB_1:13;
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 A26, NAT_1:12; :: thesis: verum

end;( 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: verum

then x in (Intersect_Shift_Seq A) . n by Def9;

hence x in Union (Intersect_Shift_Seq A) by PROB_1:12; :: thesis: verum

for x being Element of Omega holds

( x in Union (Intersect_Shift_Seq (Complement A)) iff ex n being Nat st

for k being Nat st k >= n holds

not x in A . k )

proof

hence
( ( for X being set
let A be SetSequence of Sigma; :: thesis: for x being Element of Omega holds

( x in Union (Intersect_Shift_Seq (Complement A)) 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 (Intersect_Shift_Seq (Complement A)) iff ex n being Nat st

for k being Nat st k >= n holds

not x in A . k )

for k being Nat st k >= n holds

not x in A . k ; :: thesis: x in Union (Intersect_Shift_Seq (Complement A))

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 (Complement A) . k

then x in (Intersect_Shift_Seq (Complement A)) . n by Def9;

hence x in Union (Intersect_Shift_Seq (Complement A)) by PROB_1:12; :: thesis: verum

end;( x in Union (Intersect_Shift_Seq (Complement A)) 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 (Intersect_Shift_Seq (Complement A)) 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 (Intersect_Shift_Seq (Complement A)) )

assume
ex n being Nat st for k being Nat st k >= n holds

not x in A . k implies x in Union (Intersect_Shift_Seq (Complement A)) )

assume
x in Union (Intersect_Shift_Seq (Complement A))
; :: 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 (Intersect_Shift_Seq (Complement A)) . n by PROB_1:12;

A28: (Intersect_Shift_Seq (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

for k being Nat st k >= n holds

not x in A . k ; :: thesis: verum

end;for k being Nat st k >= n holds

not x in A . k

then consider n being Nat such that

A27: x in (Intersect_Shift_Seq (Complement A)) . n by PROB_1:12;

A28: (Intersect_Shift_Seq (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

hence
ex n being Nat st
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 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: verum

end;assume A29: n <= k ; :: thesis: not x in A . k

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: verum

for k being Nat st k >= n holds

not x in A . k ; :: thesis: verum

for k being Nat st k >= n holds

not x in A . k ; :: thesis: x in Union (Intersect_Shift_Seq (Complement A))

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 (Complement A) . k

proof

for s being Nat holds x in ((Complement A) ^\ n) . s
let k be Nat; :: thesis: ( n <= k implies x in (Complement A) . k )

assume A34: n <= k ; :: thesis: x in (Complement A) . k

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: verum

end;assume A34: n <= k ; :: thesis: x in (Complement A) . k

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: verum

proof

then
x in Intersection ((Complement A) ^\ n)
by PROB_1:13;
let s be Nat; :: thesis: x in ((Complement A) ^\ n) . s

( 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: verum

end;( 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: verum

then x in (Intersect_Shift_Seq (Complement A)) . n by Def9;

hence x in Union (Intersect_Shift_Seq (Complement A)) by PROB_1:12; :: thesis: verum

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 (Union_Shift_Seq 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 (Union_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq 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 (Intersect_Shift_Seq (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: verum