---

Step * of Lemma rel-plus-rel-immediate

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  R!+ => R+
BY
{ (RepUR ``rel_implies rel_plus rel-immediate infix_ap`` 0 THEN Auto THEN ParallelLast) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. n : ℕ+
6. λx,y. ((R x y) ∧ (∀z:T. (¬((R x z) ∧ (R z y)))))^n x y
⊢ R^n x y

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    R!\msupplus{}  =>  R\msupplus{}


By

---

Latex:
(RepUR  ``rel\_implies  rel\_plus  rel-immediate  infix\_ap``  0  THEN  Auto  THEN  ParallelLast)

---

Home Index