User:Dfeuer/Zero is Natural Number

Theorem

User:Dfeuer/Definition:Zero is a User:Dfeuer/Definition:Natural Number.

Proof

By the definition of zero, $0 = \varnothing$.

Let $a$ be any User:Dfeuer/Definition:Inductive Set.

Then by the definition of inductive set, $0 \in a$.

Since this holds for every inductive set $a$, $0$ is a natural number.

$\blacksquare$