---

Step * 1 1 1 of Lemma no-excluded-middle-quot-true1


1. ∀P:ℙ. ⇃(P ∨ (¬P))
2. EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.∀x:Base. (↓True))
3. magic : ∀t:Base. ⇃((t)↓ ∨ (¬(t)↓))
⊢ magic ∈ f,g:∀x:Base. ((x)↓ ∨ (¬(x)↓))//(∀x:Base. (↓True))
BY
{ (DoSubsume THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mneg{}P))
2.  EquivRel(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}));f,g.\mforall{}x:Base.  (\mdownarrow{}True))
3.  magic  :  \mforall{}t:Base.  \00D9((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))
\mvdash{}  magic  \mmember{}  f,g:\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))//(\mforall{}x:Base.  (\mdownarrow{}True))


By

---

Latex:
(DoSubsume  THEN  Auto)

---

Home Index