theorem :: SETLIM_1:62

for X being set
for B being SetSequence of X st B is V55() holds
lim_inf B = Intersection B by Th53;