---

Step * of Lemma isinr-implies

∀[t:Base]. (t ~ inr outr(t) ) supposing ((↑isinr(t)) and (t)↓)
BY
{ CanonicalAuto }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (t  \msim{}  inr  outr(t)  )  supposing  ((\muparrow{}isinr(t))  and  (t)\mdownarrow{})


By

---

Latex:
CanonicalAuto

---

Home Index