let X, x be set ; :: thesis: for B being SetSequence of X holds
( x in meet (rng B) iff for n being Element of NAT holds x in B . n )
let B be SetSequence of X; :: thesis: ( x in meet (rng B) iff for n being Element of NAT holds x in B . n )
B: dom B = NAT by FUNCT_2:def 1;

A00: now

let x be set ; :: thesis: ( x in meet (rng B) implies for n being Element of NAT holds x in B . n )
assume AA0: x in meet (rng B) ; :: thesis: for n being Element of NAT holds x in B . n

now

let k be Element of NAT ; :: thesis: x in B . k
B . k in rng B by FUNCT_2:6;
hence x in B . k by AA0, SETFAM_1:def 1; :: thesis: verum

end;

hence for n being Element of NAT holds x in B . n ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( for n being Element of NAT holds x in B . n ) implies x in meet (rng B) )
assume AA0: for n being Element of NAT holds x in B . n ; :: thesis: x in meet (rng B)

now

let Y be set ; :: thesis: ( Y in rng B implies x in Y )
assume Y in rng B ; :: thesis: x in Y
then consider n being set such that
AA2: ( n in NAT & Y = B . n ) by B, FUNCT_1:def 5;
reconsider n = n as Element of NAT by AA2;
thus x in Y by AA0, AA2; :: thesis: verum

end;

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

end;

hence ( x in meet (rng B) iff for n being Element of NAT holds x in B . n ) by A00; :: thesis: verum