[STATEMENT]
lemma (in finite_measure) finite_measure_Diff:
  assumes sets: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
  shows "measure M (A - B) = measure M A - measure M B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure M (A - B) = Sigma_Algebra.measure M A - Sigma_Algebra.measure M B
[PROOF STEP]
using measure_Diff[OF _ assms]
[PROOF STATE]
proof (prove)
using this:
emeasure M A \<noteq> \<infinity> \<Longrightarrow> Sigma_Algebra.measure M (A - B) = Sigma_Algebra.measure M A - Sigma_Algebra.measure M B

goal (1 subgoal):
 1. Sigma_Algebra.measure M (A - B) = Sigma_Algebra.measure M A - Sigma_Algebra.measure M B
[PROOF STEP]
by simp