---

Step * 1 2 of Lemma cut-of-singleton

.....set predicate..... 
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
⊢ (cut(X;f;{e}) closed under [f; X-pred])
BY
{ ((GenConclAtAddr [4] THEN D -2) THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Info  :  Type@i'
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  f  :  sys-antecedent(es;X)@i
5.  e  :  E(X)@i
\mvdash{}  (cut(X;f;\{e\})  closed  under  [f;  X-pred])


By

---

Latex:
((GenConclAtAddr  [4]  THEN  D  -2)  THEN  Unhide  THEN  Auto)

---

Home Index