for X being set
for A being Subset of X
for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C