Definition nat_eq

Definition. nat_eq
ℕ = ⋂{A | A ⊆ ℝ ∧ 0 ∈ A ∧ ∀n. n ∈ A → n + 1 ∈ A}

The natural numbers, defined as the smallest subset of the real numbers that contains zero and is closed with respect to the successor operation.