Step * of Lemma es-locl-trans-test

es:EO. ∀a,b,c,d,e,f:E.  (a ≤loc b   b ≤loc c   (c <loc d)  d ≤loc e   e ≤loc f   a ≤loc )
BY
Auto }


Latex:


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


By

Auto




Home Index