---

Step * 1 of Lemma rel_star_symmetric_2


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. Sym(T;x,y.x R y)
6. x (R^*) y
7. Sym(T;x,y.x (R^*) y)
⊢ y (R^*) x
BY
{ (Unfold `sym` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T
4.  y  :  T
5.  Sym(T;x,y.x  R  y)
6.  x  rel\_star(T;  R)  y
7.  Sym(T;x,y.x  rel\_star(T;  R)  y)
\mvdash{}  y  rel\_star(T;  R)  x


By

---

Latex:
(Unfold  `sym`  -1  THEN  Auto)

---

Home Index