:: deftheorem defines disjoint_valued PROB_2:def 3 :
for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma holds
( ASeq is disjoint_valued iff for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n );