theorem :: SETLIM_1:61

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