let X be set ; :: thesis: for A being Subset of X

for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Intersection B = A

let A be Subset of X; :: thesis: for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Intersection B = A

let B be SetSequence of X; :: thesis: ( ( for n being Nat holds B . n = A ) implies Intersection B = A )

assume A1: for n being Nat holds B . n = A ; :: thesis: Intersection B = A

then meet (rng B) = A by SETFAM_1:10;

hence Intersection B = A by Th8; :: thesis: verum

for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Intersection B = A

let A be Subset of X; :: thesis: for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Intersection B = A

let B be SetSequence of X; :: thesis: ( ( for n being Nat holds B . n = A ) implies Intersection B = A )

assume A1: for n being Nat holds B . n = A ; :: thesis: Intersection B = A

now :: thesis: for x being object st x in rng B holds

x = A

then
rng B = {A}
by ZFMISC_1:35;x = A

let x be object ; :: thesis: ( x in rng B implies x = A )

assume x in rng B ; :: thesis: x = A

then ex n being Nat st x = B . n by Th4;

hence x = A by A1; :: thesis: verum

end;assume x in rng B ; :: thesis: x = A

then ex n being Nat st x = B . n by Th4;

hence x = A by A1; :: thesis: verum

then meet (rng B) = A by SETFAM_1:10;

hence Intersection B = A by Th8; :: thesis: verum