---

Step * of Lemma rel_star_symmetric_2

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (Sym(T;x,y.x R y) ⇒ (x (R^*) y) ⇒ (y (R^*) x))
BY
{ ((Auto THEN FwdThruLemma `rel_star_symmetric` [(-2)]) THENA Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x,y:T.    (Sym(T;x,y.x  R  y)  {}\mRightarrow{}  (x  (R\^{}*)  y)  {}\mRightarrow{}  (y  (R\^{}*)  x))


By

---

Latex:
((Auto  THEN  FwdThruLemma  `rel\_star\_symmetric`  [(-2)])  THENA  Auto)

---

Home Index