:: deftheorem defines @lim_sup BOR_CANT:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds @lim_sup A = lim_sup A;