intro hn
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ (∀ (y : V), Inductive y → n ∈ y) → n ∈ Infinity.inductiveSet
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (y : V), Inductive y → n ∈ y
⊢ n ∈ Infinity.inductiveSet