In [1]:

```
import proveit
from proveit import Lambda
from proveit import k, q, x, y, A, B, P, S, Py, Qy
# SOME STUFF COMMENTED OUT TEMPORARILY TO ALLOW COMPILATION AFTER MASTER MERGED
# INTO THE CRAFT_EDITS_CONTAINMENT_DEMOS BRANCH WHICH ALSO REMOVED THE
# COMPREHENSION THEOREMS
# from proveit.logic import iter_q1k
from proveit.logic.sets.inclusion import proper_subset_def, subset_eq_def
from proveit.numbers import one, zero, Less, greater, Rational, RationalPos
from proveit.numbers.number_sets.rational_numbers import rationals_def, rationals_pos_def
# from proveit.logic.sets.comprehension import comprehension_is_subset
theory = proveit.Theory() # the theorem's theory
```

In [2]:

```
%proving rational_pos_within_rational
```

In [3]:

```
proper_subset_def
```

In [4]:

```
subset_def_spec = proper_subset_def.instantiate({A:RationalPos, B:Rational})
```

In [5]:

```
subset_eq_def
```

In [6]:

```
subset_eq_def_spec = subset_eq_def.instantiate({A:RationalPos, B:Rational})
```

In [7]:

```
rationals_pos_def
```

In [8]:

```
rationals_pos_def_r_h_s = rationals_pos_def.rhs
```

In [9]:

```
# comprehension_is_subset
```

In [10]:

```
# comprehension_is_subset_spec = comprehension_is_subset.instantiate(
# {k:one, S:Rational, QQ:[Lambda(q, greater(q, zero))]}, relabel_map={y:q})
```

In [11]:

```
# rationals_pos_def.sub_left_side_into(comprehension_is_subset_spec)
```

In [12]:

```
# %qed
```

These web pages were generated on 2023-08-23 by Prove-It Beta Version 0.3, licensed under the GNU Public License by Sandia Corporation.

Presented proofs are not absolutely guaranteed. For assurance, it is important to check the structure of the statement being proven, independently verify the derivation steps, track dependencies, and ensure that employed axioms are valid and properly structured. Inconsistencies may exist, unknowingly, in this system.

This material is based upon work supported by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, under the Quantum Computing Application Teams program. Sandia National Labs is managed and operated by National Technology and Engineering Solutions of Sandia, LLC, a subsidiary of Honeywell International, Inc., for the U.S. Dept. of Energy's NNSA under contract DE-NA0003525. The views expressed above do not necessarily represent the views of the DOE or the U.S. Government.

Please send questions/comments to: wwitzel@sandia.gov.