---

Step * of Lemma l_exists_nil

∀[P:Top]. ((∃x∈[]. P[x]) ⇐⇒ False)
BY
{ (RepUR ``l_exists`` 0 THEN Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Top].  ((\mexists{}x\mmember{}[].  P[x])  \mLeftarrow{}{}\mRightarrow{}  False)


By

---

Latex:
(RepUR  ``l\_exists``  0  THEN  Auto  THEN  ExRepD  THEN  Auto)

---

Home Index