---

Step * of Lemma Russell_wf

Russell ∈ 𝕌'
BY
{ (Unfold `Russell` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
Type ⋂ Base ∈ 𝕌'

2
.....subterm..... T:t
2:n
1. T : Type ⋂ Base
⊢ ¬(T ∈ T) ∈ 𝕌'

---

Latex:

---

Latex:
Russell  \mmember{}  \mBbbU{}'


By

---

Latex:
(Unfold  `Russell`  0  THEN  MemCD)

---

Home Index