---

Step * of Lemma id-graph-edge-implies-member

∀S:Id List. ∀G:Graph(S). ∀i:{i:Id| (i ∈ S)} . ∀j:Id.  ((i⟶j)∈G ⇒ (j ∈ S))
BY
{ (Unfold `id-graph-edge` 0 THEN Auto THEN Try ((Fold `id-graph` 0 THEN Auto))) }

1
1. S : Id List@i
2. G : Graph(S)@i
3. i : {i:Id| (i ∈ S)} @i
4. j : Id@i
5. (j ∈ G i)@i
⊢ (j ∈ S)

---

Latex:

---

Latex:
\mforall{}S:Id  List.  \mforall{}G:Graph(S).  \mforall{}i:\{i:Id|  (i  \mmember{}  S)\}  .  \mforall{}j:Id.    ((i{}\mrightarrow{}j)\mmember{}G  {}\mRightarrow{}  (j  \mmember{}  S))


By

---

Latex:
(Unfold  `id-graph-edge`  0  THEN  Auto  THEN  Try  ((Fold  `id-graph`  0  THEN  Auto)))

---

Home Index