---

Step * of Lemma es-cut-exists

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀s:fset(E(X)).
    ∃c:Cut(X;f). (s ⊆ c ∧ (∀[c':Cut(X;f)]. c ⊆ c' supposing s ⊆ c'))
BY
{ (Auto
   THEN InstLemma `sys-antecedent-closure` [Info; ⌜es⌝;⌜X⌝;⌜[f; X-pred]⌝;⌜s⌝]⋅
   THEN Auto
   THEN ParallelLast
   THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. s : fset(E(X))@i
6. c : fset(E(X))
7. (c = [f; X-pred] closure of s)
8. s ⊆ c
9. c' : Cut(X;f)
10. s ⊆ c'
⊢ c ⊆ c'

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}s:fset(E(X)).
        \mexists{}c:Cut(X;f).  (s  \msubseteq{}  c  \mwedge{}  (\mforall{}[c':Cut(X;f)].  c  \msubseteq{}  c'  supposing  s  \msubseteq{}  c'))


By

---

Latex:
(Auto
  THEN  InstLemma  `sys-antecedent-closure`  [Info;  \mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}[f;  X-pred]\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index