---

Step * 1 of Lemma lconnects-transitive


∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects([];i;j))
BY
{ (Auto THEN (InstConcl [q])⋅ THEN Auto THEN (NthHypEq (-1)) THEN EqCD THEN Auto) }

---

Latex:



\mforall{}q:IdLnk  List.  \mforall{}i,j,k:Id.
    (\mexists{}r:IdLnk  List.  lconnects(r;i;k))  supposing  (lconnects(q;j;k)  and  lconnects([];i;j))


By

(Auto  THEN  (InstConcl  [q])\mcdot{}  THEN  Auto  THEN  (NthHypEq  (-1))  THEN  EqCD  THEN  Auto)

---

Home Index