---

Step * 1 of Lemma sp-meet-bottom


1. x : Sierpinski
2. ⊥ = ⊤ ∈ Sierpinski
⊢ x = ⊤ ∈ Sierpinski
BY
{ TACTIC:(InstLemma `Sierpinski-unequal` [] THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Sierpinski
2.  \mbot{}  =  \mtop{}
\mvdash{}  x  =  \mtop{}


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal`  []  THEN  Auto)

---

Home Index