reconsider E = {} as Event of Sigma by Th4;
let P be Probability of Sigma; :: thesis: P is zeroed
A1: ( {} misses [#] Sigma & {} \/ ([#] Sigma) = [#] Sigma ) by XBOOLE_1:65;
1 = P . ([#] Sigma) by Def8;
then 1 = (P . E) + 1 by A1, Def8;
hence P . {} = 0 ; :: according to VALUED_0:def 19 :: thesis: verum