---

Step * of Lemma member-not

∀[A:ℙ]. ∀[z:Top].  λx.z ∈ ¬A supposing ¬A
BY
{ (Intros THEN RepUR ``not implies`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbP{}].  \mforall{}[z:Top].    \mlambda{}x.z  \mmember{}  \mneg{}A  supposing  \mneg{}A


By

---

Latex:
(Intros  THEN  RepUR  ``not  implies``  0  THEN  Auto)

---

Home Index