True ↔ ∀ (V : Type) (G : SimpleGraph V) (A B : Set V), Disjoint A B → G.IsIndepSet A → G.IsIndepSet B → ∃ ι a b p S, (∀ (i : ι), a i ∈ A) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧ S ⊆ {v | ∃ i, v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S