---

Step * of Lemma es-p-locl-test

∀es:EO. ∀p:E ─→ (E + Top). ∀a,b,c,d,e:E.  (c p≤ d ⇒ d p≤ e ⇒ a p≤ b ⇒ b p< c ⇒ a p< e)
BY
{ (Auto THEN RelRST THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).  \mforall{}a,b,c,d,e:E.    (c  p\mleq{}  d  {}\mRightarrow{}  d  p\mleq{}  e  {}\mRightarrow{}  a  p\mleq{}  b  {}\mRightarrow{}  b  p<  c  {}\mRightarrow{}  a  p<  e)


By

(Auto  THEN  RelRST  THEN  Auto)

---

Home Index