---

Step * of Lemma rel-immediate-preserves-order

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Trans(T;x,y.R x y) ⇒ sum_of_torder(T;R) ⇒ (∀x,y,x',y':T.  ((R x y) ⇒ (R! x' x) ⇒ (R! y' y) ⇒ (R x' y'))))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.R x y)
4. sum_of_torder(T;R)
5. x : T
6. y : T
7. x' : T
8. y' : T
9. R x y
10. R! x' x
11. R! y' y
⊢ R x' y'

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T;x,y.R  x  y)
    {}\mRightarrow{}  sum\_of\_torder(T;R)
    {}\mRightarrow{}  (\mforall{}x,y,x',y':T.    ((R  x  y)  {}\mRightarrow{}  (R!  x'  x)  {}\mRightarrow{}  (R!  y'  y)  {}\mRightarrow{}  (R  x'  y'))))


By

---

Latex:
Auto

---

Home Index