---

Step * of Lemma rel_plus_functionality_wrt_brle

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 ≡>{T} R2) ⇒ (R1+ ≡>{T} R2+))
BY
{ (InstLemma `rel_plus_functionality_wrt_rel_implies` []
   THEN RepUR ``rel_implies infix_ap`` -1
   THEN Fold `binrel_le` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R1  \mequiv{}>\{T\}  R2)  {}\mRightarrow{}  (R1\msupplus{}  \mequiv{}>\{T\}  R2\msupplus{}))


By

---

Latex:
(InstLemma  `rel\_plus\_functionality\_wrt\_rel\_implies`  []
  THEN  RepUR  ``rel\_implies  infix\_ap``  -1
  THEN  Fold  `binrel\_le`  (-1)
  THEN  Trivial)

---

Home Index