ax-succ-succ - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-succ-succ

Axiom ax-succ-succ 488

Description: Successors of natural numbers are also natural numbers, and each natural number has exactly one successor. This is equivalent to Robinson axiom 2 and, as such, should be provable from ax-baihei-inj 473

**Assertion**
Ref	Expression
ax-succ-succ	⊢ ganai ko'a .e ko'e kacli'e ko'i gi ko'a du ko'e

This axiom is referenced by: succ-succi 489

W3C validator