theorem :: SETLIM_1:56

for X being set
for B being SetSequence of X holds lim_sup B = lim (superior_setsequence B) by Th49;