let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A being thin of M holds A in COM (S,M)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A being thin of M holds A in COM (S,M)
let M be sigma_Measure of S; :: thesis: for A being thin of M holds A in COM (S,M)
let A be thin of M; :: thesis: A in COM (S,M)
reconsider B = {} as Element of S by MEASURE1:7;
B \/ A in COM (S,M) by MEASURE3:def 3;
hence A in COM (S,M) ; :: thesis: verum