[STATEMENT]
lemma (in ring) genideal_minimal:
  assumes "ideal I R" "S \<subseteq> I"
  shows "Idl S \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Idl S \<subseteq> I
[PROOF STEP]
unfolding genideal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter> {I. ideal I R \<and> S \<subseteq> I} \<subseteq> I
[PROOF STEP]
by rule (elim InterD, simp add: assms)