theorem Th7: :: SETLIM_1:7

for x being object
for X being set
for B being SetSequence of X holds
( x in meet (rng B) iff for n being Nat holds x in B . n )