---

Step * of Lemma Sierpinski-cases

∀[x:Sierpinski]. (¬((¬(x = ⊤ ∈ Sierpinski)) ∧ (¬(x = ⊥ ∈ Sierpinski))))
BY
{ TACTIC:(Auto THEN D 0 THEN Auto THEN FLemma `not-Sierpinski-top` [-2] THEN Auto) }

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto  THEN  D  0  THEN  Auto  THEN  FLemma  `not-Sierpinski-top`  [-2]  THEN  Auto)

---

Home Index