---

Step * 1 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'
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
BY
{ OnMaybeHyp 8 (\h. (UnfoldTopAb h THEN (RWO "l_all_iff" h THENM BHyp h ) THEN CompleteAuto))⋅ }

---

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'
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
\mvdash{}  f  e  \mmember{}  v


By

---

Latex:
OnMaybeHyp  8  (\mbackslash{}h.  (UnfoldTopAb  h  THEN  (RWO  "l\_all\_iff"  h  THENM  BHyp  h  )  THEN  CompleteAuto))\mcdot{}

---

Home Index