[STATEMENT]
lemma SPRAY_event:
  "SPRAY x \<noteq> {} \<Longrightarrow> x \<in> \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPRAY x \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
proof (unfold SPRAY_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {R \<in> \<P>. x \<in> R} \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
assume nonempty_SPRAY: "{R \<in> \<P>. x \<in> R} \<noteq> {}"
[PROOF STATE]
proof (state)
this:
{R \<in> \<P>. x \<in> R} \<noteq> {}

goal (1 subgoal):
 1. {R \<in> \<P>. x \<in> R} \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{R \<in> \<P>. x \<in> R} \<noteq> {}
[PROOF STEP]
have x_in_path_R: "\<exists>R \<in> \<P>. x \<in> R"
[PROOF STATE]
proof (prove)
using this:
{R \<in> \<P>. x \<in> R} \<noteq> {}

goal (1 subgoal):
 1. \<exists>R\<in>\<P>. x \<in> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>R\<in>\<P>. x \<in> R

goal (1 subgoal):
 1. {R \<in> \<P>. x \<in> R} \<noteq> {} \<Longrightarrow> x \<in> \<E>
[PROOF STEP]
thus "x \<in> \<E>"
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<in>\<P>. x \<in> R

goal (1 subgoal):
 1. x \<in> \<E>
[PROOF STEP]
using in_path_event
[PROOF STATE]
proof (prove)
using this:
\<exists>R\<in>\<P>. x \<in> R
\<lbrakk>?Q \<in> \<P>; ?a \<in> ?Q\<rbrakk> \<Longrightarrow> ?a \<in> \<E>

goal (1 subgoal):
 1. x \<in> \<E>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> \<E>

goal:
No subgoals!
[PROOF STEP]
qed