[STATEMENT]
lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
have "emeasure lborel (cbox a b - box a b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure lborel (cbox a b - box a b) = 0
[PROOF STEP]
by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox)
[PROOF STATE]
proof (state)
this:
emeasure lborel (cbox a b - box a b) = 0

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure lborel (cbox a b - box a b) = 0
[PROOF STEP]
have "cbox a b - box a b \<in> null_sets lborel"
[PROOF STATE]
proof (prove)
using this:
emeasure lborel (cbox a b - box a b) = 0

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
by (auto simp: null_sets_def)
[PROOF STATE]
proof (state)
this:
cbox a b - box a b \<in> null_sets lborel

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cbox a b - box a b \<in> null_sets lborel

goal (1 subgoal):
 1. cbox a b - box a b \<in> null_sets lborel
[PROOF STEP]
by (auto dest!: AE_not_in)
[PROOF STATE]
proof (state)
this:
cbox a b - box a b \<in> null_sets lborel

goal:
No subgoals!
[PROOF STEP]
qed