∀ {α : Type u_1} {G : SimpleGraph α} {x v w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α]
  [inst_1 : DecidableRel G.Adj] (a b c : α),
  a ∈ insert w₁ s →
    ¬G.Adj x a →
      b ∈ insert w₂ t →
        ¬G.Adj x b →
          c ∈ insert v s →
            ¬G.Adj x c →
              a ≠ b →
                b ≠ c →
                  a ∉ t →
                    b ∉ s →
                      ¬a = c →
                        a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
                          b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
                            c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ ¬a = b ∧ ¬a = c ∧ ¬b = c