---

Step * 1 3 of Lemma no-excluded-middle-quot-true

.....aux..... 
1. magic : ∀P:ℙ. ⇃(P ∨ (↓¬P))
2. v : Base
3. v2 : Base
4. (magic (⊥)↓) = v ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
5. v1 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
6. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ istype((v ∈ (⊥)↓ ∨ (↓¬(⊥)↓)) ∧ (v2 ∈ (⊥)↓ ∨ (↓¬(⊥)↓)) ∧ True)
BY
{ Auto }

---

Latex:

---

Latex:
.....aux..... 
1.  magic  :  \mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mdownarrow{}\mneg{}P))
2.  v  :  Base
3.  v2  :  Base
4.  (magic  (\mbot{})\mdownarrow{})  =  v
5.  v1  :  \00D9((0  \mleq{}  0)  \mvee{}  (\mdownarrow{}\mneg{}(0  \mleq{}  0)))
6.  (magic  (0  \mleq{}  0))  =  v1
\mvdash{}  istype((v  \mmember{}  (\mbot{})\mdownarrow{}  \mvee{}  (\mdownarrow{}\mneg{}(\mbot{})\mdownarrow{}))  \mwedge{}  (v2  \mmember{}  (\mbot{})\mdownarrow{}  \mvee{}  (\mdownarrow{}\mneg{}(\mbot{})\mdownarrow{}))  \mwedge{}  True)


By

---

Latex:
Auto

---

Home Index