In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Card, EmptySet, Equals, Union, Set, InSet, NotInSet, Forall
from proveit.numbers import num, Add, Natural
from proveit import x, S
%begin axioms
```

**The cardinality of the empty set, $\emptyset$, is zero (the base case of an induction for the cardinality of finite sets):**

In [2]:

```
empty_card = Equals(Card(EmptySet), num(0))
```

**When a new element is added to a finite set, its cardinality increases by one (the induction rule for the cardinality of finite sets):**

In [3]:

```
card_induction = Forall((x, S), Equals(Card(Union(S, Set(x))),
Add(Card(S), num(1))), conditions=[InSet(Card(S), Natural), NotInSet(x, S)])
```

**The cardinality of inifite sets should be defined via 1-to-1 and onto mappings between them.**

In [ ]:

```
```

In [4]:

```
%end axioms
```