---

Step * of Lemma quot-implies-squash

∀P:ℙ. (⇃(P) ⇒ (↓P))
BY
{ ((UnivCD THENA Auto) THEN UseWitness⌜Ax⌝⋅ THEN newQuotientElim1 (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}P:\mBbbP{}.  (\00D9(P)  {}\mRightarrow{}  (\mdownarrow{}P))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  UseWitness\mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  newQuotientElim1  (-1)\mcdot{}  THEN  Auto)

---

Home Index