---

Step * of Lemma eo-forward-le

∀eo:EO. ∀e:E. ∀a,b:E.  (a ≤loc b  ⇐⇒ a ≤loc b )
BY
{ ((UnivCD THENA (Auto THEN BLemma `eo-forward-wf` THEN Auto))
   THEN RepUR ``es-le es-locl`` 0
   THEN (RWO "eo-forward-loc" 0 THENA Auto)
   THEN (RWO "eo-forward-less" 0 THENA Auto)
   THEN InstLemma `eo-forward-E-subtype` [⌈eo⌉;⌈e⌉]⋅
   THEN Auto
   THEN Try ((BLemma `eo-forward-wf` THEN Auto))) }

1
1. eo : EO@i'
2. e : E@i
3. a : E@i
4. b : E@i
5. E ⊆r E
6. ((loc(a) = loc(b) ∈ Id) ∧ (a < b)) ∨ (a = b ∈ E)@i
⊢ ((loc(a) = loc(b) ∈ Id) ∧ (a < b)) ∨ (a = b ∈ E)

2
1. eo : EO@i'
2. e : E@i
3. a : E@i
4. b : E@i
5. E ⊆r E
6. ((loc(a) = loc(b) ∈ Id) ∧ (a < b)) ∨ (a = b ∈ E)@i
⊢ ((loc(a) = loc(b) ∈ Id) ∧ (a < b)) ∨ (a = b ∈ E)

---

Latex:


\mforall{}eo:EO.  \mforall{}e:E.  \mforall{}a,b:E.    (a  \mleq{}loc  b    \mLeftarrow{}{}\mRightarrow{}  a  \mleq{}loc  b  )


By

((UnivCD  THENA  (Auto  THEN  BLemma  `eo-forward-wf`  THEN  Auto))
  THEN  RepUR  ``es-le  es-locl``  0
  THEN  (RWO  "eo-forward-loc"  0  THENA  Auto)
  THEN  (RWO  "eo-forward-less"  0  THENA  Auto)
  THEN  InstLemma  `eo-forward-E-subtype`  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `eo-forward-wf`  THEN  Auto)))

---

Home Index