---

Step * of Lemma cut-order-test

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[a,b,c:E(X)].
  (a ≤(X;f) c) supposing (b ≤(X;f) c and a ≤(X;f) b)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[a,b,c:E(X)].
    (a  \mleq{}(X;f)  c)  supposing  (b  \mleq{}(X;f)  c  and  a  \mleq{}(X;f)  b)


By

---

Latex:
Auto

---

Home Index