---

Step * 1 of Lemma eo-forward-E-subtype

.....subterm..... T:t
1:n
1. eo : EO
2. e : E
3. x : {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))} @i
⊢ x ∈ {e:es-base-E(eo)| ↑(es-dom(eo) e)} 
BY
{ D (-1) }

1
1. eo : EO
2. e : E
3. x : es-base-E(eo)@i
4. ↑((es-dom(eo) x) ∧b (e ≤loc x ∨b(¬bloc(x) = loc(e))))@i
⊢ x ∈ {e:es-base-E(eo)| ↑(es-dom(eo) e)} 

---

Latex:


.....subterm.....  T:t
1:n
1.  eo  :  EO
2.  e  :  E
3.  x  :  \{e@0:es-base-E(eo)|  \muparrow{}((es-dom(eo)  e@0)  \mwedge{}\msubb{}  (e  \mleq{}loc  e@0  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e@0)  =  loc(e))))\}  @i
\mvdash{}  x  \mmember{}  \{e:es-base-E(eo)|  \muparrow{}(es-dom(eo)  e)\} 


By

D  (-1)

---

Home Index