---

Step * 1 of Lemma eo-forward-le2


1. eo : EO@i'
2. e : E@i
3. ∀a,b:E.  (a ≤loc b  ⇐⇒ a ≤loc b )
4. eo.e ∈ EO
5. a : E@i
6. b : E@i
7. a ≤loc b @i
⊢ a ≤loc b 
BY
{ ((InstHyp [⌈a⌉;⌈b⌉] 3⋅ THENA Auto) THEN D (-1) THEN BackThruSomeHyp THEN Auto) }

---

Latex:



1.  eo  :  EO@i'
2.  e  :  E@i
3.  \mforall{}a,b:E.    (a  \mleq{}loc  b    \mLeftarrow{}{}\mRightarrow{}  a  \mleq{}loc  b  )
4.  eo.e  \mmember{}  EO
5.  a  :  E@i
6.  b  :  E@i
7.  a  \mleq{}loc  b  @i
\mvdash{}  a  \mleq{}loc  b 


By

((InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  D  (-1)  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index