---

Step * of Lemma isaxiom-implies

∀[t:Base]. (t ~ Ax) supposing ((↑isaxiom(t)) and (t)↓)
BY
{ CanonicalAuto }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (t  \msim{}  Ax)  supposing  ((\muparrow{}isaxiom(t))  and  (t)\mdownarrow{})


By

---

Latex:
CanonicalAuto

---

Home Index