---

Step * of Lemma proof-by-cont-implies-LEM

(∀p:ℙ. ((¬¬p) ⇒ p)) ⇒ (∀p:ℙ. (p ∨ (¬p)))
BY
{ ((D 0 THENA Auto)
   THEN (D 0 THENA (Thin 1 THEN Auto))
   THEN (BHyp (-2)  THENA (Thin 1 THEN Auto))
   THEN (D 0 THENA (Thin 1 THEN Auto))
   THEN RWO "not_over_or" (-1)
   THEN Thin 1
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (D  0  THENA  (Thin  1  THEN  Auto))
  THEN  (BHyp  (-2)    THENA  (Thin  1  THEN  Auto))
  THEN  (D  0  THENA  (Thin  1  THEN  Auto))
  THEN  RWO  "not\_over\_or"  (-1)
  THEN  Thin  1
  THEN  Auto)

---

Home Index