let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds {} is thin of P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds {} is thin of P
let P be Probability of Sigma; :: thesis: {} is thin of P
( P . {} = 0 & {} in Sigma ) by PROB_1:4, VALUED_0:def 19;
hence {} is thin of P by Def4; :: thesis: verum