for X being set

for A being SetSequence of X ex S being SetSequence of X st

for n being Nat holds S . n = Intersection (A ^\ n)_{1} being SetSequence of X st

for n being Nat holds b_{1} . n = Intersection (A ^\ n)
; :: thesis: verum

for A being SetSequence of X ex S being SetSequence of X st

for n being Nat holds S . n = Intersection (A ^\ n)

proof

hence
ex b
let X be set ; :: thesis: for A being SetSequence of X ex S being SetSequence of X st

for n being Nat holds S . n = Intersection (A ^\ n)

let A be SetSequence of X; :: thesis: ex S being SetSequence of X st

for n being Nat holds S . n = Intersection (A ^\ n)

A1: ex J being SetSequence of X st

( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) )

A5: ( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) ) by A1;

A6: ( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) implies for n being Nat holds J . n = Intersection (A ^\ n) )

thus for n being Nat holds J . n = Intersection (A ^\ n) by A5, A6; :: thesis: verum

end;for n being Nat holds S . n = Intersection (A ^\ n)

let A be SetSequence of X; :: thesis: ex S being SetSequence of X st

for n being Nat holds S . n = Intersection (A ^\ n)

A1: ex J being SetSequence of X st

( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) )

proof

consider J being SetSequence of X such that
defpred S_{1}[ set , set , set ] means for x, y being Subset of X

for k being Nat st k = $1 & x = $2 & y = $3 holds

y = Intersection (A ^\ (k + 1));

A2: for n being Nat

for x being Subset of X ex y being Subset of X st S_{1}[n,x,y]

A3: J . 0 = Intersection (A ^\ 0) and

A4: for n being Nat holds S_{1}[n,J . n,J . (n + 1)]
from RECDEF_1:sch 2(A2);

take J ; :: thesis: ( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) )

thus J . 0 = Intersection (A ^\ 0) by A3; :: thesis: for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1))

let n be Nat; :: thesis: J . (n + 1) = Intersection (A ^\ (n + 1))

reconsider nn = n, nn1 = n + 1 as Element of NAT by ORDINAL1:def 12;

S_{1}[n,J . nn,J . nn1]
by A4;

hence J . (n + 1) = Intersection (A ^\ (n + 1)) ; :: thesis: verum

end;for k being Nat st k = $1 & x = $2 & y = $3 holds

y = Intersection (A ^\ (k + 1));

A2: for n being Nat

for x being Subset of X ex y being Subset of X st S

proof

consider J being SetSequence of X such that
let n be Nat; :: thesis: for x being Subset of X ex y being Subset of X st S_{1}[n,x,y]

let x be Subset of X; :: thesis: ex y being Subset of X st S_{1}[n,x,y]

take y = Intersection (A ^\ (n + 1)); :: thesis: S_{1}[n,x,y]

thus S_{1}[n,x,y]
; :: thesis: verum

end;let x be Subset of X; :: thesis: ex y being Subset of X st S

take y = Intersection (A ^\ (n + 1)); :: thesis: S

thus S

A3: J . 0 = Intersection (A ^\ 0) and

A4: for n being Nat holds S

take J ; :: thesis: ( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) )

thus J . 0 = Intersection (A ^\ 0) by A3; :: thesis: for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1))

let n be Nat; :: thesis: J . (n + 1) = Intersection (A ^\ (n + 1))

reconsider nn = n, nn1 = n + 1 as Element of NAT by ORDINAL1:def 12;

S

hence J . (n + 1) = Intersection (A ^\ (n + 1)) ; :: thesis: verum

A5: ( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) ) by A1;

A6: ( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) implies for n being Nat holds J . n = Intersection (A ^\ n) )

proof

take
J
; :: thesis: for n being Nat holds J . n = Intersection (A ^\ n)
assume A7:
( J . 0 = Intersection (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Intersection (A ^\ (n + 1)) ) )
; :: thesis: for n being Nat holds J . n = Intersection (A ^\ n)

let n be Nat; :: thesis: J . n = Intersection (A ^\ n)

end;let n be Nat; :: thesis: J . n = Intersection (A ^\ n)

per cases
( n = 0 or ex q being Nat st n = q + 1 )
by NAT_1:6;

end;

suppose
ex q being Nat st n = q + 1
; :: thesis: J . n = Intersection (A ^\ n)

then consider q being Nat such that

A8: n = q + 1 ;

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

J . (q + 1) = Intersection (A ^\ (q + 1)) by A7;

hence J . n = Intersection (A ^\ n) by A8; :: thesis: verum

end;A8: n = q + 1 ;

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

J . (q + 1) = Intersection (A ^\ (q + 1)) by A7;

hence J . n = Intersection (A ^\ n) by A8; :: thesis: verum

thus for n being Nat holds J . n = Intersection (A ^\ n) by A5, A6; :: thesis: verum

for n being Nat holds b