---

Step * of Lemma not-isl-assert-isr

∀x:Top + Top. ((¬↑isl(x)) ⇒ (↑isr(x)))
BY
{ (Auto THEN RWO "not-isl-isr" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:Top  +  Top.  ((\mneg{}\muparrow{}isl(x))  {}\mRightarrow{}  (\muparrow{}isr(x)))


By

---

Latex:
(Auto  THEN  RWO  "not-isl-isr"  0  THEN  Auto)

---

Home Index