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 SetNotEquiv, SubsetEq, NotSubsetEq, ProperSubset, NotProperSubset
from proveit.logic import Forall, Equals, And, InSet, Not
from proveit import A, B, x
%begin axioms
```

**$A \subseteq B$ is equivalent to saying that every element in $A$ is also in $B$:**

In [2]:

```
subset_eq_def = Forall((A, B), Equals(SubsetEq(A, B), Forall(x, InSet(x, B), domain=A)))
```

**Define $A \nsubseteq B$ as $\lnot (A \subseteq B)$:**

In [3]:

```
not_subset_eq_def = Forall((A, B), Equals(NotSubsetEq(A, B), Not(SubsetEq(A, B))))
```

**$A$ is a proper subset of $B$, $A \subset B$, means that $A \subseteq B$ but $B \nsubseteq A$; that is, every element in $A$ is also in $B$ but not the other way around (i.e. there are elements in $B$ that are not in $A$):**

In [4]:

```
proper_subset_def = Forall((A, B), Equals(ProperSubset(A, B), And(SubsetEq(A, B), SetNotEquiv(B, A))))
```

In [5]:

```
not_proper_subset_def = Forall((A, B), Equals(NotProperSubset(A, B), Not(ProperSubset(A, B))))
```

In [6]:

```
%end axioms
```