Step
*
of Lemma
not-isr-assert-isl
∀x:Top + Top. ((¬↑isr(x)) 
⇒ (↑isl(x)))
BY
{ (Auto THEN RWO "not-isr-isl" 0 THEN Auto) }
Latex:
Latex:
\mforall{}x:Top  +  Top.  ((\mneg{}\muparrow{}isr(x))  {}\mRightarrow{}  (\muparrow{}isl(x)))
By
Latex:
(Auto  THEN  RWO  "not-isr-isl"  0  THEN  Auto)
Home
Index