theorem :: SETLIM_1:54

for X being set
for B being SetSequence of X holds Intersection B c= lim_inf B