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 import a, b, r, x
from proveit.logic import And, Equals, Forall, InSet, SetOfAll
from proveit.numbers import greater, Less, LessEq, number_ordering
from proveit.numbers import (zero, IntervalOO, IntervalCO, IntervalOC,
IntervalCC, Real, RealPos)
```

In [2]:

```
%begin axioms
```

In [3]:

```
real_pos_def = Equals(RealPos,
SetOfAll(r, r, conditions=[greater(r, zero)],
domain=Real))
```

**Being in a real interval means being real and being bound appropriately between the lower and upper bounds of the interval, and we define this for each of the 4 possible types of (finite) real intervals:**

In [4]:

```
in_IntervalOO_def = Forall((a, b),
Forall(x,
Equals(InSet(x, IntervalOO(a, b)),
And(InSet(x, Real),
number_ordering(Less(a, x), Less(x, b))))),
domain=Real)
```

In [5]:

```
in_IntervalOC_def = \
Forall((a, b),
Forall(x,
Equals(InSet(x, IntervalOC(a, b)),
And(InSet(x, Real),
number_ordering(Less(a, x), LessEq(x, b))))),
domain=Real)
```

In [6]:

```
in_IntervalCO_def = \
Forall((a, b),
Forall(x,
Equals(InSet(x, IntervalCO(a, b)),
And(InSet(x, Real),
number_ordering(LessEq(a, x), Less(x, b))))),
domain=Real)
```

In [7]:

```
in_IntervalCC_def = \
Forall((a, b),
Forall(x,
Equals(InSet(x, IntervalCC(a, b)),
And(InSet(x, Real),
number_ordering(LessEq(a, x), LessEq(x, b))))),
domain=Real)
```

In [8]:

```
%end axioms
```