---

Step * of Lemma rel-immediate-property

No Annotations
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (sum_of_torder(T;R) ⇒ (∀x,y,x',y':T.  ((R x y) ⇒ (R! y' y) ⇒ ((R x y') ∨ (x = y' ∈ T)))))
BY
{ (Auto THEN Unfold `sum_of_torder` -7) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀a,b,x:T.  ((((R a x) ∧ (R b x)) ∨ ((R x a) ∧ (R x b))) ⇒ (((R a b) ∨ (a = b ∈ T)) ∨ (R b a)))
4. x : T@i
5. y : T@i
6. x' : T@i
7. y' : T@i
8. R x y
9. R! y' y
⊢ (R x y') ∨ (x = y' ∈ T)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `sum\_of\_torder`  -7)

---

Home Index