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

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