---

Step * of Lemma squash-from-quotient

∀[Q:ℙ]. (⇃(Q) ⇒ (↓Q))
BY
{ ((D 0 THENA Auto) THEN BLemma `quotient-implies-squash` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Q:\mBbbP{}].  (\00D9(Q)  {}\mRightarrow{}  (\mdownarrow{}Q))


By

---

Latex:
((D  0  THENA  Auto)  THEN  BLemma  `quotient-implies-squash`  THEN  Auto)

---

Home Index