rng ASeq c= Sigma by RELAT_1:def 19;
hence Intersection ASeq is Event of Sigma by PROB_1:def 6; :: thesis: verum