let X be set ; :: thesis:
let B be SetSequence of X; :: thesis:
let f be Function; :: thesis:
assume that
A1: dom f = NAT and
A2: for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ; :: thesis:
rng f c= bool X

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng f ; :: thesis:
then consider x being object such that
A3: x in dom f and
A4: z = f . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A1, A3;
set Y = { (B . k) where k is Nat : n <= k } ;
set y = meet { (B . k) where k is Nat : n <= k } ;
A5: meet { (B . k) where k is Nat : n <= k } is Subset of X

per cases ) where k is Nat : n <= k } <> {} or { (B . k) where k is Nat : n <= k } = {} ) ;

then consider Z1 being object such that
A6: Z1 in { (B . k) where k is Nat : n <= k } by XBOOLE_0:def 1;
reconsider Z1 = Z1 as set by TARSKI:1;
consider k1 being Nat such that
A7: ( Z1 = B . k1 & n <= k1 ) by A6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

let x be object ; :: thesis:
assume x in meet { (B . k) where k is Nat : n <= k } ; :: thesis:
then x in Z1 by A6, SETFAM_1:def 1;
then x in B . k1 by A7;
hence x in X ; :: thesis:

end;

hence meet { (B . k) where k is Nat : n <= k } is Subset of X by TARSKI:def 3; :: thesis:

end;

suppose { (B . k) where k is Nat : n <= k } = {} ; :: thesis:

then meet { (B . k) where k is Nat : n <= k } = {} by SETFAM_1:def 1;
hence meet { (B . k) where k is Nat : n <= k } is Subset of X by XBOOLE_1:2; :: thesis:

end;

z = meet { (B . k) where k is Nat : n <= k } by A2, A4;
hence z in bool X by A5; :: thesis:

end;