Theorem: Matroid.Modular_pair_comm (Matroid/Old/ModularCut.lean)

State before:
α✝ : Type u_1
M : Matroid α✝
X Y : Set α✝
h : M.Modular_pair X Y
⊢ M.Modular_pair Y X
Tactic:
obtain ⟨B, B_Base, B_modular⟩ := h
State after:
no goals