---

Step * of Lemma prob2.1

∀[U:Type]. ∀[P:U ⟶ ℙ].  ∀x:U. ((P x) ⇒ (∃x:U. (P x)))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[U:Type].  \mforall{}[P:U  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x:U.  ((P  x)  {}\mRightarrow{}  (\mexists{}x:U.  (P  x)))


By

---

Latex:
Auto

---

Home Index