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