---

Step * of Lemma no-excluded-middle

¬(∀P:ℙ. (P ∨ (¬P)))
BY
{ (InstLemma `no-excluded-middle-using-partial` [] THEN Auto) }

---

Latex:

---

Latex:
\mneg{}(\mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P)))


By

---

Latex:
(InstLemma  `no-excluded-middle-using-partial`  []  THEN  Auto)

---

Home Index