---

Step * of Lemma AbstractFOAtomic_wf

∀[n:Atom]. ∀[L:ℤ List].  (AbstractFOAtomic(n;L) ∈ AbstractFOFormula(L))
BY
{ (Auto THEN Unfold `AbstractFOFormula` 0 THEN (Assert L ∈ {z:ℤ| (z ∈ L)}  List BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n:Atom].  \mforall{}[L:\mBbbZ{}  List].    (AbstractFOAtomic(n;L)  \mmember{}  AbstractFOFormula(L))


By

---

Latex:
(Auto  THEN  Unfold  `AbstractFOFormula`  0  THEN  (Assert  L  \mmember{}  \{z:\mBbbZ{}|  (z  \mmember{}  L)\}    List  BY  Auto)  THEN  ProveWfL\000Cemma)

---

Home Index