---

Step * of Lemma inductive-set-property

∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀bdd:Bounded(x,a.R[x;a]). inductively-defined{i:l}(x,a.R[x;a];inductive-set(bdd))
BY
{ (Auto
   THEN RepeatFor 3 (D -1)
   THEN Unfold `inductive-set` 0
   THEN Reduce 0
   THEN (BLemma `least-closed-set-inductively-defined` THENA Auto)
   THEN (Trivial ORELSE (Reduce 0 THEN (UnivCD THENA Auto)))) }

1
1. [R] : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
2. b1 : ∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ R[x1;a1] ⇒ R[x2;a2])
3. b3 : ∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y))
4. B : Set{i:l}
5. b5 : ∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
6. x : Set{i:l}
7. z : Set{i:l}
⊢ (z ∈ closure-set(B;λz.(fst((b3 z)));x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])

---

Latex:

---

Latex:
\mforall{}[R:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}']
    \mforall{}bdd:Bounded(x,a.R[x;a]).  inductively-defined\{i:l\}(x,a.R[x;a];inductive-set(bdd))


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (D  -1)
  THEN  Unfold  `inductive-set`  0
  THEN  Reduce  0
  THEN  (BLemma  `least-closed-set-inductively-defined`  THENA  Auto)
  THEN  (Trivial  ORELSE  (Reduce  0  THEN  (UnivCD  THENA  Auto))))

---

Home Index