---

Step * of Lemma cosetTC-least

∀a,s:coSet{i:l}.  ((a ⊆ s) ⇒ transitive-set(s) ⇒ (cosetTC(a) ⊆ s))
BY
{ (Auto
   THEN UseTrans ⌜cosetTC(s)⌝⋅
   THEN EAuto 1
   THEN ThinVar `a'
   THEN RWO "setsubset-iff" 0
   THEN Auto
   THEN SetMemDef (-1)
   THEN RWO "-1" 0
   THEN Auto
   THEN ThinVar `x') }

1
1. s : coSet{i:l}
2. transitive-set(s)
3. t : {p:copath(T.T;s)| 0 < copath-length(p)} 
⊢ (copath-at(s;t) ∈ s)

---

Latex:

---

Latex:
\mforall{}a,s:coSet\{i:l\}.    ((a  \msubseteq{}  s)  {}\mRightarrow{}  transitive-set(s)  {}\mRightarrow{}  (cosetTC(a)  \msubseteq{}  s))


By

---

Latex:
(Auto
  THEN  UseTrans  \mkleeneopen{}cosetTC(s)\mkleeneclose{}\mcdot{}
  THEN  EAuto  1
  THEN  ThinVar  `a'
  THEN  RWO  "setsubset-iff"  0
  THEN  Auto
  THEN  SetMemDef  (-1)
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  ThinVar  `x')

---

Home Index