[STATEMENT]
lemma ID_inf: "Der_inf \<phi> \<Longrightarrow> Int_inf(\<I>\<^sub>D \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Der_inf \<phi> \<Longrightarrow> Int_inf (\<I>\<^sub>D \<phi>)
[PROOF STEP]
by (simp add: CD_inf dual_der2 iADDI_MULT_dual1)