for X being set
for F being SetSequence of X holds meet F c= lim_inf F