In [1]:

```
from proveit.logic import Forall, NotInSet, EmptySet
from proveit._common_ import x
%begin theorems
```

**Nothing is in the empty set (everything is not in the empty set):**

In [2]:

```
allNotInEmpty = Forall(x, NotInSet(x, EmptySet))
```

Out[2]:

In [3]:

```
%end theorems
```