---

Step * 2 of Lemma member-eo-forward-E


1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
5. (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' 
6. e' = e' ∈ {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } 
⊢ {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' }  ⊆r E
BY
{ (BLemma `eo-forward-E-subtype2`⋅ THENA Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  e'  :  E
5.  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e' 
6.  e'  =  e'
\mvdash{}  \{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e'  \}    \msubseteq{}r  E


By

(BLemma  `eo-forward-E-subtype2`\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index