---

Step * 1 1 of Lemma no-excluded-middle-using-partial2

.....assertion..... 
1. ∀P:ℙ. ((↓P) ∨ (¬P))
⊢ n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 
BY
{ TACTIC:RenameVar `magic' (-1)⋅ }

1
1. magic : ∀P:ℙ. ((↓P) ∨ (¬P))
⊢ n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 

---

Latex:

---

Latex:
.....assertion..... 
1.  \mforall{}P:\mBbbP{}.  ((\mdownarrow{}P)  \mvee{}  (\mneg{}P))
\mvdash{}  n:partial(\mBbbZ{})  {}\mrightarrow{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  (n)\mdownarrow{}\} 


By

---

Latex:
TACTIC:RenameVar  `magic'  (-1)\mcdot{}

---

Home Index