---

Step * of Lemma es-causle_weakening_locl

∀es:EO. ∀a,b:E.  (a ≤loc b  ⇒ a c≤ b)
BY
{ (Unfolds ``es-causle es-le`` 0 THEN Auto THEN ParallelLast) }

1
1. es : EO@i'
2. a : E@i
3. b : E@i
4. (a <loc b)@i
⊢ (a < b)

---

Latex:


\mforall{}es:EO.  \mforall{}a,b:E.    (a  \mleq{}loc  b    {}\mRightarrow{}  a  c\mleq{}  b)


By

(Unfolds  ``es-causle  es-le``  0  THEN  Auto  THEN  ParallelLast)

---

Home Index