let X be set ; :: thesis: 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 Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A
let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A
let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A )
assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A
let n be Element of NAT ; :: thesis: meet { (B . k) where k is Element of NAT : n <= k } = A
set Y = { (B . k) where k is Element of NAT : n <= k } ;

A2: now

let x be set ; :: thesis: ( x in { (B . k) where k is Element of NAT : n <= k } implies x = A )
assume x in { (B . k) where k is Element of NAT : n <= k } ; :: thesis: x = A
then ex k being Element of NAT st
( x = B . k & n <= k ) ;
hence x = A by A1, Lm2; :: thesis: verum

end;

{ (B . k) where k is Element of NAT : n <= k } <> {} by Th1;
then { (B . k) where k is Element of NAT : n <= k } = {A} by A2, ZFMISC_1:35;
hence meet { (B . k) where k is Element of NAT : n <= k } = A by SETFAM_1:10; :: thesis: verum