[STATEMENT]
lemma i_set_i_set0_mem_conv: "(I \<in> i_set) = (I \<in> i_set0 \<and> I \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<in> i_set) = (I \<in> i_set0 \<and> I \<noteq> {})
[PROOF STEP]
apply (insert i_set_imp_not_empty[of I])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<in> i_set \<Longrightarrow> I \<noteq> {}) \<Longrightarrow> (I \<in> i_set) = (I \<in> i_set0 \<and> I \<noteq> {})
[PROOF STEP]
apply (fastforce simp: i_set0_i_set_mem_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done