. intros h
  apply ext
  intros s
  apply Iff.intro
  . intros _; exact True.intro
  . intros _; exact superset_mem h (Set.empty_subset _)
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥

case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f