rw [Ne, eq_comm, ModularCut.eq_top_iff]
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ ⊤ ≠ ⊥
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ M.cl ∅ ∉ ⊥