---

Step * of Lemma plus-set-transitive

No Annotations
∀a:coSet{i:l}. (transitive-set(a) ⇒ transitive-set((a)+))
BY
{ ((RWO "transitive-set-iff" 0 THENA Auto) THEN RWW "setmem-plus-set setsubset-iff" 0 THEN Auto THEN D -3 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:coSet\{i:l\}.  (transitive-set(a)  {}\mRightarrow{}  transitive-set((a)+))


By

---

Latex:
((RWO  "transitive-set-iff"  0  THENA  Auto)
  THEN  RWW  "setmem-plus-set  setsubset-iff"  0
  THEN  Auto
  THEN  D  -3
  THEN  Auto)

---

Home Index