---

Step * 1 1 2 1 of Lemma cut-of-closed

.....equality..... 
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) ~ X-pred e
BY
{ (Unfold `es-interface-pred` 0 THEN Reduce 0 THEN SplitOnConclITE THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
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'
7.  v  :  fset(E(X))@i
8.  (v  closed  under  [f;  X-pred])@i
9.  cut(X;f;s)  =  v@i
10.  s  \msubseteq{}  v@i
11.  e  :  E(X)@i
12.  e  \mmember{}  s@i
13.  f  e  \mmember{}  v
14.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
\mvdash{}  prior(X)(e)  \msim{}  X-pred  e


By

---

Latex:
(Unfold  `es-interface-pred`  0  THEN  Reduce  0  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index