rw [← sInter_pair]
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ F ∩ F' ∈ C
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ ⋂₀ {F, F'} ∈ C