[STATEMENT]
lemma ample_subset:
      assumes "ample_set q A"
      shows "A \<subseteq> {a. en a q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> {a. en a q}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ample_set q A

goal (1 subgoal):
 1. A \<subseteq> {a. en a q}
[PROOF STEP]
unfolding ample_set_def
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> {a. en a q} \<and> (A \<subset> {a. en a q} \<longrightarrow> A \<noteq> {}) \<and> (\<forall>a. A \<subset> {a. en a q} \<longrightarrow> a \<in> A \<longrightarrow> src (ex a q) q) \<and> (A \<subset> {a. en a q} \<longrightarrow> A \<subseteq> invisible) \<and> (\<forall>w. A \<subset> {a. en a q} \<longrightarrow> path w q \<longrightarrow> A \<inter> set w = {} \<longrightarrow> Ind A (set w))

goal (1 subgoal):
 1. A \<subseteq> {a. en a q}
[PROOF STEP]
by auto