theorem Th8: :: SETLIM_1:8

for X being set
for B being SetSequence of X holds Intersection B = meet (rng B)