```
(def-constant set%prec
"lambda(a,b:sets[ind_1], a subseteq b)"
(theory generic-theory-1))

```

```(def-theorem ()
"forall(a,c:sets[ind_1],
forsome(b:sets[ind_1],a set%prec b and b set%prec c)
implies
a set%prec c)"
(theory generic-theory-1)
(proof
(

unfold-defined-constants
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-transitivity)
auto-instantiate-existential
)))
```

```(def-theorem ()
"forall(a:sets[ind_1],a set%prec a)"
(theory generic-theory-1)
(proof
(
(unfold-single-defined-constant (0) set%prec)
)))
```

```(def-theorem ()
"forall(a,b:sets[ind_1],
a set%prec b and b set%prec a implies a=b)"
(theory generic-theory-1)
(proof
(
unfold-defined-constants
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
)))
```

```(def-theorem ()
"forall(p:[sets[ind_1],prop],
nonvacuous_q{p}
and
forsome(alpha:sets[ind_1],
forall(theta:sets[ind_1],
p(theta) implies theta set%prec alpha))
implies
forsome(gamma:sets[ind_1],
forall(theta:sets[ind_1],
p(theta) implies theta set%prec gamma)
and
forall(gamma_1:sets[ind_1],
forall(theta:sets[ind_1],
p(theta) implies theta set%prec gamma_1)
implies
gamma set%prec gamma_1)))"
(theory generic-theory-1)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-existential ("indic{x:ind_1, forsome(b:sets[ind_1], p(b) and x in b)}"))
simplify-insistently
direct-and-antecedent-inference-strategy
auto-instantiate-existential
simplify-insistently
)))
```

```
(def-translation complete-partial-order-to-generic-theory-1
(source complete-partial-order)
(target generic-theory-1)
(fixed-theories h-o-real-arithmetic)
(constant-pairs
(prec set%prec))
(sort-pairs (uu "sets[ind_1]"))
(theory-interpretation-check using-simplification))
```

```(def-transported-symbols monotone
(translation complete-partial-order-to-generic-theory-1)
(renamer cpo-gt-renamer)
)

```

```(def-overloading monotone
(complete-partial-order monotone)
(generic-theory-1  gt%monotone))
```

```
(def-theorem monotonicity-of-sb-functional
"forall(f:[ind_2,ind_1],g:[ind_1,ind_2],
monotone(lambda(x:sets[ind_1],image(f,image(g,x)^^)^^)))"
(theory generic-theory-2)
lemma
(proof
(
(unfold-single-defined-constant-globally gt%monotone)
(unfold-single-defined-constant-globally set%prec)
simplify-insistently
(prove-by-logic-and-simplification 3)
)))
```