---

Step * of Lemma set_blt_functionality_wrt_set_lt_r

∀[s:QOSet]. ∀[a,b,b':|s|].  ↑(a <b b ⇒b (a <b b')) supposing b <s b'
BY
{ (Intros THEN RW assert_pushdownC 0 THEN Try (Complete ((Auto THEN RelRST THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[s:QOSet].  \mforall{}[a,b,b':|s|].    \muparrow{}(a  <\msubb{}  b  {}\mRightarrow{}\msubb{}  (a  <\msubb{}  b'))  supposing  b  <s  b'


By

---

Latex:
(Intros  THEN  RW  assert\_pushdownC  0  THEN  Try  (Complete  ((Auto  THEN  RelRST  THEN  Auto))))

---

Home Index