---

Step * of Lemma Regularset-regularset

∀A:Set{i:l}. (Regular(A) ⇒ regular(A))
BY
{ (Auto
   THEN Unfold `Regularset` -1
   THEN Unfold `regularset` 0
   THEN Auto
   THEN (InstHyp [⌜B⌝] 3⋅ THENA Auto)
   THEN Thin 3) }

1
1. A : Set{i:l}
2. transitive-set(A)
3. transitive-set(A)
4. B : coSet{i:l}
5. (B ∈ A)
6. R : coSet{i:l}
7.  setrel(R):(B ⇒ A)
8. ∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
     (SetRelation(R) ⇒  R:(B ⇒ A) ⇒ (∃b:Set{i:l}. ((b ∈ A) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))))
⊢ ∃b:coSet{i:l}. ((b ∈ A) ∧  setrel(R):(B ⇒ b) ∧ setrel(R):(B ─>> b))

---

Latex:

---

Latex:
\mforall{}A:Set\{i:l\}.  (Regular(A)  {}\mRightarrow{}  regular(A))


By

---

Latex:
(Auto
  THEN  Unfold  `Regularset`  -1
  THEN  Unfold  `regularset`  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}B\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  Thin  3)

---

Home Index