:: deftheorem defines lim_sup SETLIM_1:def 5 :
for X being set
for B being SetSequence of X holds lim_sup B = Intersection (superior_setsequence B);