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