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 Forall, Equals, And, InSet, NotInSet, Difference
from proveit import A, B, x
%begin axioms
```

** The difference of two sets includes all of the members of the minuend (first operand) except those contained in the subtrahend (second operand):**

In [2]:

```
difference_def = Forall((x, A, B), Equals(InSet(x, Difference(A, B)),
And(InSet(x, A), NotInSet(x, B))))
```

In [3]:

```
%end axioms
```