lem:separation in its literal set-theoretic form. Direct-sum background is expanded using rank partitions; the source cocircuit criterion is not audited.

theorem TutteFormalization.decomposable_iff_separation {α : Type u_1} {M : Matroid α} [M.Finite] {F : Set α} (hF : M.IsFlat F) : ¬Indecomposable M F ↔ ∃ (X₁ : Set α) (X₂ : Set α), F = X₁ ∩ X₂ ∧ X₁ ∪ X₂ = M.E ∧ X₁ ≠ F ∧ X₂ ≠ F ∧ ∀ (H : Set α), IsHyperplane M H → F ⊆ H → X₁ ⊆ H ∨ X₂ ⊆ H