theorem Th7: :: MEASURE4:7

for A, X being set
for C being C_Measure of X st A in sigma_Field C holds
X \ A in sigma_Field C