theorem :: SETLIM_1:59

for X being set
for B being SetSequence of X st B is V56() holds
lim_sup B = Union B by Th43;