let X be set ; for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Nat holds meet { (B . k) where k is Nat : n <= k } = A
let A be Subset of X; for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Nat holds meet { (B . k) where k is Nat : n <= k } = A
let B be SetSequence of X; ( B is constant & the_value_of B = A implies for n being Nat holds meet { (B . k) where k is Nat : n <= k } = A )
assume A1:
( B is constant & the_value_of B = A )
; for n being Nat holds meet { (B . k) where k is Nat : n <= k } = A
let n be Nat; meet { (B . k) where k is Nat : n <= k } = A
set Y = { (B . k) where k is Nat : n <= k } ;
A2:
now for x being object st x in { (B . k) where k is Nat : n <= k } holds
x = Alet x be
object ;
( x in { (B . k) where k is Nat : n <= k } implies x = A )assume
x in { (B . k) where k is Nat : n <= k }
;
x = Athen
ex
k being
Nat st
(
x = B . k &
n <= k )
;
hence
x = A
by A1, Lm2;
verum end;
{ (B . k) where k is Nat : n <= k } <> {}
by Th1;
then
{ (B . k) where k is Nat : n <= k } = {A}
by A2, ZFMISC_1:35;
hence
meet { (B . k) where k is Nat : n <= k } = A
by SETFAM_1:10; verum