---

Step * of Lemma not-Sierpinski-bottom

∀[x:Sierpinski]. ((¬(x = ⊥ ∈ Sierpinski)) ⇒ (x = ⊤ ∈ Sierpinski))
BY
{ TACTIC:(InstLemma `Sierpinski-unequal-1` []
          THEN Auto
          THEN Thin 2
          THEN D 2
          THEN ThinVar `x1'
          THEN EqTypeCD
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:Sierpinski].  ((\mneg{}(x  =  \mbot{}))  {}\mRightarrow{}  (x  =  \mtop{}))


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal-1`  []
                THEN  Auto
                THEN  Thin  2
                THEN  D  2
                THEN  ThinVar  `x1'
                THEN  EqTypeCD
                THEN  Auto)

---

Home Index