let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F holds (C_Meas M) . {} = 0
let F be Field_Subset of X; :: thesis: for M being Measure of F holds (C_Meas M) . {} = 0
let M be Measure of F; :: thesis: (C_Meas M) . {} = 0
(C_Meas M) . {} <= M . {} by Th9, PROB_1:4;
then A1: (C_Meas M) . {} <= 0 by VALUED_0:def 19;
{} X in bool X ;
then {} in dom (C_Meas M) by FUNCT_2:def 1;
then A2: (C_Meas M) . {} in rng (C_Meas M) by FUNCT_1:3;
C_Meas M is nonnegative by Th10;
then rng (C_Meas M) is nonnegative ;
hence (C_Meas M) . {} = 0. by A1, A2; :: thesis: verum