obtain ⟨B, _, h2⟩ := h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ∃ t, IsNClique G s t
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U B : Finset α
left✝ : B ⊆ U
h2 : IsNClique G s B
⊢ ∃ t, IsNClique G s t