---

Step * 1 1 of Lemma cut-of-closed


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))))
BY
{ (GenConclAtAddr [1;4] THEN D -2 THEN Unhide THEN Auto) }

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'
7. v : fset(E(X))@i
8. (v closed under [f; X-pred])@i
9. cut(X;f;s) = v ∈ Cut(X;f)@i
10. s ⊆ v@i
11. e : E(X)@i
12. e ∈ s@i
⊢ f e ∈ v

2
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'
7. v : fset(E(X))@i
8. (v closed under [f; X-pred])@i
9. cut(X;f;s) = v ∈ Cut(X;f)@i
10. s ⊆ v@i
11. e : E(X)@i
12. e ∈ s@i
13. f e ∈ v
14. ↑e ∈b prior(X)
⊢ prior(X)(e) ∈ v

---

Latex:

---

Latex:

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.  \mforall{}[c':Cut(X;f)].  cut(X;f;s)  \msubseteq{}  c'  supposing  s  \msubseteq{}  c'
\mvdash{}  s  \msubseteq{}  cut(X;f;s)
{}\mRightarrow{}  (\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:
(GenConclAtAddr  [1;4]  THEN  D  -2  THEN  Unhide  THEN  Auto)

---

Home Index