---

Step * 1 of Lemma cut-of-closed


∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀s:fset(E(X)). ∀e:E(X).
  (e ∈ s ⇒ (f e ∈ cut(X;f;s) ∧ prior(X)(e) ∈ cut(X;f;s) supposing ↑e ∈b prior(X) ∧ e ∈ cut(X;f;s)))
BY
{ (InstLemma `cut-of-property` [] THEN RepeatFor 5 (ParallelLast') THEN D -1 THEN MoveToConcl (-2))⋅ }

1
1. Info : Type@i'
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':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'
⊢ s ⊆ cut(X;f;s)
⇒ (∀e:E(X). (e ∈ s ⇒ (f e ∈ cut(X;f;s) ∧ prior(X)(e) ∈ cut(X;f;s) supposing ↑e ∈b prior(X) ∧ e ∈ cut(X;f;s))))

---

Latex:

---

Latex:

\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}s:fset(E(X)).  \mforall{}e:E(X).
    (e  \mmember{}  s  {}\mRightarrow{}  (f  e  \mmember{}  cut(X;f;s)  \mwedge{}  prior(X)(e)  \mmember{}  cut(X;f;s)  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)  \mwedge{}  e  \mmember{}  cut(X;f;s)))


By

---

Latex:
(InstLemma  `cut-of-property`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  D  -1  THEN  MoveToConcl  (-2))\mcdot{}

---

Home Index