---

Step * of Lemma sp-le-bottom

∀[x:Sierpinski]. ⊥ ≤ x
BY
{ TACTIC:(InstLemma `Sierpinski-unequal` [] THEN TACTIC:(Unfold `sp-le` 0 THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[x:Sierpinski].  \mbot{}  \mleq{}  x


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal`  []  THEN  TACTIC:(Unfold  `sp-le`  0  THEN  Auto))

---

Home Index