simp only [Ne, ModularCut.eq_top_iff, ModularCut.mem_principal_iff, cl_flat, true_and]
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ModularCut.principal M M.E ≠ ⊤
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ¬M.E ⊆ M.cl ∅