---

Step * 1 1 of Lemma fl0-not-1


1. I : fset(ℕ)
2. x : names(I)
3. {inl x} = {} ∈ fset(names(I) + names(I))
⊢ False
BY
{ (Assert inl x ∈ {inl x} BY
         Auto) }

1
1. I : fset(ℕ)
2. x : names(I)
3. {inl x} = {} ∈ fset(names(I) + names(I))
4. inl x ∈ {inl x}
⊢ False

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  names(I)
3.  \{inl  x\}  =  \{\}
\mvdash{}  False


By

---

Latex:
(Assert  inl  x  \mmember{}  \{inl  x\}  BY
              Auto)

---

Home Index