```
(def-theorem removing-an-element-from-a-finite-set
"forall(s:sets[ind_1], x:ind_1, f_indic_q{s} and x in s implies
f_card{s}=f_card{s diff singleton{x}}+1)"
(usages transportable-macete)
(theory generic-theory-1)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "s" "(s diff singleton{x}) union singleton{x}
" (0))
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%diff-union-equal-whole)
simplify-insistently
(apply-macete-with-minor-premises f-card-disjoint-union)
(apply-macete-with-minor-premises singleton-has-f-card-one-rewrite)
(cut-with-single-formula "#(f_card{s diff singleton{x}})")
simplify
(apply-macete-with-minor-premises subset-of-finite-indic-is-finite)
(instantiate-existential ("s"))
simplify-insistently
(apply-macete-with-minor-premises iota-free-definition-of-f-indic-q)
(apply-macete-with-minor-premises singleton-has-f-card-one-rewrite)
(instantiate-existential ("1"))
(apply-macete-with-minor-premises tr%diff-with-indic-is-disj-from-indic)
)))
```

```
(def-constant maximal
"lambda(x:uu,s:sets[uu], x in s and forall(y:uu, y in s and x prec y implies x=y))"
(theory partial-order))
```

```
(def-theorem finite-sets-have-maximal-elements
"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s}
implies
forsome(x:uu, maximal(x,s)))"
(theory partial-order)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(m:zz, 1<=m and n=m)")
(move-to-sibling 1)
(instantiate-existential ("n"))
(backchain-backwards "with(n:nn,n=n);")
(force-substitution "1" "f_card{singleton{x}}" (0))
(apply-macete-with-minor-premises tr%f-card-leq-iff-finite-and-embeds)
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
direct-and-antecedent-inference-strategy
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%subset-embeds-in-superset)
simplify-insistently
(instantiate-existential ("n"))
(apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite)
(antecedent-inference "with(p:prop,forsome(m:zz,p));")
(incorporate-antecedent "with(n:nn,n=n);")
(backchain "with(p:prop,p and p);")
(antecedent-inference "with(p:prop,p and p);")
(weaken (0))
(weaken (1))
(cut-with-single-formula "forall(s:sets[uu], f_card{s}=m implies forsome(x_\$4:uu,maximal(x_\$4,s)))")
(backchain "with(p:prop,forall(s:sets[uu],p));")
(induction trivial-integer-inductor ("m"))
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%singleton-has-f-card-one)
direct-and-antecedent-inference-strategy
(instantiate-existential ("y"))
(unfold-single-defined-constant (0) maximal)
(backchain "with(p:prop,p);")
(backchain "with(p:prop,p);")
(apply-macete-with-minor-premises tr%singleton-equality-conversion)
simplify
(cut-with-single-formula "forsome(x:uu, x in s)")
(antecedent-inference "with(s:sets[uu],nonempty_indic_q{s});")
(instantiate-universal-antecedent "with(p:prop,forall(s:sets[uu],p));"
("s diff singleton{x}"))
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "f_card{s}=f_card{s diff singleton{x}}+1")
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%removing-an-element-from-a-finite-set)
simplify
(case-split ("x_\$9 prec x"))
(instantiate-existential ("x"))
(unfold-single-defined-constant (0) maximal)
direct-and-antecedent-inference-strategy
(contrapose "with(f:sets[uu],x_\$9:uu,maximal(x_\$9,f));")
(unfold-single-defined-constant (0) maximal)
(contrapose "with(p:prop,not(p));")
(antecedent-inference "with(p:prop,p and p);")
(contrapose "with(p:prop,forall(y_\$0:uu,p));")
(instantiate-existential ("y"))
simplify-insistently
(apply-macete-with-minor-premises prec-transitivity)
auto-instantiate-existential
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises prec-anti-symmetry)
simplify
(instantiate-existential ("x_\$9"))
(incorporate-antecedent "with(f:sets[uu],x_\$9:uu,maximal(x_\$9,f));")
(unfold-single-defined-constant-globally maximal)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(x_\$9:uu,f,s:sets[uu],x_\$9 in s diff f);")
simplify-insistently
simplify
(backchain "with(p:prop,forall(y_\$0:uu,p));")
(cut-with-single-formula "not(x=y)")
(move-to-ancestor 1)
simplify-insistently
(simplify-antecedent "with(y,x_\$9:uu,x_\$9 prec y);")
(apply-macete-with-minor-premises tr%rev%positive-f-card-iff-nonempty)
simplify
)))
```

```(def-transported-symbols (maximal)
(translation order-reverse)
(renamer third-renamer))
```

```
(def-theorem finite-sets-have-minimal-elements
"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s}
implies
forsome(x:uu, minimal(x,s)))"
(theory partial-order)
(usages transportable-macete)
(proof
(

(apply-macete-with-minor-premises tr%finite-sets-have-maximal-elements)
)))
```

```
(def-theory linear-order
(component-theories partial-order)
(axioms
(totality-of-order
"forall(a,b:uu, a prec b or b prec a)")))
```

```
(def-constant maximum
"lambda(x:uu, s:sets[uu], x in s and forall(y:uu, y in s implies y prec x))"
(theory partial-order))
```

```
(def-theorem maximal-is-maximum
"forall(a:uu, s:sets[uu], maximal(a,s) implies maximum(a,s))"
(usages transportable-macete)
(theory linear-order)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(cut-with-single-formula "y prec a or a prec a")
(move-to-ancestor 1)
(cut-with-single-formula "y prec a or a prec y")
(move-to-sibling 1)
(apply-macete-with-minor-premises totality-of-order)
(antecedent-inference "with(p:prop,p or p);")
(instantiate-universal-antecedent "with(p:prop,forall(y:uu,p));" ("y"))
simplify
)))

```

```(def-transported-symbols (maximum)
(translation order-reverse)
(renamer fourth-renamer))
```

```
(def-translation linear-order-reverse
(source linear-order)
(target linear-order)
(core-translation order-reverse)
(theory-interpretation-check using-simplification))
```

```
(def-theorem minimal-is-minimum
"forall(a:uu, s:sets[uu], minimal(a,s) implies minimum(a,s))"
(theory linear-order)
(proof
(
(apply-macete-with-minor-premises tr%maximal-is-maximum)
)))
```

```
(def-theorem finite-sets-have-maximum-elements
"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s}
implies
forsome(x:uu, maximum(x,s)))"
(theory linear-order)
(usages transportable-macete)
(proof
(

direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises maximal-is-maximum)
(apply-macete-with-minor-premises finite-sets-have-maximal-elements)
direct-and-antecedent-inference-strategy
(instantiate-existential ("x"))
)))
```

```
(def-theorem finite-sets-have-minimum-elements
"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s}
implies
forsome(x:uu, minimum(x,s)))"
(theory linear-order)
(usages transportable-macete)
(proof
(

(apply-macete-with-minor-premises tr%finite-sets-have-maximum-elements)
)))
```