---

Step * of Lemma fl-join_wf

∀[I:fset(ℕ)]. ∀[x,y:𝔽(I)].  (fl-join(I;x;y) ∈ 𝔽(I))
BY
{ Auto }

1
1. I : fset(ℕ)
2. x : 𝔽(I)
3. y : 𝔽(I)
⊢ fl-join(I;x;y) ∈ 𝔽(I)

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x,y:\mBbbF{}(I)].    (fl-join(I;x;y)  \mmember{}  \mBbbF{}(I))


By

---

Latex:
Auto

---

Home Index