no goals
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator ⊤ = ⊥
rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]