[STATEMENT]
lemma iffd_iffb_demorgan: "Sup_pres \<phi> \<Longrightarrow> fd\<^sup>-\<^sub>\<F> \<phi> = (fb\<^sup>-\<^sub>\<F> \<circ> \<partial>\<^sub>F) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_pres \<phi> \<Longrightarrow> fd\<^sup>-\<^sub>\<F> \<phi> = (fb\<^sup>-\<^sub>\<F> \<circ> \<partial>\<^sub>F) \<phi>
[PROOF STEP]
by (smt Sup_pres_Inf_pres comp_apply iffb_ifbd_dual iffd_def map_dual_dual)