---

Step * 1 of Lemma quotient-top-union-top-not-subtype


1. ⇃(Top + Top) ⊆r (Top + Top)
2. (inl ⋅) = (inr ⋅ ) ∈ (Top + Top)
⊢ False
BY
{ ((ApFunToHypEquands `Z' ⌜case Z of inl(a) => 0 | inr(b) => 1⌝ ⌜ℤ⌝ (-1)⋅ THENA Auto) THEN Reduce -1) }

1
1. ⇃(Top + Top) ⊆r (Top + Top)
2. (inl ⋅) = (inr ⋅ ) ∈ (Top + Top)
3. 0 = 1 ∈ ℤ
⊢ False

---

Latex:

---

Latex:

1.  \00D9(Top  +  Top)  \msubseteq{}r  (Top  +  Top)
2.  (inl  \mcdot{})  =  (inr  \mcdot{}  )
\mvdash{}  False


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}case  Z  of  inl(a)  =>  0  |  inr(b)  =>  1\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  -1)

---

Home Index