apply Iff.intro
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f ↔ s ∈ ⊥
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥

case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f