obtain ⟨w, hw⟩ := exists_mem_nempty G hA
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
⊢ ¬CliqueFreeSet A 2
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬CliqueFreeSet A 2