let x be object ; :: thesis:
let X be set ; :: thesis:
let B be SetSequence of X; :: thesis:
A1: dom B = NAT by FUNCT_2:def 1;

A2: now :: thesis:

let x be object ; :: thesis:
assume A3: for n being Nat holds x in B . n ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume Y in rng B ; :: thesis:
then consider n being object such that
A4: n in NAT and
A5: Y = B . n by A1, FUNCT_1:def 3;
thus x in Y by A3, A4, A5; :: thesis:

end;

hence x in meet (rng B) by SETFAM_1:def 1; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A6: x in meet (rng B) ; :: thesis:

now :: thesis:

let k be Nat; :: thesis:
k in NAT by ORDINAL1:def 12;
then B . k in rng B by FUNCT_2:4;
hence x in B . k by A6, SETFAM_1:def 1; :: thesis:

end;

hence for n being Nat holds x in B . n ; :: thesis:

end;

hence ( x in meet (rng B) iff for n being Nat holds x in B . n ) by A2; :: thesis: