rng ASeq c= Sigma by PROB_1:def 9;
then Intersection ASeq in Sigma by PROB_1:def 8;
hence Intersection ASeq is Event of Sigma ; :: thesis: verum