lim_sup A = @Intersection (superior_setsequence A) ;
hence lim_sup A is Event of Sigma ; :: thesis: verum