* see dependencies *

In [1]:

```
import proveit
from proveit import A, B
from proveit.logic.sets.inclusion import subset_eq_def
%proving unfold_subset_eq
```

In [2]:

```
subset_eq_def
```

In [3]:

```
SubsetEqDef_inst = subset_eq_def.instantiate()
```

In [4]:

```
SubsetEqDef_inst.derive_right_via_equality(assumptions=[SubsetEqDef_inst.lhs])
```

In [5]:

```
%qed
```

Out[5]: