---

Step * of Lemma exception-sqle-is-exception

∀[u,v,t:Base].  is-exception(t) supposing exception(u; v) ≤ t
BY
{ (Auto THEN Unfold `is-exception` 0 THEN SqLeTrans (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[u,v,t:Base].    is-exception(t)  supposing  exception(u;  v)  \mleq{}  t


By

---

Latex:
(Auto  THEN  Unfold  `is-exception`  0  THEN  SqLeTrans  (-1)  THEN  Auto)

---

Home Index