```(def-theorem ()
"<= = lambda(a,b:rr,a<=b)"
(theory h-o-real-arithmetic)
(proof
(
extensionality
simplify
)))
```

```(def-theorem ()
"forall(a,c:rr,forsome(b:rr,b<=a and c<=b) implies c<=a)"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
simplify
)))
```

```(def-theorem ()
"forall(p:[rr,prop],
nonvacuous_q{p}
and
forsome(alpha:rr,
forall(theta:rr,p(theta) implies alpha<=theta))
implies
forsome(gamma:rr,
forall(theta:rr,p(theta) implies gamma<=theta)
and
forall(gamma_1:rr,
forall(theta:rr,p(theta) implies gamma_1<=theta)
implies
gamma_1<=gamma)))"
(theory h-o-real-arithmetic)
lemma
(proof
(
(apply-macete-with-minor-premises tr%unfolded-completeness-from-below-condition)
)))
```

```
(def-translation complete-partial-order-to-h-o-real-arithmetic-reverse
(source complete-partial-order)
(target h-o-real-arithmetic)
(fixed-theories h-o-real-arithmetic)
(constant-pairs
(prec ">=")
(prec%sup inf)
(prec%majorizes minorizes)
(rev%prec <=))
(sort-pairs (uu rr))
(theory-interpretation-check using-simplification))

```

```
(def-theorem inf-plus-epsilon
"forall(s:sets[rr],eps:rr,0<eps implies not(inf(s)+eps minorizes s))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(inf(s)) or not(#(inf(s)))")
(antecedent-inference "with(s:sets[rr],#(inf(s)) or not(#(inf(s))));")
(cut-with-single-formula "not(inf(s)>=inf(s)+eps)")
(contrapose "with(eps:rr,s:sets[rr],not(inf(s)>=inf(s)+eps));")
(apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
direct-and-antecedent-inference-strategy
simplify
simplify
simplify)))
```

```
(def-theorem inf-plus-epsilon-corollary
"forall(s:sets[rr],eps:rr, 0<eps and #(inf(s)) implies forsome(x:rr, x in s and x < inf(s)+eps))"

(proof

(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not(inf(s)+eps minorizes s)")
(contrapose "with(eps:rr,s:sets[rr],not(inf(s)+eps minorizes s));")
(unfold-single-defined-constant (0) minorizes)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p,q:prop,forall(x:rr,p or q))" ("x_\$0"))
simplify
(apply-macete-with-minor-premises inf-plus-epsilon)
)
)
(theory h-o-real-arithmetic))
```

```
(def-theorem inf-defined-implies-non-empty
"forall(s:sets[rr],#(inf(s)) implies forsome(x:rr, x in s))"

(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(s:sets[rr],#(inf(s)));")
(cut-with-single-formula "#(inf(s)) implies inf(s)>=inf(s)+1")
(antecedent-inference "with(p,q:prop, p implies q)")
(simplify-antecedent "with(s:sets[rr],inf(s)>=inf(s)+1);")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) minorizes)
direct-and-antecedent-inference-strategy
)))
```

```
(def-theorem discrete-sets-contain-inf
"forall(s:sets[rr], discrete%set(s) and #(inf(s)) implies inf(s) in s)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) discrete%set)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(x:rr, x in s and x<inf(s)+a)")
(antecedent-inference "with(a:rr,s:sets[rr],forsome(x:rr,x in s and x<inf(s)+a));")
(cut-with-single-formula "x=inf(s) or inf(s)<x")
(antecedent-inference "with(s:sets[rr],x:rr,x=inf(s) or inf(s)<x);")
simplify
(cut-with-single-formula "with(x:rr,s:sets[rr],forsome(y:rr,y in s and y<x));")
(antecedent-inference "with(x:rr,s:sets[rr],forsome(y:rr,y in s and y<x));")
(instantiate-universal-antecedent "with(a:rr,forall(x,y:rr,x<y implies a<=y-x));" ("y" "x"))
(cut-with-single-formula "y>=inf(s)")
(simplify-antecedent "with(s:sets[rr],y:rr,y>=inf(s));")
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("y"))
simplify
(force-substitution "x" "inf(s)+(x-inf(s))" (0))
(apply-macete-with-minor-premises inf-plus-epsilon-corollary)
direct-and-antecedent-inference-strategy
simplify
simplify
(cut-with-single-formula "inf(s)<=x")
simplify
(force-substitution "inf(s)<=x" "x>=inf(s)" (0))
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("x"))
simplify
(unfold-single-defined-constant (0) >=)
(apply-macete-with-minor-premises inf-plus-epsilon-corollary)
direct-and-antecedent-inference-strategy
)))
```

```
(def-constant next
"lambda(s:sets[rr],a:rr, inf(indic{x:rr,x in s and a<x}))"
(theory h-o-real-arithmetic))
```

```
(def-theorem next-for-discrete-sets
"forall(s:sets[rr], x:rr, discrete%set(s) and #(next(s,x)) implies next(s,x) in s)"
(proof
(
(unfold-single-defined-constant (0 1) next)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(a,b:sets[rr],inf(a) in a and a subseteq b implies inf(a) in b)")
(backchain "forall(a,b:sets[rr],inf(a) in a and a subseteq b implies inf(a) in b)")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises discrete-sets-contain-inf)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(s:sets[rr],discrete%set(s));")
unfold-defined-constants
simplify-insistently
simplify
))
(theory h-o-real-arithmetic))
```

```
(def-theorem next-definedness-condition
"forall(s:sets[rr], x:rr,  #(next(s,x)) iff forsome(y:rr, y in s and x<y))"

(proof
(
(unfold-single-defined-constant (0) next)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(y:rr, y in indic{x_\$1:rr,  x_\$1 in s and x<x_\$1})")
(antecedent-inference "with(x:rr,s:sets[rr],
nonempty_indic_q{indic{x_\$1:rr,  x_\$1 in s and x<x_\$1}});")
(instantiate-existential ("y"))
(contrapose "with(y,x:rr,s:sets[rr],
y in indic{x_\$1:rr,  x_\$1 in s and x<x_\$1});")
simplify-insistently
(contrapose "with(y,x:rr,s:sets[rr],
y in indic{x_\$1:rr,  x_\$1 in s and x<x_\$1});")
simplify-insistently
(apply-macete-with-minor-premises inf-defined-implies-non-empty)
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
simplify-insistently
auto-instantiate-existential
(instantiate-existential ("x"))
(unfold-single-defined-constant (0) minorizes)
simplify-insistently
))
(theory h-o-real-arithmetic))
```