:: deftheorem defines @Intersection PROB_2:def 1 :
for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma holds @Intersection ASeq = Intersection ASeq;