apply Iff.intro
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b ↔ as_filter b = as_filter c
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c

case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b