---

Step * of Lemma loopset-transitive

transitive-set(loopset())
BY
{ ((RWO "transitive-set-iff" 0 THENA Auto) THEN RWO "setmem-loopset" 0 THEN Auto) }

1
1. x : coSet{i:l}
2. seteq(x;loopset())
⊢ (x ⊆ loopset())

---

Latex:

---

Latex:
transitive-set(loopset())


By

---

Latex:
((RWO  "transitive-set-iff"  0  THENA  Auto)  THEN  RWO  "setmem-loopset"  0  THEN  Auto)

---

Home Index